Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Probability.IndicatorDensity

IndicatorDensity #

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

Carrier-neutral indicator-density layer for the Appendix-D concentration output #

ABK26, §4.1. This module is the abstract-Ω bridge between Proposition p.concentration.for.scales (Algsuperdiff.Section4.Probability.ScalesConcentration.Statement) and the "proportion of good scales" statements of §4.1: it defines the Cesàro density of the scales at which a family of events holds, and proves the three purely measure-theoretic facts that every §4.1 ratio lemma consumes.

Contents #

Orientation of the conclusions (complementarity note) #

Pointwise 𝟙{ω ∈ Ev m} + 𝟙{ω ∈ (Ev m)ᶜ} = 1, so over the M+1 scales scaleProp Ev M ω + scaleProp (·ᶜ) M ω = 1. Hence the paper's good-proportion clause avsum 𝟙{𝒢} ≤ 1 − θ and the bad-proportion clause θ < avsum 𝟙{𝒢ᶜ} — the form concentration natively delivers — are complementary. Every conclusion below is phrased in the bad-proportion form. This is recorded as a note, not as a lemma.

Scope #

Provider material: carrier-neutral local helpers over an abstract probability space, with no ABK carrier and no model. They are conditional A: the concentration output and the deterministic reduction enter as hypotheses. No sorry, no custom axioms, no set_option maxHeartbeats.

The proportion of good / bad scales over a window {0,…,M} #

source
noncomputable def Algsuperdiff.Section4.Probability.IndicatorDensity.scaleProp {Ω : Type u_1} (Ev : ℤ → Set Ω) (M : ℕ) (ω : Ω) :
ℝ

The (Cesàro) proportion of scales m ∈ {0,…,M} at which Ev m holds, avsum_{m=0}^M 𝟙{ω ∈ Ev m}. With Ev the good event this is the paper's avsum 𝟙{𝒢(m;s,ε)}; with Ev = (𝒢ᵢ ·)ᶜ it is the density of bad scales.

Equations
Instances For

    The two-fold split: p.concentration.for.scales applied twice at ½θ #

    source
    theorem Algsuperdiff.Section4.Probability.IndicatorDensity.scaleProp_inter_le {Ω : Type u_1} (A B : ℤ → Set Ω) (M : ℕ) (ω : Ω) :
    scaleProp (fun (m : ℤ) => (A m ∩ B m)ᶜ) M ω ≤ scaleProp (fun (m : ℤ) => (A m)ᶜ) M ω + scaleProp (fun (m : ℤ) => (B m)ᶜ) M ω

    Two-fold subadditivity of the bad-scale density. Pointwise 𝟙{(A∩B)ᶜ} ≤ 𝟙{Aᶜ} + 𝟙{Bᶜ}; averaging over the window keeps it.

    source
    theorem Algsuperdiff.Section4.Probability.IndicatorDensity.setOf_scaleProp_inter_subset {Ω : Type u_1} (A B : ℤ → Set Ω) (M : ℕ) {θ θ₁ θ₂ : ℝ} (hθ : θ₁ + θ₂ ≤ θ) :
    {ω : Ω | θ < scaleProp (fun (m : ℤ) => (A m ∩ B m)ᶜ) M ω} ⊆ {ω : Ω | θ₁ < scaleProp (fun (m : ℤ) => (A m)ᶜ) M ω} ∪ {ω : Ω | θ₂ < scaleProp (fun (m : ℤ) => (B m)ᶜ) M ω}

    The ½θ split, as an inclusion of events. A θ-density of (A ∩ B)-bad scales forces a θ₁-density for A or a θ₂-density for B, whenever θ₁ + θ₂ ≤ θ.

    This is the Lean form of the paper's own bookkeeping in l.ratio.of.good.scales.for.k: are two separate applications of p.concentration.for.scales, each at level ½θ, combined at the end of Step

    The three-fold union bound #

    source
    theorem Algsuperdiff.Section4.Probability.IndicatorDensity.scaleProp_subadd {Ω : Type u_1} (A B Cev : ℤ → Set Ω) (M : ℕ) (ω : Ω) :
    scaleProp (fun (m : ℤ) => (A m ∩ B m ∩ Cev m)ᶜ) M ω ≤ scaleProp (fun (m : ℤ) => (A m)ᶜ) M ω + scaleProp (fun (m : ℤ) => (B m)ᶜ) M ω + scaleProp (fun (m : ℤ) => (Cev m)ᶜ) M ω

    Bad-scale density is subadditive under intersection. With 𝒢 = A ∩ B ∩ C, the density of scales at which 𝒢 fails is at most the sum of the densities at which each factor fails. Pointwise 𝟙{(A∩B∩C)ᶜ} ≤ 𝟙{Aᶜ} + 𝟙{Bᶜ} + 𝟙{Cᶜ}.

    source
    theorem Algsuperdiff.Section4.Probability.IndicatorDensity.measure_bad_density_union {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (A B Cev : ℤ → Set Ω) (M : ℕ) (θ e₀ e₁ e₂ : ℝ) (hA : P {ω : Ω | θ / 3 < scaleProp (fun (m : ℤ) => (A m)ᶜ) M ω} ≤ ENNReal.ofReal e₀) (hB : P {ω : Ω | θ / 3 < scaleProp (fun (m : ℤ) => (B m)ᶜ) M ω} ≤ ENNReal.ofReal e₁) (hC : P {ω : Ω | θ / 3 < scaleProp (fun (m : ℤ) => (Cev m)ᶜ) M ω} ≤ ENNReal.ofReal e₂) :
    P {ω : Ω | θ < scaleProp (fun (m : ℤ) => (A m ∩ B m ∩ Cev m)ᶜ) M ω} ≤ ENNReal.ofReal e₀ + ENNReal.ofReal e₁ + ENNReal.ofReal e₂

    The measure union bound over three bad-scale densities. Given the three ratio-lemma tails at level θ/3 and the subadditivity scaleProp_subadd, the density of scales at which A ∩ B ∩ C fails exceeds θ with probability at most e₀ + e₁ + e₂.