Coarse-graining support: Support.Probability.IndependentSums.Rosenthal.CenteredTruncation #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.IndependentSums.mgf_centeredFinsetSum_absTruncation_le_bennett
{Ω : Type u_1}
{ι : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : ι → Ω → ℝ}
{r : ι → ℝ}
{s : Finset ι}
{y l : ℝ}
(h_indep : ProbabilityTheory.iIndepFun X μ)
(h_meas : ∀ (i : ι), Measurable (X i))
(h_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ)
(hy : 0 < y)
(hl : 0 ≤ l)
(hr_nonneg : ∀ i ∈ s, 0 ≤ r i)
(hr_bdd : ∀ i ∈ s, 2 * r i ≤ y)
:
ProbabilityTheory.mgf (centeredFinsetSum (fun (i : ι) => absTruncation (X i) (r i)) μ s) μ l ≤ Real.exp
((∑ i ∈ s, ProbabilityTheory.moment (centeredAbsTruncationFamily X r μ i) 2 μ) / y ^ 2 * (Real.exp (l * y) - 1 - l * y))
Bennett mgf bound for the finite sum of centered bounded truncations.
theorem
HCPolySupport.IndependentSums.measureReal_upperTailEvent_centeredFinsetSum_absTruncation_le_bennett
{Ω : Type u_1}
{ι : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : ι → Ω → ℝ}
{r : ι → ℝ}
{s : Finset ι}
{y a : ℝ}
(h_indep : ProbabilityTheory.iIndepFun X μ)
(h_meas : ∀ (i : ι), Measurable (X i))
(h_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ)
(hy : 0 < y)
(hv : 0 < ∑ i ∈ s, ProbabilityTheory.moment (centeredAbsTruncationFamily X r μ i) 2 μ)
(ha : 0 ≤ a)
(hr_nonneg : ∀ i ∈ s, 0 ≤ r i)
(hr_bdd : ∀ i ∈ s, 2 * r i ≤ y)
:
μ.real (upperTailEvent (centeredFinsetSum (fun (i : ι) => absTruncation (X i) (r i)) μ s) a) ≤ Real.exp
(-((∑ i ∈ s, ProbabilityTheory.moment (centeredAbsTruncationFamily X r μ i) 2 μ) / y ^ 2 * bennettH (a * y / ∑ i ∈ s, ProbabilityTheory.moment (centeredAbsTruncationFamily X r μ i) 2 μ)))
Bennett upper-tail bound for the finite sum of centered bounded truncations.
theorem
HCPolySupport.IndependentSums.measureReal_absTailEvent_centeredFinsetSum_absTruncation_le_bennett
{Ω : Type u_1}
{ι : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : ι → Ω → ℝ}
{r : ι → ℝ}
{s : Finset ι}
{y a : ℝ}
(h_indep : ProbabilityTheory.iIndepFun X μ)
(h_meas : ∀ (i : ι), Measurable (X i))
(h_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ)
(hy : 0 < y)
(hv : 0 < ∑ i ∈ s, ProbabilityTheory.moment (centeredAbsTruncationFamily X r μ i) 2 μ)
(ha : 0 ≤ a)
(hr_nonneg : ∀ i ∈ s, 0 ≤ r i)
(hr_bdd : ∀ i ∈ s, 2 * r i ≤ y)
:
μ.real (absTailEvent (centeredFinsetSum (fun (i : ι) => absTruncation (X i) (r i)) μ s) a) ≤ 2 * Real.exp
(-((∑ i ∈ s, ProbabilityTheory.moment (centeredAbsTruncationFamily X r μ i) 2 μ) / y ^ 2 * bennettH (a * y / ∑ i ∈ s, ProbabilityTheory.moment (centeredAbsTruncationFamily X r μ i) 2 μ)))
Bennett absolute-tail bound for the finite sum of centered bounded truncations.
theorem
HCPolySupport.IndependentSums.measureReal_absTailEvent_centeredFinsetSum_le_bennett_add_tail
{Ω : Type u_1}
{ι : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : ι → Ω → ℝ}
{r : ι → ℝ}
{s : Finset ι}
{y a b : ℝ}
(h_indep : ProbabilityTheory.iIndepFun X μ)
(h_meas : ∀ (i : ι), Measurable (X i))
(h_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ)
(hy : 0 < y)
(hv : 0 < ∑ i ∈ s, ProbabilityTheory.moment (centeredAbsTruncationFamily X r μ i) 2 μ)
(ha : 0 ≤ a)
(hr_nonneg : ∀ i ∈ s, 0 ≤ r i)
(hr_bdd : ∀ i ∈ s, 2 * r i ≤ y)
:
μ.real (absTailEvent (centeredFinsetSum X μ s) (a + b)) ≤ 2 * Real.exp
(-((∑ i ∈ s, ProbabilityTheory.moment (centeredAbsTruncationFamily X r μ i) 2 μ) / y ^ 2 * bennettH (a * y / ∑ i ∈ s, ProbabilityTheory.moment (centeredAbsTruncationFamily X r μ i) 2 μ))) + μ.real (absTailEvent (centeredFinsetSum (fun (i : ι) => absTailIndicator (X i) (r i)) μ s) b)
Splitting the centered sum into bounded truncation plus tail yields an absolute-tail bound with a Bennett term for the truncation piece and a residual tail term for the large-value part.
theorem
HCPolySupport.IndependentSums.measureReal_absTailEvent_centeredFinsetSum_absTailIndicator_le_two_mul_div
{Ω : Type u_1}
{ι : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : ι → Ω → ℝ}
{r : ι → ℝ}
{s : Finset ι}
{b : ℝ}
(hb : 0 < b)
(h_meas : ∀ (i : ι), Measurable (X i))
(h_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ)
:
μ.real (absTailEvent (centeredFinsetSum (fun (i : ι) => absTailIndicator (X i) (r i)) μ s) b) ≤ (2 * ∑ i ∈ s, ∫ (ω : Ω), |absTailIndicator (X i) (r i) ω| ∂μ) / b
The residual centered tail piece is controlled by the first moments of the
large-value tails via Markov's inequality and the bound
∫ |Y - E[Y]| ≤ 2 ∫ |Y|.
theorem
HCPolySupport.IndependentSums.measureReal_absTailEvent_centeredFinsetSum_le_bennett_add_tailIntegrals
{Ω : Type u_1}
{ι : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : ι → Ω → ℝ}
{r : ι → ℝ}
{s : Finset ι}
{y a b : ℝ}
(h_indep : ProbabilityTheory.iIndepFun X μ)
(h_meas : ∀ (i : ι), Measurable (X i))
(h_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ)
(hy : 0 < y)
(hv : 0 < ∑ i ∈ s, ProbabilityTheory.moment (centeredAbsTruncationFamily X r μ i) 2 μ)
(ha : 0 ≤ a)
(hb : 0 < b)
(hr_nonneg : ∀ i ∈ s, 0 ≤ r i)
(hr_bdd : ∀ i ∈ s, 2 * r i ≤ y)
:
μ.real (absTailEvent (centeredFinsetSum X μ s) (a + b)) ≤ 2 * Real.exp
(-((∑ i ∈ s, ProbabilityTheory.moment (centeredAbsTruncationFamily X r μ i) 2 μ) / y ^ 2 * bennettH (a * y / ∑ i ∈ s, ProbabilityTheory.moment (centeredAbsTruncationFamily X r μ i) 2 μ))) + (2 * ∑ i ∈ s, ∫ (ω : Ω), |absTailIndicator (X i) (r i) ω| ∂μ) / b
Combined note-facing tail estimate: the centered sum is bounded by the Bennett truncation term plus an explicit first-moment tail contribution.
@[simp]
@[simp]