English
**The Law of the Unconscious Statistician** for nonnegative random variables: the expectation of f ∘ X equals the integral of f against the distribution induced by X.
Русский
**Закон неосознанной статистики** для неотрицательных случайных величин: ожидание f(X) равно интегралу f по распределению, индуцированному X.
LaTeX
$$$\\int⁻ x, pdf X \\ℙ μ x \\cdot f x \\; dμ = \\int⁻ x, f(X x) \\; d\\ℙ$$$
Lean4
/-- **The Law of the Unconscious Statistician** for nonnegative random variables. -/
theorem lintegral_pdf_mul {X : Ω → E} [HasPDF X ℙ μ] {f : E → ℝ≥0∞} (hf : AEMeasurable f μ) :
∫⁻ x, pdf X ℙ μ x * f x ∂μ = ∫⁻ x, f (X x) ∂ℙ := by
rw [pdf_def, ← lintegral_map' (hf.mono_ac HasPDF.absolutelyContinuous) (HasPDF.aemeasurable X ℙ μ),
lintegral_rnDeriv_mul HasPDF.absolutelyContinuous hf]
