BadEventEstimate

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

The bad event estimate — [ABK] l.bad.event.lemma

Under the induction state at scale m0 - 1, the probability that the local good event at scales n <= m around a base point z fails is at most the sum of two terms: a stretched-exponential term exp(-c cstar gamma^{-1} 3^{...}) carrying the triadic scale gap, and a doubly exponential rare term exp(-exp(c E^{-2} gamma^{-1})). The coarse constant Ccg is at least d^6.

Proved; reduces to the standard axioms.

theorem Algsuperdiff.Frozen.Section3.bad_event_estimate (d : ℕ) : ∃ (Ccg : ℝ) (c : ℝ), ↑d ^ 6 ≤ Ccg ∧ 1 ≤ Ccg ∧ 0 < c ∧ ∀ (M : Section3.ABKModel d) (m0 : ℤ) (E : { E : ℝ // 1 ≤ E }), inductionState M (m0 - 1) E → c⁻¹ * (Section3.Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (m n : ℤ), n ≤ m0 - 1 → (n < m → 3 ^ (5 * Section3.Provider.BadEvents.scaleGapPos n m) ≤ c * Section3.Disorder.cstar M * M.gamma⁻¹) → (n < m → ↑d * (↑m - ↑n) * Real.log 3 + Real.exp (1 / 8 * (Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)) ≤ Real.exp (1 / 4 * (Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) → ∀ (z : HCPolySupport.Vec d), (↑(Section3.Cutoff.cutoffSampleLaw M)).real (goodLocalEventAt M (2 * Ccg) m n z)ᶜ ≤ Real.exp (-(c * Section3.Disorder.cstar M * M.gamma⁻¹ * 3 ^ (-5 * Section3.Provider.BadEvents.scaleGapPos n m) * 3 ^ Section3.Provider.BadEvents.scaleGapPos m n)) + Real.exp (-Real.exp (c * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))