English
KL divergence equals zero if and only if μ = ν for finite measures.
Русский
KL-дивергенция равна нулю тогда и только тогда, когда μ = ν для конечных мер.
LaTeX
$$[IsFiniteMeasure μ] [IsFiniteMeasure ν] : klDiv μ ν = 0 ↔ μ = ν$$
Lean4
/-- **Converse Gibbs' inequality**: the Kullback-Leibler divergence between two finite measures is
zero if and only if the two measures are equal. -/
theorem klDiv_eq_zero_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] : klDiv μ ν = 0 ↔ μ = ν :=
by
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ klDiv_self _⟩
have h_ne : klDiv μ ν ≠ ⊤ := by simp [h]
rw [klDiv_ne_top_iff] at h_ne
rw [klDiv_eq_lintegral_klFun, if_pos h_ne.1, lintegral_eq_zero_iff (by fun_prop)] at h
refine (Measure.rnDeriv_eq_one_iff_eq h_ne.1).mp ?_
filter_upwards [h] with x hx
simp only [Pi.zero_apply, ENNReal.ofReal_eq_zero] at hx
have hx' : klFun (μ.rnDeriv ν x).toReal = 0 := le_antisymm hx (klFun_nonneg ENNReal.toReal_nonneg)
rwa [klFun_eq_zero_iff ENNReal.toReal_nonneg, ENNReal.toReal_eq_one_iff] at hx'
