Concentration for independent finite samples

The finite-PMF form of Hoeffding's inequality exposes ordinary sums and event probabilities. Its proof specializes McDiarmid's bounded-differences inequality (Complexity.Probability.BoundedDifferences) to sums of bounded coordinate scores via linearity of expectation (sum_pi_mul_sum). No measurable-space choices appear in the client-facing statements.

Main results

• Cslib.Probability.PMF.pi_sum_le_mean_sub: lower-tail concentration of bounded scores.
• Cslib.Probability.PMF.pi_sum_ge_mean_add: the corresponding upper-tail bound.
• Cslib.Probability.PMF.pi_sum_abs_sub_mean_ge: the two-sided bound.
• Cslib.Probability.PMF.uniform_abs_sum_div_sub_expect_ge_le: the two-sided bound for the empirical average of a [-1, 1]-valued function at independent uniform points.

References

• W. Hoeffding, Probability inequalities for sums of bounded random variables.
• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Section 3.3 and Proposition 1. These bounded-score estimates support repetition in entropy extraction; they do not assert the full smoothed conditional-entropy statement of that proposition.

Adapted from Probability/Concentration.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, reusing Mathlib's sub-Gaussian estimates.

theorem Cslib.Probability.PMF.pi_sum_le_mean_sub {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] (p : (i : ι) → PMF (α i)) (score : (i : ι) → α i → ℝ) {bound ε : ℝ} (hbound : 0 ≤ bound) (hscore : ∀ (i : ι), ∀ a ∈ (p i).support, score i a ∈ Set.Icc 0 bound) (hε : 0 ≤ ε) : ((pi p).toOuterMeasure {outcome : (i : ι) → α i | ∑ i : ι, score i (outcome i) ≤ ∑ i : ι, ∑ a : α i, ((p i) a).toReal * score i a - ε}).toReal ≤ Real.exp (-2 * ε ^ 2 / (↑(Fintype.card ι) * bound ^ 2))

The sum of independent bounded scores falls below its mean only with exponentially small probability. The scores and their means are finite sums; all probabilities are ordinary PMFs.

theorem Cslib.Probability.PMF.pi_sum_ge_mean_add {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] (p : (i : ι) → PMF (α i)) (score : (i : ι) → α i → ℝ) {bound ε : ℝ} (hbound : 0 ≤ bound) (hscore : ∀ (i : ι), ∀ a ∈ (p i).support, score i a ∈ Set.Icc 0 bound) (hε : 0 ≤ ε) : ((pi p).toOuterMeasure {outcome : (i : ι) → α i | ∑ i : ι, ∑ a : α i, ((p i) a).toReal * score i a + ε ≤ ∑ i : ι, score i (outcome i)}).toReal ≤ Real.exp (-2 * ε ^ 2 / (↑(Fintype.card ι) * bound ^ 2))

The upper-tail counterpart of pi_sum_le_mean_sub, obtained by clamping scores outside the support and applying HasBoundedDifferences.pi_ge_mean_add.

theorem Cslib.Probability.PMF.pi_sum_abs_sub_mean_ge {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] (p : (i : ι) → PMF (α i)) (score : (i : ι) → α i → ℝ) {bound ε : ℝ} (hbound : 0 ≤ bound) (hscore : ∀ (i : ι), ∀ a ∈ (p i).support, score i a ∈ Set.Icc 0 bound) (hε : 0 ≤ ε) : ((pi p).toOuterMeasure {outcome : (i : ι) → α i | ε ≤ |∑ i : ι, score i (outcome i) - ∑ i : ι, ∑ a : α i, ((p i) a).toReal * score i a|}).toReal ≤ 2 * Real.exp (-2 * ε ^ 2 / (↑(Fintype.card ι) * bound ^ 2))

The two-sided finite Hoeffding bound, with an explicit factor of two for the two tails.

theorem Cslib.Probability.PMF.uniform_abs_sum_div_sub_expect_ge_le {m : ℕ} {α : Type u_3} [Fintype α] [Nonempty α] (s : α → ℝ) (hs : ∀ (a : α), |s a| ≤ 1) (hm : 0 < m) {γ : ℝ} (hγ : 0 ≤ γ) : (uniformOfFintype (Fin m → α)).toOuterMeasure {ω : Fin m → α | γ ≤ |(∑ j : Fin m, s (ω j)) / ↑m - Finset.univ.expect fun (a : α) => s a|} ≤ ENNReal.ofReal (2 * Real.exp (-(↑m * γ ^ 2) / 2))

Hoeffding's inequality for an empirical average: the average of a function with values in [-1, 1] at m > 0 independent uniform points is off from its mean by at least γ with probability at most 2 exp (-m γ² / 2).