Defs

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

Concentration for scale arrays — definitions and constants

This module formalizes the setup of Proposition p.concentration.for.scales (ABK26, Appendix D): a concentration inequality for exceedance counts in a triangular array {X_{k,j}} with geometric weights within rows and column-wise r-dependence.

We work over an abstract probability space (Ω, P) with a nonnegative array X : ℤ → ℤ → Ω → ℝ. This file collects:

• the geometric weights wt s k j = 3^{-s|k-j|} and the weighted row sums Yk (the paper's Y_k, e.Yk.def.twosided);
• the exceedance thresholds thr and the column exceedance counts Zcount (the paper's Z_j, e.Zj.def.twosided);
• the universal constants C₂, C₃, and the exponential-moment rate mgfRate (a = ⅛ (log 3) s p);
• the positivity facts one_sub_rpow_pos, C₂_pos, C₃_pos and mgfRate_pos those constants need. The geometric row-sum bound that Step 1 uses is Reduction.sum_wt_half_le, one module on.

Design of the independence hypothesis

The paper assumes r-dependence across columns (e.independent.columns.twosided): for I, J ⊆ ℤ with dist(I,J) ≥ r, the families {X_{·,j} : j ∈ I} and {X_{·,j} : j ∈ J} are independent. What the proof actually uses (Step 4) is the mutual independence, within each residue class b modulo r, of the columns {X_{·, jr+b} : j ∈ ℤ} — these columns are pairwise at distance ≥ r, and {i} is at distance ≥ r from {i', i'', …} for any earlier members, so the paper's two-set hypothesis yields mutual independence by induction. We therefore take as the hypothesis the mutual independence of each residue class, phrased with mathlib's iIndepFun over the whole columns viewed as (ℤ → ℝ)-valued random variables: ∀ b : ℤ, iIndepFun (fun j : ℤ => fun ω k => X k (j * r + b) ω) P.

This is the weakest faithful hypothesis mathlib's independence A supports cleanly; it is implied by e.independent.columns.twosided. Since Zcount j is a measurable function of column j alone, iIndepFun.comp transports this to independence of the Z's within each residue class.

noncomputable def Algsuperdiff.Section4.Probability.ScalesConcentration.idist (k j : ℤ) : ℝ

Real distance between integer indices, |k - j|.

Equations

• Algsuperdiff.Section4.Probability.ScalesConcentration.idist k j = |↑k - ↑j|

noncomputable def Algsuperdiff.Section4.Probability.ScalesConcentration.wt (s : ℝ) (k j : ℤ) : ℝ

Geometric row weight 3^{-s|k-j|} (e.Yk.def.twosided).

Equations

• Algsuperdiff.Section4.Probability.ScalesConcentration.wt s k j = 3 ^ (-(s * Algsuperdiff.Section4.Probability.ScalesConcentration.idist k j))

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.wt_pos (s : ℝ) (k j : ℤ) : 0 < wt s k j

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.wt_nonneg (s : ℝ) (k j : ℤ) : 0 ≤ wt s k j

noncomputable def Algsuperdiff.Section4.Probability.ScalesConcentration.Yk {Ω : Type u_1} (X : ℤ → ℤ → Ω → ℝ) (s : ℝ) (k : ℤ) (ω : Ω) : ℝ

The weighted row sum Y_k = ∑_j 3^{-s|k-j|} X_{k,j} (e.Yk.def.twosided).

Equations

• Algsuperdiff.Section4.Probability.ScalesConcentration.Yk X s k ω = ∑' (j : ℤ), Algsuperdiff.Section4.Probability.ScalesConcentration.wt s k j * X k j ω

noncomputable def Algsuperdiff.Section4.Probability.ScalesConcentration.thr (s lam : ℝ) (k j : ℤ) : ℝ

The Step-1/Step-2 exceedance threshold ½ λ 3^{(s/2)|k-j|}.

Equations

• Algsuperdiff.Section4.Probability.ScalesConcentration.thr s lam k j = lam / 2 * 3 ^ (s / 2 * Algsuperdiff.Section4.Probability.ScalesConcentration.idist k j)

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

The column exceedance count Z_j = ∑_{k=0}^{m} 𝟙{X_{k,j} > ½ λ 3^{(s/2)|k-j|}} (e.Zj.def.twosided), as a natural number.

Equations

• Algsuperdiff.Section4.Probability.ScalesConcentration.Zcount X s lam m j ω = ∑ k ∈ Finset.Icc 0 ↑m, if Algsuperdiff.Section4.Probability.ScalesConcentration.thr s lam k j < X k j ω then 1 else 0

Universal constants

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

C₂ = 4 / (1 - 3^{-1/2}) from Step 2 (e.Zj.tail.twosided).

Equations

• Algsuperdiff.Section4.Probability.ScalesConcentration.C₂ = 4 / (1 - 3 ^ (-(1 / 2)))

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

C₃ = 2 (1 - 3^{-1/8})⁻¹ C₂ from Step 3 (e.Zj.mgf.twosided).

Equations

• Algsuperdiff.Section4.Probability.ScalesConcentration.C₃ = 2 * (1 - 3 ^ (-(1 / 8)))⁻¹ * Algsuperdiff.Section4.Probability.ScalesConcentration.C₂

noncomputable def Algsuperdiff.Section4.Probability.ScalesConcentration.mgfRate (s p : ℝ) : ℝ

The exponential-moment rate a = ⅛ (log 3) s p from Step 3.

Equations

• Algsuperdiff.Section4.Probability.ScalesConcentration.mgfRate s p = 1 / 8 * Real.log 3 * s * p

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.one_sub_rpow_pos {c : ℝ} (hc : 0 < c) : 0 < 1 - 3 ^ (-c)

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

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

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.mgfRate_pos {s p : ℝ} (hs : 0 < s) (hp : 0 < p) : 0 < mgfRate s p