Coarse-graining support: Support.Probability.IndependentSums.Rosenthal.Corollaries #

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

(∫ (ω : Ω), |centeredFinsetSum X μ s ω| ^ p ∂μ) ^ (1 / ↑p) ≤ 2 * ↑p * (∑ i ∈ s, ∫ (ω : Ω), |X i ω| ^ p ∂μ) ^ (1 / ↑p) + 4 * rosenthalBennettIntegralConst * (√↑p * √(∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ))

Note-facing polynomial-moment Rosenthal bound with the maximal term replaced by the sum of the individual L^p moments.

theorem HCPolySupport.IndependentSums.integral_absSum_pow_rpow_inv_le_rosenthalPolynomial {Ω : 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)) (hLp_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => |X i ω| ^ p) μ) (hXmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0) :

(∫ (ω : Ω), |∑ i ∈ s, X i ω| ^ p ∂μ) ^ (1 / ↑p) ≤ 2 * ↑p * (∑ i ∈ s, ∫ (ω : Ω), |X i ω| ^ p ∂μ) ^ (1 / ↑p) + 4 * rosenthalBennettIntegralConst * (√↑p * √(∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ))

Rosenthal's polynomial-moment corollary for finite sums of centered independent real random variables.

theorem HCPolySupport.IndependentSums.centeredIndependent_sum_moment_le_RosenthalBound {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p : ℕ} {K : ℝ} (hp : 2 ≤ p) (hK_nonneg : 0 ≤ K) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hLp_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => |X i ω| ^ p) μ) (hXmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0) (hK : ∀ i ∈ s, (∫ (ω : Ω), |X i ω| ^ p ∂μ) ^ (1 / ↑p) ≤ K) :

(∫ (ω : Ω), |∑ i ∈ s, X i ω| ^ p ∂μ) ^ (1 / ↑p) ≤ 2 * ↑p * (↑s.card ^ (1 / ↑p) * K) + 4 * rosenthalBennettIntegralConst * (√↑p * (√↑s.card * K))

Uniform-K polynomial-moment Rosenthal corollary in the note-facing finite-sum form.

(∫ (ω : Ω), |centeredFinsetSum X μ s ω| ^ p ∂μ) ^ p⁻¹ ≤ 2 * p * (∑ i ∈ s, ∫ (ω : Ω), |X i ω| ^ p ∂μ) ^ p⁻¹ + 4 * rosenthalBennettIntegralConst * (√p * √(∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ))

Real-exponent polynomial-moment Rosenthal bound with the maximal term replaced by the sum of the individual L^p moments.

(∫ (ω : Ω), |∑ i ∈ s, X i ω| ^ p ∂μ) ^ p⁻¹ ≤ 2 * p * (∑ i ∈ s, ∫ (ω : Ω), |X i ω| ^ p ∂μ) ^ p⁻¹ + 4 * rosenthalBennettIntegralConst * (√p * √(∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ))

Real-exponent Rosenthal polynomial-moment corollary for centered independent finite sums.

theorem HCPolySupport.IndependentSums.integral_abs_finiteSum_rpow_rpow_inv_le_rosenthal_uniform_polynomial {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p K : ℝ} (hp : 2 ≤ p) (hK_nonneg : 0 ≤ K) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hLp_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => |X i ω| ^ p) μ) (hXmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0) (hK : ∀ i ∈ s, (∫ (ω : Ω), |X i ω| ^ p ∂μ) ^ p⁻¹ ≤ K) :

(∫ (ω : Ω), |∑ i ∈ s, X i ω| ^ p ∂μ) ^ p⁻¹ ≤ 2 * p * (↑s.card ^ p⁻¹ * K) + 4 * rosenthalBennettIntegralConst * (√p * (√↑s.card * K))

Uniform real-exponent polynomial-moment Rosenthal corollary in the finite-sum form.

Documentation