Coarse-graining support: Support.Probability.IndependentSums.IndependentCopy #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.IndependentSums.identDistrib_comp_fst_comp_snd_prod
{Ω : Type u_1}
{𝓧 : Type u_3}
[MeasurableSpace Ω]
[MeasurableSpace 𝓧]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : Ω → 𝓧}
(hX : AEMeasurable X μ)
:
ProbabilityTheory.IdentDistrib (fun (ω : Ω × Ω) => X ω.1) (fun (ω : Ω × Ω) => X ω.2) (μ.prod μ) (μ.prod μ)
On the product probability space Ω × Ω, the two coordinate copies of a
random variable have the same law. This is the basic independent-copy package
used later in the symmetrization step of Rosenthal's inequality.
theorem
HCPolySupport.IndependentSums.indepFun_comp_fst_comp_snd_prod
{Ω : Type u_1}
{𝓧 : Type u_3}
{𝓨 : Type u_4}
[MeasurableSpace Ω]
[MeasurableSpace 𝓧]
[MeasurableSpace 𝓨]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : Ω → 𝓧}
{Y : Ω → 𝓨}
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
:
ProbabilityTheory.IndepFun (fun (ω : Ω × Ω) => X ω.1) (fun (ω : Ω × Ω) => Y ω.2) (μ.prod μ)
On the product probability space Ω × Ω, functions of the first
coordinate are independent from functions of the second coordinate.
theorem
HCPolySupport.IndependentSums.identDistrib_finset_sum_comp_fst_comp_snd_prod
{Ω : Type u_1}
{ι : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : ι → Ω → ℝ}
[MeasureTheory.IsProbabilityMeasure μ]
{s : Finset ι}
(hX : ∀ (i : ι), Measurable (X i))
:
ProbabilityTheory.IdentDistrib (fun (ω : Ω × Ω) => ∑ i ∈ s, X i ω.1) (fun (ω : Ω × Ω) => ∑ i ∈ s, X i ω.2) (μ.prod μ)
(μ.prod μ)
The finite-sum copy obtained from the first coordinate and the corresponding
copy obtained from the second coordinate are identically distributed on
Ω × Ω.
theorem
HCPolySupport.IndependentSums.indepFun_finset_sum_comp_fst_comp_snd_prod
{Ω : Type u_1}
{ι : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : ι → Ω → ℝ}
[MeasureTheory.IsProbabilityMeasure μ]
{s t : Finset ι}
(hX : ∀ (i : ι), Measurable (X i))
:
ProbabilityTheory.IndepFun (fun (ω : Ω × Ω) => ∑ i ∈ s, X i ω.1) (fun (ω : Ω × Ω) => ∑ i ∈ t, X i ω.2) (μ.prod μ)
Finite sums formed from the first and second coordinate copies are
independent on Ω × Ω.