integrable_rnDeriv_mul_log_iff — Mathlib

English

With σ-finite μ and ν having Lebesgue decomposition relative to μ, the integrability of (μ.rnDeriv ν)·log((μ.rnDeriv ν)) and llr(μ, ν) are equivalent with respect to the appropriate measures.

Русский

При наличии конечной меры μ и разложения Лебега ν относительно μ, взаимозависимость интегрируемости (μ.rnDeriv ν)·log((μ.rnDeriv ν)) и llr(μ, ν) равна между мерами ν и μ.

LaTeX

$$$\\text{Integrable}\\left( (\\mu\\r nDeriv\\nu)\\!^{\\toReal} \\cdot \\log((\\mu\\r nDeriv\\nu)\\!^{\\toReal})\\right)_{\\nu} \\\\iff \\\\ \\text{Integrable}(\\llr(\\mu, \\nu))_{\\mu}$$$

Lean4

theorem integrable_rnDeriv_mul_log_iff [SigmaFinite μ] [μ.HaveLebesgueDecomposition ν] (hμν : μ ≪ ν) :
    Integrable (fun a ↦ (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal) ν ↔ Integrable (llr μ ν) μ :=
  integrable_rnDeriv_smul_iff hμν

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