awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : ¬AEMeasurable X ℙ
⊢ pdf X ℙ μ =ᶠ[ae μ] 0
have rw : rnDeriv 0 μ =ᶠ[ae μ] 0
Tactic: rw [pdf_def, map_of_not_aemeasurable hX]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : ¬pdf X ℙ μ =ᶠ[ae μ] 0
⊢ AEMeasurable X ℙ
have contrapose : ∀ (h : ¬AEMeasurable X ℙ), pdf X ℙ μ =ᶠ[ae μ] 0
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬pdf X ℙ μ =ᶠ[ae μ] 0
⊢ HasPDF X ℙ μ
have refine_1 : AEMeasurable X ℙ
Tactic: refine ⟨?_, ?_, hac⟩
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬pdf X ℙ μ =ᶠ[ae μ] 0
refine_1 : AEMeasurable X ℙ
⊢ HasPDF X ℙ μ
have refine_2 : HaveLebesgueDecomposition (map X ℙ) μ
Tactic: refine ⟨?_, ?_, hac⟩
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬pdf X ℙ μ =ᶠ[ae μ] 0
⊢ HaveLebesgueDecomposition (map X ℙ) μ
have refine_2 : ∀ (hpdf : ¬HaveLebesgueDecomposition (map X ℙ) μ), pdf X ℙ μ =ᶠ[ae μ] 0
Tactic: contrapose hpdf
Cleared hypotheses: hpdf
-- Lean 4 proof step from Mathlib.Probability.Density (hypothesis)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬HaveLebesgueDecomposition (map X ℙ) μ
⊢ pdf X ℙ μ =ᶠ[ae μ] 0
have this : pdf X ℙ μ = 0
Tactic: have := pdf_of_not_haveLebesgueDecomposition hpdf
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬HaveLebesgueDecomposition (map X ℙ) μ
this : pdf X ℙ μ = 0
⊢ pdf X ℙ μ =ᶠ[ae μ] 0
have refine_2 : ∀ (a : E), Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ pdf X ℙ μ x = 0 x) x} a
Tactic: filter_upwards using congrFun this
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬HaveLebesgueDecomposition (map X ℙ) μ
this : pdf X ℙ μ = 0
refine_2 : ∀ (a : E), Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ pdf X ℙ μ x = 0 x) x} a
⊢ pdf X ℙ μ =ᶠ[ae μ] 0
have refine_2₁ : ∀ (a : E), pdf X ℙ μ a = 0 a
Tactic: filter_upwards using congrFun this
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
⊢ ∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ ≤ ((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s
have apply : LE.le (α := ℝ≥0∞) ((μ.withDensity (pdf X ℙ μ) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
  (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: apply (withDensity_apply_le _ s).trans
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : HasPDF X ℙ μ
⊢ map X ℙ = μ.withDensity (pdf X ℙ μ)
have rw : map X ℙ = μ.withDensity (rnDeriv (map X ℙ) μ)
Tactic: rw [pdf_def, withDensity_rnDeriv_eq _ _ hX.absolutelyContinuous]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : HasPDF X ℙ μ
rw : map X ℙ = μ.withDensity (rnDeriv (map X ℙ) μ)
⊢ map X ℙ = μ.withDensity (pdf X ℙ μ)
have rw₁ : Eq (α := Measure E) (map X ℙ) (map X ℙ)
Tactic: rw [pdf_def, withDensity_rnDeriv_eq _ _ hX.absolutelyContinuous]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : HasPDF X ℙ μ
s : Set E
hs : MeasurableSet s
⊢ ((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s = ∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ
have rw : Eq (α := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
  ((μ.withDensity (pdf X ℙ μ) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← withDensity_apply _ hs, map_eq_withDensity_pdf X ℙ μ]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : HasPDF X ℙ μ
s : Set E
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity (pdf X ℙ μ) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s = ∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ
have rw₁ : Eq (α := ℝ≥0∞) ((μ.withDensity (pdf X ℙ μ) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
  ((μ.withDensity (pdf X ℙ μ) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← withDensity_apply _ hs, map_eq_withDensity_pdf X ℙ μ]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X Y : Ω → E
hXY : X =ᶠ[ae ℙ] Y
⊢ pdf X ℙ μ = pdf Y ℙ μ
have rw : rnDeriv (map X ℙ) μ = pdf Y ℙ μ
Tactic: rw [pdf_def, pdf_def, map_congr hXY]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X Y : Ω → E
hXY : X =ᶠ[ae ℙ] Y
rw : rnDeriv (map X ℙ) μ = pdf Y ℙ μ
⊢ pdf X ℙ μ = pdf Y ℙ μ
have rw₁ : rnDeriv (map X ℙ) μ = rnDeriv (map Y ℙ) μ
Tactic: rw [pdf_def, pdf_def, map_congr hXY]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X Y : Ω → E
hXY : X =ᶠ[ae ℙ] Y
rw : rnDeriv (map X ℙ) μ = pdf Y ℙ μ
rw₁ : rnDeriv (map X ℙ) μ = rnDeriv (map Y ℙ) μ
⊢ pdf X ℙ μ = pdf Y ℙ μ
have rw₂ : rnDeriv (map Y ℙ) μ = rnDeriv (map Y ℙ) μ
Tactic: rw [pdf_def, pdf_def, map_congr hXY]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst_1 : HasPDF X ℙ μ
⊢ ∫⁻ (x : E), pdf X ℙ μ x ∂μ = (ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ
have rw : ∫⁻ (x : E) in Set.univ, pdf X ℙ μ x ∂μ = (ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ
Tactic: rw [← setLIntegral_univ, ← map_eq_setLIntegral_pdf X ℙ μ MeasurableSet.univ,
    map_apply_of_aemeasurable (HasPDF.aemeasurable X ℙ μ) MeasurableSet.univ, Set.preimage_univ]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst_1 : HasPDF X ℙ μ
rw : ∫⁻ (x : E) in Set.univ, pdf X ℙ μ x ∂μ = (ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ
⊢ ∫⁻ (x : E), pdf X ℙ μ x ∂μ = (ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ
have rw₁ : Eq (α := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: rw [← setLIntegral_univ, ← map_eq_setLIntegral_pdf X ℙ μ MeasurableSet.univ,
    map_apply_of_aemeasurable (HasPDF.aemeasurable X ℙ μ) MeasurableSet.univ, Set.preimage_univ]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst_1 : HasPDF X ℙ μ
rw : ∫⁻ (x : E) in Set.univ, pdf X ℙ μ x ∂μ = (ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ
rw₁ :
  Eq (α := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ ∫⁻ (x : E), pdf X ℙ μ x ∂μ = (ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ
have rw₂ : Eq (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' Set.univ) : ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: rw [← setLIntegral_univ, ← map_eq_setLIntegral_pdf X ℙ μ MeasurableSet.univ,
    map_apply_of_aemeasurable (HasPDF.aemeasurable X ℙ μ) MeasurableSet.univ, Set.preimage_univ]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst_1 : HasPDF X ℙ μ
rw : ∫⁻ (x : E) in Set.univ, pdf X ℙ μ x ∂μ = (ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ
rw₁ :
  Eq (α := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
rw₂ : Eq (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' Set.univ) : ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ ∫⁻ (x : E), pdf X ℙ μ x ∂μ = (ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ
have rw₃ : Eq (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: rw [← setLIntegral_univ, ← map_eq_setLIntegral_pdf X ℙ μ MeasurableSet.univ,
    map_apply_of_aemeasurable (HasPDF.aemeasurable X ℙ μ) MeasurableSet.univ, Set.preimage_univ]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst_1 : IsFiniteMeasure ℙ
X : Ω → E
inst_2 : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ map X ℙ = μ.withDensity f ↔ pdf X ℙ μ =ᶠ[ae μ] f
have rw : μ.withDensity (pdf X ℙ μ) = μ.withDensity f ↔ pdf X ℙ μ =ᶠ[ae μ] f
Tactic: rw [map_eq_withDensity_pdf X ℙ μ]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst_1 : IsFiniteMeasure ℙ
X : Ω → E
inst_2 : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ μ.withDensity (pdf X ℙ μ) = μ.withDensity f ↔ pdf X ℙ μ =ᶠ[ae μ] f
have apply : ∫⁻ (x : E), pdf X ℙ μ x ∂μ ≠ ∞
Tactic: apply withDensity_eq_iff (measurable_pdf X ℙ μ).aemeasurable hmf
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst_1 : IsFiniteMeasure ℙ
X : Ω → E
inst_2 : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ ∫⁻ (x : E), pdf X ℙ μ x ∂μ ≠ ∞
have rw : Ne (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [lintegral_eq_measure_univ]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst_1 : HasPDF X ℙ μ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (x : E), pdf X ℙ μ x * f x ∂μ = ∫⁻ (x : Ω), f (X x) ∂ℙ
have rw : ∫⁻ (x : E), rnDeriv (map X ℙ) μ x * f x ∂μ = ∫⁻ (x : Ω), f (X x) ∂ℙ
Tactic: rw [pdf_def,
    ← lintegral_map' (hf.mono_ac HasPDF.absolutelyContinuous) (HasPDF.aemeasurable X ℙ μ),
    lintegral_rnDeriv_mul HasPDF.absolutelyContinuous hf]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst_1 : HasPDF X ℙ μ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
rw : ∫⁻ (x : E), rnDeriv (map X ℙ) μ x * f x ∂μ = ∫⁻ (x : Ω), f (X x) ∂ℙ
⊢ ∫⁻ (x : E), pdf X ℙ μ x * f x ∂μ = ∫⁻ (x : Ω), f (X x) ∂ℙ
have rw₁ : ∫⁻ (x : E), rnDeriv (map X ℙ) μ x * f x ∂μ = ∫⁻ (a : E), f a ∂map X ℙ
Tactic: rw [pdf_def,
    ← lintegral_map' (hf.mono_ac HasPDF.absolutelyContinuous) (HasPDF.aemeasurable X ℙ μ),
    lintegral_rnDeriv_mul HasPDF.absolutelyContinuous hf]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst_1 : HasPDF X ℙ μ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
rw : ∫⁻ (x : E), rnDeriv (map X ℙ) μ x * f x ∂μ = ∫⁻ (x : Ω), f (X x) ∂ℙ
rw₁ : ∫⁻ (x : E), rnDeriv (map X ℙ) μ x * f x ∂μ = ∫⁻ (a : E), f a ∂map X ℙ
⊢ ∫⁻ (x : E), pdf X ℙ μ x * f x ∂μ = ∫⁻ (x : Ω), f (X x) ∂ℙ
have rw₂ : ∫⁻ (x : E), f x ∂map X ℙ = ∫⁻ (a : E), f a ∂map X ℙ
Tactic: rw [pdf_def,
    ← lintegral_map' (hf.mono_ac HasPDF.absolutelyContinuous) (HasPDF.aemeasurable X ℙ μ),
    lintegral_rnDeriv_mul HasPDF.absolutelyContinuous hf]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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 μ
⊢ Integrable.{u_3, u_2} (ε := F) (fun (x : E) ↦ (pdf X ℙ μ x).toReal • f x) μ ↔
    Integrable.{u_3, u_1} (ε := F) (fun (x : Ω) ↦ f (X x)) ℙ
have rw : @Integrable _ _ _ _ inst f (map X ℙ) ↔ Integrable f (μ.withDensity (rnDeriv (map X ℙ) μ))
Tactic: rw [← Function.comp_def,
    ← integrable_map_measure (hf.mono_ac HasPDF.absolutelyContinuous) (HasPDF.aemeasurable X ℙ μ),
    map_eq_withDensity_pdf X ℙ μ, pdf_def, integrable_rnDeriv_smul_iff HasPDF.absolutelyContinuous]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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 μ
⊢ @Integrable _ _ _ _ inst f (map X ℙ) ↔ Integrable f (μ.withDensity (rnDeriv (map X ℙ) μ))
have rw : @Integrable _ _ _ _ inst f (map X ℙ) ↔ @Integrable _ _ _ _ inst f (map X ℙ)
Tactic: rw [withDensity_rnDeriv_eq _ _ HasPDF.absolutelyContinuous]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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 μ
⊢ Eq.{u_3 + 1} (α := F) (∫ (x : E), (pdf X ℙ μ x).toReal • f x ∂μ) (∫ (x : Ω), f (X x) ∂ℙ)
have rw : Eq.{u_3 + 1} (α := F) (∫ (x : E), (pdf X ℙ μ x).toReal • f x ∂μ) (@integral _ _ _ _ inst (map X ℙ) fun (y : E) ↦ f y)
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]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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)
⊢ Eq.{u_3 + 1} (α := F) (∫ (x : E), (pdf X ℙ μ x).toReal • f x ∂μ) (∫ (x : Ω), f (X x) ∂ℙ)
have rw₁ : Eq.{u_3 + 1} (α := F) (∫ (x : E), (pdf X ℙ μ x).toReal • f x ∂μ) (∫ (y : E), f y ∂μ.withDensity (pdf 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]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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 ℙ μ))
⊢ Eq.{u_3 + 1} (α := F) (∫ (x : E), (pdf X ℙ μ x).toReal • f x ∂μ) (∫ (x : Ω), f (X x) ∂ℙ)
have rw₂ : Eq.{u_3 + 1} (α := F) (∫ (x : E), (rnDeriv (map X ℙ) μ x).toReal • f x ∂μ)
  (∫ (y : E), f y ∂μ.withDensity (rnDeriv (map 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]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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 ℙ) μ))
⊢ Eq.{u_3 + 1} (α := F) (∫ (x : E), (pdf X ℙ μ x).toReal • f x ∂μ) (∫ (x : Ω), f (X x) ∂ℙ)
have rw₃ : Eq.{u_3 + 1} (α := F) (@integral _ _ _ _ inst (map X ℙ) fun (x : E) ↦ f x)
  (∫ (y : E), f y ∂μ.withDensity (rnDeriv (map 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]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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 ℙ) μ))
⊢ Eq.{u_3 + 1} (α := F) (∫ (x : E), (pdf X ℙ μ x).toReal • f x ∂μ) (∫ (x : Ω), f (X x) ∂ℙ)
have rw₄ : Eq.{u_3 + 1} (α := F) (@integral _ _ _ _ inst (map X ℙ) fun (x : E) ↦ f x)
  (@integral _ _ _ _ inst (map X ℙ) fun (y : E) ↦ f y)
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]
-- Lean 4 proof step from Mathlib.Probability.Density (hypothesis)
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 ℙ)) ν
⊢ HasPDF (g ∘ X) ℙ ν
have hgm : AEMeasurable (_m := inst) g (map X ℙ)
Tactic: have hgm : AEMeasurable g (map X ℙ) := hg.aemeasurable.mono_ac HasPDF.absolutelyContinuous
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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 ℙ)
⊢ HasPDF (g ∘ X) ℙ ν
have rw : AEMeasurable (g ∘ X) ℙ ∧ HaveLebesgueDecomposition (map g (map X ℙ)) ν ∧ map g (map X ℙ) ≪ ν
Tactic: rw [hasPDF_iff, ← AEMeasurable.map_map_of_aemeasurable hgm (HasPDF.aemeasurable X ℙ μ)]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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 ℙ) ≪ ν
have refine : map g (map X ℙ) ≪ ν
Tactic: refine ⟨hg.measurable.comp_aemeasurable (HasPDF.aemeasurable _ _ μ), hmap, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : SFinite ℙ
⊢ HasPDF X ℙ volume ↔ AEMeasurable X ℙ ∧ AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume
have 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
Tactic: rw [hasPDF_iff, and_iff_right (inferInstance : HaveLebesgueDecomposition _ _)]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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
⊢ HasPDF X ℙ volume ↔ AEMeasurable X ℙ ∧ AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume
have rw₁ : AEMeasurable X ℙ ∧ AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume ↔
  AEMeasurable X ℙ ∧ AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume
Tactic: rw [hasPDF_iff, and_iff_right (inferInstance : HaveLebesgueDecomposition _ _)]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : SFinite ℙ
hX : AEMeasurable X ℙ
⊢ HasPDF X ℙ volume ↔ AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume
have rw : AEMeasurable X ℙ ∧ AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume ↔
  AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume
Tactic: rw [Real.hasPDF_iff, and_iff_right hX]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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
⊢ HasPDF X ℙ volume ↔ AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume
have rw₁ : AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume ↔
  AbsolutelyContinuous (_m0 := Real.measurableSpace) (map X ℙ) volume
Tactic: rw [Real.hasPDF_iff, and_iff_right hX]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
inst_1 : HasPDF X ℙ volume
⊢ 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)
have e_f : ∀ (x : ℝ), x * (pdf X ℙ volume x).toReal = (pdf X ℙ volume x).toReal * x
Tactic: congr with x