theorem
ProbabilityTheory.IdentDistrib.prod
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{μ : MeasureTheory.Measure Ω}
{ν : MeasureTheory.Measure Ω'}
{X Y : Ω → ℝ}
{Z W : Ω' → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hXZ : IdentDistrib X Z μ ν)
(hYW : IdentDistrib Y W μ ν)
(hXY : IndepFun X Y μ)
(hZW : IndepFun Z W ν)
:
theorem
ProbabilityTheory.IdentDistrib.pi
{Ω : Type u_1}
{Ω' : Type u_2}
{ι : Type u_3}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{μ : MeasureTheory.Measure Ω}
{ν : MeasureTheory.Measure Ω'}
[Countable ι]
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
{X : ι → Ω → ℝ}
{Y : ι → Ω' → ℝ}
(h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν)
(hX_ind : iIndepFun X μ)
(hY_ind : iIndepFun Y ν)
:
IdentDistrib (fun (ω : Ω) (x : ι) => X x ω) (fun (ω : Ω') (x : ι) => Y x ω) μ ν