pith. machine review for the scientific record. sign in
def definition def or abbrev

kl_divergence

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 197noncomputable def kl_divergence {Ω : Type*} [Fintype Ω] (q p : Ω → ℝ) : ℝ :=

proof body

Definition body.

 198  ∑ ω, if q ω > 0 ∧ p ω > 0 then q ω * log (q ω / p ω) else 0
 199
 200/-- KL divergence is non-negative (Gibbs' inequality).
 201    D_KL(q || p) ≥ 0 with equality iff q = p. -/

used by (18)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.