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

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

theorem HCPolySupport.IndependentSums.integral_abs_centeredFinsetSum_pow_le_integral_abs_symmetrizedFinsetSum_pow {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {p : ℕ} (hp : 1 ≤ p) (hX_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ) (hsymm_int : MeasureTheory.Integrable (fun (ω : Ω × Ω) => |symmetrizedFinsetSum X s ω| ^ p) (μ.prod μ)) : ∫ (ω : Ω), |centeredFinsetSum X μ s ω| ^ p ∂μ ≤ ∫ (ω : Ω × Ω), |symmetrizedFinsetSum X s ω| ^ p ∂μ.prod μ

First symmetrization step for Rosenthal's inequality: the absolute L^p norm of the centered finite sum is bounded by the corresponding L^p norm of the symmetrized difference sum on the product probability space.

theorem HCPolySupport.IndependentSums.abs_symmetrizedFinsetSum_pow_le {Ω : Type u_1} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} {p : ℕ} (ω : Ω × Ω) : |symmetrizedFinsetSum X s ω| ^ p ≤ 2 ^ (p - 1) * (|∑ i ∈ s, X i ω.1| ^ p + |∑ i ∈ s, X i ω.2| ^ p)

Pointwise L^p control of the symmetrized finite sum by the two coordinate copies of the original finite sum.

theorem HCPolySupport.IndependentSums.integrable_abs_symmetrizedFinsetSum_pow_of_integrable_abs_finsetSum_pow {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {p : ℕ} (hX_meas : ∀ i ∈ s, Measurable (X i)) (hsum_int : MeasureTheory.Integrable (fun (ω : Ω) => |∑ i ∈ s, X i ω| ^ p) μ) : MeasureTheory.Integrable (fun (ω : Ω × Ω) => |symmetrizedFinsetSum X s ω| ^ p) (μ.prod μ)

Integrability of the symmetrized p-moment follows from integrability of the original finite-sum p-moment.

theorem HCPolySupport.IndependentSums.integral_abs_symmetrizedFinsetSum_pow_le_two_pow_mul_integral_abs_finsetSum_pow {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {p : ℕ} (hp : 1 ≤ p) (hX_meas : ∀ i ∈ s, Measurable (X i)) (hsum_int : MeasureTheory.Integrable (fun (ω : Ω) => |∑ i ∈ s, X i ω| ^ p) μ) : ∫ (ω : Ω × Ω), |symmetrizedFinsetSum X s ω| ^ p ∂μ.prod μ ≤ 2 ^ p * ∫ (ω : Ω), |∑ i ∈ s, X i ω| ^ p ∂μ

Product-space L^p control of the symmetrized finite sum by the original finite sum. This is the note-facing symmetrization estimate with the standard 2^p factor.

theorem HCPolySupport.IndependentSums.integral_abs_centeredFinsetSum_pow_le_two_pow_mul_integral_abs_finsetSum_pow {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {p : ℕ} (hp : 1 ≤ p) (hX_meas : ∀ i ∈ s, Measurable (X i)) (hX_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ) (hsum_int : MeasureTheory.Integrable (fun (ω : Ω) => |∑ i ∈ s, X i ω| ^ p) μ) : ∫ (ω : Ω), |centeredFinsetSum X μ s ω| ^ p ∂μ ≤ 2 ^ p * ∫ (ω : Ω), |∑ i ∈ s, X i ω| ^ p ∂μ

Moment symmetrization inequality for the centered finite sum.

theorem HCPolySupport.IndependentSums.integral_abs_centeredFinsetSum_rpow_le_integral_abs_symmetrizedFinsetSum_rpow {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {p : ℝ} (hp : 1 ≤ p) (hX_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ) (hsymm_int : MeasureTheory.Integrable (fun (ω : Ω × Ω) => |symmetrizedFinsetSum X s ω| ^ p) (μ.prod μ)) : ∫ (ω : Ω), |centeredFinsetSum X μ s ω| ^ p ∂μ ≤ ∫ (ω : Ω × Ω), |symmetrizedFinsetSum X s ω| ^ p ∂μ.prod μ

First symmetrization step for real L^p exponents.

theorem HCPolySupport.IndependentSums.abs_symmetrizedFinsetSum_rpow_le {Ω : Type u_1} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} {p : ℝ} (hp : 1 ≤ p) (ω : Ω × Ω) : |symmetrizedFinsetSum X s ω| ^ p ≤ 2 ^ (p - 1) * (|∑ i ∈ s, X i ω.1| ^ p + |∑ i ∈ s, X i ω.2| ^ p)

Pointwise real-L^p control of the symmetrized finite sum by the two coordinate copies of the original finite sum.

theorem HCPolySupport.IndependentSums.integrable_abs_symmetrizedFinsetSum_rpow_of_integrable_abs_finsetSum_rpow {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {p : ℝ} (hp : 1 ≤ p) (hX_meas : ∀ i ∈ s, Measurable (X i)) (hsum_int : MeasureTheory.Integrable (fun (ω : Ω) => |∑ i ∈ s, X i ω| ^ p) μ) : MeasureTheory.Integrable (fun (ω : Ω × Ω) => |symmetrizedFinsetSum X s ω| ^ p) (μ.prod μ)

Integrability of the symmetrized real p-moment follows from integrability of the original finite-sum real p-moment.

theorem HCPolySupport.IndependentSums.integral_abs_symmetrizedFinsetSum_rpow_le_two_rpow_mul_integral_abs_finsetSum_rpow {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {p : ℝ} (hp : 1 ≤ p) (hX_meas : ∀ i ∈ s, Measurable (X i)) (hsum_int : MeasureTheory.Integrable (fun (ω : Ω) => |∑ i ∈ s, X i ω| ^ p) μ) : ∫ (ω : Ω × Ω), |symmetrizedFinsetSum X s ω| ^ p ∂μ.prod μ ≤ 2 ^ p * ∫ (ω : Ω), |∑ i ∈ s, X i ω| ^ p ∂μ

Product-space real-L^p control of the symmetrized finite sum by the original finite sum.

theorem HCPolySupport.IndependentSums.integral_abs_centeredFinsetSum_rpow_le_two_rpow_mul_integral_abs_finsetSum_rpow {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} {p : ℝ} (hp : 1 ≤ p) (hX_meas : ∀ i ∈ s, Measurable (X i)) (hX_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) μ) (hsum_int : MeasureTheory.Integrable (fun (ω : Ω) => |∑ i ∈ s, X i ω| ^ p) μ) : ∫ (ω : Ω), |centeredFinsetSum X μ s ω| ^ p ∂μ ≤ 2 ^ p * ∫ (ω : Ω), |∑ i ∈ s, X i ω| ^ p ∂μ

Real-exponent moment symmetrization inequality for the centered finite sum.