feat(Measure/WithDensityFinite): redefine Measure.toFinite

[urkud]

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

---

[github-actions]

PR summary db8a216269

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ ae_toFinite
+ ae_toFiniteAux
+ instance [SFinite μ] [NeZero μ] : IsProbabilityMeasure μ.toFinite := by
+ isFiniteMeasure_toFiniteAux
+ sFiniteSeq_le
+ toFinite_apply_eq_zero_iff
+ toFinite_eq_self
- instance [SFinite μ] : IsFiniteMeasure μ.toFiniteAux
- instance [SFinite μ] [h_zero : NeZero μ] : IsProbabilityMeasure μ.toFinite := by
- sFiniteSeq_absolutelyContinuous_toFiniteAux
- toFiniteAux_absolutelyContinuous_toFinite
- toFiniteAux_apply
- toFiniteAux_eq_zero_iff
- toFiniteAux_univ_le_one
- toFiniteAux_zero
- toFinite_apply

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[RemyDegenne]

Please update the file docstring to reflect the changes.

[urkud]

@RemyDegenne I updated docs