LocalizationActualSplit #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: X_z = S_z + tilde S_z and a generic pre-mesh intermediate toward the insertion step, #
at the actual carriers
Source displays in ABK26:
e.recurrence.P.def,e.def.w,e.Pz.def,e.Fz.def;S_z := S(., z+cu_n, -P_z, 0; a_m);- the
X_zdisplay, and thetilde S_zdisplay; - the sentence "Observe that
X_z = S_z + tilde S_z" and the gluing clause;
LocalizationSelection*.lean and LocalizationGluing*.lean prove all of this
for abstract slope data, carrying caller propositions.
LocalizationActualBackground.lean derives those propositions at the genuine
P_z, bfF_z and correctors. This module composes the two: it selects the
per-cell S_z and tilde S_z at the actual carriers, D the cell field as
their sum, and feeds the resulting family into the gluing competitor bound and
the cell algebra.
Why the sum is a definition and not a comparison #
The manuscript defines X_z by its own argmin display and then observes
X_z = S_z + tilde S_z. Selecting X_z independently would make that
observation an a.e. identity only, because the two argmins are unique only up
to a null set. Below, the cell field is defined as the sum S_z + tilde S_z, so is literally true, and what is proved instead is that the sum
satisfies the minimizer property (isDoubledMuMinimizerField. (localizationBackground.) (S R + T R)). What
exists_localizationActualCellFields records as its uniqueness clauses is the
a.e. uniqueness of S_z and of tilde S_z individually; the agreement of the
defined sum with an independently selected X_z is NOT recorded as a theorem
here — a caller wanting it must apply
LocalizationSelectionExistence.sameAE_of_isDoubledMuMinimizerField to the
sum's minimizer property itself.
What is proved #
exists_localizationActualCellFields-- on one localization cell:S_zandtilde S_zexist, are a.e. unique, their sum satisfies theX_zminimizer property,tilde S_zis a doubled response field (the Euler--Lagrange equation), and the Step-2 identity holds for it.two_mul_doubledMuValue_localizationActual_add_eq-- the second line ofe.lower.bound.basic.splitat the actual carriers.exists_localizationActualCellSplit-- the whole family over the descendant cells, produced by choice from the per-cell statement.exists_localizationActualCellSplit_blockVecDot_coarseBlockMatrix_le-- a generic pre-mesh intermediate (a term-level consumer of the selection and gluing layers, but NOT the manuscript's first insertion line): the glued field of the actualS_z + tilde S_zsatisfies the pre-mesh shape,P. bfA_m(cu_K) P <= fint_{cu_K} X. bfA_m X, withPthe genuinebfAhom_{m-h}^{-1/2}(e'; e)ofe.recurrence.P.def, the coefficient family abstract and the mesh average not composed.
Divergences from the printed statement #
- . Carrier as in
LocalizationSelectionExistence. - ** /.** The manuscript's site set
3^n Z^d cap cu_Kis the full descendant familydescendantsAtDepth Q j, inherited fromLocalizationGluingAdmissible.lean. - . Only the inequality direction of the insertion is produced; nothing below asserts that the glued field minimizes anything.
- .
SandTbelow are total functions onTriadicCube dobtained by choice, and every conclusion is quantified overdescendantsAtDepth Q j; the values off that family are not load-bearing and no statement mentions them. The manuscript'sX_zis likewise indexed by the sites only. - . The identity is justified below by the Euler--Lagrange equation of
tilde S_z, never by mean-zeroness ofbfF_z. - The per-cell coefficient. As in
LocalizationSelectionFamily.lean, the cell problems are posed at a familyaCell: (R: TriadicCube d) -> CoeffOn (cubeDomain R); a caller wanting the manuscript'sbfA_mon every cell instantiates it withBook.Ch02.pointwiseCoeffOnRestrict. - The mesh average is absent.
avsum_{z in 3^n Z^d cap cu_K}and the tiling identity belong to a separate lane; the bound below is stated at the glued field oncu_K, exactly asLocalizationGluingCompetitor.leanstates it. The per-cell identity that the mesh average would consume isLocalizationGluingAdmissible.gluedDoubledField_eval_of_mem_openCubeSet: on its own open cell the glued field is the cell field.
One localization cell #
S_z, tilde S_z and X_z = S_z + tilde S_z on one localization cell.
At the actual carriers: R is the cell z + cu_n inside cu_K, P_z is
e.Pz.def, bfF_z is e.Fz.def, and the background of the X_z display is
localizationBackground. The conclusions are, in order:
Tis a doubled response field, i.e. satisfies the Euler--Lagrange equation (first variation);- the Step-2 identity holds for
T, proved from that first variation and not from mean-zeroness.
: on hwN, the defining property of w_{N,e'}^{(K)}, and on the inclusion
hsub : openCubeSet R ⊆ openCubeSet Q (the cell sits inside the big cube;
discharged by the descendant geometry at the call sites).
The second line of e.lower.bound.basic.split at the actual carriers.
With S = S_z the constant-load minimizer at P_z and T = tilde S_z a
doubled response field on the cell,
fint_R (S+T) . bfA (S+T)
= P_z . bfA(R) P_z + 2 P_z . fint_R bfA (tilde S_z) + fint_R tilde S_z . bfA tilde S_z .
This is LocalizationBasicSplit.two_mul_doubledMuValue_add_eq with the load
instantiated at e.Pz.def; the factor 2 is that module's normalization
convention.: on the two binders hS, hT, both of which
exists_localizationActualCellFields produces.
The whole descendant family #
The per-cell split over the whole localization family.
S and T are the families z |-> S_z and z |-> tilde S_z, and the cell
field is defined as fun R => S R + T R, so "Observe that X_z = S_z + tilde S_z" is literally true of it. Every conclusion is quantified over
descendantsAtDepth Q j, the rendering of 3^n Z^d cap cu_K.
: on hwN, the defining property of w_{N,e'}^{(K)}.
The term consumer #
A generic pre-mesh intermediate toward the insertion step and the first line
of e.lower.bound.basic.split. This is NOT the manuscript's first insertion
line: the printed line carries the mesh average over the scale-n grid and the
actual cutoff coefficient bfA_m (the
coefficientCutoffTriadicCoeffFamily.coeffOn instantiation) on the cube and on
every cell; here the per-cell coefficient family aCell is abstract and the
mesh average is not composed. Both are the successor module's mandate.
P . bfA_m(cu_K) P <= fint_{cu_K} X . bfA_m X ,
X = sum_{z} (S_z + tilde S_z) 1_{z+cu_n} , P = bfAhom_{m-h}^{-1/2}(e'; e) .
Genuine ingredients: P is e.recurrence.P.def, the cell fields are the
actual S_z + tilde S_z, and the background whose class they live in is the
actual bfAhom_{m-h}^{-1/2}(e' + grad w_D; e + grad w_N + shom^{-1} h e'),
whose membership in P + L^2_{pot,0}(cu_K) x Lsolo(cu_K) is derived by
isDoubledMuAdmissible_localizationBackground and not assumed. NOT yet
genuine: the coefficient family (abstract aCell, not the actual cutoff
coefficients) and the mesh form (absent).
Per this direction, and only this direction, is available; the mesh average of the right-hand side is a separate lane's item.
: on hwN, the defining property of w_{N,e'}^{(K)}.