Commit 2025-09-12 14:29 9f97c819

View on Github →

feat(Probability/Kernel): change the def of IsFiniteKernel.bound to make it more informative (#29137) Previously, IsFiniteKernel.bound was a finite upper bound on the measure of the univ set for all measures in the image of the kernel. This PR changes it to the least upper bound. In particular, for a Markov kernel it now has value 1.

Estimated changes

Modified Mathlib/Probability/Kernel/Composition/Comp.lean

modified theorem ProbabilityTheory.Kernel.comp_apply_univ_le

Modified Mathlib/Probability/Kernel/Composition/MapComap.lean

Modified Mathlib/Probability/Kernel/Defs.lean

added theorem ProbabilityTheory.IsFiniteKernel.bound_eq_zero_of_isEmpty'

added theorem ProbabilityTheory.IsFiniteKernel.bound_eq_zero_of_isEmpty

added theorem ProbabilityTheory.IsFiniteKernel.bound_zero

added theorem ProbabilityTheory.IsMarkovKernel.bound_eq_one

added theorem ProbabilityTheory.IsZeroOrMarkovKernel.bound_le_one

modified theorem ProbabilityTheory.Kernel.measure_le_bound

Modified Mathlib/Probability/Kernel/RadonNikodym.lean