1.3. Exponential concentration🔗

Lemma1.3.1

uses 0

Used by 3

Reverse dependency previews

Preview

Proposition 1.3.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsscalarconcentrationmgfsource-chen-shao-2005fidelity-generalized-parameter-form

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

theoremdefined in ProbabilityApproximation/ChenShao/ExponentialConcentration.lean

complete

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.lean

complete

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. The formal statement retains t as a parameter; optimizing it recovers the paper's equations (6.3)--(6.4).

Proposition1.3.2

uses 1used by 1✓L∃∀N

Tagsscalarconcentrationupper-truncationsource-chen-shao-2005fidelity-corrected-relaxed-constants

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

theoremdefined in ProbabilityApproximation/ChenShao/ExponentialConcentration.lean

complete

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; the formal theorem uses 24,48 because its proof keeps the one-sided truncation drift that is absent from a displayed exchange equality in the source.