feat(Probability/Density): Random variables are independent iff joint…

… density is product (#8026)

This PR proves that two random variables are independent, iff their joint distribution is the product measure of marginal distributions, iff their joint density is a product of their marginal densities up to AE equality. It also uses lemmas stating that `μ.withDensity` is injective up to AE equality.

Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

@@ -648,4 +648,25 @@ theorem AEMeasurable.ae_eq_of_forall_set_lintegral_eq {f g : α → ℝ≥0∞}
 
 end Lintegral
 
+section WithDensity
+
+variable {m : MeasurableSpace α} {μ : Measure α}
+
+theorem withDensity_eq_iff_of_sigmaFinite [SigmaFinite μ] {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
+    (hg : AEMeasurable g μ) : μ.withDensity f = μ.withDensity g ↔ f =ᵐ[μ] g :=
+  ⟨fun hfg ↦ by
+    refine ae_eq_of_forall_set_lintegral_eq_of_sigmaFinite₀ hf hg fun s hs _ ↦ ?_
+    rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg], withDensity_congr_ae⟩
+
+theorem withDensity_eq_iff {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
+    (hg : AEMeasurable g μ) (hfi : ∫⁻ x, f x ∂μ ≠ ∞) :
+    μ.withDensity f = μ.withDensity g ↔ f =ᵐ[μ] g :=
+  ⟨fun hfg ↦ by
+    refine AEMeasurable.ae_eq_of_forall_set_lintegral_eq hf hg hfi ?_ fun s hs _ ↦ ?_
+    · rwa [← set_lintegral_univ, ← withDensity_apply g MeasurableSet.univ, ← hfg,
+        withDensity_apply f MeasurableSet.univ, set_lintegral_univ]
+    · rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg], withDensity_congr_ae⟩
+
+end WithDensity
+
 end MeasureTheory

Mathlib/Probability/Density.lean

@@ -5,6 +5,7 @@ Authors: Kexing Ying
 -/
 import Mathlib.MeasureTheory.Decomposition.RadonNikodym
 import Mathlib.MeasureTheory.Measure.Haar.OfBasis
+import Mathlib.Probability.Independence.Basic
 
 #align_import probability.density from "leanprover-community/mathlib"@"c14c8fcde993801fca8946b0d80131a1a81d1520"
 
@@ -136,13 +137,25 @@ theorem lintegral_eq_measure_univ {X : Ω → E} [HasPDF X ℙ μ] :
     Measure.map_apply (HasPDF.measurable X ℙ μ) MeasurableSet.univ, Set.preimage_univ]
 #align measure_theory.pdf.lintegral_eq_measure_univ MeasureTheory.pdf.lintegral_eq_measure_univ
 
+theorem unique [IsFiniteMeasure ℙ] {X : Ω → E} [HasPDF X ℙ μ] (f : E → ℝ≥0∞)
+    (hmf : AEMeasurable f μ) : ℙ.map X = μ.withDensity f ↔ pdf X ℙ μ =ᵐ[μ] f := by
+  rw [map_eq_withDensity_pdf X ℙ μ]
+  apply withDensity_eq_iff (measurable_pdf X ℙ μ).aemeasurable hmf
+  rw [lintegral_eq_measure_univ]
+  exact measure_ne_top _ _
+
+theorem unique' [SigmaFinite μ] {X : Ω → E} [HasPDF X ℙ μ] (f : E → ℝ≥0∞) (hmf : AEMeasurable f μ) :
+    ℙ.map X = μ.withDensity f ↔ pdf X ℙ μ =ᵐ[μ] f :=
+  map_eq_withDensity_pdf X ℙ μ ▸
+    withDensity_eq_iff_of_sigmaFinite (measurable_pdf X ℙ μ).aemeasurable hmf
+
 nonrec theorem ae_lt_top [IsFiniteMeasure ℙ] {μ : Measure E} {X : Ω → E} :
     ∀ᵐ x ∂μ, pdf X ℙ μ x < ∞ := by
   by_cases hpdf : HasPDF X ℙ μ
   · haveI := hpdf
     refine' ae_lt_top (measurable_pdf X ℙ μ) _
     rw [lintegral_eq_measure_univ]
-    exact (measure_lt_top _ _).ne
+    exact measure_ne_top _ _
   · simp [pdf, hpdf]
 #align measure_theory.pdf.ae_lt_top MeasureTheory.pdf.ae_lt_top
 
@@ -411,6 +424,33 @@ end IsUniform
 
 end
 
+section TwoVariables
+
+open ProbabilityTheory
+
+variable {F : Type*} [MeasurableSpace F] {ν : Measure F} {X : Ω → E} {Y : Ω → F}
+
+/-- Random variables are independent iff their joint density is a product of marginal densities. -/
+theorem indepFun_iff_pdf_prod_eq_pdf_mul_pdf
+    [IsFiniteMeasure ℙ] [SigmaFinite μ] [SigmaFinite ν] [HasPDF (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν)] :
+    IndepFun X Y ℙ ↔
+      pdf (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν) =ᵐ[μ.prod ν] fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2 := by
+  have : HasPDF X ℙ μ := quasiMeasurePreserving_hasPDF' (μ := μ.prod ν) (X := fun ω ↦ (X ω, Y ω))
+    quasiMeasurePreserving_fst
+  have : HasPDF Y ℙ ν := quasiMeasurePreserving_hasPDF' (μ := μ.prod ν) (X := fun ω ↦ (X ω, Y ω))
+    quasiMeasurePreserving_snd
+  have h₀ : (ℙ.map X).prod (ℙ.map Y) =
+      (μ.prod ν).withDensity fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2 :=
+    prod_eq fun s t hs ht ↦ by rw [withDensity_apply _ (hs.prod ht), ← prod_restrict,
+      lintegral_prod_mul (measurable_pdf X ℙ μ).aemeasurable (measurable_pdf Y ℙ ν).aemeasurable,
+      map_eq_set_lintegral_pdf X ℙ μ hs, map_eq_set_lintegral_pdf Y ℙ ν ht]
+  rw [indepFun_iff_map_prod_eq_prod_map_map (HasPDF.measurable X ℙ μ) (HasPDF.measurable Y ℙ ν),
+    ← unique, h₀]
+  exact (((measurable_pdf X ℙ μ).comp measurable_fst).mul
+    ((measurable_pdf Y ℙ ν).comp measurable_snd)).aemeasurable
+
+end TwoVariables
+
 end pdf
 
 end MeasureTheory

Mathlib/Probability/Independence/Basic.lean

@@ -634,6 +634,21 @@ theorem indepFun_iff_indepSet_preimage {mβ : MeasurableSpace β} {mβ' : Measur
     Filter.eventually_pure, kernel.const_apply]
 #align probability_theory.indep_fun_iff_indep_set_preimage ProbabilityTheory.indepFun_iff_indepSet_preimage
 
+theorem indepFun_iff_map_prod_eq_prod_map_map {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
+    [IsFiniteMeasure μ] (hf : Measurable f) (hg : Measurable g) :
+    IndepFun f g μ ↔ μ.map (fun ω ↦ (f ω, g ω)) = (μ.map f).prod (μ.map g) := by
+  rw [indepFun_iff_measure_inter_preimage_eq_mul]
+  have h₀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) :
+      μ (f ⁻¹' s) * μ (g ⁻¹' t) = μ.map f s * μ.map g t ∧
+      μ (f ⁻¹' s ∩ g ⁻¹' t) = μ.map (fun ω ↦ (f ω, g ω)) (s ×ˢ t) :=
+    ⟨by rw [Measure.map_apply hf hs, Measure.map_apply hg ht],
+      (Measure.map_apply (hf.prod_mk hg) (hs.prod ht)).symm⟩
+  constructor
+  · refine fun h ↦ (Measure.prod_eq fun s t hs ht ↦ ?_).symm
+    rw [← (h₀ hs ht).1, ← (h₀ hs ht).2, h s t hs ht]
+  · intro h s t hs ht
+    rw [(h₀ hs ht).1, (h₀ hs ht).2, h, Measure.prod_prod]
+
 @[symm]
 nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {f g : Ω → β} (hfg : IndepFun f g μ) :
     IndepFun g f μ := hfg.symm