klDiv_eq_integral_klFun — Mathlib

English

If μ and ν are finite measures, then KL(μ, ν) equals ENNReal.ofReal (∫ ν klFun (μ.rnDeriv ν x).toReal dν) on the AC case, otherwise ∞.

Русский

Если μ и ν конечны, KL(μ, ν) равно ENNReal.ofReal ∫ ν klFun(μ.rnDeriv ν x).toReal dν на случае AC; иначе ∞.

LaTeX

$$$klDiv\\,μ\\,ν = \\text{if } μ \\ll ν \\land Integrable(llr\\,μ\\,ν)\\,μ\\text{ then } ENNReal.ofReal\\left(\\int_ν klFun(μ.rnDeriv\nν x).toReal\\right) else ∞$$

Lean4

theorem klDiv_eq_integral_klFun :
    klDiv μ ν = if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ x, klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞ :=
  by
  rw [klDiv_def]
  exact if_ctx_congr Iff.rfl (fun h ↦ by rw [integral_klFun_rnDeriv h.1 h.2]) fun _ ↦ rfl

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