Binary KL divergence and its boundary values

klBin p q = p·log(p/q) + (1 − p)·log((1 − p)/(1 − q)), the KL divergence between Bernoulli(p) and Bernoulli(q). Well-defined for q ∈ (0, 1); the boundary values at p = 0, p = 1, and p = q reduce to explicit log-terms via the conventional log 0 = 0.

noncomputable def InformationTheory.klBin (p q : ℝ) : ℝ

Binary KL divergence between Bernoulli(p) and Bernoulli(q).

Equations

• InformationTheory.klBin p q = p * Real.log (p / q) + (1 - p) * Real.log ((1 - p) / (1 - q))

theorem InformationTheory.klBin_self (p : ℝ) (hp₀ : 0 < p) (hp₁ : p < 1) : klBin p p = 0

klBin p p = 0 for p ∈ (0, 1).

theorem InformationTheory.klBin_zero_left (q : ℝ) : klBin 0 q = -Real.log (1 - q)

Boundary case: klBin 0 q = -log(1 - q).

theorem InformationTheory.klBin_one_left (q : ℝ) : klBin 1 q = -Real.log q

Boundary case: klBin 1 q = -log q.

theorem InformationTheory.klBin_expand (p q : ℝ) (hp₀ : 0 < p) (hp₁ : p < 1) (hq₀ : 0 < q) (hq₁ : q < 1) : klBin p q = p * Real.log p - p * Real.log q + (1 - p) * Real.log (1 - p) - (1 - p) * Real.log (1 - q)

Expanded form: split into constants and q-dependent pieces. Used to compute the derivative via HasDerivAt in the next shard.