Sharp bounded-differences (McDiarmid) inequality

The sharp McDiarmid bound carries the constant 2 in the exponent, exp (-2 t^2 / ∑ c_i^2), four times tighter than the Azuma constant exp (-t^2 / (2 ∑ c_i^2)). The factor of 4 comes from the per-increment sub-Gaussian variance proxy: the sharp proxy is (c_i / 2)^2 (range c_i), whereas the Azuma proxy is c_i^2 (a symmetric bound |Δ_i| ≤ c_i, range 2 c_i).

Relationship to the existing development. FormalSLT/Azuma/ proves both the Azuma-constant bounded-differences inequality (FormalSLT.Azuma.ExposureMartingale.hasBoundedDifferences_tail_azuma) and the sharp McDiarmid-constant version (FormalSLT.Azuma.ExposureMartingale.hasBoundedDifferences_tail_sharp). The sharp route feeds the exposure-martingale increments into mathlib's conditional Azuma-Hoeffding engine ProbabilityTheory.measure_sum_ge_le_of_hasCondSubgaussianMGF with the per-increment proxy (‖c_k‖₊ / 2)^2, obtained from the conditional range-width kernel theorem in FormalSLT.Azuma.ExposureMartingale.

What this file adds:

• mcdiarmid_additive_independent - the sharp constant 2 for the additive, independent case. For a sum of independent variables each supported in [a_i, b_i], the per-coordinate range is directly b_i - a_i (no conditioning is needed), so the sharp proxy ((b_i - a_i)/2)^2 is available from mathlib's hasSubgaussianMGF_of_mem_Icc, and the bound is sharp. The general exposure-martingale theorem above does not give this constant.
• mcdiarmid_of_hasBoundedDifferences_sharp - the general product-measure bounded-differences theorem with the sharp McDiarmid constant.
• mcdiarmid_of_hasBoundedDifferences_sharp_lower - the matching lower-tail theorem, obtained by applying the upper-tail theorem to -f.
• mcdiarmid_twoSided_of_hasBoundedDifferences_sharp - the two-sided textbook bounded-differences theorem for |f - E[f]| over a homogeneous product measure.
• sharp_mcdiarmid_of_doob_increments - an abstract reduction recording that given Doob increments that are conditionally sub-Gaussian with the sharp proxy (c_i / 2)^2, the sharp tail bound follows from the same engine. It pinpoints the exact hypothesis a sharpened general theorem must supply.

theorem FormalSLT.Concentration.sharp_mcdiarmid_of_doob_increments {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [StandardBorelSpace Ω] [MeasureTheory.IsZeroOrProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ mΩ} {Y : ℕ → Ω → ℝ} {c : ℕ → NNReal} (n : ℕ) (h_adapted : MeasureTheory.StronglyAdapted ℱ Y) (h0 : ProbabilityTheory.HasSubgaussianMGF (Y 0) ((c 0 / 2) ^ 2) μ) (h_subG : ∀ i < n - 1, ProbabilityTheory.HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) ((c (i + 1) / 2) ^ 2) μ) {g : Ω → ℝ} (hg : ∀ (ω : Ω), g ω = ∑ i ∈ Finset.range n, Y i ω) {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | t ≤ g ω} ≤ Real.exp (-2 * t ^ 2 / ∑ i ∈ Finset.range n, ↑(c i) ^ 2)

Sharp McDiarmid, abstract reduction form.

Let g be a centered statistic that decomposes as the sum of a Doob martingale difference sequence Y adapted to a filtration ℱ, where each increment is conditionally sub-Gaussian with the sharp variance proxy (c i / 2) ^ 2 (the proxy of an increment of conditional range c i). Then g satisfies the sharp upper-tail bound

μ {ω | t ≤ g ω} ≤ exp (-2 t^2 / ∑ c_i^2).

The sharp constant 2 is produced by mathlib's conditional Azuma-Hoeffding engine when fed the proxies (c_i / 2) ^ 2; this lemma performs that reduction and the exponent bookkeeping. It records exactly the hypothesis a sharpened general theorem must establish: the existing FormalSLT.Azuma.ExposureMartingale.exposureIncrement_hasCondSubgaussianMGF supplies its increments with the Azuma proxy ‖c_k‖₊^2, not (c_k / 2)^2, which is why the assembled hasBoundedDifferences_tail_azuma lands at the Azuma constant. See docs/SharpMcDiarmid.md.

theorem FormalSLT.Concentration.mcdiarmid_of_hasBoundedDifferences_sharp {n : ℕ} {Z : Type u_2} [Nonempty Z] [MeasurableSpace Z] [StandardBorelSpace Z] {μ : MeasureTheory.Measure Z} [MeasureTheory.IsProbabilityMeasure μ] {f : (Fin n → Z) → ℝ} {c : Fin n → ℝ} (hbdd : Azuma.BoundedDifferences.HasBoundedDifferences f c) (hf : MeasureTheory.StronglyMeasurable f) (hfi : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin n) => μ)) (hc : ∀ (k : Fin n), 0 ≤ c k) {ε : ℝ} (hε : 0 ≤ ε) : (MeasureTheory.Measure.pi fun (x : Fin n) => μ).real {S : Fin n → Z | (∫ (s : Fin n → Z), f s ∂MeasureTheory.Measure.pi fun (x : Fin n) => μ) + ε ≤ f S} ≤ Real.exp (-2 * ε ^ 2 / ∑ k : Fin n, c k ^ 2)

Sharp McDiarmid bounded-differences inequality over a product measure.

If f : (Fin n → Z) → ℝ changes by at most c k when coordinate k is altered, with nonnegative widths c k, then its upper tail under the homogeneous product measure satisfies the sharp McDiarmid bound

μⁿ {S | E[f] + ε ≤ f S} ≤ exp (-2 * ε^2 / ∑ k, c k ^ 2).

The proof is routed through the exposure martingale and the checked conditional range-width theorem for its increments.

theorem FormalSLT.Concentration.mcdiarmid_of_hasBoundedDifferences_sharp_lower {n : ℕ} {Z : Type u_2} [Nonempty Z] [MeasurableSpace Z] [StandardBorelSpace Z] {μ : MeasureTheory.Measure Z} [MeasureTheory.IsProbabilityMeasure μ] {f : (Fin n → Z) → ℝ} {c : Fin n → ℝ} (hbdd : Azuma.BoundedDifferences.HasBoundedDifferences f c) (hf : MeasureTheory.StronglyMeasurable f) (hfi : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin n) => μ)) (hc : ∀ (k : Fin n), 0 ≤ c k) {ε : ℝ} (hε : 0 ≤ ε) : (MeasureTheory.Measure.pi fun (x : Fin n) => μ).real {S : Fin n → Z | f S + ε ≤ ∫ (s : Fin n → Z), f s ∂MeasureTheory.Measure.pi fun (x : Fin n) => μ} ≤ Real.exp (-2 * ε ^ 2 / ∑ k : Fin n, c k ^ 2)

Lower-tail form of the sharp product-measure bounded-differences theorem.

This is the upper-tail theorem applied to -f; the bounded-differences widths are unchanged by negation.

theorem FormalSLT.Concentration.mcdiarmid_twoSided_of_hasBoundedDifferences_sharp {n : ℕ} {Z : Type u_2} [Nonempty Z] [MeasurableSpace Z] [StandardBorelSpace Z] {μ : MeasureTheory.Measure Z} [MeasureTheory.IsProbabilityMeasure μ] {f : (Fin n → Z) → ℝ} {c : Fin n → ℝ} (hbdd : Azuma.BoundedDifferences.HasBoundedDifferences f c) (hf : MeasureTheory.StronglyMeasurable f) (hfi : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin n) => μ)) (hc : ∀ (k : Fin n), 0 ≤ c k) {ε : ℝ} (hε : 0 ≤ ε) : (MeasureTheory.Measure.pi fun (x : Fin n) => μ).real {S : Fin n → Z | ε ≤ |f S - ∫ (s : Fin n → Z), f s ∂MeasureTheory.Measure.pi fun (x : Fin n) => μ|} ≤ 2 * Real.exp (-2 * ε ^ 2 / ∑ k : Fin n, c k ^ 2)

Two-sided sharp McDiarmid bounded-differences inequality.

For an arbitrary function on a homogeneous product space whose coordinate sensitivity is bounded by c k, the centered absolute deviation has the textbook Boucheron-Lugosi-Massart/McDiarmid tail

P(|f(S) - E[f]| >= ε) <= 2 * exp(-2 * ε^2 / sum_k c_k^2).

The proof combines the sharp upper-tail wrapper with the lower-tail wrapper above and applies the finite union bound for the two events.

theorem FormalSLT.Concentration.mcdiarmid_additive_independent {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} {a b : ι → ℝ} (hmeas : ∀ (i : ι), Measurable (X i)) (hindep : ProbabilityTheory.iIndepFun X μ) (hab : ∀ (i : ι), a i ≤ b i) (hX : ∀ (i : ι), ∀ᵐ (ω : Ω) ∂μ, X i ω ∈ Set.Icc (a i) (b i)) {s : Finset ι} {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | t ≤ ∑ i ∈ s, (X i ω - ∫ (x : Ω), X i x ∂μ)} ≤ Real.exp (-2 * t ^ 2 / ∑ i ∈ s, (b i - a i) ^ 2)

McDiarmid bounded-differences inequality, additive independent case.

For an additive statistic ∑ i ∈ s, X i of independent random variables with each X i supported almost surely in [a i, b i], McDiarmid's bounded- differences inequality coincides with Hoeffding's inequality for sums of independent sub-Gaussian variables: the bounded difference in coordinate i is exactly b i - a i, and the centered statistic obeys the sharp tail bound exp (-2 t^2 / ∑ (b_i - a_i)^2).

This is the special case exercised by the standard test instances (c_i = 1, c_i = 1/n). The genuinely non-additive bounded-differences case (arbitrary f over a product measure) is proved by mcdiarmid_of_hasBoundedDifferences_sharp, using the exposure-martingale kernel route.