Repository navigation
feat: kernel measurable space and KL generalizations from LML - #81
Merged
Merged
Conversation
Add `Statlib/ForMathlib/Probability/Kernel/MeasurableSpace.lean` with LML's instance `instMeasurableSpaceKernel` (the comap of the coercion to functions), `measurable_kernel_iff` and `Kernel.measurable_const`, and move `Kernel.measurable_eval` and `Kernel.measurable_eval'` there. Remove the instance of `Inference.lean`, which defined the same σ-algebra but is not definitionally equal to LML's, and its `Kernel.measurable_iff` and `Kernel.measurable_of_measurable_eval` (use `measurable_kernel_iff`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo
…ct_restrict` Assume `μ.HaveLebesgueDecomposition ν` instead of `SigmaFinite μ` (and, for the singular part, no assumption on `ν`). The proofs are unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo
`KL(μ ⊗ₘ κ, ν ⊗ₘ κ) = KL(μ, ν)` when `κ` is a probability measure on a measurable set of full `μ`- and `ν`-measure. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo
`klDiv_finsetSum_smul_le`, `klDiv_sum_smul_le` and the versions in each argument, proved by induction from `klDiv_add_add_le`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo
RemyDegenne
added a commit
to LeanMachineLearning/LML
that referenced
this pull request
Nov 13, 2026
…xity Bump Statlib to af34969 (stat-lib/statlib#81), which provides LML's measurable space on kernels, `klDiv_compProd_left_of_ae`, the convexity of `klDiv` for finite mixtures and the generality of `rnDeriv_restrict_restrict`, and delete LML's copies: - `LeanMachineLearning.ForMathlib.Probability.Kernel.MeasurableSpace`: the same declarations are in `Statlib.ForMathlib.Probability.Kernel.MeasurableSpace`. - `LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.ChainRule`: `measurable_klDiv_kernel` is `ProbabilityTheory.measurable_klDiv`, `klDiv_compProd_right_eq_lintegral` is `ProbabilityTheory.condKL_eq_lintegral` (`condKL κ η μ` is `klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)`), `klDiv_compProd_eq_add_lintegral` follows from `klDiv_compProd_eq_add_condKL`, and `klDiv_compProd_left_of_ae` keeps its name. - `LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Convex`: the lemmas are in Statlib, in the `ProbabilityTheory` namespace. - `MeasureTheory.Measure.rnDeriv_restrict_restrict'`: Statlib's `rnDeriv_restrict_restrict` now has the same generality. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Brings over material from LML that is more general than Statlib's or missing from it, so that LML, which is about to depend on Statlib (LeanMachineLearning/LML#298), can delete its copies.
Measurable space on kernels
Statlib/ForMathlib/Probability/Kernel/MeasurableSpace.lean, with LML's instanceinstMeasurableSpaceKernel(the comap of the coercionKernel 𝓧 𝓨 → (𝓧 → Measure 𝓨)),measurable_kernel_iffandKernel.measurable_const.Kernel.measurable_evalandKernel.measurable_eval'move there fromInference.lean.Inference.lean(a supremum of comaps of the evaluations). It defined the same σ-algebra, but it is not definitionally equal to LML's, so the two instances could not coexist.Generalizations
Measure.rnDeriv_restrict_restrictnow assumes[μ.HaveLebesgueDecomposition ν]instead of[SigmaFinite μ], as in LML.Measure.singularPart_restrict_restrictnow assumes only[μ.HaveLebesgueDecomposition ν], instead of[SigmaFinite μ] [SigmaFinite ν]. Both proofs are unchanged.InformationTheory.klDiv_compProd_left_of_ae(from LML):KL(μ ⊗ₘ κ, ν ⊗ₘ κ) = KL(μ, ν)whenκis only a probability measure on a measurable set of fullμ- andν-measure.klDiv_finsetSum_smul_leandklDiv_sum_smul_le, with convexity in each argument (klDiv_finsetSum_smul_left_le,klDiv_sum_smul_left_le,klDiv_finsetSum_smul_right_le,klDiv_sum_smul_right_le). They are proved by induction fromklDiv_add_add_le, which is shorter than LML's proof.Removed or renamed
ProbabilityTheory.Kernel.instMeasurableSpaceKernelProbabilityTheory.instMeasurableSpaceKernelProbabilityTheory.Kernel.measurable_iffProbabilityTheory.measurable_kernel_iffProbabilityTheory.Kernel.measurable_of_measurable_eval(measurable_kernel_iff κ).2Checks run locally
lake build --iofail,lake lintandlake exe mk_all --checkpass.subverso-extract-modand the:highlightedfiles ofStatlib.Inference.InferenceandStatlib.Inference.QMD) succeed.main.This PR stays on Mathlib
2ddf59c, which LML#298 needs.🤖 Generated with Claude Code
https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo