PrincipalResponseMomentsCloseEighth

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

Binder descriptions below are an informal inventory only, NOT a source certification; certification vocabulary is reserved for frozen source-facing declarations.

Provider: the eighth-moment display

The second inequality of the first moment display in Step 3 of l.approximate.recurrence.formula reads,

E[ |Ahom_{m-1}^{-1/2} A_m(cu_n) Ahom_{m-1}^{-1/2}|^8 ]^{1/8}
  <= C E[ ( shom_{m-1}^{-1} Lambda_{cgamma,1}(cu_m)
             + shom_{m-1} lambda^{-1}_{cgamma,1}(cu_m) )^8 ]^{1/8}
  <= C cgamma^{-1} .

This module supplies the second inequality, i.e. the eighth moment of the gauged sum of the two multiscale ellipticity endpoints, directly from the frozen coarse-graining ellipticity anchor Algsuperdiff.Frozen.Section3.coarse_ellipticity_bounds at s = cgamma, q = finite 1. The first inequality (the deterministic operator bound) is the subject of PrincipalResponseMomentsOperator.lean and is not touched here.

How the anchor is used

The anchor supplies, for one dimensional constant Ccg, two weak-Orlicz legs:

• an IsDeterministicShiftTwoTermOneSidedOrlicz upper leg for Lambda_{s,q}(cu_m; a_m) shom_{m-1}^{-1}, at deterministic shift Ccg and two lanes Gamma_1 and Gamma_{(1-sigma)/3}, of amplitudes Ccg cstar^{-1} s cgamma (2s-cgamma)^{-3} and exp(-Ccg^{-1}E^{-2}cgamma^{-1});
• an IsLowerIntegerFamilyOrlicz lower leg for lambda^{-1}_{s,q}(cu_m; a_L) shom_{m-1} valid simultaneously for every L >= m-1 with a single witness, at deterministic profile lowerEllipticityProfile Ccg cgamma s q and one lane Gamma_{(1-sigma)/2} of amplitude exp(-Ccg^{-1}E^{-2}cgamma^{-1}).

Adding the two endpoints therefore gives one deterministic shift and three lanes, which is exactly the hypothesis of the engine integral_rpow_eight_le_of_shift_add_three_orlicz. Because the lower carrier's witness does not depend on L, the supremum over L >= m-1 costs nothing: the statement below is uniform in L, quantified after the moment.

The free exponent sigma of the anchor is instantiated at its most permissive admissible value sigma = 1/2, which is also the value that makes the anchor's own premise exp(Ccg/sigma) <= E weakest. The two small lanes then sit at the fixed classes Gamma_{1/6} and Gamma_{1/4}, so the moment constants are absolute and no uniformity in sigma is needed.

Where s = cgamma sits in the window

The anchor's window is s in [cgamma/2 + exp(-Ccg^{-1}E^{-2}cgamma^{-1}), 1]. Taking s = cgamma requires exp(-Ccg^{-1}E^{-2}cgamma^{-1}) <= cgamma/2, which is a genuine smallness condition; it is carried below as the explicit gate hgap, stated with the exported constant C (which the proof chooses >= Ccg, so that hgap implies the anchor's own window condition). No printed buffer constant is hard-coded, as required.

This is lowerEllipticityProfile_at_gamma_one.

Main results

• coarseExponentOne: the admissible finite exponent q = 1.
• lowerEllipticityProfile_at_gamma_one: the corrected lower profile collapses to Ccg at s = cgamma, q = finite 1.
• integral_coarseEllipticityGauge_rpow_eight_le: the eighth-moment bound.

References

• ABK26 (the moment display of Step 3).
• ABK26, p.cg.ellipticity.bounds.
• ABK26, e.cgamma.constraints ("increasing M.").

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.coarseExponentOne : CoarseEllipticityExponent

The admissible finite exponent q = 1.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.lowerEllipticityProfile_at_gamma_one (Ccg gamma : ℝ) (hgamma : 0 < gamma) : lowerEllipticityProfile Ccg gamma gamma coarseExponentOne = Ccg

The corrected lower profile is Ccg at s = cgamma, q = 1. The base s / (2s - cgamma) of the corrected finite-q real power is exactly 1 there, so its pole is inert.

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.eighthLaneConst (Ccg : ℝ) : ℝ

The aggregate lane constant of the display: the deterministic shifts of the two legs plus the three class constants of the lanes, at sigma = 1/2.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.eighthLane_rpow_absorption {d : ℕ} (M : ABKModel d) (E Ccg C : ℝ) (hCcg0 : 0 < Ccg) (hLaneC : eighthLaneConst Ccg ≤ C) : (4 * (2 * Ccg + orliczEighthMomentScale 1 * (Ccg * (Disorder.cstar M)⁻¹ * M.gamma⁻¹) + orliczEighthMomentScale ((1 - 1 / 2) / 3) * Real.exp (-(Ccg⁻¹ * E⁻¹ ^ 2 * M.gamma⁻¹)) + orliczEighthMomentScale ((1 - 1 / 2) / 2) * Real.exp (-(Ccg⁻¹ * E⁻¹ ^ 2 * M.gamma⁻¹)))) ^ 8 ≤ (C * (Disorder.cstar M)⁻¹ * M.gamma⁻¹) ^ 8

Absorb the common deterministic and Orlicz lanes into the eighth-moment constant.

The eighth moment of the gauged ellipticity sum

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integral_coarseEllipticityGauge_rpow_eight_le (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m - 1) E → max (Real.exp (2 * C)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → M.gamma / 2 + Real.exp (-(C⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)) ≤ M.gamma → ∀ (L : ℤ), m - 1 ≤ L → MeasureTheory.MemLp (fun (omega : Cutoff.CutoffSample d) => Observable.cutoffUpperEllipticity M m m M.gamma ⋯ coarseExponentOne omega * (↑(Annealed.sigmaBar M (m - 1)))⁻¹ + Observable.cutoffLowerEllipticityInv M m L M.gamma ⋯ coarseExponentOne omega * ↑(Annealed.sigmaBar M (m - 1))) 8 ↑(Cutoff.cutoffSampleLaw M) ∧ ∫ (omega : Cutoff.CutoffSample d), (Observable.cutoffUpperEllipticity M m m M.gamma ⋯ coarseExponentOne omega * (↑(Annealed.sigmaBar M (m - 1)))⁻¹ + Observable.cutoffLowerEllipticityInv M m L M.gamma ⋯ coarseExponentOne omega * ↑(Annealed.sigmaBar M (m - 1))) ^ 8 ∂↑(Cutoff.cutoffSampleLaw M) ≤ (C * (Disorder.cstar M)⁻¹ * M.gamma⁻¹) ^ 8

The second inequality of the moment display at ABK26.

For one constant C depending only on the dimension, whenever the induction state holds at scale m-1 with parameter E, the parameters obey the anchor's own premises, and the anchor's lower window endpoint sits below cgamma, the gauged sum of the two multiscale ellipticity endpoints lies in L^8 and has eighth moment inside (C cstar^{-1} cgamma^{-1})^8, uniformly over the family index L >= m-1 of the anchor's lower leg.