-- Mathlib/Probability/Density.lean
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

Proof state:
Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)
this✝ : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
s : Set E
t : Set F
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((μ.prod ν).withDensity fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2) (s ×ˢ t) = (map X ℙ) s * (map Y ℙ) t

Tactic:
rw [withDensity_apply _ (hs.prod ht), ← prod_restrict,
lintegral_prod_mul (measurable_pdf X ℙ μ).aemeasurable (measurable_pdf Y ℙ ν).aemeasurable,
map_eq_setLIntegral_pdf X ℙ μ hs, map_eq_setLIntegral_pdf Y ℙ ν ht]

Result:
no goals

Proof state:
Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)
⊢ IndepFun X Y ℙ ↔ pdf (fun ω => (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2

Tactic:
have : HasPDF X ℙ μ := quasiMeasurePreserving_hasPDF' (μ := μ.prod ν) (fun ω ↦ (X ω, Y ω))
  quasiMeasurePreserving_fst

Result:
Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)
this : HasPDF X ℙ μ
⊢ IndepFun X Y ℙ ↔ pdf (fun ω => (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2

Proof state:
Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)
this✝ : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
h₀ : (map X ℙ).prod (map Y ℙ) = (μ.prod ν).withDensity fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
⊢ IndepFun X Y ℙ ↔ pdf (fun ω => (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2

Tactic:
rw [indepFun_iff_map_prod_eq_prod_map_map (HasPDF.aemeasurable X ℙ μ) (HasPDF.aemeasurable Y ℙ ν),
  ← eq_of_map_eq_withDensity, h₀]

Result:
case hmf
Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)
this✝ : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
h₀ : (map X ℙ).prod (map Y ℙ) = (μ.prod ν).withDensity fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
⊢ AEMeasurable (fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2) (μ.prod ν)

Proof state:
Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)
this : HasPDF X ℙ μ
⊢ IndepFun X Y ℙ ↔ pdf (fun ω => (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2

Tactic:
have : HasPDF Y ℙ ν := quasiMeasurePreserving_hasPDF' (μ := μ.prod ν) (fun ω ↦ (X ω, Y ω))
  quasiMeasurePreserving_snd

Result:
Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)
this✝ : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
⊢ IndepFun X Y ℙ ↔ pdf (fun ω => (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2

Proof state:
case hmf
Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)
this✝ : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
h₀ : (map X ℙ).prod (map Y ℙ) = (μ.prod ν).withDensity fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
⊢ AEMeasurable (fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2) (μ.prod ν)

Tactic:
exact (((measurable_pdf X ℙ μ).comp measurable_fst).mul
  ((measurable_pdf Y ℙ ν).comp measurable_snd)).aemeasurable

Result:
no goals

Proof state:
Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)
this✝ : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
⊢ IndepFun X Y ℙ ↔ pdf (fun ω => (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2

Tactic:
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_setLIntegral_pdf X ℙ μ hs, map_eq_setLIntegral_pdf Y ℙ ν ht]

Result:
Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)
this✝ : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
h₀ : (map X ℙ).prod (map Y ℙ) = (μ.prod ν).withDensity fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
⊢ IndepFun X Y ℙ ↔ pdf (fun ω => (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2