LocalizationFluctuationGammaFold #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The three quantitative folds of Step 2 of l.approximate.recurrence.formula #
ABK26, Step 2 of l.approximate.recurrence.formula. After the per-cube bound
(LocalizationFluctuationPerCube.perCube_localizationFluctuation_le), the
ellipticity transfer
(doubledPoincareEllipticityFactor_sq_le_descendant_gaugedEllipticitySum)
and the oscillation/Besov bridge
(cubeBesovPositiveVectorDepthAverage_le_descendantsAverage_sq)
have been applied, three purely quantitative folds remain between the proved
inputs and the display e.lower.bound.localization.terms. This module proves
all three, each as a standalone, unconditional statement.
1. The eighth-moment envelope #
sqrt(d 3^{g - p}) * sqrt( avsum_{R in mesh} ( E[ (F R)^4 ] )^2 ) ,
and leaves the squared fourth-moment grid average to the consumer. Here that average is closed by Cauchy--Schwarz in the sample,
( E[ X^4 ] )^2 <= E[ X^8 ] (any probability measure) ,
so the remainder is controlled by the eighth-moment grid average -- the
quantity that e.nablaw.in.L.eight supplies after the per-cube Jensen step and
the mesh tiling identity.
gridFourthMoment_mesoCubeGrid_le_interior_add_of_eighthMoment is the composed
form.
exists_gamma_threshold_mesh_boundary then absorbs the geometric factor: under
the recurrence's own large-cube gate 10^10 gamma^{-1} <= K - m the boundary
remainder is below gamma^100, for every prefactor, once gamma is small --
the machine-checked form of the manuscript's "increasing M in
e.cgamma.constraints, if necessary".
2. The multi-depth geometric fold #
The finite-depth positive q = 2 Besov seminorm that the duality leg consumes is
(sum_{j <= N} 3^{2 s j} A_j)^{1/2} in the depth averages A_j. Instantiating
the free-buffer oscillation display at buffer Q.scale - j bounds each A_j by
(A 3^{-(B + j)})^2 with a j-independent amplitude A -- the display's
second and third terms carry 3^{-N} 3^{gamma (n + N)} whose exponent
n + N = m - h does not move with the depth. For s <= 1/2 the ratio
3^{2s - 2} is at most 1/2, so the depth sum is geometric and
[ u ]_{B^s_{2,2}, <= N} <= sqrt 2 * A * 3^{-B}
uniformly in N. That is cubeBesovPositiveVectorPartialSeminormTwo_le_of_depthAverage_le,
whose conclusion is exactly the envelope Bg of the per-cube bound.
3. The annealed Hoelder fold #
ABK26 combines an ellipticity moment C gamma^{-1}, a load moment C and an
oscillation moment C gamma^{14} by Hoelder into gamma^{10}.
integral_mul_mul_le_L4_L4_L2 is the pairing itself, at the exponents 1/4 + 1/4 + 1/2 = 1 (the quadratic summand is the case g = h); the resulting
numerical obligation is c1 gamma^13 + c2 gamma^27 <= gamma^10, which
exists_gamma_threshold_holder_fold discharges for every pair of nonnegative
constants once gamma is small -- again the manuscript's "increasing M".
Auxiliary #
The descendantsAverage form of the grid
Cauchy--Schwarz (avsum F)^2 <= avsum F^2 is the step that passes from the grid
average of squared oscillation cells (the majorant of the Besov depth average)
to the grid average of their fourth powers, which is what
e.lower.bound.oscillations controls.
Binders #
Every statement below is either finite combinatorics, real arithmetic, or a
single application of Cauchy--Schwarz on a probability space. No smallness
gate is assumed: the three gamma-thresholds are produced, not required.
Nothing about the corrector, the coefficient field or the sample space is
assumed.
Scope #
There is no sorry.
References #
- ABK26,
l.approximate.recurrence.formulaStep 2,e.lower.bound.localization.terms,e.lower.bound.oscillations,e.nablaw.in.L.eight,e.recurrence.params.
Elementary rpow bookkeeping #
Fold 1: the eighth-moment envelope of the mesh boundary remainder #
Cauchy--Schwarz in the sample. On a probability space the square of a
fourth moment is below the eighth moment. This is the step that turns the
remainder of gridFourthMoment_mesoCubeGrid_le_interior_add into a consumer of
e.nablaw.in.L.eight.
on the nonnegativity of f and on the L^2 membership of f^4, which is the
standing integrability of the moment being formed.
The grid form of the previous statement: the squared fourth-moment grid average that the mesh transfer leaves open is below the eighth-moment grid average.
The mesh transfer, closed against an eighth-moment envelope. The
full-mesh fourth-moment average of e.lower.bound.oscillations is the interior
one plus a geometric boundary remainder carrying the square root of any
envelope E of the eighth-moment grid average -- which is exactly what
e.nablaw.in.L.eight supplies after the per-cube Jensen step and the mesh
tiling identity.
on the scale bookkeeping, the nonnegativity of F, the standing L^2
membership of the fourth powers, and the envelope hE.
Fold 1, continued: absorbing the boundary factor into a power of gamma #
The boundary remainder is below every power of gamma. Under the
recurrence's own large-cube gate, read on the mesh as 10^10 gamma^{-1} <= p - g with p = K - n the mesh depth and g = (m-h) - n the window gap, the
geometric boundary factor of the mesh transfer, times any prefactor C >= 0,
is at most gamma^100 once gamma is small.
The threshold is produced, not assumed: this is the machine-checked form of
the manuscript's "for a sufficiently large choice of M in
e.cgamma.constraints".
Fold 3: the annealed Hoelder fold #
The three-factor Hoelder inequality in L^4 x L^4 x L^2. This is the
pairing the manuscript uses: the ellipticity moment, the load moment and the
oscillation moment enter at the exponents 1/4 + 1/4 + 1/2 = 1. Taking g = h gives the quadratic term of e.lower.bound.localization.terms.
: the four L^2 memberships are the analytic side conditions of the two
Cauchy--Schwarz steps and are caller obligations; they are not premises of the
pinned source statement.