English
If hg is a quasi-measure-preserving map and the pushforward of X has Lebesgue decomposition with ν, then HasPDF (g ∘ X) from Ω to F holds with respect to ν.
Русский
Если g — квази-измеримо-представляющее отображение, и (map g (map X ℙ)).HaveLebesgueDecomposition ν, то HasPDF (g ∘ X) ℙ ν выполняется.
LaTeX
$$$\\text{(hg : QuasiMeasurePreserving g μ ν)} \\land \\text{(hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν)} \\Rightarrow HasPDF (g \\circ X) ℙ ν$$$
Lean4
/-- **The Law of the Unconscious Statistician**: Given a random variable `X` and a measurable
function `f`, `f ∘ X` is a random variable with expectation `∫ x, pdf X x • f x ∂μ`
where `μ` is a measure on the codomain of `X`. -/
theorem integral_pdf_smul [IsFiniteMeasure ℙ] {X : Ω → E} [HasPDF X ℙ μ] {f : E → F} (hf : AEStronglyMeasurable f μ) :
∫ x, (pdf X ℙ μ x).toReal • f x ∂μ = ∫ x, f (X x) ∂ℙ := by
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]
