LocalizationGluingAdmissible

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: gluing admissibility of the localization cells

Source sentence in ABK26.

Since  grad w_{D,e}^{(K)} in L^2_{pot,0}(cu_K)  and
grad w_{N,e'}^{(K)} + shom_{m-h}^{-1} h e' in Lsolo(cu_K),
we have that  sum_{z in 3^n Z^d cap cu_K} X_z 1_{z+cu_n}
  in  P + L^2_{pot,0}(cu_K) x Lsolo(cu_K),
and we may insert it into the minimization problem in
(e.variational.mu.U.P) for bfA_m(cu_K).

This module proves exactly the membership assertion of that sentence, in the two halves the manuscript's phrase names:

• the potential half — a family of fields that are L^2_{pot,0} on their own cell glues, cell by cell, to an L^2_{pot,0} field on the union;
• the solenoidal half — the same statement for Lsolo, i.e. for zero normal trace.

Both halves reduce to the extension-by-zero maps already available in this repository (Algsuperdiff.Section3.Provider.Whitney.potentialZeroTraceFieldOn_indicator_of_subset and ..._solenoidalZeroNormalTraceFieldOn_indicator_of_subset, both proved for l.subadd.betterer), plus the exact triadic tiling of cu_K by its depth-(K-n) descendants, which is CoarseGraining geometry: Homogenization.exists_mem_descendantsAtDepth_of_mem_cubeSet, Homogenization.pairwiseDisjoint_openCubeSet_descendantsAtDepth, Homogenization.volume_cubeBoundary_eq_zero.

What is proved

• gluedDoubledField — the manuscript's sum_z X_z 1_{z+cu_n}, rendered with the open cells openCubeSet R of the depth-j descendant family.
• gluedDoubledField_eval_of_mem_openCubeSet — the glued field agrees with the cell field X_R at every point of the open cell R.
• isDoubledMuAdmissible_gluedDoubledField — the sentence itself: if the affine background G is admissible at load P on cu_K, and each cell field X_R differs from G by a test field on its own cell, then the glued field is admissible at load P on cu_K.

Divergences from the printed statement

• Pin correction. LocalizationBasicSplit.lean cites this sentence as "". Verified against \label{e.Pz.def}, \label{e.Fz.def} and \label{e.lower.bound.basic.split}. The mathematical content cited is unchanged.
• This is the principal (A_4) leg of the reconciliation entry, not the interior-filtered display leg.
• . The glued field is totalized off the null set: it is defined by the open cells openCubeSet R, hence is 0 on the Lebesgue-null union of the internal faces. Every conclusion below is an a.e. statement on openCubeSet Q, so no value on that null set is load-bearing.
• . Nothing in this module asserts that the glued field minimizes anything: the only conclusion drawn is membership in the admissible class. The competitor insertion this membership licenses is an inequality, and it is not performed here.

The exact triadic tiling of a cube by its descendants

A.e. robustness of the two zero-trace classes

The glued field

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gluedDoubledField {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) (X : HCPolySupport.TriadicCube d → HCPolySupport.Book.Ch02.DoubledField d) : HCPolySupport.Book.Ch02.DoubledField d

The manuscript's sum_{z in 3^n Z^d cap cu_K} X_z 1_{z+cu_n}, with the lattice sites z rendered as the depth-j triadic descendants of Q and the cell z+cu_n rendered as the open cell openCubeSet R.

Per the field is totalized off the null set: on the union of the internal faces every indicator vanishes and the glued field is 0.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gluedDoubledField_eval_of_mem_openCubeSet {d : ℕ} {Q : HCPolySupport.TriadicCube d} {j : ℕ} (X : HCPolySupport.TriadicCube d → HCPolySupport.Book.Ch02.DoubledField d) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth Q j) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet R) : (gluedDoubledField Q j X).eval x = (X R).eval x

On its own open cell the glued field is the cell field: this is the sense in which sum_z X_z 1_{z+cu_n} restricts to X_z on z+cu_n.

The gluing admissibility

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.isDoubledMuAdmissible_gluedDoubledField {d : ℕ} {Q : HCPolySupport.TriadicCube d} {j : ℕ} {P : HCPolySupport.BlockVec d} {G : HCPolySupport.Book.Ch02.DoubledField d} {X : HCPolySupport.TriadicCube d → HCPolySupport.Book.Ch02.DoubledField d} (hG : HCPolySupport.Book.Ch02.IsDoubledMuAdmissible (HCPolySupport.Book.Ch02.cubeDomain Q) P G) (hX : ∀ R ∈ HCPolySupport.descendantsAtDepth Q j, HCPolySupport.Book.Ch02.IsDoubledTestField (HCPolySupport.Book.Ch02.cubeDomain R) (X R - G)) : HCPolySupport.Book.Ch02.IsDoubledMuAdmissible (HCPolySupport.Book.Ch02.cubeDomain Q) P (gluedDoubledField Q j X)

Generic gluing admissibility (a conditional A toward; it is not itself the manuscript's sentence, which operates at the specific corrector background and minimizers).

Let G be a doubled field admissible at load P on the cube Q — the manuscript's bfAhom^{-1/2}(e' + grad w_D^{(K)}, e + grad w_N^{(K)} + shom^{-1} h e'). Its membership in P + L^2_{pot,0}(cu_K) x Lsolo(cu_K) is NOT a stated hypothesis of the manuscript: D it from the gradient/solenoidal structure of the corrector fields; here it enters as the caller proposition hG. Let X_R be, for each depth-j descendant R of Q, a field differing from G by a test field on R — this is exactly the admissible class of the manuscript's X_z (printed: X_z is the argmin over bfAhom^{-1/2}(...) + (L^2_{pot,0} x Lsolo)(z+cu_n)). Then the glued field sum_ 1_R is admissible at load P on Q.

The potential half is piecewise H^1_0 gluing (an H^1_0(R) primitive extends by zero to an H^1_0(Q) primitive, and the gradient of the extension is the extension of the gradient); the solenoidal half is that testing the glued flux against phi in H^1(Q) splits over the cells, and each cell integral vanishes because phi restricts to H^1(R).

Per this is a membership statement only: it licenses inserting the glued field into e.variational.mu.U.P as one competitor, and no declaration here asserts that it is a minimizer.