Lemmas about independence #
@[simp]
theorem
ProbabilityTheory.indepFun_zero_measure
{α : Type u_6}
{β : Type u_7}
{γ : Type u_8}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(X : α → β)
(Y : α → γ)
:
IndepFun X Y 0
theorem
ProbabilityTheory.indepFun_cond_of_indepFun
{α : Type u_6}
{β : Type u_7}
{γ : Type u_8}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → γ}
(hXY : IndepFun X Y μ)
(hY : Measurable Y)
{s : Set γ}
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.indepFun_cond_comp
{α : Type u_6}
{β : Type u_7}
{γ : Type u_8}
{δ : Type u_9}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
[MeasurableSingletonClass δ]
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → γ}
(hXY : IndepFun X Y μ)
(hY : Measurable Y)
{Z : γ → δ}
(hZ : Measurable Z)
(z : δ)
:
theorem
ProbabilityTheory.indepFun_cond_preimage_singleton_left
{α : Type u_6}
{β : Type u_7}
{γ : Type u_8}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSingletonClass β]
{μ : MeasureTheory.Measure α}
{X : α → β}
(hX : Measurable X)
(b : β)
(Y : α → γ)
:
Under μ conditioned on the event X = b, the random variable X is almost surely constant,
hence independent of any other random variable.
theorem
ProbabilityTheory.indepFun_cond_preimage_singleton_right
{α : Type u_6}
{β : Type u_7}
{γ : Type u_8}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSingletonClass β]
{μ : MeasureTheory.Measure α}
{X : α → β}
(hX : Measurable X)
(b : β)
(Y : α → γ)
:
Under μ conditioned on the event X = b, the random variable X is almost surely constant,
hence independent of any other random variable.
theorem
ProbabilityTheory.iIndepFun_nat_iff_forall_indepFun
{Ω : Type u_2}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{mE : MeasurableSpace E}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : ℕ → Ω → E}
(hX : ∀ (n : ℕ), AEMeasurable (X n) μ)
:
theorem
ProbabilityTheory.IndepFun_map_iff
{Ω : Type u_2}
{Ω' : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{mE : MeasurableSpace E}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{X Y : Ω' → E}
{f : Ω → Ω'}
(hf : AEMeasurable f μ)
(hX : AEMeasurable X (MeasureTheory.Measure.map f μ))
(hY : AEMeasurable Y (MeasureTheory.Measure.map f μ))
:
theorem
ProbabilityTheory.iIndepFun_map_iff
{Ω : Type u_2}
{Ω' : Type u_3}
{E : Type u_4}
{ι : Type u_5}
[Countable ι]
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{mE : MeasurableSpace E}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : ι → Ω' → E}
{f : Ω → Ω'}
(hf : AEMeasurable f μ)
(hX : ∀ (n : ι), AEMeasurable (X n) (MeasureTheory.Measure.map f μ))
:
theorem
ProbabilityTheory.identDistrib_map_right_iff
{Ω : Type u_2}
{Ω' : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{mE : MeasurableSpace E}
{μ ν : MeasureTheory.Measure Ω}
{X : Ω → E}
{Y : Ω' → E}
{f : Ω → Ω'}
(hf : AEMeasurable f ν)
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y (MeasureTheory.Measure.map f ν))
:
theorem
ProbabilityTheory.identDistrib_comm
{Ω : Type u_2}
{Ω' : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{mE : MeasurableSpace E}
{μ : MeasureTheory.Measure Ω}
(X : Ω → E)
(Y : Ω' → E)
{ν : MeasureTheory.Measure Ω'}
:
theorem
ProbabilityTheory.identDistrib_map_left_iff
{Ω : Type u_2}
{Ω' : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{mE : MeasurableSpace E}
{μ ν : MeasureTheory.Measure Ω}
{X : Ω → E}
{Y : Ω' → E}
{f : Ω → Ω'}
(hf : AEMeasurable f ν)
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y (MeasureTheory.Measure.map f ν))
:
theorem
ProbabilityTheory.hasLaw_fst_prod
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure β)
[MeasureTheory.IsProbabilityMeasure ν]
:
theorem
ProbabilityTheory.hasLaw_snd_prod
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsProbabilityMeasure μ]
(ν : MeasureTheory.Measure β)
[MeasureTheory.SFinite ν]
:
theorem
ProbabilityTheory.IndepFun.snd_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsProbabilityMeasure μ]
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
{X : β → γ}
{T : β → δ}
(h : IndepFun X T ν)
(hX : Measurable X)
(hT : Measurable T)
:
If X and T are independent under ν, then under μ.prod ν the function X ∘ Prod.snd
is independent of (Prod.fst, T ∘ Prod.snd).
theorem
ProbabilityTheory.IndepFun.fst_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SFinite μ]
{ν : MeasureTheory.Measure β}
[MeasureTheory.IsProbabilityMeasure ν]
{X : α → γ}
{T : α → δ}
(h : IndepFun X T μ)
(hX : Measurable X)
(hT : Measurable T)
:
If X and T are independent under μ, then under μ.prod ν the function X ∘ Prod.fst
is independent of (T ∘ Prod.fst, Prod.snd).
theorem
ProbabilityTheory.iIndepFun.indepFun_of_measurable_iSup_comap
{ι : Type u_1}
{Ω : Type u_2}
{β : Type u_3}
{𝓧 : ι → Type u_4}
[(i : ι) → MeasurableSpace (𝓧 i)]
{mΩ : MeasurableSpace Ω}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure Ω}
{X : (i : ι) → Ω → 𝓧 i}
(hX : iIndepFun X μ)
(hXm : ∀ (i : ι), Measurable (X i))
{S : Set ι}
{i : ι}
(hi : i ∉ S)
{Y : Ω → β}
(hY : Measurable Y)
:
IndepFun (X i) Y μ
A coordinate of an independent family is independent of any function that is measurable with respect to the other coordinates.