kl_divergence_nonneg

formal source

 199
 200/-- KL divergence is non-negative (Gibbs' inequality).
 201    D_KL(q || p) ≥ 0 with equality iff q = p. -/
 202theorem kl_divergence_nonneg {Ω : Type*} [Fintype Ω]
 203    (q p : Ω → ℝ) (hq : ∀ ω, 0 ≤ q ω) (hp : ∀ ω, 0 < p ω)
 204    (hq_sum : ∑ ω, q ω = 1) (hp_sum : ∑ ω, p ω = 1) :
 205    0 ≤ kl_divergence q p := by
 206  unfold kl_divergence
 207  -- Use log x ≤ x - 1, which implies -log x ≥ 1 - x
 208  -- q log (q/p) = -q log (p/q) ≥ q (1 - p/q) = q - p
 209  have h_le : ∀ ω, (if q ω > 0 ∧ p ω > 0 then q ω * log (q ω / p ω) else 0) ≥ q ω - p ω := by
 210    intro ω
 211    split_ifs with h
 212    · -- case q ω > 0 and p ω > 0
 213      obtain ⟨hq_pos, hp_pos⟩ := h
 214      have hr_pos : 0 < p ω / q ω := div_pos hp_pos hq_pos
 215      have : log (q ω / p ω) ≥ 1 - p ω / q ω := by
 216        rw [log_div hq_pos.ne' hp_pos.ne']
 217        have h_log_le := log_le_sub_one_of_pos hr_pos
 218        rw [log_div hp_pos.ne' hq_pos.ne'] at h_log_le
 219        linarith
 220      have hq_q : q ω * log (q ω / p ω) ≥ q ω * (1 - p ω / q ω) := by
 221        apply mul_le_mul_of_nonneg_left this hq_pos.le
 222      rw [mul_sub, mul_one, mul_div_cancel₀ _ hq_pos.ne'] at hq_q
 223      exact hq_q
 224    · -- case q ω ≤ 0 or p ω ≤ 0
 225      have hq0 : q ω = 0 := by
 226        have : ¬ (q ω > 0 ∧ p ω > 0) := h
 227        simp only [hp ω, and_true, not_lt] at this
 228        exact le_antisymm this (hq ω)
 229      rw [hq0]
 230      linarith [hp ω]
 231
 232  -- Sum over all ω