hasPDF_of_map_eq_withDensity — Mathlib

English

If map X ℙ = μ.withDensity f for some a.e.-measurable f, then HasPDF X ℙ μ.

Русский

Если map X ℙ = μ.withDensity f для некоторой a.e.-измеримой f, тогда HasPDF X ℙ μ.

LaTeX

$$$map X \\ℙ = μ.withDensity f \\Rightarrow HasPDF X \\ℙ μ$$$

Lean4

/-- X `HasPDF` if there is a pdf `f` such that `map X ℙ = μ.withDensity f`. -/
theorem hasPDF_of_map_eq_withDensity (hX : AEMeasurable X ℙ) (f : E → ℝ≥0∞) (hf : AEMeasurable f μ)
    (h : map X ℙ = μ.withDensity f) : HasPDF X ℙ μ :=
  by
  refine ⟨hX, ?_, ?_⟩ <;> rw [h]
  · rw [withDensity_congr_ae hf.ae_eq_mk]
    exact haveLebesgueDecomposition_withDensity μ hf.measurable_mk
  · exact withDensity_absolutelyContinuous μ f

Похожие утверждения