Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-07-25 13:48
69d98d94
View on Github →
feat(Probability/Kernel/Basic): Evaluation function of a finite kernel is integrable (
#6111
)
Estimated changes
Modified
Mathlib/Probability/Kernel/Basic.lean
added
theorem
ProbabilityTheory.kernel.IsFiniteKernel.integrable
added
theorem
ProbabilityTheory.kernel.IsMarkovKernel.integrable