klFun — Mathlib

English

If μ ≪ ν and μ univ = ν univ, then (klDiv μ ν).toReal equals ∫ llr μ ν dμ; if llr not integrable, the integral is interpreted accordingly.

Русский

Если μ ≪ ν и μ univ = ν univ, то (klDiv μ ν).toReal равно ∫ llr μ ν dμ; если llr не интегрируем, трактуется соответствующим образом.

LaTeX

$$$(klDiv\\,μ\\,ν).toReal = ∫ a\\, llr\\,μ\\,ν\\,a \\,∂μ$$$

Lean4

/-- The function `x : ℝ ↦ x * log x + 1 - x`.
The Kullback-Leibler divergence is an f-divergence for this function. -/
noncomputable def klFun (x : ℝ) : ℝ :=
  x * log x + 1 - x

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