English
For IsFinite ℙ and HasPDF X ℙ μ, and any f: E → F with AEStronglyMeasurable f μ, the smoothed pdf integrability condition is equivalent to the integrability of f ∘ X under ℙ.
Русский
Пусть ℙ конечно, HasPDF X ℙ μ; для любого f: E → F с AEStronglyMeasurable f μ, условие интегрируемости дела при умножении плотности на f эквивалентно интегрируемости f(X) по ℙ.
LaTeX
$$$\\text{AEStronglyMeasurable } f μ \\Rightarrow (\\text{Integrable } (pdf X ℙ μ x \\cdot f x) μ \\iff \\text{Integrable } (f (X x)) ℙ)$$$
Lean4
theorem integrable_pdf_smul_iff [IsFiniteMeasure ℙ] {X : Ω → E} [HasPDF X ℙ μ] {f : E → F}
(hf : AEStronglyMeasurable f μ) :
Integrable (fun x => (pdf X ℙ μ x).toReal • f x) μ ↔ Integrable (fun x => f (X x)) ℙ :=
by
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]
rw [withDensity_rnDeriv_eq _ _ HasPDF.absolutelyContinuous]
