feat(InformationTheory/KullbackLeibler): finite Kullback-Leibler divergence

[elazarg]

Add finite-sum formulas for InformationTheory.klDiv on finite measurable spaces, including equal-mass and probability-measure specializations and formulas for sums of weighted Dirac measures. Provide both ℝ≥0∞-valued and toReal versions.

Supporting API includes a formula for the Radon–Nikodym derivative at points of nonzero reference-measure mass, a finite-sum formula for the integral of the log-likelihood ratio, and singleton-mass and absolute-continuity lemmas for sums of weighted Dirac measures.

---

Continuing #42584, another part of https://github.com/elazarg/kraft.

Following review, this uses the existing klDiv instead of introducing klDivFin. The toReal formulas connect it to real-valued sums in downstream code.

For measures of unequal mass, the formulas retain the correction term ν.real univ - μ.real univ.

The KL formulas are in KullbackLeibler/Basic.lean; the supporting lemmas are in the corresponding measure-theory modules.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary c258e30e24

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ absolutelyContinuous_sum_smul_dirac_iff
+ integral_llr_fintype
+ klDiv_eq_sum
+ klDiv_eq_sum_of_isProbabilityMeasure
+ klDiv_eq_sum_of_measure_eq
+ klDiv_sum_smul_dirac
+ rnDeriv_eq_div_measure_singleton
+ sum_smul_dirac_real_singleton
+ sum_smul_dirac_real_univ
+ toReal_klDiv_eq_sum
+ toReal_klDiv_eq_sum_of_isProbabilityMeasure
+ toReal_klDiv_eq_sum_of_measure_eq
+ toReal_klDiv_sum_smul_dirac

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit c258e30).

• +13 new declarations
• −0 removed declarations

+InformationTheory.klDiv_eq_sum
+InformationTheory.klDiv_eq_sum_of_isProbabilityMeasure
+InformationTheory.klDiv_eq_sum_of_measure_eq
+InformationTheory.klDiv_sum_smul_dirac
+InformationTheory.toReal_klDiv_eq_sum
+InformationTheory.toReal_klDiv_eq_sum_of_isProbabilityMeasure
+InformationTheory.toReal_klDiv_eq_sum_of_measure_eq
+InformationTheory.toReal_klDiv_sum_smul_dirac
+MeasureTheory.Measure.absolutelyContinuous_sum_smul_dirac_iff
+MeasureTheory.Measure.rnDeriv_eq_div_measure_singleton
+MeasureTheory.Measure.sum_smul_dirac_real_singleton
+MeasureTheory.Measure.sum_smul_dirac_real_univ
+MeasureTheory.integral_llr_fintype

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit c258e30e24
Reference commit 572e4d091b

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).

[vlad902]

Since the linked GitHub repo mentions significant AI use, you should comment LLM-generated to add the LLM-generated flag if the material in this PR constitutes a part of that.

[elazarg]

Since the linked GitHub repo mentions significant AI use, you should comment LLM-generated to add the LLM-generated flag if the material in this PR constitutes a part of that.

I am using LLMs (of course) but I'm signing every term and every word here (and an earlier version has underwent an independent human review). LLMs are a source of discovery/review, not the source of confidence that the definitions are correct. So the question is what does LLM-generated mean in this context.

[EtienneC30]

It means that the code was written with substantial input by an LLM, as indicated under the label. Even long time contributors who carefully reviewed every line of their code written by an LLM tag the PR with the label, this is meant as an information to reviewers as LLMs are more prone to certain errors. In any case, you should always mention LLM involvement in the PR description as per the AI policy.

[elazarg]

LLM-generated

[EtienneC30]

I think it would be much better to use InformationTheory.klDiv directly, and adding some API for it and for sums of Dirac measures when needed, maybe introducing a klDivReal definition if you really need an real valued version.

[elazarg]

@EtienneC30 Done. The proofs work and look good to me (and mostly straightforward), and the kraft codebase works well with this API. I don't know measure theory though, so it's definitely LLM-generated.