theorem ProbabilityTheory.iIndepFun.reindex_four_abcd {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {G : Type u_2} [hG : MeasurableSpace G] {Z₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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

@[reducible, inline]

abbrev ProbabilityTheory.iIndepFun.κ : Fin 3 → Type

Equations

• ProbabilityTheory.iIndepFun.κ x = match x with | 0 => Fin 1 | 1 => Fin 1 | 2 => Fin 2

theorem ProbabilityTheory.iIndepFun.apply_two_last {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type u_2} [hG : MeasurableSpace G] {Z₁ : Ω → G} {Z₂ : Ω → G} {Z₃ : Ω → G} {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 φ.