toReal_klDiv — Mathlib

English

If μ ≪ ν and Integrable(llr μ ν) μ, then (klDiv μ ν).toReal equals the integral form of llr.

Русский

Если μ ≪ ν и Integrable(llr μ ν) μ, то (klDiv μ ν).toReal равен интегральной форме llr.

LaTeX

$$$\\,(klDiv\\,μ\\,ν).toReal = \\int x\\, llr\\,μ\\,ν\\,x\\,∂μ + ν.real univ - μ.real univ$$$

Lean4

theorem toReal_klDiv (h : μ ≪ ν) (h_int : Integrable (llr μ ν) μ) :
    (klDiv μ ν).toReal = ∫ a, llr μ ν a ∂μ + ν.real univ - μ.real univ :=
  by
  rw [klDiv_of_ac_of_integrable h h_int, ENNReal.toReal_ofReal]
  exact integral_llr_add_sub_measure_univ_nonneg h h_int

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