[RemyDegenne]

Makes LML depend on Statlib, and get Mathlib through it (now 2ddf59c, the commit Tau Ceti's main pins). LML's copies of Statlib material are replaced with Statlib's.
With Statlib, we gain access to many properties of klDiv and other information divergences. No Statlib definition is added to the dependencies of the LML definitions.

Dependencies

• Requires Statlib at af34969.
• No longer requires Mathlib directly: Mathlib comes through Statlib, at the commit Statlib pins, so LML always builds against the Mathlib that Statlib was tested with.
• Statlib comes before Verso in the lakefile: Lake gives precedence to later requires for shared dependencies, so Verso keeps its own subverso (892d6dc).
• Mathlib 6135ffb → 2ddf59c. The fixes for Mathlib changes are the EventuallyEqSet refactor ([Merged by Bors] - refactor: change the definition of EventuallyEqSet leanprover-community/mathlib4#45712), the enorm → eNorm rename ([Merged by Bors] - chore: rename enorm to eNorm leanprover-community/mathlib4#45735), and the new hypothesis of Submartingale.ae_tendsto_limitProcess in the martingale tutorial page.

Using Statlib

stat-lib/statlib#81 moved into Statlib the LML material that Statlib lacked or had in less generality: the measurable space on kernels, klDiv_compProd_left_of_ae, the convexity of klDiv for finite mixtures, and the generality of rnDeriv_restrict_restrict. LML now uses Statlib's versions, and removes its copies together with the material that duplicated Statlib:

• Three files are removed: LeanMachineLearning.ForMathlib.Probability.Kernel.MeasurableSpace, LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.ChainRule and LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Convex.
• klDiv_eq_iSup_map: the 130-line proof (Lévy's upward theorem and Fatou) becomes a 4-line corollary of Statlib's tendsto_fDiv_map_of_iSup_comap_eq.
• klDiv_restrict_add_restrict_compl: now a corollary of Statlib's klDiv_eq_klDiv_restrict_add_klDiv_restrict_compl.

Before this PR, LML and Statlib declared some of the same names, two instances of MeasurableSpace (Kernel α β) that are not definitionally equal, and a klDiv_smul_add_smul_le in two namespaces. None of these remain.

Removed or renamed declarations

Old	Replacement
ProbabilityTheory.instMeasurableSpaceKernel, ProbabilityTheory.measurable_kernel_iff, ProbabilityTheory.Kernel.measurable_const	the same names, from Statlib
InformationTheory.klDiv_map_measurableEmbedding, InformationTheory.klDiv_comp_le_compProd, InformationTheory.klDiv_compProd_left_of_ae	the same names, from Statlib
MeasureTheory.Measure.rnDeriv_restrict_restrict	the same name, from Statlib (now as general)
InformationTheory.klDiv_le_compProd	InformationTheory.le_klDiv_compProd
InformationTheory.klDiv_smul_add_smul_le	ProbabilityTheory.klDiv_smul_add_smul_le
InformationTheory.measurable_klDiv_kernel	ProbabilityTheory.measurable_klDiv
InformationTheory.klDiv_compProd_right_eq_lintegral	ProbabilityTheory.condKL_eq_lintegral, where condKL κ η μ is klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η) (rewrite with ← condKL first)
InformationTheory.klDiv_compProd_eq_add_lintegral	ProbabilityTheory.klDiv_compProd_eq_add_condKL, then condKL_eq_lintegral
InformationTheory.klDiv_finsetSum_smul_le, klDiv_sum_smul_le, klDiv_finsetSum_smul_left_le, klDiv_sum_smul_left_le, klDiv_finsetSum_smul_right_le, klDiv_sum_smul_right_le	the same names in ProbabilityTheory, from Statlib

Automatic updates

update.yml now bumps Statlib instead of Mathlib. Every six hours it does the following:

1. Runs lake update Statlib. This moves Statlib to its latest main and Mathlib to the commit Statlib pins; I checked this locally from an older Statlib pin.
2. Builds LML and its tutorial with --wfail.
3. Opens or updates a pull request on the statlib-bump branch.

Pull requests opened with the workflow token do not trigger the Build workflow, so the job builds before opening one.

The two downstream-reports jobs are removed (bump-to-latest and track-incompatibility). They act on a direct Mathlib requirement, which LML no longer has. Statlib's own updater keeps it close to Mathlib master and tracks the incompatibilities there.

LML's entry in downstream-reports' inventory (ci/inventory/downstreams.json, with dependency_name: "mathlib") assumes a direct Mathlib requirement, so it should probably be disabled there.

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo