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

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

theorem HCPolySupport.IndependentSums.integral_abs_symmetrizedFinsetSum_pow_le_rosenthal {Ω : 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) μ) (hmax_int : MeasureTheory.Integrable (fun (ω : Ω) => (s.sup' hs fun (i : ι) => |X i ω|) ^ p) μ) : ∫ (ω : Ω × Ω), |symmetrizedFinsetSum X s ω| ^ p ∂μ.prod μ ≤ ↑p ^ p * 2 ^ p * ∫ (ω : Ω), (s.sup' hs fun (i : ι) => |X i ω|) ^ p ∂μ + 2 * (2 * rosenthalBennettIntegralConst * (√↑p * √(∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ))) ^ p

Rosenthal bound for the symmetrized difference sum on the product probability space.

theorem HCPolySupport.IndependentSums.integrable_abs_symmetrizedFinsetSum_pow_of_rosenthal {Ω : 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) μ) (hmax_int : MeasureTheory.Integrable (fun (ω : Ω) => (s.sup' hs fun (i : ι) => |X i ω|) ^ p) μ) : MeasureTheory.Integrable (fun (ω : Ω × Ω) => |symmetrizedFinsetSum X s ω| ^ p) (μ.prod μ)

Integrability of the symmetrized sum under the Rosenthal assumptions.

theorem HCPolySupport.IndependentSums.integral_abs_centeredFinsetSum_pow_le_rosenthal {Ω : 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_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ) (h_sq_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) (hmax_int : MeasureTheory.Integrable (fun (ω : Ω) => (s.sup' hs fun (i : ι) => |X i ω|) ^ p) μ) : ∫ (ω : Ω), |centeredFinsetSum X μ s ω| ^ p ∂μ ≤ ↑p ^ p * 2 ^ p * ∫ (ω : Ω), (s.sup' hs fun (i : ι) => |X i ω|) ^ p ∂μ + 2 * (2 * rosenthalBennettIntegralConst * (√↑p * √(∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ))) ^ p

Rosenthal bound for the centered finite sum on the original probability space.

theorem HCPolySupport.IndependentSums.integral_abs_centeredFinsetSum_pow_rpow_inv_le_rosenthal {Ω : 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_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ) (h_sq_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) (hmax_int : MeasureTheory.Integrable (fun (ω : Ω) => (s.sup' hs fun (i : ι) => |X i ω|) ^ p) μ) : (∫ (ω : Ω), |centeredFinsetSum X μ s ω| ^ p ∂μ) ^ (1 / ↑p) ≤ 2 * ↑p * (∫ (ω : Ω), (s.sup' hs fun (i : ι) => |X i ω|) ^ p ∂μ) ^ (1 / ↑p) + 4 * rosenthalBennettIntegralConst * (√↑p * √(∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ))

Note-facing L^p-scale form of Rosenthal's inequality: taking the 1 / p power of the moment estimate yields the standard sum of the maximal L^p term and the square-function term.

theorem HCPolySupport.IndependentSums.integral_abs_symmetrizedFinsetSum_rpow_le_rosenthal {Ω : 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) μ) (hmax_int : MeasureTheory.Integrable (fun (ω : Ω) => (s.sup' hs fun (i : ι) => |X i ω|) ^ p) μ) : ∫ (ω : Ω × Ω), |symmetrizedFinsetSum X s ω| ^ p ∂μ.prod μ ≤ p ^ p * 2 ^ p * ∫ (ω : Ω), (s.sup' hs fun (i : ι) => |X i ω|) ^ p ∂μ + 2 * (2 * rosenthalBennettIntegralConst * (√p * √(∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ))) ^ p

Real-exponent Rosenthal bound for the symmetrized difference sum on the product probability space.

theorem HCPolySupport.IndependentSums.integrable_abs_symmetrizedFinsetSum_rpow_of_rosenthal {Ω : 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) μ) (hmax_int : MeasureTheory.Integrable (fun (ω : Ω) => (s.sup' hs fun (i : ι) => |X i ω|) ^ p) μ) : MeasureTheory.Integrable (fun (ω : Ω × Ω) => |symmetrizedFinsetSum X s ω| ^ p) (μ.prod μ)

Integrability of the symmetrized real-exponent sum under the Rosenthal assumptions.

theorem HCPolySupport.IndependentSums.integral_abs_centeredFinsetSum_rpow_le_rosenthal {Ω : 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_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ) (h_sq_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) (hmax_int : MeasureTheory.Integrable (fun (ω : Ω) => (s.sup' hs fun (i : ι) => |X i ω|) ^ p) μ) : ∫ (ω : Ω), |centeredFinsetSum X μ s ω| ^ p ∂μ ≤ p ^ p * 2 ^ p * ∫ (ω : Ω), (s.sup' hs fun (i : ι) => |X i ω|) ^ p ∂μ + 2 * (2 * rosenthalBennettIntegralConst * (√p * √(∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ))) ^ p

Real-exponent Rosenthal bound for the centered finite sum on the original probability space.

theorem HCPolySupport.IndependentSums.integral_abs_centeredFinsetSum_rpow_rpow_inv_le_rosenthal {Ω : 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_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ) (h_sq_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) (hmax_int : MeasureTheory.Integrable (fun (ω : Ω) => (s.sup' hs fun (i : ι) => |X i ω|) ^ p) μ) : (∫ (ω : Ω), |centeredFinsetSum X μ s ω| ^ p ∂μ) ^ (1 / p) ≤ 2 * p * (∫ (ω : Ω), (s.sup' hs fun (i : ι) => |X i ω|) ^ p ∂μ) ^ (1 / p) + 4 * rosenthalBennettIntegralConst * (√p * √(∑ i ∈ s, ProbabilityTheory.moment (X i) 2 μ))

Real-exponent L^p-scale Rosenthal bound for the centered finite sum.