LocalizationFluctuationPerCube #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The per-cube fluctuation bound of Step 2, at the localization carriers #
Source displays in ABK26, inside Step 2 of l.approximate.recurrence.formula:
- The Euler--Lagrange identity and the block Besov duality bound (proved as
LocalizationFluctuationDuality.two_mul_doubledMuValue_le_besovDualityConst_localizationFz); - The doubled coarse Poincare inequality (proved as
partialSeminormTwo_blockGaugeDown_le_of_isDoubledResponseField); - The self-improvement that cancels one power of
|| bfA_m^{1/2} tilde S_z ||, the cross-term bound; - The display
e.lower.bound.localization.terms, whose bracketed integrand is2 P_z. fint bfA_m tilde S_z + fint tilde S_z. bfA_m tilde S_z-- verbatim the two fluctuation summands ofLocalizationRecurrenceMesh.exists_localizationRecurrenceMeshSplit_le_descendantsAverage_expanded.
What is proved #
2 (kappa Theta^2) | bfAhom^{1/2} P_z | Bg + (kappa Theta Bg)^2 ,
kappa = besovDualityConst R s being the pinned constant, Theta = doubledPoincareEllipticityFactor the factor of e.CG.Poincare.doubled.vars, and
Bg any envelope of the finite-depth positive q = 2 Besov seminorms of the
gauged bfF_z.
The cross term is taken by the depth-zero route
(CoarseEllipticity.abs_blockVecDot_cubeAverage_le), after the gauge
conjugation.
Binders #
Beyond the geometry (hsub), the defining property of w_{N,e'}^{(K)}
(hwN), the names of tilde S_z (hT, hresp) and the exponent/gauge
windows 0 < s < 1, 0 < sigma_0, the hypotheses are the analytic side
conditions of the two consumed displays: four L^2 memberships, two
integrabilities of the gauged pairing integrands, the sign of Bg and the two
positive-seminorm envelopes. They are conditional A obligations of this
module, discharged by the caller at its carrier, and are not premises of the
pinned source statement. No smallness, moment or measurability proposition
occurs.
Scope #
No anchor, frozen theorem or external input is consumed, and there is no
sorry.
References #
- ABK26,
l.approximate.recurrence.formulaStep 2.
Integrability of the coordinates of an L^2 field #
A field in L^2 of the normalized cube measure has integrable coordinates on
the cube.
A linear functional of an L^2 field is integrable on the cube.
The cube average of a linear functional of a field is the functional of the cube average.
The cross term by the depth-zero route #
** at the localization cell, after the gauge conjugation.**
| fint_R P_z . bfA_m tilde S_z | <= | bfAhom^{1/2} P_z | * Bu
for any envelope Bu of the finite-depth negative q = 2 Besov seminorms of
the two components of bfAhom^{-1/2} bfA_m tilde S_z, the doubled norm being
read in the component-sum rendering blockVecNormSum.
: the two L^2 memberships and the two envelopes are caller obligations.
The pinned duality constant is nonnegative #
The per-cube bound #
The bracketed integrand on one mesoscopic cell.
2 P_z . fint_R bfA_m tilde S_z + 2 mu_R(tilde S_z)
<= 2 kappa Theta^2 | bfAhom^{1/2} P_z | Bg + (kappa Theta Bg)^2 ,
kappa = besovDualityConst R s, Theta = doubledPoincareEllipticityFactor,
and Bg an envelope of the finite-depth positive q = 2 Besov seminorms of
the gauged bfF_z. The two summands carry exactly the manuscript's power of
the ellipticity factor: once in the cross term and once in the quadratic term.
The left-hand side is verbatim the fluctuation part of the integrand of
LocalizationRecurrenceMesh.exists_localizationRecurrenceMeshSplit_le_descendantsAverage_expanded.
as described in the module docstring.
The per-cube bound with the ellipticity factor in the gauged form. The
square of the Poincare factor is replaced by 32 c_{s,2}^{-1} times
gaugedEllipticitySum, which is the quantity the ellipticity display then
transfers from the mesoscopic cell to the recurrence scale by
gaugedEllipticitySum_descendant_le.