English
KL divergence between two measures μ and ν is finite and given by the integral of the log-likelihood ratio when μ is absolutely continuous w.r.t. ν and llr μ ν is μ-integrable; otherwise it is infinite.
Русский
KL-дивергенция между мерами μ и ν равна интегралу по μ от лог-вероятности; если μ << ν и llr μ ν интегрируем по μ, иначе бесконечна.
LaTeX
$$$\\text{klDiv}(\\mu,\\nu) = \\begin{cases} \\mathrm{ENNReal.ofReal}\\left(\\int llr(\\mu,\\nu) \\, d\\mu\\right) & (\\mu \\ll \\nu \\\\ \\text{Integrable}_{\\mu}(llr(\\mu,\\nu))) \\\\ +\\infty & \\text{otherwise} \\end{cases}$$$
Lean4
instance : PseudoMetricSpace (Hamming β)
where
dist_self := by
push_cast
exact mod_cast hammingDist_self
dist_comm := by
push_cast
exact mod_cast hammingDist_comm
dist_triangle := by
push_cast
exact mod_cast hammingDist_triangle
toUniformSpace := ⊥
uniformity_dist :=
uniformity_dist_of_mem_uniformity _ _ fun s => by
push_cast
constructor
· refine fun hs => ⟨1, zero_lt_one, fun hab => ?_⟩
rw_mod_cast [hammingDist_lt_one] at hab
rw [ofHamming_inj, ← mem_idRel] at hab
exact hs hab
· rintro ⟨_, hε, hs⟩ ⟨_, _⟩ hab
rw [mem_idRel] at hab
rw [hab]
refine hs (lt_of_eq_of_lt ?_ hε)
exact mod_cast hammingDist_self _
toBornology := ⟨⊥, bot_le⟩
cobounded_sets := by
ext
push_cast
refine iff_of_true (Filter.mem_sets.mpr Filter.mem_bot) ⟨Fintype.card ι, fun _ _ _ _ => ?_⟩
exact mod_cast hammingDist_le_card_fintype
