def BoundedDifferences.HasBoundedDifferences {n : ℕ} {α : Fin n → Type u_1} [(i : Fin n) → DecidableEq (α i)] (f : ((i : Fin n) → α i) → ℝ) (c : Fin n → ℝ) : Prop

The function $f$ has bounded differences with coefficients $c_i$: changing the $i$-th coordinate of the input changes $f$ by at most $c_i$ in absolute value.

noncomputable def BoundedDifferences.liftToNat {n : ℕ} (c : Fin n → ℝ) : ℕ → ℝ

Lift a function Fin n → ℝ to a function ℕ → ℝ by extending with zeros for indices ≥ $n$.

theorem BoundedDifferences.liftToNat_nonneg {n : ℕ} (c : Fin n → ℝ) (hc : ∀ (i : Fin n), 0 ≤ c i) (i : ℕ) : 0 ≤ liftToNat c i

The nat-lifted version of a nonnegative Fin n-indexed function is nonnegative.

noncomputable def BoundedDifferences.hoeffdingParam (c : ℝ) (_hc : 0 ≤ c) : NNReal

The Hoeffding sub-Gaussian parameter $c^2/4$ associated with a bounded random variable of range $c$, packaged as a nonnegative real.

theorem BoundedDifferences.sum_hoeffdingParam_eq {n : ℕ} (c : Fin n → ℝ) (hc : ∀ (i : Fin n), 0 ≤ c i) : ↑(∑ i ∈ Finset.range n, hoeffdingParam (liftToNat c i) ⋯) = (∑ i : Fin n, c i ^ 2) / 4

The sum of Hoeffding parameters $\sum_{i<n} c_i^2/4$ equals $(\sum_i c_i^2)/4$.

theorem BoundedDifferences.doob_martingale_from_bounded_differences {n : ℕ} {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace Ω] {α : Fin n → Type u_2} [(i : Fin n) → MeasurableSpace (α i)] [(i : Fin n) → DecidableEq (α i)] (X : (i : Fin n) → Ω → α i) (hX_indep : ProbabilityTheory.iIndepFun X μ) (f : ((i : Fin n) → α i) → ℝ) (hf_meas : Measurable fun (ω : Ω) => f fun (i : Fin n) => X i ω) (c : Fin n → ℝ) (hc : ∀ (i : Fin n), 0 ≤ c i) (hbd : HasBoundedDifferences f c) : ∃ (ℱ : MeasureTheory.Filtration ℕ mΩ) (Y : ℕ → Ω → ℝ), (∀ (ω : Ω), ∑ i ∈ Finset.range n, Y i ω = (f fun (i : Fin n) => X i ω) - ∫ (ω' : Ω), f fun (i : Fin n) => X i ω' ∂μ) ∧ MeasureTheory.StronglyAdapted ℱ Y ∧ ProbabilityTheory.HasSubgaussianMGF (Y 0) (hoeffdingParam (liftToNat c 0) ⋯) μ ∧ ∀ i < n - 1, ProbabilityTheory.HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (hoeffdingParam (liftToNat c (i + 1)) ⋯) μ

The Doob martingale construction for a bounded-differences function: given independent $X_i$ and $f$ with bounded differences $c_i$, the martingale differences $Y_i$ satisfy $\sum_i Y_i = f(X) - \mathbb{E}[f(X)]$ and each $Y_{i+1}$ is conditionally sub-Gaussian with parameter $c_{i+1}^2/4$ given $\mathcal{F}_i$.

theorem BoundedDifferences.bounded_differences_upper_tail {n : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace Ω] {α : Fin n → Type u_2} [(i : Fin n) → MeasurableSpace (α i)] [(i : Fin n) → DecidableEq (α i)] (X : (i : Fin n) → Ω → α i) (hX_indep : ProbabilityTheory.iIndepFun X μ) (f : ((i : Fin n) → α i) → ℝ) (hf_meas : Measurable fun (ω : Ω) => f fun (i : Fin n) => X i ω) (c : Fin n → ℝ) (hc : ∀ (i : Fin n), 0 ≤ c i) (hbd : HasBoundedDifferences f c) {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | t ≤ (f fun (i : Fin n) => X i ω) - ∫ (x : Ω), (fun (ω : Ω) => f fun (i : Fin n) => X i ω) x ∂μ} ≤ Real.exp (-2 * t ^ 2 / ∑ i : Fin n, c i ^ 2)

Upper-tail bounded differences inequality (Theorem 9.1.3): if $f$ has bounded differences $c_i$ on independent coordinates $X_1, \dots, X_n$, then $\mathbb{P}(f(X) - \mathbb{E}f(X) \geq t) \leq \exp(-2t^2 / \sum_i c_i^2)$.

theorem BoundedDifferences.bounded_differences_lower_tail {n : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace Ω] {α : Fin n → Type u_2} [(i : Fin n) → MeasurableSpace (α i)] [(i : Fin n) → DecidableEq (α i)] (X : (i : Fin n) → Ω → α i) (hX_indep : ProbabilityTheory.iIndepFun X μ) (f : ((i : Fin n) → α i) → ℝ) (hf_meas : Measurable fun (ω : Ω) => f fun (i : Fin n) => X i ω) (c : Fin n → ℝ) (hc : ∀ (i : Fin n), 0 ≤ c i) (hbd : HasBoundedDifferences f c) {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | (f fun (i : Fin n) => X i ω) - ∫ (x : Ω), (fun (ω : Ω) => f fun (i : Fin n) => X i ω) x ∂μ ≤ -t} ≤ Real.exp (-2 * t ^ 2 / ∑ i : Fin n, c i ^ 2)

Lower-tail bounded differences inequality (Theorem 9.1.3): if $f$ has bounded differences $c_i$, then $\mathbb{P}(f(X) - \mathbb{E}f(X) \leq -t) \leq \exp(-2t^2 / \sum_i c_i^2)$.

theorem BoundedDifferences.bounded_differences_inequality {n : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace Ω] {α : Fin n → Type u_2} [(i : Fin n) → MeasurableSpace (α i)] [(i : Fin n) → DecidableEq (α i)] (X : (i : Fin n) → Ω → α i) (hX_indep : ProbabilityTheory.iIndepFun X μ) (f : ((i : Fin n) → α i) → ℝ) (hf_meas : Measurable fun (ω : Ω) => f fun (i : Fin n) => X i ω) (c : Fin n → ℝ) (hc : ∀ (i : Fin n), 0 ≤ c i) (hbd : HasBoundedDifferences f c) {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | t ≤ (f fun (i : Fin n) => X i ω) - ∫ (x : Ω), (fun (ω : Ω) => f fun (i : Fin n) => X i ω) x ∂μ} ≤ Real.exp (-2 * t ^ 2 / ∑ i : Fin n, c i ^ 2) ∧ μ.real {ω : Ω | (f fun (i : Fin n) => X i ω) - ∫ (x : Ω), (fun (ω : Ω) => f fun (i : Fin n) => X i ω) x ∂μ ≤ -t} ≤ Real.exp (-2 * t ^ 2 / ∑ i : Fin n, c i ^ 2)

The two-sided bounded differences inequality (Theorem 9.1.3, McDiarmid): both tails $\mathbb{P}(|f(X) - \mathbb{E}f(X)| \geq t)$ are bounded by $\exp(-2t^2 / \sum_i c_i^2)$.

theorem BoundedDifferences.bounded_differences_uniform_upper_tail {n : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace Ω] {α : Fin n → Type u_2} [(i : Fin n) → MeasurableSpace (α i)] [(i : Fin n) → DecidableEq (α i)] (X : (i : Fin n) → Ω → α i) (hX_indep : ProbabilityTheory.iIndepFun X μ) (f : ((i : Fin n) → α i) → ℝ) (hf_meas : Measurable fun (ω : Ω) => f fun (i : Fin n) => X i ω) (hbd : HasBoundedDifferences f fun (x : Fin n) => 1) {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | t ≤ (f fun (i : Fin n) => X i ω) - ∫ (x : Ω), (fun (ω : Ω) => f fun (i : Fin n) => X i ω) x ∂μ} ≤ Real.exp (-2 * t ^ 2 / ↑n)

Bounded differences inequality with uniform constant $c_i = 1$ (Theorem 9.1.1): if $f$ is $1$-Lipschitz per coordinate, then $\mathbb{P}(f(X) - \mathbb{E}f(X) \geq t) \leq \exp(-2t^2/n)$.