McDiarmid's bounded-differences inequality at MGF level (issue #72, item 1, commit 1) #

Mathlib has Hoeffding's LEMMA (ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc) but no McDiarmid/Azuma inequality. This module proves the specialized MGF form needed for sampling concentration: a function f of n i.i.d. coordinates with uniform two-point bounded differences ≤ c in each coordinate has, after centering, a sub-Gaussian moment-generating function with variance proxy n * (c / 2) ^ 2. Coordinate-peeling induction over Measure.pi (fun _ : Fin n ↦ ν), each peeled coordinate handled by Hoeffding's lemma.

ProbabilityTheory.hasSubgaussianMGF_of_bounded_differences' — the primary public result, over an arbitrary Fintype index, packaged as Mathlib's ProbabilityTheory.HasSubgaussianMGF, so that the one-sided Chernoff bound HasSubgaussianMGF.measure_ge_le and the reflected tail via HasSubgaussianMGF.neg are immediately available.
ProbabilityTheory.hasSubgaussianMGF_of_bounded_differences — the Fin n special case.

The intermediate lemmas (Graphon.McDiarmid.abs_sub_le_of_boundedDiff, the Fin n induction Graphon.McDiarmid.integral_exp_mul_centered_le_pi_fin, and its Fintype.equivFin/measurePreserving_piCongrLeft transport Graphon.McDiarmid.integral_exp_mul_centered_le_pi) are private. This module owns the single project implementation of the peeling induction: Graphon/SamplingPointwise.lean §(II) consumes the public theorems. This module deliberately imports Mathlib only.

source

theorem ProbabilityTheory.hasSubgaussianMGF_of_bounded_differences' {ι : Type u_1} [Fintype ι] [DecidableEq ι] {β : Type u_2} [MeasurableSpace β] (ν : MeasureTheory.Measure β) [MeasureTheory.IsProbabilityMeasure ν] (f : (ι → β) → ℝ) (hf : Measurable f) (c : ℝ) (hc : 0 ≤ c) (hosc : ∀ (x : ι → β) (i : ι) (b : β), |f (Function.update x i b) - f x| ≤ c) :

HasSubgaussianMGF (fun (x : ι → β) => f x - ∫ (y : ι → β), f y ∂MeasureTheory.Measure.pi fun (x : ι) => ν) (↑(Fintype.card ι) * (c.toNNReal / 2) ^ 2) (MeasureTheory.Measure.pi fun (x : ι) => ν)

McDiarmid's bounded-differences inequality at MGF level on a finite i.i.d. product over an arbitrary finite index type: if the measurable f changes by at most c under any single-coordinate update, then the centered f has a sub-Gaussian moment-generating function with variance proxy card ι * (c / 2) ^ 2 under Measure.pi (fun _ : ι ↦ ν). The one-sided Chernoff tail is then ProbabilityTheory.HasSubgaussianMGF.measure_ge_le; the reflected tail follows via ProbabilityTheory.HasSubgaussianMGF.neg.

source

theorem ProbabilityTheory.hasSubgaussianMGF_of_bounded_differences {n : ℕ} {β : Type u_1} [MeasurableSpace β] (ν : MeasureTheory.Measure β) [MeasureTheory.IsProbabilityMeasure ν] (f : (Fin n → β) → ℝ) (hf : Measurable f) (c : ℝ) (hc : 0 ≤ c) (hosc : ∀ (x : Fin n → β) (i : Fin n) (b : β), |f (Function.update x i b) - f x| ≤ c) :

HasSubgaussianMGF (fun (x : Fin n → β) => f x - ∫ (y : Fin n → β), f y ∂MeasureTheory.Measure.pi fun (x : Fin n) => ν) (↑n * (c.toNNReal / 2) ^ 2) (MeasureTheory.Measure.pi fun (x : Fin n) => ν)

McDiarmid's bounded-differences inequality at MGF level on a finite i.i.d. product over Fin n: the special case ι := Fin n of ProbabilityTheory.hasSubgaussianMGF_of_bounded_differences'. The one-sided Chernoff tail is then ProbabilityTheory.HasSubgaussianMGF.measure_ge_le; the reflected tail follows via ProbabilityTheory.HasSubgaussianMGF.neg.