Documentation

PFR.Mathlib.Probability.Independence.ThreeVariables

theorem ProbabilityTheory.iIndepFun.reindex_three_abc {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {G : Type u_2} [hG : MeasurableSpace G] {Z₁ Z₂ Z₃ : ΩG} (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, Z₃] MeasureTheory.volume) :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, Z₃] MeasureTheory.volume
theorem ProbabilityTheory.iIndepFun.reindex_three_acb {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {G : Type u_2} [hG : MeasurableSpace G] {Z₁ Z₂ Z₃ : ΩG} (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, Z₃] MeasureTheory.volume) :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₃, Z₂] MeasureTheory.volume
theorem ProbabilityTheory.iIndepFun.reindex_three_bac {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {G : Type u_2} [hG : MeasurableSpace G] {Z₁ Z₂ Z₃ : ΩG} (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, Z₃] MeasureTheory.volume) :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![Z₂, Z₁, Z₃] MeasureTheory.volume
theorem ProbabilityTheory.iIndepFun.reindex_three_bca {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {G : Type u_2} [hG : MeasurableSpace G] {Z₁ Z₂ Z₃ : ΩG} (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, Z₃] MeasureTheory.volume) :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![Z₂, Z₃, Z₁] MeasureTheory.volume
theorem ProbabilityTheory.iIndepFun.reindex_three_cab {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {G : Type u_2} [hG : MeasurableSpace G] {Z₁ Z₂ Z₃ : ΩG} (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, Z₃] MeasureTheory.volume) :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![Z₃, Z₁, Z₂] MeasureTheory.volume
theorem ProbabilityTheory.iIndepFun.reindex_three_cba {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {G : Type u_2} [hG : MeasurableSpace G] {Z₁ Z₂ Z₃ : ΩG} (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, Z₃] MeasureTheory.volume) :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![Z₃, Z₂, Z₁] MeasureTheory.volume
theorem ProbabilityTheory.iIndepFun.pair_last_of_three {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {G : Type u_2} [hG : MeasurableSpace G] {Z₁ Z₂ Z₃ : ΩG} (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, Z₃] MeasureTheory.volume) (hZ₁ : Measurable Z₁) (hZ₂ : Measurable Z₂) (hZ₃ : Measurable Z₃) :
ProbabilityTheory.IndepFun Z₁ (⟨Z₂, Z₃⟩) MeasureTheory.volume