InductionBounds

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

theorem Algsuperdiff.Frozen.Section3.induction_bounds (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → (∀ (m : ℤ) (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1), Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Section3.Observable.cutoffHomogenizationError M m ⟨s, ⋯⟩) (C * (Section3.Disorder.cstar M)⁻¹ * s⁻¹ * √M.gamma) (Real.exp (-(C⁻¹ * Section3.Disorder.cstar M ^ 3 * M.gamma⁻¹)))) ∧ ∀ (m : ℤ), |↑(Section3.Annealed.sigmaBar M m) - √(M.nu ^ 2 + Section3.Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m))| ≤ C * (Section3.Disorder.cstar M)⁻¹ ^ 2 * √M.gamma * |Real.log M.gamma| * ↑(Section3.Annealed.sigmaBar M m)