independent iff joint density is product

Stream: Is there code for X?

[Thomas Zhu]

Is there code for the fact that two random variables are independent iff their joint pdf is a product of the marginal pdfs?

[Thomas Zhu]

I have proven the result myself:

import Mathlib.Probability.Density
import Mathlib.Probability.Independence.Basic
import Mathlib.MeasureTheory.Measure.MeasureSpaceDef
import Mathlib.MeasureTheory.Function.AEEqOfIntegral

open MeasureTheory ProbabilityTheory ENNReal

noncomputable section

variable {Ω : Type*} [MeasurableSpace Ω]
variable {E : Type*} [MeasurableSpace E] (X : Ω → E)
variable {F : Type*} [MeasurableSpace F] (Y : Ω → F)
variable (ℙ : Measure Ω) [IsFiniteMeasure ℙ]
variable (μ : Measure E := by volume_tac) [SigmaFinite μ]
variable (ν : Measure F := by volume_tac) [SigmaFinite ν]
variable [HasPDF X ℙ μ]
variable [HasPDF Y ℙ ν]
variable [HasPDF (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν)]

theorem pdf_unique_ae (f g : E → ℝ≥0∞)
    (hmf : Measurable f) (hmg : Measurable g)
    (hf : ℙ.map X = μ.withDensity f) (hg : ℙ.map X = μ.withDensity g) :
    f =ᵐ[μ] g := by
  apply ae_eq_of_forall_set_lintegral_eq_of_sigmaFinite hmf hmg
  intro s hs _
  rw [←withDensity_apply, ←withDensity_apply, ←hf, ←hg] <;> assumption

theorem ae_eq_pdf_of_withDensity (f : E → ℝ≥0∞)
    (hmf : Measurable f) (hf : ℙ.map X = μ.withDensity f) : pdf X ℙ μ =ᵐ[μ] f :=
  pdf_unique_ae X ℙ μ (pdf X ℙ μ) f (measurable_pdf X ℙ μ) hmf (map_eq_withDensity_pdf X ℙ μ) hf

theorem ae_eq_pdf_iff_withDensity (f : E → ℝ≥0∞) (hmf : Measurable f) :
    ℙ.map X = μ.withDensity f ↔ pdf X ℙ μ =ᵐ[μ] f :=
  ⟨ae_eq_pdf_of_withDensity X ℙ μ f hmf, fun hf ↦ Measure.ext fun s hs ↦ by
    rw [map_eq_withDensity_pdf X ℙ μ, withDensity_apply _ hs, withDensity_apply _ hs,
      set_lintegral_congr_fun hs (hf.mono fun _ h _ ↦ h)]⟩

theorem indepFun_iff_pdf_prod_mk_eq_pdf_mul_pdf [IsFiniteMeasure ℙ] :
    IndepFun X Y ℙ ↔
      pdf (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν) =ᵐ[μ.prod ν] fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2 := by
  rw [indepFun_iff_measure_inter_preimage_eq_mul, ←ae_eq_pdf_iff_withDensity (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν)]
  case hmf =>
    exact Measurable.mul (Measurable.comp (measurable_pdf X ℙ μ) measurable_fst)
      (Measurable.comp (measurable_pdf Y ℙ ν) measurable_snd)
  constructor
  · intro h
    trans (ℙ.map X).prod (ℙ.map Y)
    · symm; apply Measure.prod_eq
      intro s t hs ht
      have hst : MeasurableSet (s ×ˢ t) := .prod hs ht
      rw [Measure.map_apply (HasPDF.measurable _ ℙ (μ.prod ν)) hst,
        Measure.map_apply (HasPDF.measurable X ℙ μ) hs, Measure.map_apply (HasPDF.measurable Y ℙ ν) ht]
      exact h s t hs ht
    · apply Measure.prod_eq
      intro s t hs ht
      have hst : MeasurableSet (s ×ˢ t) := .prod hs ht
      rw [withDensity_apply _ hst, ←Measure.prod_restrict,
        lintegral_prod_mul (measurable_pdf _ _ _).aemeasurable (measurable_pdf _ _ _).aemeasurable,
        map_eq_set_lintegral_pdf X ℙ μ hs, map_eq_set_lintegral_pdf Y ℙ ν ht]
  · intro h s t hs ht
    have hst : MeasurableSet (s ×ˢ t) := .prod hs ht
    change ℙ ((fun ω ↦ (X ω, Y ω)) ⁻¹' s ×ˢ t) = _
    rw [←Measure.map_apply (HasPDF.measurable _ ℙ (μ.prod ν)) hst, h, withDensity_apply _ hst,
      ←Measure.map_apply (HasPDF.measurable X ℙ μ) hs, map_eq_set_lintegral_pdf X ℙ μ hs,
      ←Measure.map_apply (HasPDF.measurable Y ℙ ν) ht, map_eq_set_lintegral_pdf Y ℙ ν ht,
      ←lintegral_prod_mul (measurable_pdf _ _ _).aemeasurable (measurable_pdf _ _ _).aemeasurable,
      Measure.prod_restrict]

[Thomas Zhu]

Is there any value for contributing this to mathlib if it's not already there?

[Kalle Kytölä]

I think we definitely want that in Mathlib!

I suspect we don't have it yet, but @Rémy Degenne (ping!) knows more about the status and plans around independence.

I believe this would be a very welcome PR.

[Thomas Zhu]

I submitted PR #8026 for this code, though I am happy to change it around if needed

[Rémy Degenne]

This is very nice! I left some comments on the PR.