English
If μ ≪ ν and μ(univ) = ν(univ), then (klDiv μ ν).toReal equals ∫ llr μ ν dμ; if llr is not integrable, the equality is interpreted via undefined integral.
Русский
Если μ ≪ ν и μ(univ) = ν(univ), то (klDiv μ ν).toReal равно ∫ llr μ ν dμ; при неинтегрируемости интеграл трактуется как неопределённый.
LaTeX
$$$(klDiv\\,μ\\,ν).toReal = \\int a\\, llr\\,μ\\,ν\\,a\\,∂μ$ при $μ\\ll ν$ и $μ(univ)=ν(univ)$, с корректировкой при отсутствии интегрируемости llr$$
Lean4
/-- **Gibbs' inequality**: the Kullback-Leibler divergence is nonnegative.
Note that since `klDiv` takes value in `ℝ≥0∞` (defined when it is finite as `ENNReal.ofReal (...)`),
it is nonnegative by definition. This lemma proves that the argument of `ENNReal.ofReal`
is also nonnegative. -/
theorem integral_llr_add_sub_measure_univ_nonneg (hμν : μ ≪ ν) (h_int : Integrable (llr μ ν) μ) :
0 ≤ ∫ x, llr μ ν x ∂μ + ν.real univ - μ.real univ :=
by
rw [← integral_klFun_rnDeriv hμν h_int]
exact integral_nonneg fun x ↦ klFun_nonneg ENNReal.toReal_nonneg
