feat: the law of independent random variables is the product of their laws (leanprover-community#37830)

Author: EtienneC30

Mathlib/Probability/HasLaw.lean

@@ -150,4 +150,35 @@ lemma HasPDF.hasLaw [h : HasPDF X P μ] : HasLaw X (μ.withDensity (pdf X P μ))
   aemeasurable := h.aemeasurable
   map_eq := map_eq_withDensity_pdf X P μ
 
+lemma indepFun_iff_hasLaw_prodMk_prod [IsFiniteMeasure P] {𝓨 : Type*} {m𝓨 : MeasurableSpace 𝓨}
+    {ν : Measure 𝓨} {Y : Ω → 𝓨} (hX : HasLaw X μ P) (hY : HasLaw Y ν P) :
+    X ⟂ᵢ[P] Y ↔ HasLaw (fun ω ↦ (X ω, Y ω)) (μ.prod ν) P where
+  mp h :=
+    { map_eq := by
+        rw [(indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop)).1 h, hX.map_eq,
+          hY.map_eq] }
+  mpr h := by
+    rw [indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop),
+      h.map_eq, hX.map_eq, hY.map_eq]
+
+alias ⟨IndepFun.hasLaw_prod, _⟩ := indepFun_iff_hasLaw_prodMk_prod
+
+lemma iIndepFun.hasLaw_pi {ι : Type*} [Fintype ι] {𝓧 : ι → Type*} {m𝓧 : ∀ i, MeasurableSpace (𝓧 i)}
+    {μ : (i : ι) → Measure (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i} (hX : ∀ i, HasLaw (X i) (μ i) P)
+    (h : iIndepFun X P) :
+    HasLaw (fun ω i ↦ X i ω) (Measure.pi μ) P where
+  map_eq := by
+    have := h.isProbabilityMeasure
+    rw [(iIndepFun_iff_map_fun_eq_pi_map (by fun_prop)).1 h]
+    simp_rw [fun i ↦ (hX i).map_eq]
+
+lemma iIndepFun_iff_hasLaw_pi_pi [IsProbabilityMeasure P] {ι : Type*} [Fintype ι] {𝓧 : ι → Type*}
+    {m𝓧 : ∀ i, MeasurableSpace (𝓧 i)} {μ : (i : ι) → Measure (𝓧 i)}
+    {X : (i : ι) → Ω → 𝓧 i} (hX : ∀ i, HasLaw (X i) (μ i) P) :
+    iIndepFun X P ↔ HasLaw (fun ω i ↦ X i ω) (Measure.pi μ) P where
+  mp h := h.hasLaw_pi hX
+  mpr h := by
+    rw [iIndepFun_iff_map_fun_eq_pi_map (by fun_prop), h.map_eq]
+    simp_rw [fun i ↦ (hX i).map_eq]
+
 end ProbabilityTheory

Mathlib/Probability/Independence/InfinitePi.lean

@@ -5,6 +5,7 @@ Authors: Etienne Marion
 -/
 module
 
+public import Mathlib.Probability.HasLaw
 public import Mathlib.Probability.Independence.Basic
 public import Mathlib.Probability.ProductMeasure
 
@@ -79,6 +80,24 @@ lemma iIndepFun_iff_map_fun_eq_infinitePi_map (mX : ∀ i, Measurable (X i)) :
     iIndepFun X P ↔ P.map (fun ω i ↦ X i ω) = infinitePi (fun i ↦ P.map (X i)) :=
   iIndepFun_iff_map_fun_eq_infinitePi_map₀ <| measurable_pi_iff.2 mX |>.aemeasurable
 
+omit [IsProbabilityMeasure P] in
+lemma iIndepFun.hasLaw_infinitePi {μ : (i : ι) → Measure (𝓧 i)} (hX : ∀ i, HasLaw (X i) (μ i) P)
+    (h1 : iIndepFun X P) (h2 : AEMeasurable (fun ω i ↦ X i ω) P) :
+    HasLaw (fun ω i ↦ X i ω) (infinitePi μ) P where
+  aemeasurable := h2
+  map_eq := by
+    have := h1.isProbabilityMeasure
+    rw [(iIndepFun_iff_map_fun_eq_infinitePi_map₀ h2).1 h1]
+    simp_rw [fun i ↦ (hX i).map_eq]
+
+lemma iIndepFun_iff_hasLaw_Pi_infinitePi {μ : (i : ι) → Measure (𝓧 i)}
+    (hX : ∀ i, HasLaw (X i) (μ i) P) (hm : AEMeasurable (fun ω i ↦ X i ω) P) :
+    iIndepFun X P ↔ HasLaw (fun ω i ↦ X i ω) (infinitePi μ) P where
+  mp h := h.hasLaw_infinitePi hX hm
+  mpr h := by
+    rw [iIndepFun_iff_map_fun_eq_infinitePi_map₀ hm, h.map_eq]
+    simp_rw [fun i ↦ (hX i).map_eq]
+
 /-- Given random variables `X i : Ω i → 𝓧 i`, they are independent when viewed as random
 variables defined on the product space `Π i, Ω i`. -/
 lemma iIndepFun_infinitePi {Ω : ι → Type*} {mΩ : ∀ i, MeasurableSpace (Ω i)}