theorem
ProbabilityTheory.identDistrib_of_finiteRange
{Ω : Type u_8}
{Ω₀ : Type u_9}
{S : Type u_10}
[MeasurableSpace Ω]
[MeasurableSpace Ω₀]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[hS : Nonempty S]
{μ : MeasureTheory.Measure Ω}
{μ₀ : MeasureTheory.Measure Ω₀}
{X₀ : Ω₀ → S}
[FiniteRange X₀]
{X : Ω → S}
(hX : Measurable X)
(hi : IdentDistrib X₀ X μ₀ μ)
:
∃ (X' : Ω → S), Measurable X' ∧ FiniteRange X' ∧ X' =ᵐ[μ] X
If X has identical distribution to X₀, and X₀ has finite range, then X is almost everywhere equivalent to a random variable of finite range.
theorem
ProbabilityTheory.independent_copies_finiteRange
{Ω : Type u_1}
{Ω' : Type u_2}
{α : Type u_3}
{β : Type u_5}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{X : Ω → α}
{Y : Ω' → β}
(hX : Measurable X)
(hY : Measurable Y)
[FiniteRange X]
[FiniteRange Y]
[MeasurableSingletonClass α]
[MeasurableSingletonClass β]
(μ : MeasureTheory.Measure Ω)
(μ' : MeasureTheory.Measure Ω')
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure μ']
:
∃ (ν : MeasureTheory.Measure (α × β)) (X' : α × β → α) (Y' : α × β → β),
MeasureTheory.IsProbabilityMeasure ν ∧ Measurable X' ∧ Measurable Y' ∧ IndepFun X' Y' ν ∧ IdentDistrib X' X ν μ ∧ IdentDistrib Y' Y ν μ' ∧ FiniteRange X' ∧ FiniteRange Y'
A version of independent_copies that guarantees that the copies have FiniteRange if the original variables do.
theorem
ProbabilityTheory.independent_copies3_nondep_finiteRange
{α : Type u}
[mS : MeasurableSpace α]
[MeasurableSingletonClass α]
{Ω₁ : Type u_1}
{Ω₂ : Type u_2}
{Ω₃ : Type u_3}
[MeasurableSpace Ω₁]
[MeasurableSpace Ω₂]
[MeasurableSpace Ω₃]
{X₁ : Ω₁ → α}
{X₂ : Ω₂ → α}
{X₃ : Ω₃ → α}
(hX₁ : Measurable X₁)
(hX₂ : Measurable X₂)
(hX₃ : Measurable X₃)
[FiniteRange X₁]
[FiniteRange X₂]
[FiniteRange X₃]
(μ₁ : MeasureTheory.Measure Ω₁)
(μ₂ : MeasureTheory.Measure Ω₂)
(μ₃ : MeasureTheory.Measure Ω₃)
[hμ₁ : MeasureTheory.IsProbabilityMeasure μ₁]
[hμ₂ : MeasureTheory.IsProbabilityMeasure μ₂]
[hμ₃ : MeasureTheory.IsProbabilityMeasure μ₃]
:
∃ (A : Type (max u_1 u_2 u_3)) (x : MeasurableSpace A) (μA : MeasureTheory.Measure A) (X₁' : A → α) (X₂' : A → α) (X₃' :
A → α),
MeasureTheory.IsProbabilityMeasure μA ∧ iIndepFun ![X₁', X₂', X₃'] μA ∧ Measurable X₁' ∧ Measurable X₂' ∧ Measurable X₃' ∧ IdentDistrib X₁' X₁ μA μ₁ ∧ IdentDistrib X₂' X₂ μA μ₂ ∧ IdentDistrib X₃' X₃ μA μ₃ ∧ FiniteRange X₁' ∧ FiniteRange X₂' ∧ FiniteRange X₃'
A version of independent_copies3_nondep that guarantees that the copies have FiniteRange
if the original variables do.
theorem
ProbabilityTheory.independent_copies4_nondep_finiteRange
{α : Type u}
[mS : MeasurableSpace α]
[MeasurableSingletonClass α]
{Ω₁ : Type u_1}
{Ω₂ : Type u_2}
{Ω₃ : Type u_3}
{Ω₄ : Type u_4}
[MeasurableSpace Ω₁]
[MeasurableSpace Ω₂]
[MeasurableSpace Ω₃]
[MeasurableSpace Ω₄]
{X₁ : Ω₁ → α}
{X₂ : Ω₂ → α}
{X₃ : Ω₃ → α}
{X₄ : Ω₄ → α}
(hX₁ : Measurable X₁)
(hX₂ : Measurable X₂)
(hX₃ : Measurable X₃)
(hX₄ : Measurable X₄)
[FiniteRange X₁]
[FiniteRange X₂]
[FiniteRange X₃]
[FiniteRange X₄]
(μ₁ : MeasureTheory.Measure Ω₁)
(μ₂ : MeasureTheory.Measure Ω₂)
(μ₃ : MeasureTheory.Measure Ω₃)
(μ₄ : MeasureTheory.Measure Ω₄)
[hμ₁ : MeasureTheory.IsProbabilityMeasure μ₁]
[hμ₂ : MeasureTheory.IsProbabilityMeasure μ₂]
[hμ₃ : MeasureTheory.IsProbabilityMeasure μ₃]
[hμ₄ : MeasureTheory.IsProbabilityMeasure μ₄]
:
∃ (A : Type (max u_1 u_2 u_3 u_4)) (x : MeasurableSpace A) (μA : MeasureTheory.Measure A) (X₁' : A → α) (X₂' : A → α)
(X₃' : A → α) (X₄' : A → α),
MeasureTheory.IsProbabilityMeasure μA ∧ iIndepFun ![X₁', X₂', X₃', X₄'] μA ∧ Measurable X₁' ∧ Measurable X₂' ∧ Measurable X₃' ∧ Measurable X₄' ∧ IdentDistrib X₁' X₁ μA μ₁ ∧ IdentDistrib X₂' X₂ μA μ₂ ∧ IdentDistrib X₃' X₃ μA μ₃ ∧ IdentDistrib X₄' X₄ μA μ₄ ∧ FiniteRange X₁' ∧ FiniteRange X₂' ∧ FiniteRange X₃' ∧ FiniteRange X₄'
A version of independent_copies4_nondep that guarantees that the copies have FiniteRange
if the original variables do.