Documentation

TauCeti.Probability.Moments.Azuma

Azuma-Hoeffding inequality #

This file proves the Azuma-Hoeffding tail bound for a finite sum of bounded martingale differences, on an arbitrary probability space. A conditional form of Hoeffding's lemma bounds the conditional exponential moment of each bounded, conditionally centered increment, using a chord bound and the two-point law rather than regular conditional distributions. Induction on the partial sums then shows that the sum is sub-Gaussian, and the Chernoff bound gives the tail. Only hasCondSubgaussianMGF_of_mem_Icc_of_condExp_eq_zero, whose conclusion is Mathlib's kernel predicate, needs a standard Borel space.

Main results #

References #

source
theorem MeasureTheory.Measure.integral_exp_mul_sub_integral_le_of_abs_sub_le {β : Type u_2} [MeasurableSpace β] (ν : Measure β) [IsProbabilityMeasure ν] {X : β → ℝ} (hX : AEMeasurable X ν) {C : ℝ} (hosc : ∀ (a a' : β), |X a - X a'| ≤ C) (t : ℝ) :
∫ (a : β), Real.exp (t * (X a - ∫ (a' : β), X a' ∂ν)) ∂ν ≤ Real.exp ((C / 2) ^ 2 * t ^ 2 / 2)

Hoeffding's lemma, oscillation form. If an almost everywhere measurable real function on a probability space has oscillation at most C, then its centered exponential moment is at most exp ((C / 2) ^ 2 * t ^ 2 / 2).

source
theorem TauCeti.Probability.hasCondSubgaussianMGF_of_mem_Icc_of_condExp_eq_zero {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [StandardBorelSpace Ω] [MeasureTheory.IsProbabilityMeasure μ] {m : MeasurableSpace Ω} (hm : m ≤ mΩ) {X : Ω → ℝ} {a b : ℝ} (hX : Measurable X) (hbound : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) (hmean : μ[X | m] =ᵐ[μ] 0) :
ProbabilityTheory.HasCondSubgaussianMGF m hm X ((‖b - a‖₊ / 2) ^ 2) μ

A conditionally centered random variable whose values lie in [a, b] is conditionally sub-Gaussian with parameter ((‖b - a‖₊ / 2) ^ 2).

source
theorem TauCeti.Probability.chord_le_exp {a b : ℝ} (ha : a ≤ 0) (hb : 0 ≤ b) (hab : a < b) (t : ℝ) :
(b * Real.exp (t * a) - a * Real.exp (t * b)) / (b - a) ≤ Real.exp ((↑‖b - a‖₊ / 2) ^ 2 * t ^ 2 / 2)

The chord value (b e^{ta} - a e^{tb}) / (b - a) is at most exp (((b - a) / 2) ^ 2 t ^ 2 / 2) for a ≤ 0 ≤ b, by Hoeffding's lemma applied to the mean-zero two-point law on {a, b}.

source
theorem TauCeti.Probability.condExp_exp_mul_le {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {m : MeasurableSpace Ω} (hm : m ≤ mΩ) {X : Ω → ℝ} {a b : ℝ} (hX : AEMeasurable X μ) (hbound : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) (hmean : μ[X | m] =ᵐ[μ] 0) (t : ℝ) :
μ[fun (ω : Ω) => Real.exp (t * X ω) | m] ≤ᵐ[μ] fun (x : Ω) => Real.exp ((↑‖b - a‖₊ / 2) ^ 2 * t ^ 2 / 2)

Conditional Hoeffding's lemma without regular conditional distributions: the conditional exponential moment of a conditionally centered random variable with values in [a, b].

source
theorem TauCeti.Probability.hasSubgaussianMGF_add_of_condExp_eq_zero {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {m : MeasurableSpace Ω} (hm : m ≤ mΩ) {S X : Ω → ℝ} {c : NNReal} {a b : ℝ} (hS : ProbabilityTheory.HasSubgaussianMGF S c μ) (hSm : MeasureTheory.AEStronglyMeasurable S μ) (hX : AEMeasurable X μ) (hbound : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) (hmean : μ[X | m] =ᵐ[μ] 0) :
ProbabilityTheory.HasSubgaussianMGF (fun (ω : Ω) => S ω + X ω) (c + (‖b - a‖₊ / 2) ^ 2) μ

A conditionally centered bounded increment adds its Hoeffding variance proxy to a sub-Gaussian m-measurable random variable.

source
theorem TauCeti.Probability.hasSubgaussianMGF_sum_range_of_mem_Icc {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ mΩ} {Y : ℕ → Ω → ℝ} {a b : ℕ → ℝ} (h_adapted : MeasureTheory.StronglyAdapted ℱ Y) (n : ℕ) (hbound : ∀ i < n, ∀ᵐ (ω : Ω) ∂μ, Y i ω ∈ Set.Icc (a i) (b i)) (hmean0 : ∫ (ω : Ω), Y 0 ω ∂μ = 0) (hmean : ∀ i < n - 1, μ[Y (i + 1) | ↑ℱ i] =ᵐ[μ] 0) :
ProbabilityTheory.HasSubgaussianMGF (fun (ω : Ω) => ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, (‖b i - a i‖₊ / 2) ^ 2) μ

A sum of conditionally centered bounded increments is sub-Gaussian with the sum of the Hoeffding variance proxies.

source
theorem TauCeti.Probability.measureReal_sum_range_ge_le_of_mem_Icc_martingale_differences {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ mΩ} {Y : ℕ → Ω → ℝ} {a b : ℕ → ℝ} (h_adapted : MeasureTheory.StronglyAdapted ℱ Y) (n : ℕ) (hbound : ∀ i < n, ∀ᵐ (ω : Ω) ∂μ, Y i ω ∈ Set.Icc (a i) (b i)) (hmean0 : ∫ (ω : Ω), Y 0 ω ∂μ = 0) (hmean : ∀ i < n - 1, μ[Y (i + 1) | ↑ℱ i] =ᵐ[μ] 0) {ε : ℝ} (hε : 0 ≤ ε) :
μ.real {ω : Ω | ε ≤ ∑ i ∈ Finset.range n, Y i ω} ≤ Real.exp (-ε ^ 2 / (2 * ∑ i ∈ Finset.range n, (↑‖b i - a i‖₊ / 2) ^ 2))

Azuma-Hoeffding inequality for interval-bounded martingale differences. Let Y i be a strongly adapted sequence with conditionally centered increments in [a i, b i] almost surely. Then the upper tail is bounded using Hoeffding's variance proxy ∑ i < n, ((‖b i - a i‖₊ / 2) ^ 2).

The hypothesis StandardBorelSpace Ω is not needed for the classical inequality; it is inherited from Mathlib's HasCondSubgaussianMGF, which is defined through the conditional expectation kernel condExpKernel, and from measure_sum_ge_le_of_hasCondSubgaussianMGF.

source
theorem TauCeti.Probability.measureReal_sum_range_ge_le_of_bounded_martingale_differences {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ mΩ} {Y : ℕ → Ω → ℝ} {b : ℕ → NNReal} (h_adapted : MeasureTheory.StronglyAdapted ℱ Y) (n : ℕ) (hbound : ∀ i < n, ∀ᵐ (ω : Ω) ∂μ, |Y i ω| ≤ ↑(b i)) (hmean0 : ∫ (ω : Ω), Y 0 ω ∂μ = 0) (hmean : ∀ i < n - 1, μ[Y (i + 1) | ↑ℱ i] =ᵐ[μ] 0) {ε : ℝ} (hε : 0 ≤ ε) :
μ.real {ω : Ω | ε ≤ ∑ i ∈ Finset.range n, Y i ω} ≤ Real.exp (-ε ^ 2 / (2 * ∑ i ∈ Finset.range n, ↑(b i) ^ 2))

Azuma-Hoeffding inequality. Let Y i be a strongly adapted sequence of martingale differences with |Y i| ≤ b i almost surely, mean zero at time zero, and conditional mean zero at each later step. Then the upper tail of the sum of its first n terms is bounded by exp (-ε ^ 2 / (2 * ∑ i < n, b i ^ 2)).

source
theorem TauCeti.Probability.measureReal_abs_sum_range_ge_le_of_mem_Icc_martingale_differences {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ mΩ} {Y : ℕ → Ω → ℝ} {a b : ℕ → ℝ} (h_adapted : MeasureTheory.StronglyAdapted ℱ Y) (n : ℕ) (hbound : ∀ i < n, ∀ᵐ (ω : Ω) ∂μ, Y i ω ∈ Set.Icc (a i) (b i)) (hmean0 : ∫ (ω : Ω), Y 0 ω ∂μ = 0) (hmean : ∀ i < n - 1, μ[Y (i + 1) | ↑ℱ i] =ᵐ[μ] 0) {ε : ℝ} (hε : 0 ≤ ε) :
μ.real {ω : Ω | ε ≤ |∑ i ∈ Finset.range n, Y i ω|} ≤ 2 * Real.exp (-ε ^ 2 / (2 * ∑ i ∈ Finset.range n, (↑‖b i - a i‖₊ / 2) ^ 2))

Two-sided Azuma-Hoeffding inequality for interval-bounded martingale differences. Under the assumptions of the one-sided interval theorem, the absolute value of the sum exceeds ε with probability at most twice its one-sided bound.

source
theorem TauCeti.Probability.measureReal_abs_sum_range_ge_le_of_bounded_martingale_differences {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ mΩ} {Y : ℕ → Ω → ℝ} {b : ℕ → NNReal} (h_adapted : MeasureTheory.StronglyAdapted ℱ Y) (n : ℕ) (hbound : ∀ i < n, ∀ᵐ (ω : Ω) ∂μ, |Y i ω| ≤ ↑(b i)) (hmean0 : ∫ (ω : Ω), Y 0 ω ∂μ = 0) (hmean : ∀ i < n - 1, μ[Y (i + 1) | ↑ℱ i] =ᵐ[μ] 0) {ε : ℝ} (hε : 0 ≤ ε) :
μ.real {ω : Ω | ε ≤ |∑ i ∈ Finset.range n, Y i ω|} ≤ 2 * Real.exp (-ε ^ 2 / (2 * ∑ i ∈ Finset.range n, ↑(b i) ^ 2))

Two-sided Azuma-Hoeffding inequality. Under the assumptions of measureReal_sum_range_ge_le_of_bounded_martingale_differences, the absolute value of the sum exceeds ε with probability at most twice the one-sided bound.