Identically distributed finite-range random variables #
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_copies'_finiteRange
{I : Type u}
[Finite I]
{α : I → Type u'}
[mS : (i : I) → MeasurableSpace (α i)]
[mS' : ∀ (i : I), MeasurableSingletonClass (α i)]
[mnon : ∀ (i : I), Nonempty (α i)]
{Ω : I → Type v}
[mΩ : (i : I) → MeasurableSpace (Ω i)]
(X : (i : I) → Ω i → α i)
(hX : ∀ (i : I), Measurable (X i))
(μ : (i : I) → MeasureTheory.Measure (Ω i))
[∀ (i : I), MeasureTheory.IsProbabilityMeasure (μ i)]
[∀ (i : I), FiniteRange (X i)]
:
∃ (A : Type (max u v)) (x : MeasurableSpace A) (μA : MeasureTheory.Measure A) (X' : (i : I) → A → α i),
MeasureTheory.IsProbabilityMeasure μA ∧ iIndepFun X' μA ∧ ∀ (i : I), Measurable (X' i) ∧ IdentDistrib (X' i) (X i) μA (μ i) ∧ FiniteRange (X' i)
A version of independent_copies' that guarantees that the copies have FiniteRange
if the original variables do.