BoundsMathcalEaL

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

Moment bounds for the two-scale coarse-graining error — [ABK] l.bounds.mathcal.E.aL

Every p-th moment of the two-scale flux-corrected error observable between scales n <= m is bounded, in the admissible range of p, by the p-th power of C 3^{s(m-n)/2} sqrt p (s^{-1} + sqrt (m-n)) sqrt gamma: the error is sub-Gaussian at size sqrt gamma, with a geometric loss in the scale gap.

Proved; reduces to the standard axioms.

theorem Algsuperdiff.Frozen.Section4.bounds_mathcal_E_aL (d : ℕ) (cstar : ℝ) (_hcstar : 0 < cstar) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ C⁻¹ ^ 10 → ∀ (m n : ℤ), n ≤ m → ↑m ≤ ↑n + M.gamma⁻¹ → ∀ s ∈ Set.Icc (C ^ 2 * √M.gamma) (1 / 4), ∀ (hs : 0 < s), ∀ p ∈ Set.Icc (2 * ↑d * s⁻¹) (C⁻¹ * M.gamma⁻¹ * s), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Section4.Support.fluxCorrectedTwoScaleErrorObservableSup M m n ⟨s, hs⟩ omega ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * Real.rpow 3 (1 / 2 * s * (↑m - ↑n)) * √p * (s⁻¹ + √(↑m - ↑n)) * √M.gamma) ^ p