feat(InformationTheory): define the Kullback-Leibler divergence between two finite measures

[RemyDegenne]

WIP

From the TestingLowerBounds project.
Co-authored-by: Lorenzo Luccioli

---

• depends on: feat: left and right derivatives of a convex function #21063
• depends on: [Merged by Bors] - feat: derivWithin lemmas #21092
• depends on: [Merged by Bors] - feat: inequality on the integral of a convex function of a RN derivative #21093

[github-actions]

PR summary 57df557ba9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.InformationTheory.KullbackLeibler.KLFun (new file)	2037
Mathlib.InformationTheory.KullbackLeibler.Basic (new file)	2042

---

Declarations diff

+ ConcaveOn.antitoneOn_slope_gt
+ ConcaveOn.antitoneOn_slope_lt
+ ConvexOn.monotoneOn_slope_gt
+ ConvexOn.monotoneOn_slope_lt
+ bddAbove_slope_Iio_of_mem_interior
+ bddBelow_slope_Ioi_of_mem_interior
+ continuous_klFun
+ convexOn_Ioi_klFun
+ convexOn_klFun
+ deriv_klFun
+ differentiableWithinAt_Iio_of_mem_interior
+ differentiableWithinAt_Ioi_of_mem_interior
+ ge_of_leftDeriv_eq_zero
+ ge_of_leftDeriv_nonpos_of_rightDeriv_nonneg
+ ge_of_rightDeriv_eq_zero
+ hasDerivAt_klFun
+ hasDerivWithinAt_leftDeriv_of_mem_interior
+ hasDerivWithinAt_rightDeriv_of_mem_interior
+ hasDerivWithinAt_sInf_slope_of_mem_interior
+ hasDerivWithinAt_sSup_slope_of_mem_interior
+ integrable_klFun_rnDeriv_iff
+ integrable_rnDeriv_mul_log_iff
+ integral_klFun_rnDeriv
+ integral_llr_add_mul_log_nonneg
+ integral_llr_add_sub_measure_univ_nonneg
+ integral_rnDeriv_mul_log
+ kl
+ klFun
+ klFun_eq_zero_iff
+ klFun_nonneg
+ klFun_one
+ klFun_zero
+ kl_eq_integral_klFun
+ kl_eq_lintegral_klFun
+ kl_eq_top_iff
+ kl_eq_zero_iff
+ kl_ne_top_iff
+ kl_of_ac_of_integrable
+ kl_of_not_ac
+ kl_of_not_integrable
+ kl_self
+ kl_zero_left
+ kl_zero_right
+ leftDeriv_eq_sSup_slope_of_mem_interior
+ leftDeriv_klFun
+ leftDeriv_klFun_one
+ leftDeriv_le_rightDeriv_of_mem_interior
+ leftDeriv_mul_log
+ llr_self
+ measurable_klFun
+ monotoneOn_leftDeriv
+ monotoneOn_rightDeriv
+ mul_log_le_kl
+ mul_log_le_toReal_kl
+ rightDeriv_eq_sInf_slope_of_mem_interior
+ rightDeriv_klFun
+ rightDeriv_klFun_eventually_eq
+ rightDeriv_klFun_one
+ rightDeriv_le_slope_of_mem_interior
+ rightDeriv_mul_log
+ slope_le_leftDeriv_of_mem_interior
+ strictConvexOn_klFun
+ stronglyMeasurable_klFun
+ tendsto_deriv_mul_log_atTop
+ tendsto_klFun_atTop
+ tendsto_rightDeriv_klFun_atTop
+ tendsto_rightDeriv_mul_log_atTop
+ toReal_kl
+ toReal_kl_of_ac

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat: left and right derivatives of a convex function #21063
• [Merged by Bors] - feat: derivWithin lemmas #21092
• [Merged by Bors] - feat: inequality on the integral of a convex function of a RN derivative #21093
  By Dependent Issues (🤖). Happy coding!