@[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.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 ν))
: