CoarseEllipticityBounds

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

theorem Algsuperdiff.Frozen.Section3.coarse_ellipticity_bounds (d : ℕ) : ∃ (Ccg : ℝ), 0 < Ccg ∧ ∀ (M : Section3.ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Ccg / sigma)) (Section3.Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (q : Section3.CoarseEllipticityExponent) (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1), Section3.Probability.IsLowerIntegerFamilyOrlicz (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) (fun (L : ℤ) (omega : Section3.Cutoff.CutoffSample d) => Section3.Observable.cutoffLowerEllipticityInv M m L s ⋯ q omega * ↑(Section3.Annealed.sigmaBar M (m - 1))) (m - 1) (Section3.lowerEllipticityProfile Ccg M.gamma s q) (Real.exp (-(Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) ∧ Section3.Probability.IsDeterministicShiftTwoTermOneSidedOrlicz (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) (fun (omega : Section3.Cutoff.CutoffSample d) => Section3.Observable.cutoffUpperEllipticity M m m s ⋯ q omega * (↑(Section3.Annealed.sigmaBar M (m - 1)))⁻¹) Ccg (Ccg * (Section3.Disorder.cstar M)⁻¹ * s * M.gamma * (2 * s - M.gamma)⁻¹ ^ 3) (Real.exp (-(Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))