GammaTenGridFold

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The grid annealed Hoelder fold of Step 2

ABK26, Step 2 of l.approximate.recurrence.formula, at the carrier of e.lower.bound.localization.terms.

The gap this module fills

LocalizationFluctuationSplitFoldArithmetic.integral_mul_mul_le_gamma_pow_twelve_of_regime performs the annealed Hoelder fold at one mesoscopic cell: it asks for the oscillation leg in the per-cell form E[h^2] <= (Cosc cgamma^{14})^2. No such per-cell moment is available. The proved oscillation producers --- the full-mesh endpoints exists_gamma0_freshShellDirichlet_step5MeshOscillation_le_gamma_pow_fifteen and its Neumann mirror --- control only the grid functional

  gridFourthMomentRoot mu (descendantsAtDepth cu_K j) osc
    =  ( avsum_{R} E[ osc_R^4 ] )^{1/4}   <=  cgamma^{15} ,

and the target of Step 2 is itself a grid average,

  fluctuationEnergyAverage  =  avsum_{R in descendantsAtDepth cu_K j} E[ cell_R ] .

So the fold has to be run jointly in the sample and on the grid: Hoelder in the sample per cell at the exponents 1/4 + 1/4 + 1/2 = 1, with the two uniform legs (ellipticity, load) released to constants, and then Jensen on the grid to collect the remaining oscillation legs into the single grid functional the producers bound. That joint step is what this module supplies.

What is proved

• integral_rpow_two_rpow_half_le_rpowFourRoot --- the L^2 leg of the Hoelder triple, released to the fourth-moment root that the grid functional is built from (Cauchy--Schwarz in the sample on a probability space).
• integral_mul_mul_le_mul_mul_rpowFourRoot --- the per-cell fold with its two uniform legs released: E[f g h] <= a b (E[h^4])^{1/4}.
• cubeFamilyAverage_integral_mul_sq_le_sq_gridFourthMomentRoot --- the quadratic term on the grid:

    avsum_R E[ F_R H_R H_R ]  <=  a * (gridFourthMomentRoot mu I H)^2 .
  

• The matching cross term avsum_R E[F_R G_R H_R], and the two legs added at the shape the per-cube bound of LocalizationFluctuationPerCube.perCube_localizationFluctuation_le delivers once its ellipticity factor has been replaced by LocalizationFluctuationEllipticity.gaugedEllipticitySum (both summands of the per-cube bound are then linear in that sum), are assembled from these pieces in Closure.GammaTenLoadFold.
• exists_gamma_threshold_gridFold --- the numerical obligation, at the exponents this route produces. With the ellipticity leg at cgamma^{-2} (LocalizationFluctuationSplitFoldArithmetic.gammaRegime_ellipticityLeg_le, the cstar^{-1} absorption) and the oscillation grid root at cgamma^{15}, the cross term is c1 cgamma^{13} and the quadratic term c2 cgamma^{28}; both exponents are strictly above 10, so exists_gamma_threshold_regime_holder_fold closes the fold. The threshold is produced, not assumed.

The exponent bookkeeping

leg	per cell	on the grid
ellipticity	(E[G^4])^{1/4} <= cgamma^{-2}	uniform in R
load	(E[L^4])^{1/4} <= Cload	uniform in R
oscillation	none	( avsum_[B_R^4] )^{1/4} <= cgamma^{15}

cross: cgamma^{-2} * Cload * cgamma^{15} = Cload cgamma^{13}; quadratic: cgamma^{-2} * (cgamma^{15})^2 = cgamma^{28}.

Binders

Everything below is measure theory and real arithmetic at a probability measure. The binders are the pointwise nonnegativity of the three families, the L^p memberships that the two Cauchy--Schwarz steps of LocalizationFluctuationGammaFold.integral_mul_mul_le_L4_L4_L2 require --- these are conditional A obligations, discharged by the caller at its carrier --- and the two uniform moment bounds. No smallness gate is assumed: the cgamma-threshold of exists_gamma_threshold_gridFold is produced. 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.formula Step 2, e.lower.bound.localization.terms, e.lower.bound.oscillations.

The L^2 leg of the Hoelder triple, released to the fourth-moment root

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integral_rpow_two_rpow_half_le_rpowFourRoot {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] {X : Omega → ℝ} (hX : ∀ (w : Omega), 0 ≤ X w) (hXm : MeasureTheory.MemLp X 4 mu) : (∫ (w : Omega), X w ^ 2 ∂mu) ^ (1 / 2) ≤ (∫ (w : Omega), X w ^ 4 ∂mu) ^ 4⁻¹

Cauchy--Schwarz in the sample, at the exponent the grid functional uses.

The oscillation leg of the annealed Hoelder fold enters as (E[h^2])^{1/2}, while gridFourthMomentRoot is built from E[h^4]. On a probability space the two are ordered:

  ( E[h^2] )^{1/2}  <=  ( E[h^4] )^{1/4} .

on the nonnegativity of h and on h in L^4, the standing integrability of the moment being formed.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.rpowFourRoot_le_of_integral_rpow_four_le {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) {X : Omega → ℝ} (hX : ∀ (w : Omega), 0 ≤ X w) {A : ℝ} (hA : 0 ≤ A) (h4 : ∫ (w : Omega), X w ^ 4 ∂mu ≤ A ^ 4) : (∫ (w : Omega), X w ^ 4 ∂mu) ^ (1 / 4) ≤ A

The fourth-moment bounds of the two uniform legs, in the fourth-root spelling the fold consumes. Unconditional apart from the sign of the majorant.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.rpowFourRoot_le_inv_sq_of_integral_rpow_four_le {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) {X : Omega → ℝ} (hX : ∀ (w : Omega), 0 ≤ X w) {gamma : ℝ} (hgamma : 0 < gamma) (h4 : ∫ (w : Omega), X w ^ 4 ∂mu ≤ (gamma ^ 8)⁻¹) : (∫ (w : Omega), X w ^ 4 ∂mu) ^ (1 / 4) ≤ (gamma ^ 2)⁻¹

The ellipticity leg at the regime amplitude. The proved producer LocalizationFluctuationSplitFoldArithmetic.exists_regime_gaugedEllipticitySum_pow_four_le delivers E[F^4] <= (cgamma^8)^{-1}; the fold consumes (E[F^4])^{1/4} <= (cgamma^2)^{-1}. The two are the same statement.

The per-cell fold with the two uniform legs released

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integral_mul_mul_le_mul_mul_rpowFourRoot {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (f g h : Omega → ℝ) (hf : ∀ (w : Omega), 0 ≤ f w) (hg : ∀ (w : Omega), 0 ≤ g w) (hh : ∀ (w : Omega), 0 ≤ h w) (hfm : MeasureTheory.MemLp (fun (w : Omega) => f w ^ 2) (ENNReal.ofReal 2) mu) (hgm : MeasureTheory.MemLp (fun (w : Omega) => g w ^ 2) (ENNReal.ofReal 2) mu) (hhm : MeasureTheory.MemLp h 4 mu) (hfgm : MeasureTheory.MemLp (fun (w : Omega) => f w * g w) (ENNReal.ofReal 2) mu) {a b : ℝ} (ha0 : 0 ≤ a) (hb0 : 0 ≤ b) (ha : (∫ (w : Omega), f w ^ 4 ∂mu) ^ (1 / 4) ≤ a) (hb : (∫ (w : Omega), g w ^ 4 ∂mu) ^ (1 / 4) ≤ b) : ∫ (w : Omega), f w * g w * h w ∂mu ≤ a * b * (∫ (w : Omega), h w ^ 4 ∂mu) ^ 4⁻¹

The three-factor Hoelder fold at one cell, with the ellipticity and load legs released to constants.

  E[ f g h ]  <=  a * b * ( E[h^4] )^{1/4}

whenever (E[f^4])^{1/4} <= a and (E[g^4])^{1/4} <= b. The point of the shape is that the third leg is left in the fourth-moment spelling, which is the one the grid functional gridFourthMomentRoot collects.

on the pointwise nonnegativity of the three factors and on the four L^p memberships of the two Cauchy--Schwarz steps; these are analytic side conditions of the pairing, not premises of the pinned source statement.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integral_mul_sq_le_mul_rpow_half {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (f h : Omega → ℝ) (hf : ∀ (w : Omega), 0 ≤ f w) (hh : ∀ (w : Omega), 0 ≤ h w) (hfm : MeasureTheory.MemLp (fun (w : Omega) => f w ^ 2) (ENNReal.ofReal 2) mu) (hhsqm : MeasureTheory.MemLp (fun (w : Omega) => h w ^ 2) (ENNReal.ofReal 2) mu) (hhm : MeasureTheory.MemLp h 4 mu) (hfhm : MeasureTheory.MemLp (fun (w : Omega) => f w * h w) (ENNReal.ofReal 2) mu) {a : ℝ} (ha0 : 0 ≤ a) (ha : (∫ (w : Omega), f w ^ 4 ∂mu) ^ (1 / 4) ≤ a) : ∫ (w : Omega), f w * h w * h w ∂mu ≤ a * (∫ (w : Omega), h w ^ 4 ∂mu) ^ 2⁻¹

The quadratic per-cell fold: the case g = h of the previous statement, with the second fourth-moment root also released against the third leg.

  E[ f h h ]  <=  a * ( E[h^4] )^{1/2} .

exactly as the cross term.

The two legs on the grid

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeFamilyAverage_integral_mul_sq_le_sq_gridFourthMomentRoot {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (I : Finset (HCPolySupport.TriadicCube d)) (F H : HCPolySupport.TriadicCube d → Omega → ℝ) (hF : ∀ (R : HCPolySupport.TriadicCube d) (w : Omega), 0 ≤ F R w) (hH : ∀ (R : HCPolySupport.TriadicCube d) (w : Omega), 0 ≤ H R w) (hFm : ∀ R ∈ I, MeasureTheory.MemLp (fun (w : Omega) => F R w ^ 2) (ENNReal.ofReal 2) mu) (hHsqm : ∀ R ∈ I, MeasureTheory.MemLp (fun (w : Omega) => H R w ^ 2) (ENNReal.ofReal 2) mu) (hHm : ∀ R ∈ I, MeasureTheory.MemLp (H R) 4 mu) (hFHm : ∀ R ∈ I, MeasureTheory.MemLp (fun (w : Omega) => F R w * H R w) (ENNReal.ofReal 2) mu) {a : ℝ} (ha0 : 0 ≤ a) (ha : ∀ R ∈ I, (∫ (w : Omega), F R w ^ 4 ∂mu) ^ (1 / 4) ≤ a) : (cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => ∫ (w : Omega), F R w * H R w * H R w ∂mu) ≤ a * gridFourthMomentRoot mu I H ^ 2

The quadratic term, folded on the grid.

  avsum_{R in I} E[ F_R H_R H_R ]  <=  a * ( gridFourthMomentRoot mu I H )^2 .

The grid step is Jensen for the concave square root (Closure.JunctionDischargeStepFiveDisplay.cubeFamilyAverage_sqrt_le).

exactly as the cross term.

The numerical obligation of the grid fold

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_gamma_threshold_gridFold (c1 c2 : ℝ) (hc1 : 0 ≤ c1) (hc2 : 0 ≤ c2) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ gamma0 ≤ 1 / 4 ∧ ∀ (gamma : ℝ), 0 < gamma → gamma ≤ gamma0 → ∀ (Bosc : ℝ), 0 ≤ Bosc → Bosc ≤ gamma ^ 15 → c1 * ((gamma ^ 2)⁻¹ * Bosc) + c2 * ((gamma ^ 2)⁻¹ * Bosc ^ 2) ≤ gamma ^ 10

The grid fold closes at cgamma^{10}.

With the ellipticity leg at a = cgamma^{-2} --- the cstar^{-1} absorption of LocalizationFluctuationSplitFoldArithmetic.gammaRegime_ellipticityLeg_le --- and the oscillation grid root at Bosc <= cgamma^{15} --- the full-mesh endpoints of e.lower.bound.oscillations --- the cross term is c1 cgamma^{13} and the quadratic term c2 cgamma^{28}. Both exponents are strictly above 10, so the sum is below cgamma^{10} once cgamma is small, for every pair of nonnegative absolute constants.

This is LocalizationFluctuationSplitFoldArithmetic.exists_gamma_threshold_regime_holder_fold read at the grid route's own numerals; the threshold is produced, not assumed.