DiffusivityAsymptotics

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

theorem Algsuperdiff.Frozen.Section3.diffusivity_asymptotics (d : ℕ) : ∃ (Cflow : ℝ), 0 < Cflow ∧ ∀ (M : Section3.ABKModel d) (m0 : ℤ) (E : { E : ℝ // 1 ≤ E }), Section3.mStar M < m0 → inductionState M (m0 - 1) E → Cflow * (Section3.Disorder.cstar M)⁻¹ ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → (∀ m ≤ m0, |↑(Section3.Annealed.sigmaBar M m) - √(M.nu ^ 2 + Section3.Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m))| ≤ Cflow * (Section3.Disorder.cstar M)⁻¹ * ↑E * √M.gamma * |Real.log M.gamma| * ↑(Section3.Annealed.sigmaBar M m)) ∧ 1 / 4 * max (Section3.Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m0)) (M.nu ^ 2) ≤ ↑(Section3.Annealed.sigmaBar M m0) ^ 2 ∧ ↑(Section3.Annealed.sigmaBar M m0) ^ 2 ≤ 4 * max (Section3.Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m0)) (M.nu ^ 2)