1.3. Exponential concentration
Bennett--Hoeffding moment-generating-function bound. Let J be finite and let
(\eta_j)_{j\in J} be independent measurable random variables with finite second
moments. Suppose \mathbb E\eta_j\le0, \eta_j\le\alpha almost surely,
\alpha>0, and
\sum_{j\in J}\mathbb E\eta_j^2\le B^2.
Then, for every t\ge0,
\mathbb E\exp\!\left(t\sum_{j\in J}\eta_j\right)
\le
\exp\!\left(\frac{e^{t\alpha}-1-t\alpha}{\alpha^2}B^2\right).
Consequently, for every x\in\mathbb R,
\Pr\left(\sum_{j\in J}\eta_j\ge x\right)
\le
\exp\!\left(-tx+\frac{e^{t\alpha}-1-t\alpha}{\alpha^2}B^2\right).
Lean code for Lemma1.3.1●2 theorems
Associated Lean declarations
-
theoremdefined in ProbabilityApproximation/ChenShao/ExponentialConcentration.leancomplete
theorem ProbabilityTheory.mgf_finsetSum_le_exp_bennett.{u_1, u_2} {I : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [Fintype I] {Y : I → Ω → ℝ} {t α B2 : ℝ} (s : Finset I) (hY_meas : ∀ (i : I), Measurable (Y i)) (h_indep : ProbabilityTheory.iIndepFun Y μ) (hY_mem : ∀ (i : I), MeasureTheory.MemLp (Y i) 2 μ) (hY_mean : ∀ (i : I), ∫ (ω : Ω), Y i ω ∂μ ≤ 0) (hY_le : ∀ (i : I), ∀ᵐ (ω : Ω) ∂μ, Y i ω ≤ α) (hsecond : ∑ i ∈ s, ∫ (ω : Ω), Y i ω ^ 2 ∂μ ≤ B2) (ht : 0 ≤ t) (hα : 0 < α) : ProbabilityTheory.mgf (∑ i ∈ s, Y i) μ t ≤ Real.exp ((Real.exp (t * α) - 1 - t * α) / α ^ 2 * B2)
theorem ProbabilityTheory.mgf_finsetSum_le_exp_bennett.{u_1, u_2} {I : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [Fintype I] {Y : I → Ω → ℝ} {t α B2 : ℝ} (s : Finset I) (hY_meas : ∀ (i : I), Measurable (Y i)) (h_indep : ProbabilityTheory.iIndepFun Y μ) (hY_mem : ∀ (i : I), MeasureTheory.MemLp (Y i) 2 μ) (hY_mean : ∀ (i : I), ∫ (ω : Ω), Y i ω ∂μ ≤ 0) (hY_le : ∀ (i : I), ∀ᵐ (ω : Ω) ∂μ, Y i ω ≤ α) (hsecond : ∑ i ∈ s, ∫ (ω : Ω), Y i ω ^ 2 ∂μ ≤ B2) (ht : 0 ≤ t) (hα : 0 < α) : ProbabilityTheory.mgf (∑ i ∈ s, Y i) μ t ≤ Real.exp ((Real.exp (t * α) - 1 - t * α) / α ^ 2 * B2)
Chen--Shao (2005), (6.2), for a finite independent family.
-
theoremdefined in ProbabilityApproximation/ChenShao/ExponentialConcentration.leancomplete
theorem ProbabilityTheory.measure_finsetSum_ge_le_exp_bennett.{u_1, u_2} {I : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [Fintype I] {Y : I → Ω → ℝ} {t α B2 x : ℝ} (s : Finset I) (hY_meas : ∀ (i : I), Measurable (Y i)) (h_indep : ProbabilityTheory.iIndepFun Y μ) (hY_mem : ∀ (i : I), MeasureTheory.MemLp (Y i) 2 μ) (hY_mean : ∀ (i : I), ∫ (ω : Ω), Y i ω ∂μ ≤ 0) (hY_le : ∀ (i : I), ∀ᵐ (ω : Ω) ∂μ, Y i ω ≤ α) (hsecond : ∑ i ∈ s, ∫ (ω : Ω), Y i ω ^ 2 ∂μ ≤ B2) (ht : 0 ≤ t) (hα : 0 < α) : μ.real {ω | x ≤ ∑ i ∈ s, Y i ω} ≤ Real.exp (-t * x + (Real.exp (t * α) - 1 - t * α) / α ^ 2 * B2)
theorem ProbabilityTheory.measure_finsetSum_ge_le_exp_bennett.{u_1, u_2} {I : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [Fintype I] {Y : I → Ω → ℝ} {t α B2 x : ℝ} (s : Finset I) (hY_meas : ∀ (i : I), Measurable (Y i)) (h_indep : ProbabilityTheory.iIndepFun Y μ) (hY_mem : ∀ (i : I), MeasureTheory.MemLp (Y i) 2 μ) (hY_mean : ∀ (i : I), ∫ (ω : Ω), Y i ω ∂μ ≤ 0) (hY_le : ∀ (i : I), ∀ᵐ (ω : Ω) ∂μ, Y i ω ≤ α) (hsecond : ∑ i ∈ s, ∫ (ω : Ω), Y i ω ^ 2 ∂μ ≤ B2) (ht : 0 ≤ t) (hα : 0 < α) : μ.real {ω | x ≤ ∑ i ∈ s, Y i ω} ≤ Real.exp (-t * x + (Real.exp (t * α) - 1 - t * α) / α ^ 2 * B2)
Chernoff consequence of the Bennett--Hoeffding MGF estimate.
This is Lemma 6.2 and equation (6.2) of Chen and Shao (2005), together with
its Chernoff consequence,
printed pp. 40--41. Keeping t as a parameter and
optimizing it recovers the paper's equations (6.3)--(6.4).
Exponential concentration for the upper-truncated leave-one-out sum. Define
\bar X_j=X_j\mathbf 1_{\{X_j\le1\}} and
\bar W^{(i)}=\sum_{j\ne i}\bar X_j. Suppose
\mathbb EX_j=0, \mathbb E X_j^2<\infty,
\sum_j\operatorname{Var}(X_j)=1, and \gamma<\infty. Then, for every
i\in I and all a\le b,
\Pr(a\le\bar W^{(i)}\le b)
\le e^{-a/2}\bigl(24(b-a)+48\gamma\bigr).
Lean code for Proposition1.3.2●1 theorem
Associated Lean declarations
-
theoremdefined in ProbabilityApproximation/ChenShao/ExponentialConcentration.leancomplete
theorem ProbabilityTheory.chenShao_exponentialConcentration_upperTruncated.{u_1, u_2} {I : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [Fintype I] [DecidableEq I] {X : I → Ω → ℝ} (hX_meas : ∀ (j : I), Measurable (X j)) (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_mem : ∀ (j : I), MeasureTheory.MemLp (X j) 2 μ) (hX_mean : ∀ (j : I), ∫ (ω : Ω), X j ω ∂μ = 0) (hvar : ∑ j, ProbabilityTheory.variance (X j) μ = 1) (h3 : ∀ (j : I), MeasureTheory.Integrable (fun ω => |X j ω| ^ 3) μ) (i : I) {a b : ℝ} (hab : a ≤ b) : μ.real {ω | ∑ j ∈ Finset.univ.erase i, ProbabilityTheory.upperTruncateOne (X j ω) ∈ Set.Icc a b} ≤ Real.exp (-a / 2) * (24 * (b - a) + 48 * ProbabilityTheory.thirdMomentSum X μ)
theorem ProbabilityTheory.chenShao_exponentialConcentration_upperTruncated.{u_1, u_2} {I : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [Fintype I] [DecidableEq I] {X : I → Ω → ℝ} (hX_meas : ∀ (j : I), Measurable (X j)) (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_mem : ∀ (j : I), MeasureTheory.MemLp (X j) 2 μ) (hX_mean : ∀ (j : I), ∫ (ω : Ω), X j ω ∂μ = 0) (hvar : ∑ j, ProbabilityTheory.variance (X j) μ = 1) (h3 : ∀ (j : I), MeasureTheory.Integrable (fun ω => |X j ω| ^ 3) μ) (i : I) {a b : ℝ} (hab : a ≤ b) : μ.real {ω | ∑ j ∈ Finset.univ.erase i, ProbabilityTheory.upperTruncateOne (X j ω) ∈ Set.Icc a b} ≤ Real.exp (-a / 2) * (24 * (b - a) + 48 * ProbabilityTheory.thirdMomentSum X μ)
Chen--Shao (2005), Proposition 6.1, with a corrected truncation-drift term and relaxed absolute constants. The paper states constants `5` and `7`. The proof below retains the same exponentially weighted shape while exposing the drift omitted by the displayed exchange equality in the paper.
This is the exponentially weighted conclusion of Chen and Shao (2005), Proposition 6.1, equation (6.1),
with the proof on printed pp. 41--43. The paper prints constants
5,7. Accounting explicitly for the one-sided truncation drift gives the
coefficients 24,48; the displayed exchange equality in the source omits this drift.