GammaTenLoadFold #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The cgamma^{10} grid fold with the load leg on the grid #
ABK26, Step 2 of l.approximate.recurrence.formula, at the carrier of
e.lower.bound.localization.terms.
The gap this module fills #
Closure.GammaTenGridFold.descendantsAverage_integral_fold_le_of_moments asks
for the load leg in the uniform per-cell form
forall R in the grid, E[ | bfAhom^{1/2} P_R |^4 ] <= Cload^4 .
Its producer cannot deliver that. The source display --- and therefore
Closure.GammaTenLoad.exists_gammaTenLoadConst --- is a grid average over
z in 3^n Zd cap cu_K, and the grid step of its proof is the tiling identity
avsum_R fint_R = fint_{cu_K}, which loses a factor 3^{jd} when read at a
single cell. This module therefore re-runs the fold with the load leg in the
grid form its producer really delivers,
hload : gridFourthMomentRoot mu (descendantsAtDepth Q j) G <= Cload ,
and changes nothing else.
What changes in the proof #
Only the cross term. In the uniform-load version the load leg is released
to a constant per cell before the grid average is taken; here it stays inside,
and the grid average of the product of two per-cell fourth roots is handled by
discrete Cauchy--Schwarz (Step5Basket.cubeFamilyAverage_sqrt_mul_le) followed
by Jensen for the concave square root on each factor
(JunctionDischargeStepFiveDisplay.cubeFamilyAverage_sqrt_le), giving
avsum_R E[ F_R G_R H_R ] <= a * gridFourthMomentRoot mu I G
* gridFourthMomentRoot mu I H .
The quadratic term is unchanged: it never involved the load, so
GammaTenGridFold.cubeFamilyAverage_integral_mul_sq_le_sq_gridFourthMomentRoot
is reused verbatim.
The numerical binder hthr of
descendantsAverage_integral_fold_le_of_grid_moments is identical to the
one of the uniform-load statement, so
GammaTenGridFold.exists_gamma_threshold_gridFold (c1 * Cload) c2 still
produces it: with the ellipticity leg at cgamma^{-2} and the oscillation
grid root at cgamma^{15} the cross term is c1 Cload cgamma^{13} and the
quadratic term c2 cgamma^{28}, both strictly above cgamma^{10}'s exponent.
Binders #
Measure theory and real arithmetic at a probability measure: the pointwise
nonnegativity of the three families, the L^p memberships of the Hoelder
pairing at each cell, the per-cell integrability of the two products, and the
three moment bounds. No smallness gate is assumed. Nothing about the
corrector, the coefficient field or the cube geometry occurs.
Scope #
There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.
References #
- ABK26,
l.approximate.recurrence.formulaStep 2,e.lower.bound.localization.terms, the load display,e.lower.bound.oscillations.
The grid root dominates the square root of the grid average of the per-cell square roots. Jensen for the concave square root, twice.
The cross term with the load leg on the grid.
The variant of
GammaTenGridFold.cubeFamilyAverage_integral_mul_mul_le_gridFourthMomentRoot
in which the load leg is controlled only in the grid-averaged form the source
display delivers:
avsum_R E[ F_R G_R H_R ] <= a * ( gridFourthMomentRoot mu I G
* gridFourthMomentRoot mu I H ) .
The per-cell step is the same Hoelder triple as the uniform-load version; the
grid step is discrete Cauchy--Schwarz
(Step5Basket.cubeFamilyAverage_sqrt_mul_le) followed by Jensen for the concave
square root on each of the two factors.
exactly as the uniform-load version, minus its uniform load binder.
The two legs added, with the load leg on the grid.
The grid-load variant of GammaTenGridFold.cubeFamilyAverage_integral_fold_le.
exactly as that statement, with its uniform load binder replaced by nothing:
the load is carried in the grid functional on the right.