Theorem ProbabilityTheory.IsMarkovKernel.bound_eq_one

Modification history

2025-09-13 15:32

Mathlib/Probability/Kernel/Defs.lean

chore(Probability): rename IsFiniteKernel.bound to Kernel.bound (#29613) …

Deleted ProbabilityTheory.IsMarkovKernel.bound_eq_one View on Github →

2025-09-12 14:29

Mathlib/Probability/Kernel/Defs.lean

feat(Probability/Kernel): change the def of `IsFiniteKernel.bound` to make it more informative (#29137) …

Added ProbabilityTheory.IsMarkovKernel.bound_eq_one View on Github →