theorem
proved
tactic proof
kl_divergence_nonneg
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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 ω
233 calc 0 = (∑ ω, q ω) - (∑ ω, p ω) := by rw [hq_sum, hp_sum, sub_self]
234 _ = ∑ ω, (q ω - p ω) := by rw [Finset.sum_sub_distrib]
235 _ ≤ ∑ ω, (if q ω > 0 ∧ p ω > 0 then q ω * log (q ω / p ω) else 0) := Finset.sum_le_sum (fun ω _ => h_le ω)
236
237
238
239/-! ## Connecting to RS: φ-Temperature Scale -/
240
241/-- The natural temperature scale in RS is set by the φ-ladder.
242 T_φ = J_bit = ln(φ) where φ is the golden ratio. -/