Commit 2024-10-11 13:11 69715a18
View on Github →feat(Measure/WithDensityFinite): redefine Measure.toFinite
(#17421)
- Redefine
Measure.toFinite
usingexists_isFiniteMeasure_absolutelyContinuous
. - Redefine
Measure.densityToFinite
asrnDeriv
, deprecate it. - Drop some lemmas about
toFiniteAux
. - Simplify proofs.