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

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

theorem HCPolySupport.IndependentSums.iIndepFun_prodMk_comp_fst_comp_snd_prod {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [Finite ι] [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) : ProbabilityTheory.iIndepFun (fun (i : ι) (ω : Ω × Ω) => (X i ω.1, X i ω.2)) (μ.prod μ)

For a finite independent family, pairing the first and second coordinate copies on the product probability space preserves independence across the index set.

theorem HCPolySupport.IndependentSums.iIndepFun_sub_comp_fst_comp_snd_prod {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [Finite ι] [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) : ProbabilityTheory.iIndepFun (fun (i : ι) (ω : Ω × Ω) => X i ω.1 - X i ω.2) (μ.prod μ)

The symmetrized difference family on the product probability space is independent across the index set.

theorem HCPolySupport.IndependentSums.identDistrib_sub_comp_fst_comp_snd_prod_neg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (h_meas : Measurable X) : ProbabilityTheory.IdentDistrib (fun (ω : Ω × Ω) => X ω.1 - X ω.2) (fun (ω : Ω × Ω) => -(X ω.1 - X ω.2)) (μ.prod μ) (μ.prod μ)

A first-minus-second coordinate difference is symmetric on the product probability space.

theorem HCPolySupport.IndependentSums.sup'_abs_sub_pow_le {Ω : Type u_1} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p : ℕ} (ω : Ω × Ω) : (s.sup' hs fun (i : ι) => |X i ω.1 - X i ω.2|) ^ p ≤ 2 ^ (p - 1) * ((s.sup' hs fun (i : ι) => |X i ω.1|) ^ p + (s.sup' hs fun (i : ι) => |X i ω.2|) ^ p)

Pointwise L^p control of the finite maximum of the symmetrized family by the maxima of the two coordinate copies.

theorem HCPolySupport.IndependentSums.sup'_abs_sub_rpow_le {Ω : Type u_1} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p : ℝ} (hp : 1 ≤ p) (ω : Ω × Ω) : (s.sup' hs fun (i : ι) => |X i ω.1 - X i ω.2|) ^ p ≤ 2 ^ (p - 1) * ((s.sup' hs fun (i : ι) => |X i ω.1|) ^ p + (s.sup' hs fun (i : ι) => |X i ω.2|) ^ p)

Real-exponent pointwise L^p control of the finite maximum of the symmetrized family by the maxima of the two coordinate copies.

theorem HCPolySupport.IndependentSums.integral_sup'_abs_sub_pow_le_two_pow_mul_integral_sup'_abs_pow {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p : ℕ} (hp : 1 ≤ p) (h_meas : ∀ (i : ι), Measurable (X i)) (hmax_int : MeasureTheory.Integrable (fun (ω : Ω) => (s.sup' hs fun (i : ι) => |X i ω|) ^ p) μ) : ∫ (ω : Ω × Ω), (s.sup' hs fun (i : ι) => |X i ω.1 - X i ω.2|) ^ p ∂μ.prod μ ≤ 2 ^ p * ∫ (ω : Ω), (s.sup' hs fun (i : ι) => |X i ω|) ^ p ∂μ

Product-space L^p control of the finite maximum of the symmetrized family by the original maximum.

theorem HCPolySupport.IndependentSums.integrable_pow_two_sub_comp_fst_comp_snd {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (h_meas : Measurable X) (h_sq_int : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 2) μ) : MeasureTheory.Integrable (fun (ω : Ω × Ω) => (X ω.1 - X ω.2) ^ 2) (μ.prod μ)

Square-integrability of the symmetrized copy follows from square integrability of the original variable.

theorem HCPolySupport.IndependentSums.moment_sub_comp_fst_comp_snd_le_four_mul {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (h_meas : Measurable X) (h_sq_int : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 2) μ) : ProbabilityTheory.moment (fun (ω : Ω × Ω) => X ω.1 - X ω.2) 2 (μ.prod μ) ≤ 4 * ProbabilityTheory.moment X 2 μ

The second moment of the symmetrized copy is controlled by the original second moment.

theorem HCPolySupport.IndependentSums.integrable_sup'_abs_sub_pow_of_integrable_sup'_abs_pow {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p : ℕ} (h_meas : ∀ (i : ι), Measurable (X i)) (hmax_int : MeasureTheory.Integrable (fun (ω : Ω) => (s.sup' hs fun (i : ι) => |X i ω|) ^ p) μ) : MeasureTheory.Integrable (fun (ω : Ω × Ω) => (s.sup' hs fun (i : ι) => |X i ω.1 - X i ω.2|) ^ p) (μ.prod μ)

Integrability of the symmetrized finite maximum follows from integrability of the original finite maximum.

theorem HCPolySupport.IndependentSums.integrable_sup'_abs_sub_rpow_of_integrable_sup'_abs_rpow {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p : ℝ} (hp : 1 ≤ p) (h_meas : ∀ (i : ι), Measurable (X i)) (hmax_int : MeasureTheory.Integrable (fun (ω : Ω) => (s.sup' hs fun (i : ι) => |X i ω|) ^ p) μ) : MeasureTheory.Integrable (fun (ω : Ω × Ω) => (s.sup' hs fun (i : ι) => |X i ω.1 - X i ω.2|) ^ p) (μ.prod μ)

Real-exponent integrability of the symmetrized finite maximum follows from integrability of the original finite maximum.

theorem HCPolySupport.IndependentSums.integral_sup'_abs_sub_rpow_le_two_rpow_mul_integral_sup'_abs_rpow {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {s : Finset ι} (hs : s.Nonempty) {p : ℝ} (hp : 1 ≤ p) (h_meas : ∀ (i : ι), Measurable (X i)) (hmax_int : MeasureTheory.Integrable (fun (ω : Ω) => (s.sup' hs fun (i : ι) => |X i ω|) ^ p) μ) : ∫ (ω : Ω × Ω), (s.sup' hs fun (i : ι) => |X i ω.1 - X i ω.2|) ^ p ∂μ.prod μ ≤ 2 ^ p * ∫ (ω : Ω), (s.sup' hs fun (i : ι) => |X i ω|) ^ p ∂μ

Product-space real-exponent L^p control of the finite maximum of the symmetrized family by the original maximum.

theorem HCPolySupport.IndependentSums.sup'_univ_subtype_eq_sup' {ι : Type u_2} {α : Type u_3} [SemilatticeSup α] {s : Finset ι} (hs : s.Nonempty) (hs_univ : Finset.univ.Nonempty) (f : ι → α) : (Finset.univ.sup' hs_univ fun (i : ↥s) => f ↑i) = s.sup' hs f

Computing sup' over the subtype attached to a nonempty finset agrees with computing sup' over the original finset.

theorem HCPolySupport.IndependentSums.sum_univ_subtype_eq_symmetrizedFinsetSum {Ω : Type u_1} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} (ω : Ω × Ω) : ∑ i : ↥s, (X (↑i) ω.1 - X (↑i) ω.2) = symmetrizedFinsetSum X s ω

The finite symmetrized sum can be rewritten as a sum over the subtype indexed by the ambient finite set.