WindowTails

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

Geometric tails for the random minimal scale

The random minimal scale of a bad-window family has an exponential tail once the individual bad-window probabilities do. This module keeps the prefactor form P[N ≤ Z] ≤ C exp (-c₀ N), which preserves the rate and makes the length-zero window free.

Contents

1. measureReal_le_tsum_of_subset — real countable subadditivity along an inclusion, with no measurability hypothesis on the sets.
2. minimalScale_tail_sum_le — the geometric summation over the windows of length ≥ M covered by minimalScaleEN_tail_eq.
3. minimalScaleEN_exp_tail_const — the packaged prefactor tail bound.
4. measureReal_le_card_mul_of_cover — the union bound over a finite family of centres covering a bad window.
5. count_exp_absorb_const — absorption of a centre count into the prefactor.
6. windowTailConst and windowScale_tail_const_of_center_tails — the assembled producer.

Everything is generic over the sample space Ω, the measure P, and the centre index type ι: no source-specific carrier appears. In particular the centre count and the covering property are inputs of the assembly lemmas here; a consumer with a concrete centre family discharges both as theorems.

theorem Algsuperdiff.Probability.ae_ne_top_of_enat_tail_tendsto_zero {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℕ∞} {b : ℕ → ENNReal} (hlim : Filter.Tendsto b Filter.atTop (nhds 0)) (htail : ∀ (N : ℕ), P {omega : Ω | ↑N ≤ X omega} ≤ b N) : ∀ᵐ (omega : Ω) ∂P, X omega ≠ ⊤

A vanishing upper bound on all natural-number tails excludes the infinite value. No measurability of the random scale is needed.

theorem Algsuperdiff.Probability.ae_ne_top_of_enat_exponential_tail {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℕ∞} (Cst : ℝ) {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (htail : ∀ (N : ℕ), P {omega : Ω | ↑N ≤ X omega} ≤ ENNReal.ofReal (Cst * Real.exp (-(a * (↑N - Cst)) / b))) : ∀ᵐ (omega : Ω) ∂P, X omega ≠ ⊤

A shifted exponential tail makes an extended-natural random scale finite almost surely.

theorem Algsuperdiff.Probability.measureReal_le_tsum_of_subset {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : Set Ω} {T : ℕ → Set Ω} (hsub : S ⊆ ⋃ (i : ℕ), T i) {b : ℕ → ℝ} (hb0 : ∀ (i : ℕ), 0 ≤ b i) (hb : ∀ (i : ℕ), P.real (T i) ≤ b i) (hsum : Summable b) : P.real S ≤ ∑' (i : ℕ), b i

Real countable subadditivity along an inclusion. If S ⊆ ⋃ i, T i and each P.real (T i) is dominated by a summable nonnegative b i, then P.real S ≤ ∑' i, b i. The route is measure_iUnion_le in ℝ≥0∞, which is valid for arbitrary — not necessarily measurable — sets, followed by a single toReal.

theorem Algsuperdiff.Probability.minimalScale_tail_sum_le {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (bad : ℕ → Ω → Prop) {B c₀ : ℝ} (hB : 0 ≤ B) (hc₀ : 0 < c₀) (hwin : ∀ (n : ℕ), P.real {ω : Ω | bad n ω} ≤ B * Real.exp (-c₀ * ↑n)) (M : ℕ) : P.real {ω : Ω | ↑(M + 1) ≤ minimalScaleEN bad ω} ≤ B * Real.exp (-c₀ * ↑M) / (1 - Real.exp (-c₀))

The core geometric summation. The tail at level M + 1 sums the per-window bounds over all windows of length ≥ M.

theorem Algsuperdiff.Probability.minimalScaleEN_exp_tail_const {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (bad : ℕ → Ω → Prop) {B c₀ : ℝ} (hB : 1 ≤ B) (hc₀ : 0 < c₀) (hwin : ∀ (n : ℕ), P.real {ω : Ω | bad n ω} ≤ B * Real.exp (-c₀ * ↑n)) (N : ℕ) : P.real {ω : Ω | ↑N ≤ minimalScaleEN bad ω} ≤ B * Real.exp c₀ / (1 - Real.exp (-c₀)) * Real.exp (-c₀ * ↑N)

The geometric tail of the minimal scale, prefactor form. From per-window tails P[bad n] ≤ B · exp (-c₀ n) with B ≥ 1, the minimal scale satisfies

P[N ≤ Z] ≤ (B · exp c₀ / (1 - exp (-c₀))) · exp (-c₀ N),

with the rate untouched and the geometric-summation constant explicit.

The union bound over a finite covering family

theorem Algsuperdiff.Probability.measureReal_le_card_mul_of_cover {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {ι : Type u_2} (Z : Finset ι) (p : ι → Ω → Prop) (q : Ω → Prop) {K : ℝ} (hcover : ∀ (ω : Ω), q ω → ∃ z ∈ Z, p z ω) (hz : ∀ z ∈ Z, P.real {ω : Ω | p z ω} ≤ K) : P.real {ω : Ω | q ω} ≤ ↑Z.card * K

Union bound along a finite covering family. If every sample in the event {q} is witnessed by some member z of the finite family Z, and each event {p z} has probability at most K, then P[q] ≤ |Z| · K. No measurability of any of the sets is required.

Absorbing a centre count into the rate

theorem Algsuperdiff.Probability.count_exp_absorb_const {D : ℕ} {c₁ c₀ : ℝ} (n : ℕ) (h : ↑D * Real.log 3 + c₀ ≤ c₁) : 3 ^ (D * (n + 1)) * Real.exp (-c₁ * ↑n) ≤ 3 ^ D * Real.exp (-c₀ * ↑n)

Centre-count absorption, prefactor form. 3^{D(n+1)} · exp (-c₁ n) ≤ 3^D · exp (-c₀ n) as soon as c₁ ≥ D · log 3 + c₀. Unlike count_exp_absorb this form keeps an n-proportional per-window rate; the price is the constant 3^D.

The prefactor constant

noncomputable def Algsuperdiff.Probability.windowTailConst (D : ℕ) (c₀ : ℝ) : ℝ

The prefactor of the minimal-scale tail in its rate-preserving form: a centre count 3^D times the geometric-summation constant exp c₀ / (1 - exp (-c₀)).

Equations

• Algsuperdiff.Probability.windowTailConst D c₀ = 3 ^ D * Real.exp c₀ / (1 - Real.exp (-c₀))

theorem Algsuperdiff.Probability.windowTailConst_eq (D : ℕ) (c₀ : ℝ) : windowTailConst D c₀ = 3 ^ D * Real.exp c₀ / (1 - Real.exp (-c₀))

theorem Algsuperdiff.Probability.rates_ge_of_large_power {C K gamma numerator : ℝ} (hC : 1 ≤ C) (hK : 0 < K) (hKC : K ≤ C) (hgamma : 0 < gamma) (hregime : C ^ 10 * gamma ≤ numerator) : C ≤ numerator / (K * gamma) ∧ 1 ≤ numerator / (C * gamma)

A large-power regime supplies the two rates used in window-tail absorption.

theorem Algsuperdiff.Probability.windowTailConst_mul_exp_le_shift (D : ℕ) {rate C : ℝ} (hrate : 1 ≤ rate) (hC : 2 * 3 ^ D ≤ C) (N : ℝ) : windowTailConst D rate * Real.exp (-rate * N) ≤ C * Real.exp (-rate * (N - 1))

A rate of at least one absorbs the geometric prefactor after shifting the tail by one.

theorem Algsuperdiff.Probability.measure_exponential_tail_weaken_rate {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (events : ℕ → Set Ω) {A C gamma numerator : ℝ} (hA : 1 ≤ A) (hAC : A ≤ C) (hgamma : 0 < gamma) (hnumerator : 0 ≤ numerator) (htail : ∀ (N : ℕ), 0 < N → P (events N) ≤ ENNReal.ofReal (A * Real.exp (-((↑N - 1) * numerator) / (A * gamma)))) (N : ℕ) : P (events N) ≤ ENNReal.ofReal (A * Real.exp (-((↑N - 1) * numerator) / (C * gamma)))

Weaken the rate of a probability tail, retaining its prefactor and handling length zero.

The assembled producers

theorem Algsuperdiff.Probability.windowScale_tail_const_of_center_tails {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {ι : Type u_2} {D : ℕ} (bad : ℕ → Ω → Prop) (centers : ℕ → Finset ι) (centerBad : ι → ℕ → Ω → Prop) {c₀ c₁ : ℝ} (hc₀ : 0 < c₀) (hcard : ∀ (n : ℕ), ↑(centers n).card ≤ 3 ^ (D * (n + 1))) (habsorb : ↑D * Real.log 3 + c₀ ≤ c₁) (hcover : ∀ (n : ℕ) (ω : Ω), bad n ω → ∃ z ∈ centers n, centerBad z n ω) (hcenter : ∀ (n : ℕ), 1 ≤ n → ∀ z ∈ centers n, P.real {ω : Ω | centerBad z n ω} ≤ Real.exp (-c₁ * ↑n)) (N : ℕ) : P.real {ω : Ω | ↑N ≤ minimalScaleEN bad ω} ≤ windowTailConst D c₀ * Real.exp (-c₀ * ↑N)

The minimal-scale tail from per-centre window tails, prefactor form.

Same architecture as windowScale_tail_of_center_tails, but with the per-witness tails at the n-proportional rate exp (-c₁ n) and required only for n ≥ 1: the length-0 window is absorbed by P ≤ 1 ≤ 3^D. The conclusion keeps the rate c₀ untouched and pays the prefactor windowTailConst D c₀.