theorem
ProbabilityTheory.iIndepFun_nat_iff_forall_indepFun
{Ω : Type u_2}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{mE : MeasurableSpace E}
{μ : MeasureTheory.Measure Ω}
{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 ν))
: