chore: deprecate Measure.Dirac - #42989

Open

EtienneC30 wants to merge 14 commits into

leanprover-community:masterfrom

EtienneC30:proba-map3

Commits on Aug 1, 2026

refactor: change `ProbabilityMeasure.map` to not require measurability
EtienneC30
committed
69ce77a

Commits on Aug 16, 2026

wip
EtienneC30
committed
42b4a56
Merge branch 'master' of https://github.com/leanprover-community/mathlib4 into proba-map
EtienneC30
committed
38c241a
wip
EtienneC30
committed
d660445
wip
EtienneC30
committed
3e2ee2f
wip
EtienneC30
committed
c060663
wip
EtienneC30
committed
464ee43
done
EtienneC30
committed
88c7769
fix
EtienneC30
committed
0004ccc
fix
EtienneC30
committed
3d88a8a

Commits on Aug 17, 2026

docstring
EtienneC30
committed
cd7f3fd

Commits on Aug 20, 2026

Merge branch 'master' of https://github.com/leanprover-community/mathlib4 into proba-map
EtienneC30
committed
3e860b9
fix
EtienneC30
committed
d8b667e
chore: deprecate Measure.Dirac
EtienneC30
committed
4d3aed0