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

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

theorem HCPolySupport.IndependentSums.integral_absTruncation_eq_zero_of_identDistrib_neg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {r : ℝ} (hX_symm : ProbabilityTheory.IdentDistrib X (fun (ω : Ω) => -X ω) μ μ) : ∫ (x : Ω), absTruncation X r x ∂μ = 0

A symmetric variable keeps zero mean after absolute truncation.

theorem HCPolySupport.IndependentSums.absTruncation_eq_self_of_sup'_abs_le {Ω : Type u_1} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {r : ℝ} {ω : Ω} (hω : (s.sup' hs fun (i : ι) => |X i ω|) ≤ r) (i : ι) : i ∈ s → absTruncation (X i) r ω = X i ω

If the absolute maximum of a finite family is below the truncation scale, each truncated variable agrees with the original one.

theorem HCPolySupport.IndependentSums.absTailEvent_finsetSum_subset_sup'_abs_union_absTruncation {Ω : Type u_1} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {r t : ℝ} : absTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) t ⊆ upperTailEvent (fun (ω : Ω) => s.sup' hs fun (i : ι) => |X i ω|) r ∪ absTailEvent (fun (ω : Ω) => ∑ i ∈ s, absTruncation (X i) r ω) t

In the symmetric Rosenthal proof, the tail of the finite sum splits into the tail of the finite maximum and the tail of the bounded truncation sum.

theorem HCPolySupport.IndependentSums.abs_absTruncation_le_abs {Ω : Type u_1} {X : Ω → ℝ} {r : ℝ} (ω : Ω) : |absTruncation X r ω| ≤ |X ω|

theorem HCPolySupport.IndependentSums.moment_absTruncation_two_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {r : ℝ} (hX_meas : Measurable X) (hX_sq_int : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 2) μ) : ProbabilityTheory.moment (absTruncation X r) 2 μ ≤ ProbabilityTheory.moment X 2 μ

Truncating a variable can only decrease its second moment.

theorem HCPolySupport.IndependentSums.measureReal_absTailEvent_finsetSum_le_sup'_abs_add_bennett {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {r t : ℝ} (hr : 0 < r) (ht : 0 ≤ t) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (h_symm : ∀ i ∈ s, ProbabilityTheory.IdentDistrib (X i) (fun (ω : Ω) => -X i ω) μ μ) (hv_pos : 0 < ∑ i ∈ s, ProbabilityTheory.moment (fun (ω : Ω) => absTruncation (X i) r ω) 2 μ) : μ.real (absTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) t) ≤ μ.real (upperTailEvent (fun (ω : Ω) => s.sup' hs fun (i : ι) => |X i ω|) r) + 2 * Real.exp (-((∑ i ∈ s, ProbabilityTheory.moment (fun (ω : Ω) => absTruncation (X i) r ω) 2 μ) / r ^ 2 * bennettH (t * r / ∑ i ∈ s, ProbabilityTheory.moment (fun (ω : Ω) => absTruncation (X i) r ω) 2 μ)))

Symmetric truncation tail bound: split off the event where the finite maximum exceeds the truncation scale, and apply Bennett to the bounded truncation sum.

theorem HCPolySupport.IndependentSums.bennett_truncation_exponent_eq_beta {v r t : ℝ} (hr : r ≠ 0) (hv : v ≠ 0) : v / r ^ 2 * bennettH (t * r / v) = t / r * bennettBeta (t * r / v)

theorem HCPolySupport.IndependentSums.measureReal_absTailEvent_finsetSum_le_sup'_abs_add_bennettBeta_of_scale {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p t : ℝ} (hp : 1 ≤ p) (ht : 0 < t) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (h_sq_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) (h_symm : ∀ i ∈ s, ProbabilityTheory.IdentDistrib (X i) (fun (ω : Ω) => -X i ω) μ μ) (hv_pos : 0 < ∑ i ∈ s, ProbabilityTheory.moment (fun (ω : Ω) => absTruncation (X i) (t / p) ω) 2 μ) (hSigma_pos : 0 < ∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ) : μ.real (absTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) t) ≤ μ.real (upperTailEvent (fun (ω : Ω) => s.sup' hs fun (i : ι) => |X i ω|) (t / p)) + 2 * Real.exp (-(p * bennettBeta (t ^ 2 / (p * ∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ))))

Moment-adapted truncation choice in the symmetric Rosenthal proof: specializing the truncation scale to r = t / p converts the Bennett term to the exact note-facing p β(t² / (p σ²)) form.

theorem HCPolySupport.IndependentSums.ae_eq_zero_of_moment_two_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX_sq_int : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 2) μ) (hX_moment_zero : ProbabilityTheory.moment X 2 μ = 0) : X =ᵐ[μ] 0

Vanishing second moment forces a real random variable to vanish almost everywhere. This is the degenerate case used in the Rosenthal proof when the variance proxy is zero.

theorem HCPolySupport.IndependentSums.ae_eq_zero_finsetSum_of_forall {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Y : ι → Ω → ℝ} {s : Finset ι} (hY_zero : ∀ i ∈ s, Y i =ᵐ[μ] 0) : (fun (ω : Ω) => ∑ i ∈ s, Y i ω) =ᵐ[μ] 0

A finite sum of almost-everywhere vanishing functions vanishes almost everywhere.

theorem HCPolySupport.IndependentSums.lintegral_abs_finsetSum_rpow_le_rosenthal_of_identDistrib_neg {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p : ℝ} (hp : 2 ≤ p) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (h_sq_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) (h_symm : ∀ i ∈ s, ProbabilityTheory.IdentDistrib (X i) (fun (ω : Ω) => -X i ω) μ μ) : ∫⁻ (ω : Ω), ENNReal.ofReal (|∑ i ∈ s, X i ω| ^ p) ∂μ ≤ ENNReal.ofReal (p ^ p) * ∫⁻ (ω : Ω), ENNReal.ofReal ((s.sup' hs fun (i : ι) => |X i ω|) ^ p) ∂μ + ENNReal.ofReal (2 * (rosenthalBennettIntegralConst * (√p * √(∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ))) ^ p)

Symmetric Rosenthal bound in lintegral form. This is the exact tail-integration endpoint coming from the Chapter 4 Bennett-plus-maximum split.

theorem HCPolySupport.IndependentSums.integrable_abs_finsetSum_rpow_of_identDistrib_neg {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p : ℝ} (hp : 2 ≤ p) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (h_sq_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) (h_symm : ∀ i ∈ s, ProbabilityTheory.IdentDistrib (X i) (fun (ω : Ω) => -X i ω) μ μ) (hmax_int : MeasureTheory.Integrable (fun (ω : Ω) => (s.sup' hs fun (i : ι) => |X i ω|) ^ p) μ) : MeasureTheory.Integrable (fun (ω : Ω) => |∑ i ∈ s, X i ω| ^ p) μ

Integrability consequence of the symmetric Rosenthal lintegral bound.

theorem HCPolySupport.IndependentSums.integral_abs_finsetSum_rpow_le_rosenthal_of_identDistrib_neg {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p : ℝ} (hp : 2 ≤ p) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (h_sq_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) (h_symm : ∀ i ∈ s, ProbabilityTheory.IdentDistrib (X i) (fun (ω : Ω) => -X i ω) μ μ) (hmax_int : MeasureTheory.Integrable (fun (ω : Ω) => (s.sup' hs fun (i : ι) => |X i ω|) ^ p) μ) : ∫ (ω : Ω), |∑ i ∈ s, X i ω| ^ p ∂μ ≤ p ^ p * ∫ (ω : Ω), (s.sup' hs fun (i : ι) => |X i ω|) ^ p ∂μ + 2 * (rosenthalBennettIntegralConst * (√p * √(∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ))) ^ p

Real-integral version of the symmetric Rosenthal bound.