BaseCase

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

theorem Algsuperdiff.Frozen.Section3.base_case (d : ℕ) : ∃ (C0 : ℝ) (Cstart : ℝ), 0 < C0 ∧ 0 < Cstart ∧ ∀ (M : Section3.ABKModel d), (∀ (m : ℤ), M.nu ≤ ↑(Section3.Annealed.sigmaBar M m) ∧ ↑(Section3.Annealed.sigmaBar M m) ≤ M.nu * (1 + Section3.Disorder.cstarPlus M * (2 * M.nu ^ 2)⁻¹ * M.gamma⁻¹ * (1 + 4 * M.gamma) * 3 ^ (2 * M.gamma * ↑m)) ∧ ∀ (s : { s : ℝ // s ∈ Set.Ioo 0 1 }), Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma 4) (Section3.Observable.cutoffHomogenizationError M m ⟨↑s, ⋯⟩) (C0 * M.nu⁻¹ * (√M.gamma)⁻¹ * 3 ^ (M.gamma * ↑m) * √(Section3.baseLoss d s)) (C0 * (√M.nu)⁻¹ * (√√M.gamma)⁻¹ * 3 ^ (M.gamma * ↑m / 2) * √√(Section3.baseLoss d s))) ∧ (∀ m ≤ Section3.mStarStar M, M.nu ≤ ↑(Section3.Annealed.sigmaBar M m) ∧ ↑(Section3.Annealed.sigmaBar M m) ≤ (1 + M.gamma ^ 2) * M.nu ∧ ∀ (s : { s : ℝ // s ∈ Set.Ioo 0 1 }), Section3.Probability.IsOneSidedOrlicz (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (Section3.Observable.cutoffHomogenizationError M m ⟨↑s, ⋯⟩) (C0 * (√(Section3.Disorder.cstarPlus M))⁻¹ * √M.gamma * √(Section3.baseLoss d s))) ∧ (∀ m ≤ Section3.mStar M, M.nu ≤ ↑(Section3.Annealed.sigmaBar M m) ∧ ↑(Section3.Annealed.sigmaBar M m) ≤ 2 * M.nu ∧ ∀ (s : { s : ℝ // s ∈ Set.Ioo 0 1 }), Section3.Probability.IsDeterministicShiftOneSidedOrlicz (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (Section3.Observable.cutoffHomogenizationError M m ⟨↑s, ⋯⟩) 2 (C0 * (√(Section3.Disorder.cstarPlus M))⁻¹ * √(Section3.baseLoss d s))) ∧ ∃ (Estart : { E : ℝ // 1 ≤ E }), ↑Estart = Cstart * (√(Section3.Disorder.cstar M))⁻¹ ∧ inductionState M (Section3.mStarStar M) Estart