integral_rnDeriv_mul_log — Mathlib

English

If μ ≪ ν and both measures have a Lebesgue decomposition, then the integral of (μ.rnDeriv ν)^{toReal}·log((μ.rnDeriv ν)^{toReal}) with respect to ν equals the integral of llr(μ, ν) with respect to μ.

Русский

Пусть μ ≪ ν и имеются разложения Лебега. Тогда интеграл (μ.rnDeriv ν)^{toReal}·log((μ.rnDeriv ν)^{toReal}) по ν равен интегралу llr(μ, ν) по μ.

LaTeX

$$$\\int (μ.rnDeriv ν)^{\\toReal} \\log((μ.rnDeriv ν)^{\\toReal}) \\, dν = \\int llr(μ, ν) \\, dμ$$$

Lean4

theorem integral_rnDeriv_mul_log [SigmaFinite μ] [μ.HaveLebesgueDecomposition ν] (hμν : μ ≪ ν) :
    ∫ a, (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν = ∫ a, llr μ ν a ∂μ := by
  simp_rw [← smul_eq_mul, integral_rnDeriv_smul hμν, llr]

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