McDiarmid's bounded-differences inequality

This file proves the moment-generating-function form of McDiarmid's inequality for a measurable real-valued function on a finite product of identical probability spaces. If changing coordinate i changes the function by at most c i, then the centered function is sub-Gaussian with variance proxy ∑ i, (c i / 2) ^ 2.

The proof peels off one coordinate at a time. Hoeffding's lemma controls the peeled coordinate, and the induction hypothesis controls the function obtained by averaging over it.

Main results

• TauCeti.Probability.hasSubgaussianMGF_of_bounded_differences gives the result for an arbitrary finite index type;
• TauCeti.Probability.hasSubgaussianMGF_of_bounded_differences_fin specializes it to Fin n.

References

• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics 141 (1989), 148–188.
• C. Freer, cameronfreer/graphon at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699, Apache-2.0, Graphon/McDiarmid.lean. The coordinate-peeling proof and constants are adapted from that file.

theorem TauCeti.Probability.hasSubgaussianMGF_of_bounded_differences {ι : Type u_1} [Fintype ι] {β : Type u_2} [MeasurableSpace β] (ν : MeasureTheory.Measure β) [MeasureTheory.IsProbabilityMeasure ν] (f : (ι → β) → ℝ) (hf : Measurable f) (c : ι → ℝ) (hbd : ∀ (i : ι) (x x' : ι → β), (∀ (l : ι), l ≠ i → x l = x' l) → |f x - f x'| ≤ c i) : ProbabilityTheory.HasSubgaussianMGF (fun (x : ι → β) => f x - ∫ (y : ι → β), f y ∂MeasureTheory.Measure.pi fun (x : ι) => ν) (∑ i : ι, (c i).toNNReal ^ 2 / 4) (MeasureTheory.Measure.pi fun (x : ι) => ν)

McDiarmid's bounded-differences inequality at MGF level. Let f be a measurable real-valued function on a finite i.i.d. product. If two inputs that differ only at coordinate i have outputs differing by at most c i, then the centered f is sub-Gaussian with variance proxy ∑ i, (c i)² / 4.

The result is stated using Mathlib's ProbabilityTheory.HasSubgaussianMGF; its measure_ge_le theorem gives the one-sided Chernoff tail, and applying neg gives the other side.

theorem TauCeti.Probability.hasSubgaussianMGF_of_bounded_differences_fin {n : ℕ} {β : Type u_1} [MeasurableSpace β] (ν : MeasureTheory.Measure β) [MeasureTheory.IsProbabilityMeasure ν] (f : (Fin n → β) → ℝ) (hf : Measurable f) (c : ℝ) (hosc : ∀ (x : Fin n → β) (i : Fin n) (b : β), |f (Function.update x i b) - f x| ≤ c) : ProbabilityTheory.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 for a product indexed by Fin n, stated in the convenient form where one coordinate is updated explicitly.