English
Let μ and ν be measures on a space with μ absolutely continuous with respect to ν, and suppose llr μ ν is μ-integrable. Then the Kullback–Leibler divergence KL(μ, ν) equals ENNReal.ofReal of the sum of the integral of llr μ ν with respect to μ and the difference ν.real(univ) − μ.real(univ).
Русский
Пусть μ и ν — меры на некотором пространстве, причем μ абсолютно непрерывна по ν, и llr μ ν интегрируем по μ. Тогда дивергенция Кульбак–Лейблера KL(μ, ν) равна ENNReal.ofReal суммы интеграла llr μ ν по μ и разности ν.real(univ) − μ.real(univ).
LaTeX
$$$klDiv\\,\\mu\\,\\nu = ENNReal.ofReal\\left(\\int x\\, llr\\,\\mu\\,\\nu\\,x\\, \\partial\\mu + \\nu.real univ - \\mu.real univ\\right)$$$
Lean4
theorem klDiv_of_ac_of_integrable (h1 : μ ≪ ν) (h2 : Integrable (llr μ ν) μ) :
klDiv μ ν = ENNReal.ofReal (∫ x, llr μ ν x ∂μ + ν.real univ - μ.real univ) :=
by
rw [klDiv_def]
exact if_pos ⟨h1, h2⟩
