feat(MeasureTheory): Introduce MassFunction α giving rise to a Measure α ⊤

[pfaffelh]

Define MassFunction α := α → ℝ≥0∞
Define toMeasure (w : MassFunction α) : @Measure α ⊤ as a sum of diracs
Show properties of the resulting objects

This PR intends to start a more userfriendly interaction with probability mass functions (PMF). There are two main differences between MassFunction and PMF:

• PMF hast the additional property HasSum 1, making the resulting measure a probability measure. (For MassFunction, I intend to use the typeclass IsProbabilityMeasurein a later PR instead.)
• The toMeasure function of MassFunction directly defines the measure as a sum of diracs, which immediately makes computations possible.

Discussion thread on zulip

• depends on: feat: Set.indicator on a disjoint union equals the sum of individual Set.indicator #37060

---

[github-actions]

PR summary cd20542ace

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.MeasureTheory.Measure.MassFunction (new file)	1559

---

Declarations diff

+ Function.support_subsingleton_of_disjoint
+ MassFunction
+ Set.PairwiseDisjoint.fiber_subtype
+ Set.PairwiseDisjoint.singleton_subtype'
+ Set.indicator_iUnion_of_disjoint'
+ apply_eq_zero_iff
+ apply_pos_iff
+ ext
+ indicator.mul_indicator_eq
+ instFunLike
+ mem_support_iff
+ mulIndicator_iUnion_of_disjoint
+ mulSupport_subsingleton_of_disjoint
+ restrict_toMeasure_support
+ support
+ toMeasure
+ toMeasure'
+ toMeasure_additive
+ toMeasure_apply
+ toMeasure_apply_eq_of_inter_support_eq
+ toMeasure_apply_eq_zero_iff
+ toMeasure_apply_finset
+ toMeasure_apply_fintype
+ toMeasure_apply_inter_support
+ toMeasure_apply_singleton
+ toMeasure_apply_univ
+ toMeasure_apply_univ'
+ toMeasure_apply₁
+ toMeasure_apply₂
+ toMeasure_ext
+ toMeasure_inj
+ toMeasure_injective
+ toMeasure_mono
+ toMeasure_trim_eq_toMeasure'
+ tprod_mulIndicator_of_disjoint
+ tprod_mulIndicator_of_nmem

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[ocfnash]

Thanks for this and also for splitting out #37060 which hopefully we can merge soon.

Part of the reason we've been slow with review here is that there is a plan to deprecate PMF and instead just work with sums of Dirac masses. For example there are two open PRs in this direction #36374 and #36378 which are likely to be merged soon.

I have asked for some measure theory experts to weigh up the pros and cons one last time and I hope to return here (or let them do so) with concrete proposals for how to resolve the proposal here soon.

[pfaffelh]

Thanks for the update! I welcome if PMF is deprecated. Let me mention that the MassFuntion α I want to introduce here is "only" a function α → ℝ≥0∞ (similar to PMF, but without any summability requirement). Its .toMeasure then gives a sum of diracs (similar to the other two PRs). This has two advantages:

1. Once toMeasure is applied, the sum of diracs is nice to work with.
2. MassFunction is still a LawfulMonad (as PMF), so I can e.g. use do-notation, bind, join and sequence, all of which have nice probabilistic meanings.

[pfaffelh]

WIP +

[ocfnash]

+WIP

(assuming this is what was intended here)

[ocfnash]

Thanks again for this work. I can't quite tell from these words what you're planning but I'll happily take a close look once you're ready for review again.

Note that #37060 has been delegated so it may help to resolve that first.

[pfaffelh]

Yes, thanks for taking care! (I am on vacation, back at the computer next week.) There was a disussion in the geometric distribution PR, 36768. @EtienneC30 concluded "We could treat MassFunction like ProbabilityMeasure type where it should only be used when one wants to use the structure on the type (the topology in the case of ProbabilityMeasure or the monad and do notation in the case of MF) but should otherwise just use measure and the rest of the measure theory API." which found some agreement. My idea is to change the current PR in this direction.