Bernstein's inequality

Let X₁, …, Xₙ be independent real random variables with mean zero, finite second moments and Xᵢ ≤ b almost surely, and put v = ∑ᵢ E Xᵢ². Bernstein's inequality bounds the upper tail of S = ∑ᵢ Xᵢ by exp (-ε ^ 2 / (2 * (v + b * ε / 3))) for every ε ≥ 0. For moderate ε this is the Gaussian tail with the true variance v, rather than the worst-case variance proxy of Hoeffding's inequality (ProbabilityTheory.HasSubgaussianMGF.measure_sum_ge_le_of_iIndepFun); for large ε it decays exponentially at rate 3 / (2 b).

Main results

• MeasureTheory.MemLp.mgf_le_exp_of_ae_le: if E X = 0, E X² < ∞ and X ≤ b almost surely, then E exp (t X) ≤ exp (E X² * t ^ 2 / (2 * (1 - t * b / 3))) for 0 ≤ t with t * b < 3;
• ProbabilityTheory.iIndepFun.mgf_sum_le_exp_of_ae_le: the same bound for an independent sum, with E X² replaced by v;
• ProbabilityTheory.iIndepFun.measureReal_sum_ge_le_of_ae_le: Bernstein's inequality for the upper tail;
• ProbabilityTheory.iIndepFun.measureReal_abs_sum_ge_le_of_abs_le: the two-sided form P(|S| ≥ ε) ≤ 2 * exp (-ε ^ 2 / (2 * (v + b * ε / 3))) when |Xᵢ| ≤ b.

References

• S. Bernstein, Theory of Probability (in Russian), Moscow (1927).
• S. Boucheron, G. Lugosi and P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press (2013), §2.8.

theorem MeasureTheory.MemLp.mgf_le_exp_of_ae_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ] {X : Ω → ℝ} {b t : ℝ} (hX : MemLp X 2 μ) (hmean : ∫ (x : Ω), X x ∂μ = 0) (hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b) (ht : 0 ≤ t) (htb : t * b < 3) : ProbabilityTheory.mgf X μ t ≤ Real.exp ((∫ (ω : Ω), X ω ^ 2 ∂μ) * t ^ 2 / (2 * (1 - t * b / 3)))

Bernstein's moment-generating-function bound. If X has mean zero, a finite second moment and X ≤ b almost surely, then for 0 ≤ t with t * b < 3, E exp (t X) ≤ exp (E X² * t ^ 2 / (2 * (1 - t * b / 3))).

theorem ProbabilityTheory.iIndepFun.mgf_sum_le_exp_of_ae_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) {s : Finset ι} {b t : ℝ} (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0) (hb : ∀ i ∈ s, ∀ᵐ (ω : Ω) ∂μ, X i ω ≤ b) (ht : 0 ≤ t) (htb : t * b < 3) : mgf (fun (ω : Ω) => ∑ i ∈ s, X i ω) μ t ≤ Real.exp ((∑ i ∈ s, ∫ (ω : Ω), X i ω ^ 2 ∂μ) * t ^ 2 / (2 * (1 - t * b / 3)))

Bernstein's moment-generating-function bound for independent sums. If the Xᵢ, i ∈ s, are independent with mean zero, finite second moments and Xᵢ ≤ b almost surely, then for 0 ≤ t with t * b < 3 the moment-generating function of ∑ i ∈ s, Xᵢ at t is at most exp (v * t ^ 2 / (2 * (1 - t * b / 3))), where v = ∑ i ∈ s, E Xᵢ².

theorem ProbabilityTheory.iIndepFun.measureReal_sum_ge_le_of_ae_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) {s : Finset ι} {b ε : ℝ} (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0) (hb : ∀ i ∈ s, ∀ᵐ (ω : Ω) ∂μ, X i ω ≤ b) (hε : 0 ≤ ε) : μ.real {ω : Ω | ε ≤ ∑ i ∈ s, X i ω} ≤ Real.exp (-ε ^ 2 / (2 * (∑ i ∈ s, ∫ (ω : Ω), X i ω ^ 2 ∂μ + b * ε / 3)))

Bernstein's inequality. Let the Xᵢ, i ∈ s, be independent with mean zero, finite second moments and Xᵢ ≤ b almost surely, and let v = ∑ i ∈ s, E Xᵢ². Then for 0 ≤ ε, P(ε ≤ ∑ i ∈ s, Xᵢ) ≤ exp (-ε ^ 2 / (2 * (v + b * ε / 3))).

theorem ProbabilityTheory.iIndepFun.measureReal_abs_sum_ge_le_of_abs_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) {s : Finset ι} {b ε : ℝ} (hX : ∀ i ∈ s, AEMeasurable (X i) μ) (hmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0) (hb : ∀ i ∈ s, ∀ᵐ (ω : Ω) ∂μ, |X i ω| ≤ b) (hε : 0 ≤ ε) : μ.real {ω : Ω | ε ≤ |∑ i ∈ s, X i ω|} ≤ 2 * Real.exp (-ε ^ 2 / (2 * (∑ i ∈ s, ∫ (ω : Ω), X i ω ^ 2 ∂μ + b * ε / 3)))

Bernstein's inequality, two-sided form. Let the Xᵢ, i ∈ s, be independent and almost-everywhere measurable with mean zero and |Xᵢ| ≤ b almost surely, and let v = ∑ i ∈ s, E Xᵢ². Then for 0 ≤ ε, P(ε ≤ |∑ i ∈ s, Xᵢ|) ≤ 2 * exp (-ε ^ 2 / (2 * (v + b * ε / 3))).