Documentation

Epidemics.KurtzAzuma

A maximal Azuma–Hoeffding inequality along i.i.d. uniform rounds (CRN-2) #

The martingale concentration behind Kurtz's law of large numbers (Epidemics.Kurtz), in the finite-probability layer of Dynamics: a process X_{j+1} = step X_j ρ_j driven by i.i.d. uniform rounds ρ_j : R (expectations by Dynamics.expList), and increments D (X_j) ρ_j with zero conditional mean, avg (D y) = 0 for every state y, and bounded by c. Their partial sums M_k = incrementSum step D x (l.take k) form a martingale, and

P(∃ k ≤ n, M_k ≥ λ) ≤ exp(-λ² / (2 n c²))

(K. Azuma, Weighted sums of certain dependent random variables, Tôhoku Math. J. 19, 1967; W. Hoeffding, J. Amer. Statist. Assoc. 58, 1963, Theorem 2 for the independent case), in the maximal form obtained from Ville's (Doob's) maximal inequality for the exponential supermartingale exp(θ M_k - k θ² c² / 2).

The state type σ is arbitrary (not necessarily finite), so this covers every martingale with respect to the rounds: take for σ the histories List R. Mathlib's Azuma–Hoeffding inequality (ProbabilityTheory.measure_sum_ge_le_of_hasCondSubgaussianMGF) is measure-theoretic and not maximal, and Dynamics.Concentration only treats sums of independent coordinates, hence this statement.

source
noncomputable def Epidemics.Kurtz.incrementSum {σ : Type u_1} {R : Type u_2} (step : σ → R → σ) (D : σ → R → ℝ) (x : σ) (l : List R) :
ℝ

The sum ∑_{j < |l|} D (X_j) (l_j) of the increments D along the rounds l, for the process X_0 = x, X_{j+1} = step X_j l_j. When every avg (D y) vanishes, k ↦ incrementSum step D x (l.take k) is a martingale along i.i.d. uniform rounds l.

Equations
Instances For
    source
    theorem Epidemics.Kurtz.incrementSum_mul_sub {σ : Type u_1} {R : Type u_2} (step : σ → R → σ) (D : σ → R → ℝ) (θ b : ℝ) (x : σ) (l : List R) :
    incrementSum step (fun (y : σ) (a : R) => θ * D y a - b) x l = θ * incrementSum step D x l - ↑l.length * b

    incrementSum of the affine increments θ D - b (the exponent of the exponential supermartingale).

    source
    theorem Epidemics.Kurtz.expList_azuma {σ : Type u_1} {R : Type u_2} [Fintype R] (step : σ → R → σ) (D : σ → R → ℝ) {c : ℝ} (hmean : ∀ (y : σ), Dynamics.avg (D y) = 0) (hbound : ∀ (y : σ) (a : R), |D y a| ≤ c) (x : σ) (n : ℕ) {lam : ℝ} (hlam : 0 ≤ lam) :
    (Dynamics.expList R n fun (l : List R) => if ∃ k ≤ n, lam ≤ incrementSum step D x (List.take k l) then 1 else 0) ≤ Real.exp (-(lam ^ 2 / (2 * ↑n * c ^ 2)))

    Maximal Azuma–Hoeffding inequality (Azuma 1967; Hoeffding 1963, Theorem 2, for independent summands). If the increments have zero mean over a uniform round, avg (D y) = 0, and are bounded, |D y a| ≤ c, then over n i.i.d. uniform rounds the martingale M_k = incrementSum step D x (l.take k) reaches λ ≥ 0 at some step k ≤ n with probability at most exp(-λ² / (2 n c²)).