ProportionGoodScales

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

Proportion of good scales — [ABK] p.independence.between.scales

Along any window of consecutive triadic scales the good events occur at almost every scale: the probability that the empirical proportion of good scales in a window of length Mw + 1 drops below 1 - theta decays exponentially in Mw, at a rate proportional to cstar^2 s^7 epsilon^2 theta / gamma.

Proved; reduces to the standard axioms.

theorem Algsuperdiff.Frozen.Section4.proportion_of_good_scales (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d) (s ep theta : ℝ), s ∈ Set.Ioc 0 (1 / 2) → ep ∈ Set.Ioc 0 (1 / 2) → theta ∈ Set.Ioc 0 (1 / 2) → M.gamma ≤ C⁻¹ * min (Section3.Disorder.cstar M ^ 10) (Section3.Disorder.cstar M ^ 2 * s ^ 5 * ep ^ 2) → 8 * M.gamma ≤ s → C * (Section3.Disorder.cstar M)⁻¹ ^ 2 * s⁻¹ ^ 6 * ep⁻¹ ^ 2 * M.gamma ≤ theta → ∀ (m0 : ℤ) (Mw : ℕ) (hs : 0 < s), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | 1 / (↑Mw + 1) * ∑ k ∈ Finset.range (Mw + 1), (goodEventAt M (Section4.Support.cgEllipLowerConstant d) (m0 + ↑k) 0 ⟨s, hs⟩ ep).indicator (fun (x : Section3.Cutoff.CutoffSample d) => 1) omega ≤ 1 - theta} ≤ ENNReal.ofReal (6 * Real.exp (-(Section3.Disorder.cstar M ^ 2 * s ^ 7 * ep ^ 2 * theta * (↑Mw + 1)) / (C * M.gamma)))