MultiscaleEstimate

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

theorem Algsuperdiff.Frozen.Section3.multiscale_estimate (d : ℕ) : ∃ (Cms : ℝ), 0 < Cms ∧ ∀ (M : Section3.ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), inductionState M (m - 1) E → ∀ epsilon ∈ Set.Ioc 0 (1 / 2), (Section3.Disorder.cstar M)⁻¹ * epsilon ^ (-Cms) ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1), ∃ (Y : Section3.Cutoff.CutoffSample d → ℝ) (Z : Section3.Cutoff.CutoffSample d → ℝ), Section3.Probability.IsTwoTermBigOWithWitnesses (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Section3.Observable.cutoffHomogenizationError M m ⟨s, ⋯⟩) Y Z (Cms * ↑E * s⁻¹ * √(epsilon * M.gamma)) (Cms * epsilon * s⁻¹ ^ 2 * Real.exp (-((↑E)⁻¹ ^ 3 * M.gamma⁻¹))) ∧ (s ≤ Cms * epsilon → HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) Y (Cms * epsilon * ↑E * s⁻¹ * √M.gamma))