Chernoff

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

Concentration for scale arrays — Steps 4–5 (MGF assembly + Chernoff)

This module carries the universal constants C₅, C₆, Cstar, the independence hypothesis ColumnsIndep, the MGF integrand expZfun, the within-class independence factorization lintegral_prod_class, the fully-proved Step 4 residue-class MGF bound full_mgf_bound, and the Step 5 Chernoff bound count_chernoff_bound. Both steps are sorry-free; the generic Step-4 analytic and combinatorial helpers live in MgfProduct.lean.

Integrand expZfun

expZfun X p s lam r m ω = ⨆_N ∏_{j ∈ [-N,N]} e_r^{Z_j(ω)}, where e_r = ofReal(exp(a/r)) and a = ⅛(log 3) s p = mgfRate s p. This is the ℝ≥0∞ realization of exp((a/r) ∑_j Z_j) as a monotone limit of finite-window products — clean under Chernoff's Markov step and free of toReal pitfalls.

full_mgf_bound (Step 4, e.full.mgf.bound) —

∫⁻ expZfun ≤ ofReal(exp((m+1)/r · θ log 3 / 16)). The is the paper's exp(C₆ r⁻¹ (3/λ)^p (m+1)) after substituting λ = 3 Cstar^{1/p} θ^{-1/p}: with Cstar = 16 C₆/log 3 one has C₆ (3/λ)^p = θ log 3 / 16 (as (3/λ)^p = θ/Cstar). The proof: monotone convergence (lintegral_iSup) over the [−N,N] exhaustion; residue split + Hölder over the r classes (ENNReal.lintegral_prod_norm_pow_le); within-class independence factorization (lintegral_prod_class, from ColumnsIndep via iIndepFun.comp); insert the integer MGF Zj_mgf; ∏(1+c_j) ≤ exp(∑ c_j) and the two-sided geometric ℤ-sum (MgfProduct.lean).

Step 5 (proved here)

count_chernoff_bound derives the Chernoff bound from full_mgf_bound by Markov (mul_meas_ge_le_lintegral₀) with ε = ofReal(exp((a/r) θ (m+1))) and the set inclusion {ofReal(θ(m+1)) < ∑_j Z_j} ⊆ {ε ≤ expZfun}. The final rate uses (log 3)(2sp−1) ≥ sp (from sp ≥ 1, log 3 > 1) to reach exp(−spθ(m+1)/(16r)).

noncomputable def Algsuperdiff.Section4.Probability.ScalesConcentration.C₅ : ℝ

C₅: the universal bound for ∑_j 3^{-(sp/2) d_j} ≤ C₅ (m+1) (Step 4).

Equations

• Algsuperdiff.Section4.Probability.ScalesConcentration.C₅ = 3

noncomputable def Algsuperdiff.Section4.Probability.ScalesConcentration.C₆ : ℝ

C₆ = C₃ C₅ (Step 4).

Equations

• Algsuperdiff.Section4.Probability.ScalesConcentration.C₆ = Algsuperdiff.Section4.Probability.ScalesConcentration.C₃ * Algsuperdiff.Section4.Probability.ScalesConcentration.C₅

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.C₆_pos : 0 < C₆

noncomputable def Algsuperdiff.Section4.Probability.ScalesConcentration.Cstar : ℝ

The universal constant C = 16 C₆ / log 3.

Equations

• Algsuperdiff.Section4.Probability.ScalesConcentration.Cstar = 16 * Algsuperdiff.Section4.Probability.ScalesConcentration.C₆ / Real.log 3

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.Cstar_pos : 0 < Cstar

def Algsuperdiff.Section4.Probability.ScalesConcentration.ColumnsIndep {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (X : ℤ → ℤ → Ω → ℝ) (r : ℕ) : Prop

Within each residue class modulo r, the columns of X (as (ℤ→ℝ)-valued random variables) are mutually independent. Implied by e.independent.columns.twosided; see Defs.lean.

Equations

• Algsuperdiff.Section4.Probability.ScalesConcentration.ColumnsIndep P X r = ∀ (b : ℤ), ProbabilityTheory.iIndepFun (fun (j : ℤ) (ω : Ω) (k : ℤ) => X k (j * ↑r + b) ω) P

noncomputable def Algsuperdiff.Section4.Probability.ScalesConcentration.expZfun {Ω : Type u_1} (X : ℤ → ℤ → Ω → ℝ) (p s lam : ℝ) (r m : ℕ) (ω : Ω) : ENNReal

The MGF integrand ⨆_N ∏_{j∈[-N,N]} e_r^{Z_j}.

Equations

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

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.exists_icc_superset (t : Finset ℤ) : ∃ (N : ℕ), t ⊆ Finset.Icc (-↑N) ↑N

Any finite set of integers lies inside some symmetric window [-N, N].

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.measurable_Zcount {Ω : Type u_1} [MeasurableSpace Ω] {X : ℤ → ℤ → Ω → ℝ} {s : ℝ} (hXmeas : ∀ (k j : ℤ), Measurable (X k j)) (lam : ℝ) (m : ℕ) (j : ℤ) : Measurable fun (ω : Ω) => Zcount X s lam m j ω

Measurability of the column count Z_j.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.measurable_expZfun {Ω : Type u_1} [MeasurableSpace Ω] {X : ℤ → ℤ → Ω → ℝ} {p s : ℝ} {r : ℕ} (hXmeas : ∀ (k j : ℤ), Measurable (X k j)) (lam : ℝ) (m : ℕ) : Measurable fun (ω : Ω) => expZfun X p s lam r m ω

Measurability of the MGF integrand expZfun.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.lintegral_prod_class {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : ℤ → ℤ → Ω → ℝ} {s : ℝ} {r : ℕ} (hr : 1 ≤ r) (hindep : ColumnsIndep P X r) (hXmeas : ∀ (k j : ℤ), Measurable (X k j)) (a lam : ℝ) (m : ℕ) (b : ℤ) (fib : Finset ℤ) (hdvd : ∀ j ∈ fib, ↑r ∣ j - b) : ∫⁻ (ω : Ω), ∏ j ∈ fib, ENNReal.ofReal (Real.exp a) ^ Zcount X s lam m j ω ∂P = ∏ j ∈ fib, ∫⁻ (ω : Ω), ENNReal.ofReal (Real.exp a) ^ Zcount X s lam m j ω ∂P

Within-class independence factorization (Step 4, sub-part (c)). For a finite set fib of columns all congruent to b modulo r (so r ∣ j - b), the ℤ-reindexed family i ↦ B^{Z_{ir+b}} is mutually independent via ColumnsIndep, so the ∫⁻ of the product factors into the product of ∫⁻'s.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.full_mgf_bound {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : ℤ → ℤ → Ω → ℝ} {p s : ℝ} {r : ℕ} (hp : 1 ≤ p) (hs : 0 < s) (hs1 : s ≤ 1) (hsp : 1 ≤ s * p) (hr : 1 ≤ r) (hXmeas : ∀ (k j : ℤ), Measurable (X k j)) (hmomL : ∀ (k j : ℤ), ∫⁻ (ω : Ω), ENNReal.ofReal (X k j ω ^ p) ∂P ≤ 1) (hindep : ColumnsIndep P X r) (m : ℕ) (θ : ℝ) (hrm : ↑r ≤ ↑m) (hθ0 : 0 < θ) : ∫⁻ (ω : Ω), expZfun X p s (3 * Cstar ^ (1 / p) * θ ^ (-1 / p)) r m ω ∂P ≤ ENNReal.ofReal (Real.exp ((↑m + 1) / ↑r * (θ * Real.log 3 / 16)))

Step 4 (e.full.mgf.bound).

∫⁻ expZfun ≤ ofReal(exp((m+1)/r · θ log 3 / 16)). Assembled from monotone convergence, Hölder over the r residue classes, within-class independence (lintegral_prod_class), the integer MGF Zj_mgf, and the MgfProduct helpers.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.rate_key {p s : ℝ} (hsp : 1 ≤ s * p) : s * p ≤ Real.log 3 * (2 * (s * p) - 1)

The final rate inequality (log 3)(2sp − 1) ≥ sp, from sp ≥ 1, log 3 > 1.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.rate_arith {p s : ℝ} {r : ℕ} (hrpos : 0 < ↑r) (θ : ℝ) (hθ0 : 0 < θ) (m : ℕ) (hsp : 1 ≤ s * p) : (↑m + 1) / ↑r * (θ * Real.log 3 / 16) - 1 / 8 * Real.log 3 * s * p / ↑r * (θ * (↑m + 1)) ≤ -(s * p * θ) / (16 * ↑r) * (↑m + 1)

The Chernoff exponent comparison A − B ≤ D, where A = (m+1)/r·θlog3/16, B = mgfRate/r·θ(m+1), D = −spθ/(16r)·(m+1), using D − (A − B) = ((m+1)θ/16r)·(log3(2sp−1) − sp) ≥ 0.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.count_chernoff_bound {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : ℤ → ℤ → Ω → ℝ} {p s : ℝ} {r : ℕ} (hp : 1 ≤ p) (hs : 0 < s) (hs1 : s ≤ 1) (hsp : 1 ≤ s * p) (hr : 1 ≤ r) (hXmeas : ∀ (k j : ℤ), Measurable (X k j)) (hmomL : ∀ (k j : ℤ), ∫⁻ (ω : Ω), ENNReal.ofReal (X k j ω ^ p) ∂P ≤ 1) (hindep : ColumnsIndep P X r) (m : ℕ) (θ : ℝ) (hrm : ↑r ≤ ↑m) (hθ0 : 0 < θ) : P {ω : Ω | ENNReal.ofReal (θ * (↑m + 1)) < ∑' (j : ℤ), ↑(Zcount X s (3 * Cstar ^ (1 / p) * θ ^ (-1 / p)) m j ω)} ≤ ENNReal.ofReal (Real.exp (-(s * p * θ) / (16 * ↑r) * (↑m + 1)))

Step 5 (Chernoff). The Chernoff bound on the aggregated column count, obtained from full_mgf_bound by Markov's inequality.