kl_nonneg

formal source

  66
  67We prove the inequality directly using `Real.log_le_sub_one_of_pos`. -/
  68
  69theorem kl_nonneg (p q : ProbDist ι) :
  70    0 ≤ ∑ i, p.prob i * Real.log (p.prob i / q.prob i) := by
  71  -- Equivalent: sum_i p_i log(p_i/q_i) >= 0
  72  -- Use log(x) >= 1 - 1/x (i.e. -log(1/x) <= 1 - 1/x → log(x) >= 1 - 1/x).
  73  -- Equivalent statement: -KL = sum p log(q/p) <= sum p (q/p - 1) = sum q - sum p = 0.
  74  -- So KL >= 0 follows.
  75  have h_neg_kl_le : ∑ i, p.prob i * Real.log (q.prob i / p.prob i) ≤ 0 := by
  76    have h_each : ∀ i, p.prob i * Real.log (q.prob i / p.prob i) ≤
  77        p.prob i * (q.prob i / p.prob i - 1) := by
  78      intro i
  79      have hp := p.prob_pos i
  80      have hq := q.prob_pos i
  81      have hratio_pos : 0 < q.prob i / p.prob i := div_pos hq hp
  82      have hlog_le : Real.log (q.prob i / p.prob i) ≤ q.prob i / p.prob i - 1 :=
  83        Real.log_le_sub_one_of_pos hratio_pos
  84      exact mul_le_mul_of_nonneg_left hlog_le (le_of_lt hp)
  85    calc ∑ i, p.prob i * Real.log (q.prob i / p.prob i)
  86        ≤ ∑ i, p.prob i * (q.prob i / p.prob i - 1) := Finset.sum_le_sum (fun i _ => h_each i)
  87      _ = ∑ i, (q.prob i - p.prob i) := by
  88          apply Finset.sum_congr rfl
  89          intro i _
  90          have hp := p.prob_pos i
  91          field_simp
  92      _ = (∑ i, q.prob i) - ∑ i, p.prob i := by rw [Finset.sum_sub_distrib]
  93      _ = 1 - 1 := by rw [q.prob_sum, p.prob_sum]
  94      _ = 0 := by ring
  95  have h_log_swap : ∀ i, Real.log (q.prob i / p.prob i) = -Real.log (p.prob i / q.prob i) := by
  96    intro i
  97    have hp := p.prob_pos i
  98    have hq := q.prob_pos i
  99    rw [show q.prob i / p.prob i = (p.prob i / q.prob i)⁻¹ by