English
The KL divergence is defined via the log-likelihood ratio when the first measure is absolutely continuous with respect to the second and the log-likelihood ratio is integrable; otherwise it takes an infinite value.
Русский
KL-дивергенция задаётся через отношение правдоподобности (лог-вероятностную функцию) при условии абсолютной непротивоположности одной меры другой и интегрируемости; иначе равно бесконечности.
LaTeX
$$$$\\mathrm{klDiv}(\\mu,\\nu) = \\begin{cases} \\text{finite real value given by } \\int llr(\\mu,\\nu) \\, d\\mu, \\\\ \\text{otherwise } +\\infty. \\end{cases}$$$$
Lean4
theorem klDiv_def : eta_helper Eq✝ @klDiv.{} @(delta% @definition✝) :=
by
intros
delta klDiv
rw [show wrapped✝ = ⟨@definition✝.{}, rfl✝⟩ from Subtype.ext✝ wrapped✝.2.symm✝]
rfl
