IndicatorDensityTails

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

Rate shaping for the indicator-density tails

ABK26, §4.1. IndicatorDensity.lean delivers the Appendix-D output at concentration's native rate exp(-(s p θ)/(16 r)·(M+1)) and only for windows of length M ≥ r. Two genuine steps separate that from the shape the downstream minimal-scale layer consumes, namely

∀ n : ℕ, P [ θ < density of bad scales of `Ev` over the window {0,…,n} ]
           ≤ exp(-c₁ n) / Q ,

and both are proved here over an abstract probability space.

1. The rate conversion. exp(-a(n+1)) ≤ exp(-c₁ n)/Q whenever a ≥ c₁ and a ≥ log Q, where a = s p θ/(16 r) — the paper's "by taking K(d) larger, if necessary" at the end of each ratio-lemma proof. The prefactor Q ≥ 1 is a parameter: Q = 3 for a lane run once (𝒢₀, 𝒢₂), Q = 6 for one half of the 𝒢₁ = 𝒢₁a ∩ 𝒢₁b split, whose two halves the paper itself treats as two separate applications of p.concentration.for.scales.

2. The short windows n < r. The paper states each ratio lemma for every M ∈ ℕ₀, but its only tool, Proposition p.concentration.for.scales, requires M ≥ r ("m ∈ ℕ with m ≥ r"). The gap is closed here without any new hypothesis, from the concentration output itself:

   • for a single scale k ∈ {0,…,r}, the bad event (Ev k)ᶜ already forces the bad-scale density over the longer window {0,…,r} to be ≥ 1/(r+1), hence > θ as soon as θ(r+1) < 1, so P[(Ev k)ᶜ] ≤ exp(-a(r+1)) (measure_compl_le_of_concEvent);
   • a union bound over the n+1 ≤ r scales of the short window then gives P[θ < density over {0,…,n}] ≤ (n+1)·exp(-a(r+1)), and the single rate hypothesis log(Qr) + c₁ r ≤ a dominates both regimes.

Scope

Provider material: carrier-neutral local helpers over an abstract probability space. The concentration output (hconc) and the deterministic scale-locality reduction (hreduce) enter as conditional A hypotheses; nothing new is assumed. No sorry, no custom axioms, no set_option maxHeartbeats.

The threshold event of Appendix D, at a fixed level θ

def Algsuperdiff.Section4.Probability.IndicatorDensity.concEvent {Ω : Type u_1} (X : ℤ → ℤ → Ω → ℝ) (p s' θ C : ℝ) (M : ℕ) : Set Ω

The Appendix-D count event at window {0,…,M} and level θ: the proportion of rows k ≤ M whose weighted row sum Y_k exceeds the threshold 9 s⁻¹ C^{1/p} θ^{-1/p} is more than θ. This is the left-hand side of the Appendix-D concentration bound.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Probability.IndicatorDensity.measure_badProp_le_of_concEvent {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (X : ℤ → ℤ → Ω → ℝ) {p s' θ C : ℝ} (Ev : ℤ → Set Ω) (M : ℕ) (hreduce : ∀ (m : ℤ), 0 ≤ m → m ≤ ↑M → ∀ ω ∈ (Ev m)ᶜ, 9 * s'⁻¹ * C ^ (1 / p) * θ ^ (-1 / p) < ScalesConcentration.Yk X s' m ω) : P {ω : Ω | θ < scaleProp (fun (m : ℤ) => (Ev m)ᶜ) M ω} ≤ P (concEvent X p s' θ C M)

Fixed-level form of the bad-scale density bound. The density of bad scales over the window {0,…,M} is dominated by the Appendix-D count event, at the one level θ — the form needed when θ is pinned by the consumer.

theorem Algsuperdiff.Section4.Probability.IndicatorDensity.measure_compl_le_of_concEvent {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (X : ℤ → ℤ → Ω → ℝ) {p s' θ C : ℝ} {r : ℕ} (Ev : ℤ → Set Ω) (k : ℤ) (hk0 : 0 ≤ k) (hkr : k ≤ ↑r) (_hθ0 : 0 < θ) (hθr : θ * (↑r + 1) < 1) (hreduce : ∀ (m : ℤ), 0 ≤ m → m ≤ ↑r → ∀ ω ∈ (Ev m)ᶜ, 9 * s'⁻¹ * C ^ (1 / p) * θ ^ (-1 / p) < ScalesConcentration.Yk X s' m ω) : P (Ev k)ᶜ ≤ P (concEvent X p s' θ C r)

A single bad scale inside a length-r window is already a θ-density event. If the level satisfies θ(r+1) < 1 then, for any scale k ∈ {0,…,r}, the bad event (Ev k)ᶜ is contained in the Appendix-D count event over the window {0,…,r}: a single exceeding row contributes 1/(r+1) > θ to the density.

This is the device that closes the paper's short-window gap: it converts the concentration bound at the shortest admissible window M = r into a bound on the probability of a single bad scale, with no extra hypothesis.

The rate arithmetic

theorem Algsuperdiff.Section4.Probability.IndicatorDensity.exp_rate_long {a c₁ Q : ℝ} (n : ℕ) (hQ : 0 < Q) (hc₁ : c₁ ≤ a) (hlog : Real.log Q ≤ a) : Real.exp (-a * (↑n + 1)) ≤ Real.exp (-c₁ * ↑n) / Q

Long windows. exp(-a(n+1)) ≤ exp(-c₁ n)/Q when c₁ ≤ a and log Q ≤ a.

The prefactor Q is 3 for a lane that is run once (𝒢₀, 𝒢₂) and 6 for a lane that is split into two halves at level θ/2 and recombined by a union bound (𝒢₁ = 𝒢₁a ∩ 𝒢₁b, — two separate applications of p.concentration.for.scales).

theorem Algsuperdiff.Section4.Probability.IndicatorDensity.exp_rate_short {a c₁ Q : ℝ} {n r : ℕ} (hnr : n + 1 ≤ r) (hc₁ : 0 ≤ c₁) (hQ : 0 < Q) (ha0 : 0 ≤ a) (hrate : Real.log (Q * ↑r) + c₁ * ↑r ≤ a) : (↑n + 1) * Real.exp (-a * (↑r + 1)) ≤ Real.exp (-c₁ * ↑n) / Q

Short windows. (n+1)·exp(-a(r+1)) ≤ exp(-c₁ n)/Q when n + 1 ≤ r, 0 ≤ c₁, and the single rate condition log(Q r) + c₁ r ≤ a holds.

The produced tail — generic in the event family

theorem Algsuperdiff.Section4.Probability.IndicatorDensity.ratioTail_of_concentration {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (X : ℤ → ℤ → Ω → ℝ) {p s' θ c₁ C Q : ℝ} {r : ℕ} (Ev : ℤ → Set Ω) (hr : 1 ≤ r) (hQ : 1 ≤ Q) (hθ0 : 0 < θ) (hθr : θ * (↑r + 1) < 1) (hc₁ : 0 ≤ c₁) (hrate : Real.log (Q * ↑r) + c₁ * ↑r ≤ s' * p * θ / (16 * ↑r)) (hconc : ∀ (M : ℕ), ↑r ≤ ↑M → P (concEvent X p s' θ C M) ≤ ENNReal.ofReal (Real.exp (-(s' * p * θ) / (16 * ↑r) * (↑M + 1)))) (hreduce : ∀ (m : ℤ), 0 ≤ m → ∀ ω ∈ (Ev m)ᶜ, 9 * s'⁻¹ * C ^ (1 / p) * θ ^ (-1 / p) < ScalesConcentration.Yk X s' m ω) (n : ℕ) : P {ω : Ω | θ < scaleProp (fun (k : ℤ) => (Ev k)ᶜ) n ω} ≤ ENNReal.ofReal (Real.exp (-c₁ * ↑n) / Q)

The ratio-lemma tail, in the consumer's shape.

Given, for one event family Ev:

• hconc — the Appendix-D concentration output at level θ for the family's array X and threshold constant C;
• hreduce — the deterministic scale-locality reduction (Ev m)ᶜ ⊆ {9 s⁻¹C^{1/p}θ^{-1/p} < Y_m} for m ≥ 0;

together with the level conditions 0 < θ, θ(r+1) < 1 and the single rate condition log(Qr) + c₁ r ≤ s p θ/(16 r), the bad-scale density over every window {0,…,n}, n : ℕ — including the short windows n < r that p.concentration.for.scales does not reach — obeys P[θ < density of bad scales over {0,…,n}] ≤ exp(-c₁ n)/Q.

The prefactor Q ≥ 1 is free: Q = 3 for a lane that is run once, Q = 6 for one half of a lane that is split at level θ/2 and recombined by a union bound (the 𝒢₁ = 𝒢₁a ∩ 𝒢₁b treatment/10598).