theorem
ProbabilityTheory.identDistrib_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(f : α → γ)
(g : β → γ)
(μ : MeasureTheory.Measure α := by volume_tac)
(ν : MeasureTheory.Measure β := by volume_tac)
:
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 μ)
:
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 μ)
:
IdentDistrib X id μ (MeasureTheory.Measure.map X μ)
@[simp]
theorem
ProbabilityTheory.identDistrib_id
{α : Type u_1}
[MeasurableSpace α]
{μ ν : MeasureTheory.Measure α}
:
theorem
ProbabilityTheory.IdentDistrib.fst_id
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.IsProbabilityMeasure ν]
:
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 ν]
:
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 : IdentDistrib (fun (a : α) => (f a, f' a)) (fun (b : β) => (g b, g' b)) μ ν)
:
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)
:
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)
:
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 : IdentDistrib f g μ ν)
:
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 : IdentDistrib f g μ ν)
:
IdentDistrib f (g ∘ i) μ (MeasureTheory.Measure.comap i ν)
Composing identically distributed functions with a measurable embedding of conull range gives identically distributed functions.
theorem
MeasureTheory.MeasurePreserving.identDistrib
{α : Type u_5}
{β : Type u_6}
{γ : Type u_7}
{X : β → γ}
{f : α → β}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : Measure α}
{ν : Measure β}
(hf : MeasurePreserving f μ ν)
(hX : AEMeasurable X ν)
:
ProbabilityTheory.IdentDistrib X (X ∘ f) ν μ
theorem
ProbabilityTheory.IdentDistrib.prodMk
{Ω : 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' : IdentDistrib f f' μ ν)
(hgg' : IdentDistrib g g' μ ν)
(h : IndepFun f g μ)
(h' : IndepFun f' g' ν)
:
theorem
ProbabilityTheory.AEMeasurable.piMk
{Ω : Type u_5}
{β : Type u_9}
{mΩ : MeasurableSpace Ω}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure Ω}
{I : Type u_12}
[Countable I]
{F : I → Ω → β}
(hF : ∀ (i : I), AEMeasurable (F i) μ)
:
AEMeasurable (fun (x : Ω) (i : I) => F i x) μ
Move to a different section?
theorem
ProbabilityTheory.IdentDistrib.iprodMk
{Ω : Type u_5}
{Ω' : Type u_6}
{β : Type u_9}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure Ω}
{ν : MeasureTheory.Measure Ω'}
{I : Type u_12}
[Fintype I]
{F : I → Ω → β}
{F' : I → Ω' → β}
(hFF' : ∀ (i : I), IdentDistrib (F i) (F' i) μ ν)
(hμ : MeasureTheory.IsProbabilityMeasure μ)
(hν : MeasureTheory.IsProbabilityMeasure ν)
(h : iIndepFun F μ)
(h' : iIndepFun F' ν)
:
IdentDistrib (fun (x : Ω) (i : I) => F i x) (fun (x : Ω') (i : I) => F' i x) μ ν
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' : IdentDistrib f f' μ ν)
(hgg' : IdentDistrib g g' μ ν)
(h : IndepFun f g μ)
(h' : IndepFun f' g' ν)
:
IdentDistrib (f * g) (f' * g') μ ν
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' : IdentDistrib f f' μ ν)
(hgg' : IdentDistrib g g' μ ν)
(h : IndepFun f g μ)
(h' : IndepFun f' g' ν)
:
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 Ω)
:
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)
:
IdentDistrib X (X ∘ ULift.down) μ (MeasureTheory.Measure.comap ULift.down μ)
theorem
ProbabilityTheory.identDistrib_of_sum
{Ω : Type u_5}
{Ω' : Type u_6}
{α : Type u_7}
{T : Type u_11}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
[MeasurableSpace α]
{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 → IdentDistrib X Y (μ y) (μ' y))
:
IdentDistrib X Y (∑ y ∈ s, w y • μ y) (∑ y ∈ s, 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 μ']
:
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 μ']
:
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' ∧ IndepFun X' Y' ν ∧ IdentDistrib X' X ν μ ∧ 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' ∧ IndepFun X' Y' MeasureTheory.volume ∧ IdentDistrib X' X MeasureTheory.volume MeasureTheory.volume ∧ 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)) (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)
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)) (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 μ₃
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)) (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 μ₄
A version with exactly 4 random variables that have the same codomain. It's unfortunately incredibly painful to prove this from the general case.