theorem
ProbabilityTheory.iIndepFun.reindex_four_abcd
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_abdc
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₄, Z₃] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_acbd
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₃, Z₂, Z₄] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_acdb
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₃, Z₄, Z₂] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_adbc
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₄, Z₂, Z₃] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_adcb
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₄, Z₃, Z₂] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_bacd
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₂, Z₁, Z₃, Z₄] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_badc
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₂, Z₁, Z₄, Z₃] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_bcad
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₂, Z₃, Z₁, Z₄] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_bcda
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₂, Z₃, Z₄, Z₁] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_bdac
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₂, Z₄, Z₁, Z₃] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_bdca
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₂, Z₄, Z₃, Z₁] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_cadb
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₃, Z₁, Z₄, Z₂] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_cabd
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₃, Z₁, Z₂, Z₄] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_cbad
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₃, Z₂, Z₁, Z₄] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_dabc
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₄, Z₁, Z₂, Z₃] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_dacb
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₄, Z₁, Z₃, Z₂] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_dbac
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₄, Z₂, Z₁, Z₃] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_four_dbca
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₄, Z₂, Z₃, Z₁] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.apply_two_last
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ Z₄ : Ω → G}
(h_indep :
ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume)
(hZ₁ : Measurable Z₁)
(hZ₂ : Measurable Z₂)
(hZ₃ : Measurable Z₃)
(hZ₄ : Measurable Z₄)
{phi : G → G → G}
(hphi : Measurable (Function.uncurry phi))
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, fun (ω : Ω) => phi (Z₃ ω) (Z₄ ω)]
MeasureTheory.volume
If (Z₁, Z₂, Z₃, Z₄)
are independent, so are (Z₁, Z₂, φ Z₃ Z₄)
for any measurable φ
.