theorem
ProbabilityTheory.identDistrib_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(f : α → γ)
(g : β → γ)
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
(ν : autoParam (MeasureTheory.Measure β) _auto✝)
:
ProbabilityTheory.IdentDistrib f g μ ν ↔ AEMeasurable f μ ∧ AEMeasurable g ν ∧ MeasureTheory.Measure.map f μ = MeasureTheory.Measure.map g ν
theorem
ProbabilityTheory.identDistrib_id_left
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{X : α → β}
(hX : AEMeasurable X μ)
:
ProbabilityTheory.IdentDistrib id X (MeasureTheory.Measure.map X μ) μ
theorem
ProbabilityTheory.identDistrib_id_right
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{X : α → β}
(hX : AEMeasurable X μ)
:
ProbabilityTheory.IdentDistrib X id μ (MeasureTheory.Measure.map X μ)
@[simp]
theorem
ProbabilityTheory.identDistrib_id
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
:
ProbabilityTheory.IdentDistrib id id μ ν ↔ μ = ν
theorem
ProbabilityTheory.IdentDistrib.fst_id
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.IsProbabilityMeasure ν]
:
ProbabilityTheory.IdentDistrib Prod.fst id (μ.prod ν) μ
The first projection in a product space with measure μ.prod ν is distributed like μ.
theorem
ProbabilityTheory.IdentDistrib.snd_id
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
:
ProbabilityTheory.IdentDistrib Prod.snd id (μ.prod ν) ν
The second projection in a product space with measure μ.prod ν is distributed like ν.
theorem
ProbabilityTheory.IdentDistrib.cond
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{f' : α → γ}
{g : β → γ}
{g' : β → γ}
{s : Set γ}
(hs : MeasurableSet s)
(hf' : Measurable f')
(hg' : Measurable g')
(hfg : ProbabilityTheory.IdentDistrib (fun (a : α) => (f a, f' a)) (fun (b : β) => (g b, g' b)) μ ν)
:
ProbabilityTheory.IdentDistrib f g (ProbabilityTheory.cond μ (f' ⁻¹' s)) (ProbabilityTheory.cond ν (g' ⁻¹' s))
theorem
ProbabilityTheory.identDistrib_comp_left
{α : Type u_1}
{γ : Type u_3}
{δ : Type u_4}
[MeasurableSpace α]
[MeasurableSpace γ]
[MeasurableSpace δ]
{μ : MeasureTheory.Measure α}
{f : α → γ}
{i : δ → α}
(hi : MeasurableEmbedding i)
(hi' : ∀ᵐ (a : α) ∂μ, a ∈ Set.range i)
(hf : Measurable f)
:
ProbabilityTheory.IdentDistrib (f ∘ i) f (MeasureTheory.Measure.comap i μ) μ
A function is identically distributed to itself composed with a measurable embedding of conull range.
theorem
ProbabilityTheory.identDistrib_comp_right
{α : Type u_1}
{γ : Type u_3}
{δ : Type u_4}
[MeasurableSpace α]
[MeasurableSpace γ]
[MeasurableSpace δ]
{μ : MeasureTheory.Measure α}
{f : α → γ}
{i : δ → α}
(hi : MeasurableEmbedding i)
(hi' : ∀ᵐ (a : α) ∂μ, a ∈ Set.range i)
(hf : Measurable f)
:
ProbabilityTheory.IdentDistrib f (f ∘ i) μ (MeasureTheory.Measure.comap i μ)
A function is identically distributed to itself composed with a measurable embedding of conull range.
theorem
ProbabilityTheory.IdentDistrib.comp_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[MeasurableSpace δ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
{i : δ → α}
(hi : MeasurableEmbedding i)
(hi' : ∀ᵐ (a : α) ∂μ, a ∈ Set.range i)
(hf : Measurable f)
(hfg : ProbabilityTheory.IdentDistrib f g μ ν)
:
ProbabilityTheory.IdentDistrib (f ∘ i) g (MeasureTheory.Measure.comap i μ) ν
Composing identically distributed functions with a measurable embedding of conull range gives identically distributed functions.
theorem
ProbabilityTheory.IdentDistrib.comp_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[MeasurableSpace δ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
{i : δ → β}
(hi : MeasurableEmbedding i)
(hi' : ∀ᵐ (a : β) ∂ν, a ∈ Set.range i)
(hg : Measurable g)
(hfg : ProbabilityTheory.IdentDistrib f g μ ν)
:
ProbabilityTheory.IdentDistrib f (g ∘ i) μ (MeasureTheory.Measure.comap i ν)
Composing identically distributed functions with a measurable embedding of conull range gives identically distributed functions.
theorem
ProbabilityTheory.IdentDistrib.prod_mk
{Ω : Type u_5}
{Ω' : Type u_6}
{β : Type u_9}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure Ω}
{ν : MeasureTheory.Measure Ω'}
{f : Ω → β}
{g : Ω → β}
{f' : Ω' → β}
{g' : Ω' → β}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hff' : ProbabilityTheory.IdentDistrib f f' μ ν)
(hgg' : ProbabilityTheory.IdentDistrib g g' μ ν)
(h : ProbabilityTheory.IndepFun f g μ)
(h' : ProbabilityTheory.IndepFun f' g' ν)
:
ProbabilityTheory.IdentDistrib (fun (x : Ω) => (f x, g x)) (fun (x : Ω') => (f' x, g' x)) μ ν
theorem
ProbabilityTheory.IdentDistrib.add
{Ω : Type u_5}
{Ω' : Type u_6}
{β : Type u_9}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure Ω}
{ν : MeasureTheory.Measure Ω'}
{f : Ω → β}
{g : Ω → β}
{f' : Ω' → β}
{g' : Ω' → β}
[Add β]
[MeasurableAdd₂ β]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hff' : ProbabilityTheory.IdentDistrib f f' μ ν)
(hgg' : ProbabilityTheory.IdentDistrib g g' μ ν)
(h : ProbabilityTheory.IndepFun f g μ)
(h' : ProbabilityTheory.IndepFun f' g' ν)
:
ProbabilityTheory.IdentDistrib (f + g) (f' + g') μ ν
theorem
ProbabilityTheory.IdentDistrib.mul
{Ω : Type u_5}
{Ω' : Type u_6}
{β : Type u_9}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure Ω}
{ν : MeasureTheory.Measure Ω'}
{f : Ω → β}
{g : Ω → β}
{f' : Ω' → β}
{g' : Ω' → β}
[Mul β]
[MeasurableMul₂ β]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hff' : ProbabilityTheory.IdentDistrib f f' μ ν)
(hgg' : ProbabilityTheory.IdentDistrib g g' μ ν)
(h : ProbabilityTheory.IndepFun f g μ)
(h' : ProbabilityTheory.IndepFun f' g' ν)
:
ProbabilityTheory.IdentDistrib (f * g) (f' * g') μ ν
theorem
ProbabilityTheory.identDistrib_map
{Ω : Type u_5}
{α : Type u_7}
{β : Type u_9}
{mΩ : MeasurableSpace Ω}
[MeasurableSpace α]
[MeasurableSpace β]
{X : Ω → α}
(hX : Measurable X)
{f : α → β}
(hf : Measurable f)
(μ : MeasureTheory.Measure Ω)
:
ProbabilityTheory.IdentDistrib f (f ∘ X) (MeasureTheory.Measure.map X μ) μ
A random variable is identically distributed to its pullbacks.
theorem
ProbabilityTheory.identDistrib_ulift_self
{Ω : Type u_5}
{α : Type u_7}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasurableSpace α]
{X : Ω → α}
(hX : Measurable X)
:
ProbabilityTheory.IdentDistrib X (X ∘ ULift.down) μ (MeasureTheory.Measure.comap ULift.down μ)
theorem
ProbabilityTheory.identDistrib_of_sum
{Ω : Type u_5}
{Ω' : Type u_6}
{α : Type u_7}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
[MeasurableSpace α]
{T : Type u_11}
{X : Ω → α}
{Y : Ω' → α}
{μ : T → MeasureTheory.Measure Ω}
{μ' : T → MeasureTheory.Measure Ω'}
{w : T → ENNReal}
(s : Finset T)
(hX : Measurable X)
(hY : Measurable Y)
(h_ident : ∀ (y : T), w y ≠ 0 → ProbabilityTheory.IdentDistrib X Y (μ y) (μ' y))
:
ProbabilityTheory.IdentDistrib X Y (s.sum fun (y : T) => w y • μ y) (s.sum fun (y : T) => w y • μ' y)
To show identical distribution of two random variables on a mixture of probability measures, it suffices to do so on each non-trivial component.
theorem
ProbabilityTheory.identDistrib_comp_fst
{Ω : Type u_5}
{Ω' : Type u_6}
{α : Type u_7}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
[MeasurableSpace α]
{X : Ω → α}
(hX : Measurable X)
(μ : MeasureTheory.Measure Ω)
(μ' : MeasureTheory.Measure Ω')
[MeasureTheory.IsProbabilityMeasure μ']
:
ProbabilityTheory.IdentDistrib (X ∘ Prod.fst) X (μ.prod μ') μ
A random variable is identically distributed to its lift to a product space (in the first factor).
theorem
ProbabilityTheory.identDistrib_comp_snd
{Ω : Type u_5}
{Ω' : Type u_6}
{α : Type u_7}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
[MeasurableSpace α]
{X : Ω → α}
(hX : Measurable X)
(μ : MeasureTheory.Measure Ω)
(μ' : MeasureTheory.Measure Ω')
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.IsProbabilityMeasure μ']
:
ProbabilityTheory.IdentDistrib (X ∘ Prod.snd) X (μ'.prod μ) μ
A random variable is identically distributed to its lift to a product space (in the second factor).
theorem
ProbabilityTheory.independent_copies
{Ω : Type u_5}
{Ω' : Type u_6}
{α : Type u_7}
{β : Type u_9}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
[MeasurableSpace α]
[MeasurableSpace β]
{X : Ω → α}
{Y : Ω' → β}
(hX : Measurable X)
(hY : Measurable Y)
(μ : MeasureTheory.Measure Ω)
(μ' : MeasureTheory.Measure Ω')
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure μ']
:
∃ (ν : MeasureTheory.Measure (α × β)) (X' : α × β → α) (Y' : α × β → β),
MeasureTheory.IsProbabilityMeasure ν ∧ Measurable X' ∧ Measurable Y' ∧ ProbabilityTheory.IndepFun X' Y' ν ∧ ProbabilityTheory.IdentDistrib X' X ν μ ∧ ProbabilityTheory.IdentDistrib Y' Y ν μ'
For X, Y random variables, one can find independent copies X', Y' of X, Y.
theorem
ProbabilityTheory.independent_copies_two
{α : Type u_7}
{β : Type u_9}
[MeasurableSpace α]
[MeasurableSpace β]
{Ω : Type u}
{Ω' : Type v}
[MeasureTheory.MeasureSpace Ω]
[MeasureTheory.MeasureSpace Ω']
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
{X : Ω → α}
{Y : Ω' → β}
(hX : Measurable X)
(hY : Measurable Y)
:
∃ (Ω'' : Type (max u v)) (m'' : MeasureTheory.MeasureSpace Ω'') (X' : Ω'' → α) (Y' : Ω'' → β),
MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧ Measurable X' ∧ Measurable Y' ∧ ProbabilityTheory.IndepFun X' Y' MeasureTheory.volume ∧ ProbabilityTheory.IdentDistrib X' X MeasureTheory.volume MeasureTheory.volume ∧ ProbabilityTheory.IdentDistrib Y' Y MeasureTheory.volume MeasureTheory.volume
For X, Y random variables, one can find independent copies X', Y' of X, Y. Version
formulated in spaces with a canonical measures.
theorem
ProbabilityTheory.independent_copies'
{I : Type u}
[Fintype I]
{α : I → Type u'}
[mS : (i : I) → MeasurableSpace (α 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)]
:
∃ (A : Type (max u v)) (mA : MeasurableSpace A) (μA : MeasureTheory.Measure A) (X' : (i : I) → A → α i),
MeasureTheory.IsProbabilityMeasure μA ∧ ProbabilityTheory.iIndepFun mS X' μA ∧ ∀ (i : I), Measurable (X' i) ∧ ProbabilityTheory.IdentDistrib (X' i) (X i) μA (μ i)
Let Xᵢ : Ωᵢ → Sᵢ be random variables for i = 1,...,k.
Then there exist jointly independent random variables Xᵢ' : Ω' → Sᵢ for i=1,...,k
such that each Xᵢ' is a copy of Xᵢ.
theorem
ProbabilityTheory.independent_copies3_nondep
{α : Type u}
[mS : MeasurableSpace α]
{Ω₁ : Type u_1}
{Ω₂ : Type u_2}
{Ω₃ : Type u_3}
[MeasurableSpace Ω₁]
[MeasurableSpace Ω₂]
[MeasurableSpace Ω₃]
{X₁ : Ω₁ → α}
{X₂ : Ω₂ → α}
{X₃ : Ω₃ → α}
(hX₁ : Measurable X₁)
(hX₂ : Measurable X₂)
(hX₃ : Measurable 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)) (mA : MeasurableSpace A) (μA : MeasureTheory.Measure A) (X₁' : A → α) (X₂' : A → α) (X₃'
: A → α),
MeasureTheory.IsProbabilityMeasure μA ∧ ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => mS) ![X₁', X₂', X₃'] μA ∧ Measurable X₁' ∧ Measurable X₂' ∧ Measurable X₃' ∧ ProbabilityTheory.IdentDistrib X₁' X₁ μA μ₁ ∧ ProbabilityTheory.IdentDistrib X₂' X₂ μA μ₂ ∧ ProbabilityTheory.IdentDistrib X₃' X₃ μA μ₃
A version with exactly 3 random variables that have the same codomain. It's unfortunately incredibly painful to prove this from the general case.
theorem
ProbabilityTheory.independent_copies4_nondep
{α : Type u}
[mS : MeasurableSpace α]
{Ω₁ : Type u_1}
{Ω₂ : Type u_2}
{Ω₃ : Type u_3}
{Ω₄ : Type u_4}
[mΩ₁ : MeasurableSpace Ω₁]
[mΩ₂ : MeasurableSpace Ω₂]
[mΩ₃ : MeasurableSpace Ω₃]
[mΩ₄ : MeasurableSpace Ω₄]
{X₁ : Ω₁ → α}
{X₂ : Ω₂ → α}
{X₃ : Ω₃ → α}
{X₄ : Ω₄ → α}
(hX₁ : Measurable X₁)
(hX₂ : Measurable X₂)
(hX₃ : Measurable X₃)
(hX₄ : Measurable 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)) (mA : MeasurableSpace A) (μA : MeasureTheory.Measure A) (X₁' : A → α) (X₂' : A → α)
(X₃' : A → α) (X₄' : A → α),
MeasureTheory.IsProbabilityMeasure μA ∧ ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => mS) ![X₁', X₂', X₃', X₄'] μA ∧ Measurable X₁' ∧ Measurable X₂' ∧ Measurable X₃' ∧ Measurable X₄' ∧ ProbabilityTheory.IdentDistrib X₁' X₁ μA μ₁ ∧ ProbabilityTheory.IdentDistrib X₂' X₂ μA μ₂ ∧ ProbabilityTheory.IdentDistrib X₃' X₃ μA μ₃ ∧ ProbabilityTheory.IdentDistrib X₄' X₄ μA μ₄
A version with exactly 4 random variables that have the same codomain. It's unfortunately incredibly painful to prove this from the general case.
theorem
ProbabilityTheory.identDistrib_of_finiteRange
{Ω : Type u_11}
{Ω₀ : Type u_12}
{S : Type u_13}
[MeasurableSpace Ω]
[MeasurableSpace Ω₀]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[hS : Nonempty S]
{μ : MeasureTheory.Measure Ω}
{μ₀ : MeasureTheory.Measure Ω₀}
{X₀ : Ω₀ → S}
[FiniteRange X₀]
{X : Ω → S}
(hX : Measurable X)
(hi : ProbabilityTheory.IdentDistrib X₀ X μ₀ μ)
:
∃ (X' : Ω → S), Measurable X' ∧ FiniteRange X' ∧ μ.ae.EventuallyEq 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_5}
{Ω' : Type u_6}
{α : Type u_7}
{β : Type u_9}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
[MeasurableSpace α]
[MeasurableSpace β]
{X : Ω → α}
{Y : Ω' → β}
(hX : Measurable X)
(hY : Measurable Y)
[FiniteRange X]
[FiniteRange Y]
[MeasurableSingletonClass α]
[Nonempty α]
[MeasurableSingletonClass β]
[Nonempty β]
(μ : MeasureTheory.Measure Ω)
(μ' : MeasureTheory.Measure Ω')
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure μ']
:
∃ (ν : MeasureTheory.Measure (α × β)) (X' : α × β → α) (Y' : α × β → β),
MeasureTheory.IsProbabilityMeasure ν ∧ Measurable X' ∧ Measurable Y' ∧ ProbabilityTheory.IndepFun X' Y' ν ∧ ProbabilityTheory.IdentDistrib X' X ν μ ∧ ProbabilityTheory.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 α]
[Nonempty α]
{Ω₁ : 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)) (mA : MeasurableSpace A) (μA : MeasureTheory.Measure A) (X₁' : A → α) (X₂' : A → α) (X₃'
: A → α),
MeasureTheory.IsProbabilityMeasure μA ∧ ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => mS) ![X₁', X₂', X₃'] μA ∧ Measurable X₁' ∧ Measurable X₂' ∧ Measurable X₃' ∧ ProbabilityTheory.IdentDistrib X₁' X₁ μA μ₁ ∧ ProbabilityTheory.IdentDistrib X₂' X₂ μA μ₂ ∧ ProbabilityTheory.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 α]
[Nonempty α]
{Ω₁ : 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)) (mA : MeasurableSpace A) (μA : MeasureTheory.Measure A) (X₁' : A → α) (X₂' : A → α)
(X₃' : A → α) (X₄' : A → α),
MeasureTheory.IsProbabilityMeasure μA ∧ ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => mS) ![X₁', X₂', X₃', X₄'] μA ∧ Measurable X₁' ∧ Measurable X₂' ∧ Measurable X₃' ∧ Measurable X₄' ∧ ProbabilityTheory.IdentDistrib X₁' X₁ μA μ₁ ∧ ProbabilityTheory.IdentDistrib X₂' X₂ μA μ₂ ∧ ProbabilityTheory.IdentDistrib X₃' X₃ μA μ₃ ∧ ProbabilityTheory.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.