Commit 2025-03-03 11:12 2ac93457

View on Github →

feat(InformationTheory): define the Kullback-Leibler divergence between two finite measures (#21053) From the TestingLowerBounds project.

Estimated changes

Modified Mathlib.lean

Created Mathlib/InformationTheory/KullbackLeibler/Basic.lean

added theorem InformationTheory.integral_llr_add_mul_log_nonneg

added theorem InformationTheory.integral_llr_add_sub_measure_univ_nonneg

added theorem InformationTheory.klDiv_eq_integral_klFun

added theorem InformationTheory.klDiv_eq_lintegral_klFun

added theorem InformationTheory.klDiv_eq_top_iff

added theorem InformationTheory.klDiv_eq_zero_iff

added theorem InformationTheory.klDiv_ne_top_iff

added theorem InformationTheory.klDiv_of_ac_of_integrable

added theorem InformationTheory.klDiv_of_not_ac

added theorem InformationTheory.klDiv_of_not_integrable

added theorem InformationTheory.klDiv_self

added theorem InformationTheory.klDiv_zero_left

added theorem InformationTheory.klDiv_zero_right

added theorem InformationTheory.mul_klFun_le_toReal_klDiv

added theorem InformationTheory.mul_log_le_klDiv

added theorem InformationTheory.mul_log_le_toReal_klDiv

added theorem InformationTheory.toReal_klDiv

added theorem InformationTheory.toReal_klDiv_eq_integral_klFun

added theorem InformationTheory.toReal_klDiv_of_measure_eq