Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-01-05 13:11
599c46e9
View on Github →
feat: a conditional kernel is almost everywhere a probability measure (
#20430
)
Estimated changes
Modified
Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean
added
theorem
MeasureTheory.ae_le_const_iff_forall_gt_measure_zero
Modified
Mathlib/Probability/Kernel/Disintegration/Basic.lean
added
theorem
ProbabilityTheory.Kernel.IsCondKernel.isProbabilityMeasure_ae
modified
theorem
ProbabilityTheory.Kernel.disintegrate