awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : IsFiniteMeasure ℙ
X : Ω → E
inst_4 : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
rw rw₁ : @Integrable _ _ _ _ inst f (map X ℙ) ↔ @Integrable _ _ _ _ inst f (map X ℙ)
⊢ @Integrable _ _ _ _ inst f (map X ℙ) ↔ Integrable f (μ.withDensity (rnDeriv (map X ℙ) μ))

Tactic:
rw [withDensity_rnDeriv_eq _ _ HasPDF.absolutelyContinuous]

Premises used: MeasureTheory.HasPDF.absolutelyContinuous, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : IsFiniteMeasure ℙ
X : Ω → E
inst_4 : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
rw :
  Eq.{u_3 + 1} (α := F) (∫ (x : E), (pdf X ℙ μ x).toReal • f x ∂μ) (@integral _ _ _ _ inst (map X ℙ) fun (y : E) ↦ f y)
rw₁ : Eq.{u_3 + 1} (α := F) (∫ (x : E), (pdf X ℙ μ x).toReal • f x ∂μ) (∫ (y : E), f y ∂μ.withDensity (pdf X ℙ μ))
rw₂ :
  Eq.{u_3 + 1} (α := F) (∫ (x : E), (rnDeriv (map X ℙ) μ x).toReal • f x ∂μ)
    (∫ (y : E), f y ∂μ.withDensity (rnDeriv (map X ℙ) μ))
rw₃ :
  Eq.{u_3 + 1} (α := F) (@integral _ _ _ _ inst (map X ℙ) fun (x : E) ↦ f x)
    (∫ (y : E), f y ∂μ.withDensity (rnDeriv (map X ℙ) μ))
rw₄ rw₅ :
  Eq.{u_3 + 1} (α := F) (@integral _ _ _ _ inst (map X ℙ) fun (x : E) ↦ f x)
    (@integral _ _ _ _ inst (map X ℙ) fun (y : E) ↦ f y)
⊢ Eq.{u_3 + 1} (α := F) (∫ (x : E), (pdf X ℙ μ x).toReal • f x ∂μ) (∫ (x : Ω), f (X x) ∂ℙ)

Tactic:
rw [← integral_map (HasPDF.aemeasurable X ℙ μ) (hf.mono_ac HasPDF.absolutelyContinuous),
    map_eq_withDensity_pdf X ℙ μ, pdf_def, integral_rnDeriv_smul HasPDF.absolutelyContinuous,
    withDensity_rnDeriv_eq _ _ HasPDF.absolutelyContinuous]

Premises used: MeasureTheory.integral_map, MeasureTheory.map_eq_withDensity_pdf, MeasureTheory.AEStronglyMeasurable.mono_ac, MeasureTheory.integral_rnDeriv_smul, MeasureTheory.pdf_def, MeasureTheory.HasPDF.aemeasurable, MeasureTheory.HasPDF.absolutelyContinuous, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
inst_2 : HasPDF X ℙ μ
g : E → F
hg : QuasiMeasurePreserving g μ ν
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
⊢ AEMeasurable (_m := inst) g (map X ℙ)

Tactic:
have hgm : AEMeasurable g (map X ℙ) := hg.aemeasurable.mono_ac HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
inst_2 : HasPDF X ℙ μ
g : E → F
hg : QuasiMeasurePreserving g μ ν
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
hgm : AEMeasurable (_m := inst) g (map X ℙ)
rw : AEMeasurable (g ∘ X) ℙ ∧ HaveLebesgueDecomposition (map g (map X ℙ)) ν ∧ map g (map X ℙ) ≪ ν
⊢ HasPDF (g ∘ X) ℙ ν

Tactic:
rw [hasPDF_iff, ← AEMeasurable.map_map_of_aemeasurable hgm (HasPDF.aemeasurable X ℙ μ)]

Premises used: MeasureTheory.hasPDF_iff, AEMeasurable.map_map_of_aemeasurable, MeasureTheory.HasPDF.aemeasurable
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
inst_2 : HasPDF X ℙ μ
g : E → F
hg : QuasiMeasurePreserving g μ ν
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
hgm : AEMeasurable (_m := inst) g (map X ℙ)
⊢ AEMeasurable (g ∘ X) ℙ ∧ HaveLebesgueDecomposition (map g (map X ℙ)) ν ∧ map g (map X ℙ) ≪ ν

Tactic:
⟨hg.measurable.comp_aemeasurable (HasPDF.aemeasurable _ _ μ), hmap, ?_⟩

Premises used: And.intro, Measurable.comp_aemeasurable, MeasureTheory.HasPDF.aemeasurable, MeasureTheory.Measure.QuasiMeasurePreserving.measurable
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
inst_2 : HasPDF X ℙ μ
g : E → F
hg : QuasiMeasurePreserving g μ ν
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
hgm : AEMeasurable (_m := inst) g (map X ℙ)
refine : map g (map X ℙ) ≪ ν
⊢ AEMeasurable (g ∘ X) ℙ ∧ HaveLebesgueDecomposition (map g (map X ℙ)) ν ∧ map g (map X ℙ) ≪ ν

Tactic:
refine ⟨hg.measurable.comp_aemeasurable (HasPDF.aemeasurable _ _ μ), hmap, ?_⟩
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
inst_2 : HasPDF X ℙ μ
g : E → F
hg : QuasiMeasurePreserving g μ ν
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
hgm : AEMeasurable (_m := inst) g (map X ℙ)
⊢ map g (map X ℙ) ≪ ν

Tactic:
(HasPDF.absolutelyContinuous.map hg.1).trans hg.2

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.trans, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.Measure.AbsolutelyContinuous.map, MeasureTheory.Measure.QuasiMeasurePreserving.measurable, MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
inst_2 : HasPDF X ℙ μ
g : E → F
hg : QuasiMeasurePreserving g μ ν
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
hgm : AEMeasurable (_m := inst) g (map X ℙ)
⊢ map g (map X ℙ) ≪ ν

Tactic:
exact (HasPDF.absolutelyContinuous.map hg.1).trans hg.2

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.trans, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.Measure.AbsolutelyContinuous.map, MeasureTheory.Measure.QuasiMeasurePreserving.measurable, MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
inst_2 : HasPDF X ℙ μ
g : E → F
inst_3 : SFinite ℙ
inst_4 : SigmaFinite ν
hg : QuasiMeasurePreserving g μ ν
⊢ HasPDF (g ∘ X) ℙ ν

Tactic:
quasiMeasurePreserving_hasPDF X hg inferInstance

Premises used: inferInstance, MeasureTheory.pdf.quasiMeasurePreserving_hasPDF
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : SFinite ℙ
rw :
  AEMeasurable X ℙ ∧
      HaveLebesgueDecomposition (m := Real.measurableSpace) (map X ℙ) volume ∧
        AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume ↔
    AEMeasurable X ℙ ∧ AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume
rw₁ rw₂ :
  AEMeasurable X ℙ ∧ AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume ↔
    AEMeasurable X ℙ ∧ AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume
⊢ HasPDF X ℙ volume ↔ AEMeasurable X ℙ ∧ AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume

Tactic:
rw [hasPDF_iff, and_iff_right (inferInstance : HaveLebesgueDecomposition _ _)]

Premises used: MeasureTheory.hasPDF_iff, inferInstance, and_iff_right
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : SFinite ℙ
hX : AEMeasurable X ℙ
rw :
  AEMeasurable X ℙ ∧ AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume ↔
    AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume
rw₁ rw₂ :
  AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume ↔
    AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume
⊢ HasPDF X ℙ volume ↔ AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume

Tactic:
rw [Real.hasPDF_iff, and_iff_right hX]

Premises used: and_iff_right, Real.hasPDF_iff
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
inst_1 : HasPDF X ℙ volume
e_f : ∀ (x : ℝ), x * (pdf X ℙ volume x).toReal = (pdf X ℙ volume x).toReal * x
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ x * (pdf X ℙ volume x).toReal)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ (pdf X ℙ volume x).toReal * x)

Tactic:
congr with x
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
inst_1 : HasPDF X ℙ volume
x : ℝ
⊢ x * (pdf X ℙ volume x).toReal = (pdf X ℙ volume x).toReal * x

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
inst_1 : HasPDF X ℙ volume
x : ℝ
⊢ x * (pdf X ℙ volume x).toReal = (pdf X ℙ volume x).toReal * x

Tactic:
exact mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae (F := Measure ℝ) volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
⊢ (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞) (fun (x : ℝ) ↦ ‖f x‖ₑ * g x) fun (x : ℝ) ↦
    ‖f x * (pdf X ℙ volume x).toReal‖ₑ

Tactic:
ae_eq_trans ((ae_eq_refl _).fun_mul (ae_eq_trans hg.symm ofReal_toReal_ae_eq.symm)) ?_

Premises used: MeasureTheory.ae_eq_refl, Filter.EventuallyEq.fun_mul, MeasureTheory.ae_eq_trans, Filter.EventuallyEq.symm, MeasureTheory.pdf.ofReal_toReal_ae_eq
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae (F := Measure ℝ) volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
refine :
  (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞)
    (fun (i : ℝ) ↦ ‖f i‖ₑ * ENNReal.ofReal (pdf X ℙ volume i).toReal) fun (x : ℝ) ↦ ‖f x * (pdf X ℙ volume x).toReal‖ₑ
⊢ (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞) (fun (x : ℝ) ↦ ‖f x‖ₑ * g x) fun (x : ℝ) ↦
    ‖f x * (pdf X ℙ volume x).toReal‖ₑ

Tactic:
refine ae_eq_trans ((ae_eq_refl _).fun_mul (ae_eq_trans hg.symm ofReal_toReal_ae_eq.symm)) ?_

Premises used: MeasureTheory.ae_eq_refl, Filter.EventuallyEq.fun_mul, MeasureTheory.ae_eq_trans, Filter.EventuallyEq.symm, MeasureTheory.pdf.ofReal_toReal_ae_eq
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae (F := Measure ℝ) volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
simp_rw :
  (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞)
    (fun (i : ℝ) ↦ ‖f i‖ₑ * ENNReal.ofReal (pdf X ℙ volume i).toReal) fun (x : ℝ) ↦
    ‖f x‖ₑ * ‖(pdf X ℙ volume x).toReal‖ₑ
⊢ (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞)
    (fun (i : ℝ) ↦ ‖f i‖ₑ * ENNReal.ofReal (pdf X ℙ volume i).toReal) fun (x : ℝ) ↦ ‖f x * (pdf X ℙ volume x).toReal‖ₑ

Tactic:
simp_rw [← smul_eq_mul, enorm_smul, smul_eq_mul]

Premises used: enorm_smul, smul_eq_mul
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae (F := Measure ℝ) volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
⊢ (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞)
    (fun (i : ℝ) ↦ ‖f i‖ₑ * ENNReal.ofReal (pdf X ℙ volume i).toReal) fun (x : ℝ) ↦
    ‖f x‖ₑ * ‖(pdf X ℙ volume x).toReal‖ₑ

Tactic:
.fun_mul (ae_eq_refl _) ?_

Premises used: MeasureTheory.ae_eq_refl, Filter.EventuallyEq.fun_mul
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae (F := Measure ℝ) volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
refine :
  (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞) (fun (i : ℝ) ↦ ENNReal.ofReal (pdf X ℙ volume i).toReal)
    fun (x : ℝ) ↦ ‖(pdf X ℙ volume x).toReal‖ₑ
⊢ (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞)
    (fun (i : ℝ) ↦ ‖f i‖ₑ * ENNReal.ofReal (pdf X ℙ volume i).toReal) fun (x : ℝ) ↦
    ‖f x‖ₑ * ‖(pdf X ℙ volume x).toReal‖ₑ

Tactic:
refine .fun_mul (ae_eq_refl _) ?_
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae (F := Measure ℝ) volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
⊢ (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞) (fun (i : ℝ) ↦ ENNReal.ofReal (pdf X ℙ volume i).toReal)
    fun (x : ℝ) ↦ ‖(pdf X ℙ volume x).toReal‖ₑ

Tactic:
simp only [Real.enorm_eq_ofReal ENNReal.toReal_nonneg, ae_eq_refl]

Premises used: MeasureTheory.ae_eq_refl, ENNReal.toReal_nonneg, Real.enorm_eq_ofReal
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae (F := Measure ℝ) volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
⊢ (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞) (fun (x : ℝ) ↦ ‖f x‖ₑ * g x) fun (x : ℝ) ↦
    ‖f x * (pdf X ℙ volume x).toReal‖ₑ

Tactic:
have : (fun x => ‖f x‖ₑ * g x) =ᵐ[volume] fun x => ‖f x * (pdf X ℙ volume x).toReal‖ₑ := by
    refine ae_eq_trans ((ae_eq_refl _).fun_mul (ae_eq_trans hg.symm ofReal_toReal_ae_eq.symm)) ?_
    simp_rw [← smul_eq_mul, enorm_smul, smul_eq_mul]
    refine .fun_mul (ae_eq_refl _) ?_
    simp only [Real.enorm_eq_ofReal ENNReal.toReal_nonneg, ae_eq_refl]
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae (F := Measure ℝ) volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
this :
  (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞) (fun (x : ℝ) ↦ ‖f x‖ₑ * g x) fun (x : ℝ) ↦
    ‖f x * (pdf X ℙ volume x).toReal‖ₑ
rwa : ∫⁻ (a : ℝ), ‖f a * (pdf X ℙ volume a).toReal‖ₑ ≠ ∞
rwa₁ rwa₂ rwa₃ rwa₄ : ∫⁻ (a : ℝ), ‖f a‖ₑ * g a ≠ ∞
⊢ ∫⁻ (a : ℝ), ‖f a * (pdf X ℙ volume a).toReal‖ₑ < ∞

Tactic:
rwa [lt_top_iff_ne_top, ← lintegral_congr_ae this]

Premises used: lt_top_iff_ne_top, MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst_2 : IsFiniteMeasure ℙ
inst_3 : SigmaFinite μ
inst_4 : SigmaFinite ν
inst_5 : HasPDF (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν)
⊢ HasPDF X ℙ μ

Tactic:
have : HasPDF X ℙ μ := quasiMeasurePreserving_hasPDF' (μ := μ.prod ν) (fun ω ↦ (X ω, Y ω))
    quasiMeasurePreserving_fst
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst_2 : IsFiniteMeasure ℙ
inst_3 : SigmaFinite μ
inst_4 : SigmaFinite ν
inst_5 : HasPDF (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this : HasPDF X ℙ μ
⊢ HasPDF Y ℙ ν

Tactic:
have : HasPDF Y ℙ ν := quasiMeasurePreserving_hasPDF' (μ := μ.prod ν) (fun ω ↦ (X ω, Y ω))
    quasiMeasurePreserving_snd
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst_2 : IsFiniteMeasure ℙ
inst_3 : SigmaFinite μ
inst_4 : SigmaFinite ν
inst_5 : HasPDF (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this_1 : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
s : Set E
t : Set F
hs : MeasurableSet s
ht : MeasurableSet t
rw :
  ∫⁻ (a : E × F) in s ×ˢ t, pdf X ℙ μ a.1 * pdf Y ℙ ν a.2 ∂μ.prod ν =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ :
  ∫⁻ (a : E × F), pdf X ℙ μ a.1 * pdf Y ℙ ν a.2 ∂(μ.restrict s).prod (ν.restrict t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
rw₂ :
  (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * ∫⁻ (y : F) in t, pdf Y ℙ ν y ∂ν =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
rw₃ :
  (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * ∫⁻ (y : F) in t, pdf Y ℙ ν y ∂ν =
    HMul.hMul (β := ℝ≥0∞) (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
rw₄ rw₅ :
  (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * ∫⁻ (y : F) in t, pdf Y ℙ ν y ∂ν =
    (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * ∫⁻ (x : F) in t, pdf Y ℙ ν x ∂ν
⊢ ((μ.prod ν).withDensity fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2 : (a : Set (E × F)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)

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]

Premises used: Measurable.aemeasurable, MeasureTheory.measurable_pdf, MeasurableSet.prod, MeasureTheory.Measure.prod_restrict, MeasureTheory.map_eq_setLIntegral_pdf, MeasureTheory.lintegral_prod_mul, MeasureTheory.withDensity_apply
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst_2 : IsFiniteMeasure ℙ
inst_3 : SigmaFinite μ
inst_4 : SigmaFinite ν
inst_5 : HasPDF (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this_1 : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
⊢ Measure.prod (map X ℙ) (map Y ℙ) = (μ.prod ν).withDensity fun (z : E × F) ↦ 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]
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst_2 : IsFiniteMeasure ℙ
inst_3 : SigmaFinite μ
inst_4 : SigmaFinite ν
inst_5 : HasPDF (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this_1 : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
h₀ : Measure.prod (map X ℙ) (map Y ℙ) = (μ.prod ν).withDensity fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
hmf : AEMeasurable (β := ℝ≥0∞) (fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2) (μ.prod ν)
⊢ X ⟂ᵢ[ℙ] Y ↔
    pdf (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun (z : E × F) ↦ 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₀]

Premises used: MeasureTheory.pdf.eq_of_map_eq_withDensity, MeasureTheory.HasPDF.aemeasurable, ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst_2 : IsFiniteMeasure ℙ
inst_3 : SigmaFinite μ
inst_4 : SigmaFinite ν
inst_5 : HasPDF (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this_1 : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
h₀ : Measure.prod (map X ℙ) (map Y ℙ) = (μ.prod ν).withDensity fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2) (μ.prod ν)

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

Premises used: Measurable.mul, Measurable.aemeasurable, Measurable.comp, MeasureTheory.measurable_pdf, MeasureTheory.pdf, measurable_snd, measurable_fst
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst_2 : IsFiniteMeasure ℙ
inst_3 : SigmaFinite μ
inst_4 : SigmaFinite ν
inst_5 : HasPDF (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this_1 : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
h₀ : Measure.prod (map X ℙ) (map Y ℙ) = (μ.prod ν).withDensity fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : E × F) ↦ 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

Premises used: Measurable.mul, Measurable.aemeasurable, Measurable.comp, MeasureTheory.measurable_pdf, measurable_snd, measurable_fst
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
⊢ AEMeasurable X ℙ

Tactic:
have : AEMeasurable X ℙ := HasPDF.aemeasurable' μ
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this : AEMeasurable X ℙ
⊢ AEMeasurable Y ℙ

Tactic:
have : AEMeasurable Y ℙ := HasPDF.aemeasurable' μ
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this_1 : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ AEMeasurable (X * Y) ℙ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this_1 : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ AEMeasurable X ℙ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this_1 : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ AEMeasurable Y ℙ

Tactic:
fun_prop