Coarse-graining support: Support.Probability.IndependentSums.Rosenthal.ScalarBennett

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.IndependentSums.bennettOptimalLambda_nonneg {v y t : ℝ} (hy : 0 < y) (hv : 0 < v) (ht : 0 ≤ t) : 0 ≤ bennettOptimalLambda v y t

theorem HCPolySupport.IndependentSums.bennettOptimalExponent_eq {v y t : ℝ} (hy : 0 < y) (hv : 0 < v) (ht : 0 ≤ t) : -bennettOptimalLambda v y t * t + v / y ^ 2 * (Real.exp (bennettOptimalLambda v y t * y) - 1 - bennettOptimalLambda v y t * y) = -(v / y ^ 2) * bennettH (t * y / v)

theorem HCPolySupport.IndependentSums.integrable_of_abs_le_const {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {C : ℝ} (hXm : AEMeasurable X μ) (hXbdd : ∀ᵐ (ω : Ω) ∂μ, |X ω| ≤ C) : MeasureTheory.Integrable X μ

theorem HCPolySupport.IndependentSums.integrable_pow_two_of_abs_le_const {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {C : ℝ} (hXm : AEMeasurable X μ) (hXbdd : ∀ᵐ (ω : Ω) ∂μ, |X ω| ≤ C) : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 2) μ

theorem HCPolySupport.IndependentSums.integrable_exp_mul_of_abs_le_const {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {l y : ℝ} (hl : 0 ≤ l) (hXm : AEMeasurable X μ) (hXbdd : ∀ᵐ (ω : Ω) ∂μ, |X ω| ≤ y) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * X ω)) μ

noncomputable def HCPolySupport.IndependentSums.bennettTailTerm (a : ℝ) (n : ℕ) : ℝ

The tail term in the second-order exponential remainder series.

Equations

• HCPolySupport.IndependentSums.bennettTailTerm a n = a ^ (n + 2) / ↑(n + 2).factorial

theorem HCPolySupport.IndependentSums.summable_bennettTailTerm (a : ℝ) : Summable (bennettTailTerm a)

theorem HCPolySupport.IndependentSums.exp_mul_le_bennettEnvelope_of_abs_le {x y l : ℝ} (hy : 0 < y) (hl : 0 ≤ l) (hxy : |x| ≤ y) : Real.exp (l * x) ≤ 1 + l * x + x ^ 2 / y ^ 2 * (Real.exp (l * y) - 1 - l * y)

Scalar Bennett envelope on [-y, y], proved by comparing the exponential tail series termwise against the quadratic remainder at the endpoint y.

theorem HCPolySupport.IndependentSums.mgf_le_one_add_bennett_of_abs_le_of_integral_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {y l : ℝ} (hy : 0 < y) (hl : 0 ≤ l) (hXm : AEMeasurable X μ) (hXbdd : ∀ᵐ (ω : Ω) ∂μ, |X ω| ≤ y) (hXmean : ∫ (x : Ω), X x ∂μ = 0) : ProbabilityTheory.mgf X μ l ≤ 1 + ProbabilityTheory.moment X 2 μ / y ^ 2 * (Real.exp (l * y) - 1 - l * y)

One-variable Bennett mgf estimate in the pre-exponential 1 + A form.

theorem HCPolySupport.IndependentSums.mgf_le_exp_bennett_of_abs_le_of_integral_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {y l : ℝ} (hy : 0 < y) (hl : 0 ≤ l) (hXm : AEMeasurable X μ) (hXbdd : ∀ᵐ (ω : Ω) ∂μ, |X ω| ≤ y) (hXmean : ∫ (x : Ω), X x ∂μ = 0) : ProbabilityTheory.mgf X μ l ≤ Real.exp (ProbabilityTheory.moment X 2 μ / y ^ 2 * (Real.exp (l * y) - 1 - l * y))

One-variable Bennett mgf estimate for a centered variable bounded by y.

theorem HCPolySupport.IndependentSums.measureReal_upperTailEvent_le_of_mgf_le_bennett {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {v y a : ℝ} (hy : 0 < y) (hv : 0 < v) (ha : 0 ≤ a) (h_int : ∀ (l : ℝ), 0 ≤ l → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * X ω)) μ) (hmgf : ∀ (l : ℝ), 0 ≤ l → ProbabilityTheory.mgf X μ l ≤ Real.exp (v / y ^ 2 * (Real.exp (l * y) - 1 - l * y))) : μ.real (upperTailEvent X a) ≤ Real.exp (-(v / y ^ 2) * bennettH (a * y / v))

A Bennett-type moment-generating-function bound implies the corresponding upper-tail estimate after Chernoff optimization.

theorem HCPolySupport.IndependentSums.mgf_finset_sum_le_of_iIndepFun_of_mgf_le_bennett {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {v : ι → ℝ} {s : Finset ι} {y l : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hmgf : ∀ i ∈ s, ProbabilityTheory.mgf (X i) μ l ≤ Real.exp (v i / y ^ 2 * (Real.exp (l * y) - 1 - l * y))) : ProbabilityTheory.mgf (fun (ω : Ω) => ∑ i ∈ s, X i ω) μ l ≤ Real.exp ((∑ i ∈ s, v i) / y ^ 2 * (Real.exp (l * y) - 1 - l * y))

Finite independent sums inherit Bennett-form mgf bounds with the variances adding linearly.

theorem HCPolySupport.IndependentSums.measureReal_upperTailEvent_finset_sum_le_of_iIndepFun_of_mgf_le_bennett {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → ℝ} {v : ι → ℝ} {s : Finset ι} {y a : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hy : 0 < y) (hv : 0 < ∑ i ∈ s, v i) (ha : 0 ≤ a) (h_int : ∀ i ∈ s, ∀ (l : ℝ), 0 ≤ l → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * X i ω)) μ) (hmgf : ∀ i ∈ s, ∀ (l : ℝ), 0 ≤ l → ProbabilityTheory.mgf (X i) μ l ≤ Real.exp (v i / y ^ 2 * (Real.exp (l * y) - 1 - l * y))) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) a) ≤ Real.exp (-((∑ i ∈ s, v i) / y ^ 2 * bennettH (a * y / ∑ i ∈ s, v i)))

Bennett tail bounds for finite independent sums, assuming Bennett-form mgf bounds for each summand.

theorem HCPolySupport.IndependentSums.mgf_finset_sum_le_bennett_of_iIndepFun_of_abs_le_of_integral_eq_zero {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {y l : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hy : 0 < y) (hl : 0 ≤ l) (hXbdd : ∀ i ∈ s, ∀ᵐ (ω : Ω) ∂μ, |X i ω| ≤ y) (hXmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0) : ProbabilityTheory.mgf (fun (ω : Ω) => ∑ i ∈ s, X i ω) μ l ≤ Real.exp ((∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ) / y ^ 2 * (Real.exp (l * y) - 1 - l * y))

Bounded centered independent summands satisfy the project Bennett mgf bound with variance proxy given by the sum of second moments.

theorem HCPolySupport.IndependentSums.measureReal_upperTailEvent_finset_sum_le_bennett_of_iIndepFun_of_abs_le_of_integral_eq_zero {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {y a : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hy : 0 < y) (hv : 0 < ∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ) (ha : 0 ≤ a) (hXbdd : ∀ i ∈ s, ∀ᵐ (ω : Ω) ∂μ, |X i ω| ≤ y) (hXmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) a) ≤ Real.exp (-((∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ) / y ^ 2 * bennettH (a * y / ∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ)))

Bennett upper-tail estimate for finite sums of bounded centered independent real random variables.

theorem HCPolySupport.IndependentSums.measureReal_absTailEvent_finset_sum_le_bennett_of_iIndepFun_of_abs_le_of_integral_eq_zero {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {y a : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hy : 0 < y) (hv : 0 < ∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ) (ha : 0 ≤ a) (hXbdd : ∀ i ∈ s, ∀ᵐ (ω : Ω) ∂μ, |X i ω| ≤ y) (hXmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0) : μ.real (absTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) a) ≤ 2 * Real.exp (-((∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ) / y ^ 2 * bennettH (a * y / ∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ)))

Bennett absolute-tail estimate for finite sums of bounded centered independent real random variables.