Hoeffding's lemma and Ville's maximal inequality along uniform rounds (CRN-2, helpers)

Ingredients of the maximal Azuma–Hoeffding inequality Epidemics.Kurtz.expList_azuma:

• avg_exp_mul_le: Hoeffding's lemma for a centred variable bounded by c under a uniform draw, avg (exp (θ f)) ≤ exp (θ² c² / 2) (convexity of exp, then Real.cosh_le_exp_half_sq);
• expList_ville: Ville's maximal inequality for a multiplicative process exp (M x l) with M x (a :: l) = E x a + M (step x a) l and avg (exp (E y ·)) ≤ 1 (a nonnegative supermartingale started at 1): it reaches μ > 0 within n rounds with probability at most 1 / μ. Proved by induction on n, peeling off the first round.

theorem Epidemics.Kurtz.ite_one_zero_le_of_imp {P Q : Prop} [Decidable P] [Decidable Q] (h : P → Q) : (if P then 1 else 0) ≤ if Q then 1 else 0

An indicator is monotone in its event.

theorem Epidemics.Kurtz.avg_le_one {R : Type u_2} [Fintype R] {f : R → ℝ} (h : ∀ (a : R), f a ≤ 1) : Dynamics.avg f ≤ 1

A uniform average of values at most one is at most one (also on an empty type).

theorem Epidemics.Kurtz.expList_le_one {R : Type u_2} [Fintype R] {T : ℕ} {F : List R → ℝ} (h : ∀ (l : List R), F l ≤ 1) : Dynamics.expList R T F ≤ 1

An expList average of values at most one is at most one.

theorem Epidemics.Kurtz.expList_le_expList_of_length {R : Type u_2} [Fintype R] {T : ℕ} {F G : List R → ℝ} (h : ∀ (l : List R), l.length = T → F l ≤ G l) : Dynamics.expList R T F ≤ Dynamics.expList R T G

expList is monotone as soon as the comparison holds on lists of the right length.

theorem Epidemics.Kurtz.avg_exp_mul_le {R : Type u_2} [Fintype R] {f : R → ℝ} {c : ℝ} (hmean : Dynamics.avg f = 0) (hb : ∀ (a : R), |f a| ≤ c) (θ : ℝ) : (Dynamics.avg fun (a : R) => Real.exp (θ * f a)) ≤ Real.exp (θ ^ 2 * c ^ 2 / 2)

Hoeffding's lemma (Hoeffding 1963, (4.16)) for a uniform draw: if f has mean zero and |f| ≤ c, then avg (exp (θ f)) ≤ exp (θ² c² / 2).

theorem Epidemics.Kurtz.expList_ville {σ : Type u_1} {R : Type u_2} [Fintype R] (step : σ → R → σ) (E : σ → R → ℝ) (M : σ → List R → ℝ) (hM0 : ∀ (x : σ), M x [] = 0) (hM : ∀ (x : σ) (a : R) (l : List R), M x (a :: l) = E x a + M (step x a) l) (hE : ∀ (y : σ), (Dynamics.avg fun (a : R) => Real.exp (E y a)) ≤ 1) (n : ℕ) (x : σ) {μ : ℝ} : 0 < μ → (Dynamics.expList R n fun (l : List R) => if ∃ k ≤ n, μ ≤ Real.exp (M x (List.take k l)) then 1 else 0) ≤ 1 / μ

Ville's maximal inequality along i.i.d. uniform rounds (finite horizon). Let M x (a :: l) = E x a + M (step x a) l, M x [] = 0, with avg (exp (E y ·)) ≤ 1 for every y, so that k ↦ exp (M x (l.take k)) is a nonnegative supermartingale started at 1. Then it reaches μ > 0 at some step k ≤ n with probability at most 1 / μ.