lintegral_rnDeriv_mul — Mathlib

English

Under HaveLebesgueDecomposition and μ ≪ ν, for any AEMeasurable f, the left-hand lintegral with μ.rnDeriv ν times f over ν equals the right-hand lintegral of f over μ.

Русский

При разложении Лебега и μ ≪ ν, линтегральная формула через RN-дериватив сохраняется, когда умножаем на f и используем ν или μ.

LaTeX

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

Lean4

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

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