LocalizationFluctuationOrthogonality #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Euler--Lagrange identity of Step 2 at the genuine localization carriers #
Source displays in ABK26:
e.Fz.def, the background fieldbfF_z;- the
tilde S_zdisplay;fint_{z+cu_n} tilde S_z . bfA_m tilde S_z = fint_{z+cu_n} bfF_z . bfA_m tilde S_z .
What this module does #
two_mul_doubledMuValue_eq_volumeAverage_of_isDoubledMuMinimizerField
proves the identity for an abstract ambient slope field F. This module
instantiates it at the manuscript's own data: the localization cell
R = z + cu_n, the background localizationFz of e.Fz.def, and the ambient
premise discharged by
LocalizationActualBackground.isDoubledAmbientField_localizationFz. Existence
of the argmin at the same carriers is instantiated alongside, so the identity
is never asserted about a field that has not been produced.
What mean-zeroness is used for -- the duality step, where bfF_z enters the
pairing through its cube fluctuation -- is prepared by
localizationFz_potential_eq_smul_cubeFluctuationVec and its flux companion,
which record that both legs of e.Fz.def are literal cube fluctuations on the
very cell R that indexes them.
Binders #
sigma, omega, lowScale, highScale, e', Q, R, wD, wN are the
manuscript's own data; hwN is the defining property of w_{N,e'}^{(K)};
hsub : openCubeSet R subseteq openCubeSet Q is the descendant geometry of the
mesoscopic tiling, discharged at the call sites. The two mean-zero statements
carry, in addition, the cube integrability of the corrector gradient and of the
Neumann flux field on the cell; these are conditional A obligations of this
module, not premises of the pinned source statement. No smallness or moment
proposition occurs.
Scope #
No anchor, frozen theorem or external input is consumed, and there is no
sorry.
References #
- ABK26,
l.approximate.recurrence.formulaStep 2;e.Fz.def; thetilde S_zdisplay.
bfF_z is a cube fluctuation on its own cell #
The potential leg of e.Fz.def is a scaled cube fluctuation. This is
the structural form of the manuscript's "bfF_z has mean zero in z + cu_n":
the subtracted constant is the average over the very cell that indexes the
field.
The flux leg of e.Fz.def is a scaled cube fluctuation.
The cell mean-zeroness of e.Fz.def, potential leg. bfF_z has zero
average on z + cu_n. This is the property the manuscript quotes it is not
what proves, but it is exactly what the duality step needs, since the upstream
duality theorem pairs against a cube fluctuation.
: on the cube integrability hwD of the corrector gradient, which is what
makes the subtracted average finite.
The cell mean-zeroness of e.Fz.def, flux leg.
at the genuine carriers #
The Euler--Lagrange identity, at the manuscript's own data. For a
minimizer T = tilde S_z of the doubled energy over bfF_z + (L^2_{pot,0} x Lsolo)(R),
fint_R tilde S_z . bfA_m tilde S_z = fint_R bfF_z . bfA_m tilde S_z ,
in the factor-2 normalization of LocalizationBasicSplit.lean
(fint X . bfA X = 2 * doubledMuValue).
The ambient premise is discharged by isDoubledAmbientField_localizationFz;
mean-zeroness of bfF_z is used nowhere.