Commit 2024-10-11 13:11 69715a18

View on Github →

feat(Measure/WithDensityFinite): redefine Measure.toFinite (#17421)

  • Redefine Measure.toFinite using exists_isFiniteMeasure_absolutelyContinuous.
  • Redefine Measure.densityToFinite as rnDeriv, deprecate it.
  • Drop some lemmas about toFiniteAux.
  • Simplify proofs.

Estimated changes