toReal_klDiv_of_measure_eq — Mathlib

English

If μ ≪ ν and Integrable(llr μ ν) μ, then (klDiv μ ν).toReal equals ∫ ν klFun (μ.rnDeriv ν x).toReal dν.

Русский

Если μ ≪ ν и Integrable(llr μ ν) μ, то (klDiv μ ν).toReal равно ∫ ν klFun (μ.rnDeriv ν x).toReal dν.

LaTeX

$$$(klDiv\\,μ\\,ν).toReal = \\int_ν klFun\\left( (μ.rnDeriv ν x).toReal \\right) \\,∂ν$$$

Lean4

/-- If `μ ≪ ν` and `μ univ = ν univ`, then `toReal` of the Kullback-Leibler divergence is equal to
an integral, without any integrability condition. -/
theorem toReal_klDiv_of_measure_eq (h : μ ≪ ν) (h_eq : μ univ = ν univ) : (klDiv μ ν).toReal = ∫ a, llr μ ν a ∂μ :=
  by
  by_cases h_int : Integrable (llr μ ν) μ
  · simp [toReal_klDiv h h_int, h_eq, measureReal_def]
  · rw [klDiv_of_not_integrable h_int, integral_undef h_int, ENNReal.toReal_top]

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