LocalizationFluctuationNumericEllipticity

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

The numeric ellipticity moment of Step 2, and the closure

LocalizationFluctuationEllipticity.gaugedEllipticitySum is the quantity the Step-2 fluctuation fold integrates, shom^{-1} Lambda_{s,2}(Q; a) + shom lambda_{s,2}^{-1}(Q; a), and the two halves are proved:

• the geometric half, LocalizationFluctuationAncestor.doubledPoincareEllipticityFactor_sq_le_recurrenceAncestor, which reads the per-cell display at the cell's own scale-m ancestor;
• the probabilistic half, integral_gaugedEllipticitySum_pow_ancestorAtScale_eq_originCube, which transports the annealed moment from that ancestor back to cu_m.

What was still missing is the number: a bound on the annealed fourth moment of the gauged sum at cu_m itself.

The carrier bridge

The anchor speaks about Observable.cutoffUpperEllipticity and Observable.cutoffLowerEllipticityInv, i.e. about Ch04.LambdaSqCoeffField and Ch04.lambdaSqCoeffField of the coefficient field coefficientCutoff M.nu L, while gaugedEllipticitySum reads Ch02.LambdaSq and Ch02.lambdaSq of the triadic family coefficientCutoffTriadicCoeffFamily M L. On the a.e.-elliptic support the Chapter-4 observables are the Chapter-2 ones of the canonical dependent family (Ch04.LambdaSqCoeffField's own dite_eq_left branch), and the two families have the same underlying coefficient field on every cube, so Ch02.LambdaSq_eq_ofAEEq identifies them exactly. The exported observables are their literals (Observable.cutoffUpperEllipticity_eq_literal), the clamp being inert. gaugedEllipticitySum_eq_cutoffObservables is the resulting identity; nothing is lost and no inequality is used.

The exponent

gaugedEllipticitySum is hard-coded at the Chapter-2 exponent q = 2, whereas the proved PrincipalResponseMomentsCloseEighth.integral_coarseEllipticityGauge_rpow_eight_le instantiates the anchor at q = 1. The anchor is quantified over every admissible q, and the corrected lower profile collapses to Ccg at s = gamma for q = 2 as well -- there through the q >= 2 branch `Ccg * s * (2s

• gamma)^{-1}, whose value at s = gammaisCcg exactly (lowerEllipticityProfile_at_gamma_two). So the q = 2` instantiation runs verbatim, with the same three lanes and the same constants.

From the eighth moment to the fourth

The engine integral_rpow_eight_le_of_shift_add_three_orlicz produces the eighth moment. The fourth follows by Cauchy--Schwarz against the constant 1 on the probability space (sq_integral_le_integral_sq_of_isProbabilityMeasure below, proved by expanding 0 <= E[(f - E f)^2]), which costs nothing: E[X^4] <= E[X^8]^{1/2} <= ((C cstar^{-1} gamma^{-1})^8)^{1/2}.

What is proved

• coarseExponentTwo, lowerEllipticityProfile_at_gamma_two.
• aeeq_triadicCoeffFamily_coefficientCutoff, LambdaSq_originCube_coefficientCutoffTriadicCoeffFamily_eq, lambdaSq_originCube_coefficientCutoffTriadicCoeffFamily_eq, gaugedEllipticitySum_eq_cutoffObservables -- the bridge, exact identities.
• measurable_gaugedEllipticitySum_originCube -- the measurability the stationarity transport needs, as a theorem rather than a binder.
• integral_gaugedEllipticitySum_rpow_eight_le -- the eighth moment at q = 2.
• integral_gaugedEllipticitySum_pow_four_le -- the numeric fourth moment, E[(shom_{m-1}^{-1} Lambda_{gamma,2}(cu_m) + shom_{m-1} lambda_{gamma,2}^{-1}(cu_m))^4] <= (C cstar^{-1} gamma^{-1})^4.
• integral_gaugedEllipticitySum_pow_four_ancestorAtScale_le -- the end-to-end closure: the same numeric bound at the cell's own scale-m ancestor, which is the carrier the geometric half delivers.

Binders

integral_gaugedEllipticitySum_pow_four_le carries exactly the anchor's own premises -- the induction state at m - 1, max (exp (2C)) cstar^{-1} <= E, E <= gamma^{-1/5}, and the window gate gamma/2 + exp(-C^{-1}E^{-2}gamma^{-1}) <= gamma which says that s = gamma lies in the anchor's own window -- and nothing else. The ancestor version adds hm : R.scale <= m, the existence of the ancestor. No moment, smallness or measurability proposition is assumed: the measurability that the stationarity transport asks for is produced by measurable_gaugedEllipticitySum_originCube.

The sigmabar conversion

The anchor's gauge is sigmabar_{m-1}; a consumer reading the fold at sigmabar_{m-h} converts with gaugedEllipticitySum_gauge_change from the proved running-carrier caps Provider.Multiscale.sigmaBar_le_four_mul_sigmaBar (down) and DisplayBridge.sigmaBar_le_thirtySix_mul_sigmaBar (up), which are the lower-infinite-carrier producers names, in this repository's cstar <= 3/2 form. The up cap carries its own gap gate m <= n + cstar gamma^{-1}, which the recurrence's h <= 6 cstar gamma^{-1} does not imply; the conversion is therefore left to the caller, who has the shell data, rather than performed here under a smuggled gate.

References

• ABK26, l.approximate.recurrence.formula Step 2, and the moment average; p.cg.ellipticity.bounds.

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

The admissible finite exponent q = 2 at which gaugedEllipticitySum reads the two multiscale ellipticity constants.

Equations

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

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

The corrected lower profile is Ccg at s = cgamma, q = 2. The q >= 2 branch is Ccg s (2s - cgamma)^{-1}, which is Ccg exactly at s = cgamma.

The carrier bridge

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.aeeq_triadicCoeffFamily_coefficientCutoff {d : ℕ} (M : ABKModel d) (L : ℤ) (omega : Cutoff.CutoffSample d) : (HCPolySupport.Book.Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField (Cutoff.coefficientCutoff M.nu L omega) ⋯).AEEq (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega)

Unconditional. The canonical dependent Chapter-2 family of the cutoff coefficient field and the Chapter-2 family of the cutoff are a.e. equal on every cube: they carry the very same underlying coefficient field, and differ only in the locally derived ellipticity witness.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.LambdaSq_originCube_coefficientCutoffTriadicCoeffFamily_eq {d : ℕ} (M : ABKModel d) (m L : ℤ) {s : ℝ} (hs : 0 < s) (omega : Cutoff.CutoffSample d) : HCPolySupport.Book.Ch02.LambdaSq (HCPolySupport.originCube d m) s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) = Observable.cutoffUpperEllipticity M m L s hs coarseExponentTwo omega

The upper half of the bridge, an exact identity. The Chapter-2 upper multiscale ellipticity of the cutoff family at cu_m and exponent q = 2 is the anchor's own observable Observable.cutoffUpperEllipticity.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.lambdaSq_originCube_coefficientCutoffTriadicCoeffFamily_eq {d : ℕ} (M : ABKModel d) (m L : ℤ) {s : ℝ} (hs : 0 < s) (omega : Cutoff.CutoffSample d) : (HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d m) s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega))⁻¹ = Observable.cutoffLowerEllipticityInv M m L s hs coarseExponentTwo omega

The lower half of the bridge, an exact identity.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gaugedEllipticitySum_eq_cutoffObservables {d : ℕ} (M : ABKModel d) (m L : ℤ) {s : ℝ} (hs : 0 < s) (sigmaBar : ℝ) (omega : Cutoff.CutoffSample d) : gaugedEllipticitySum sigmaBar (HCPolySupport.originCube d m) s (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) = Observable.cutoffUpperEllipticity M m L s hs coarseExponentTwo omega * sigmaBar⁻¹ + Observable.cutoffLowerEllipticityInv M m L s hs coarseExponentTwo omega * sigmaBar

The bridge. The gauged ellipticity sum of the cutoff family at cu_m is the anchor's own gauged sum of observables.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_gaugedEllipticitySum_originCube {d : ℕ} (M : ABKModel d) (m L : ℤ) {s : ℝ} (hs : 0 < s) (sigmaBar : ℝ) : Measurable fun (omega : Cutoff.CutoffSample d) => gaugedEllipticitySum sigmaBar (HCPolySupport.originCube d m) s (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega)

The measurability the stationarity transport asks for, as a theorem. The gauged ellipticity sum at cu_m is a measurable function of the sample.

Cauchy--Schwarz against the constant on a probability space

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.sq_integral_le_integral_sq_of_isProbabilityMeasure {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {f : Omega → ℝ} (hf : MeasureTheory.Integrable f mu) (hf2 : MeasureTheory.Integrable (fun (x : Omega) => f x ^ 2) mu) : (∫ (x : Omega), f x ∂mu) ^ 2 ≤ ∫ (x : Omega), f x ^ 2 ∂mu

Unconditional apart from the two integrabilities. On a probability space the square of the mean is below the mean of the square.

The eighth moment at q = 2

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

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

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gaugeEighthLaneConst Ccg = Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.eighthLaneConst Ccg

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integral_gaugedEllipticitySum_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 → MeasureTheory.MemLp (fun (omega : Cutoff.CutoffSample d) => gaugedEllipticitySum (↑(Annealed.sigmaBar M (m - 1))) (HCPolySupport.originCube d m) M.gamma (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega)) 8 ↑(Cutoff.cutoffSampleLaw M) ∧ ∫ (omega : Cutoff.CutoffSample d), gaugedEllipticitySum (↑(Annealed.sigmaBar M (m - 1))) (HCPolySupport.originCube d m) M.gamma (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) ^ 8 ∂↑(Cutoff.cutoffSampleLaw M) ≤ (C * (Disorder.cstar M)⁻¹ * M.gamma⁻¹) ^ 8

The eighth moment of the gauged ellipticity sum at cu_m, at the Chapter-2 exponent q = 2.

This is the q = 2 instance of the anchor at s = cgamma, sigma = 1/2, read through the carrier bridge, so that the observable is literally gaugedEllipticitySum -- the quantity the Step-2 fold integrates.

on the permitted frozen theorem coarse_ellipticity_bounds and on its own premises hstate, hE, hEupper, hgap.

The numeric fourth moment

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integral_gaugedEllipticitySum_pow_four_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 → ∫ (omega : Cutoff.CutoffSample d), gaugedEllipticitySum (↑(Annealed.sigmaBar M (m - 1))) (HCPolySupport.originCube d m) M.gamma (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) ^ 4 ∂↑(Cutoff.cutoffSampleLaw M) ≤ (C * (Disorder.cstar M)⁻¹ * M.gamma⁻¹) ^ 4

The numeric fourth moment of the Step-2 gauged ellipticity sum.

on the permitted frozen theorem coarse_ellipticity_bounds and on its own premises.

The end-to-end closure

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integral_gaugedEllipticitySum_pow_four_ancestorAtScale_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 → ∀ (R : HCPolySupport.TriadicCube d), R.scale ≤ m → ∫ (omega : Cutoff.CutoffSample d), gaugedEllipticitySum (↑(Annealed.sigmaBar M (m - 1))) (ancestorAtScale R m) M.gamma (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) ^ 4 ∂↑(Cutoff.cutoffSampleLaw M) ≤ (C * (Disorder.cstar M)⁻¹ * M.gamma⁻¹) ^ 4

The numeric fourth moment at the cell's own scale-m ancestor.

The geometric half (doubledPoincareEllipticityFactor_sq_le_recurrenceAncestor) puts the per-cell display on ancestorAtScale R m; the probabilistic half (integral_gaugedEllipticitySum_pow_ancestorAtScale_eq_originCube) moves the annealed fourth moment from there to cu_m; and the value of that moment is the number below. No printed quantifier changes.

on hm : R.scale <= m (the ancestor exists) and on the anchor's own premises. The measurability that the transport asks for is produced, not assumed.