refactor: change ProbabilityMeasure.map to not require measurability

[EtienneC30]

Currently, if µ : ProbabilityMeasure X and f : X -> Y, then to talk about the pushforward of µ by f one must assume hf : AEMeasurable f µ and write µ.map hf. The issue with this is that if hf is not available as is then providing it explicitly quickly gets the code hard to read (for instance in the PR I replaced some f_cont.measurable.aemeasurable by just f). Thus we change the definition so that µ.map f is some arbitrary Dirac mass if f is not measurable (note that X is not empty because it has a probability measure, and thus Y is not empty either).

The only issue seems to be that MeasureTheory.ProbabilityMeasure.toMeasure_map now requires a measurability hypothesis to trigger with simp, I personally think that's ok.

---

[github-actions]

PR summary 69ce77a4b9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 69ce77a).

• +0 new declarations
• −1 removed declarations

-MeasureTheory.ProbabilityMeasure.map.congr_simp

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 69ce77a4b9
Reference commit 1f8806b67d

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

[D-Thomine]

I don't have an opinion on whether it's desirable behaviour for map. However, if it is implemented, wouldn't it make sense to act at the level of MeasureTheory.Measure.Map? e.g. if f is not measurable, send all the mass to a single point (i.e. replace f by a constant function).

It would also be instructive to see what breaks in MeasureTheory, and what has to be adapted. AEMeasurable.of_map_ne_zero is the most obvious to me. It is a weird statement which should probably be removed, but following it, it looks like something might break at ProbabilityTheory.mgf_dirac. That statement would become false with your new convention, provided that Measure.map were replaced by ProbabilityMeasure.map, which would make sense in this context. Though an additional measurability hypothesis would fix it; there's a rabbit hole to follow here.

Edit: If both Measure.map and ProbabilityMeasure.map are used in probabilistic settings, which ProbabilityTheory.mgf_dirac suggests, it seems quite important to me to keep both definitions coherent, including with this convention.