setLIntegral_rnDeriv_mul — Mathlib

English

A restricted version of the previous equality to a measurable set s: the ν-setLIntegral of μ.rnDeriv ν times f equals the μ-setLIntegral of f over s.

Русский

Ограниченная версия равенства на множества s: L-интеграл по ν плотности μ.rnDeriv ν умноженной на f равен L-интегралу по μ на s.

LaTeX

$$$$ \int_{x \in s} μ.rnDeriv ν x \cdot f(x) \, dν = \int_{x \in s} f(x) \, dμ $$$$

Lean4

theorem setLIntegral_rnDeriv_mul [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) {f : α → ℝ≥0∞} (hf : AEMeasurable f ν)
    {s : Set α} (hs : MeasurableSet s) : ∫⁻ x in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ x in s, f x ∂μ :=
  by
  nth_rw 2 [← Measure.withDensity_rnDeriv_eq μ ν hμν]
  rw [setLIntegral_withDensity_eq_lintegral_mul₀ (measurable_rnDeriv μ ν).aemeasurable hf hs]
  simp only [Pi.mul_apply]

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