feat(ProbabilityTheory/MeasureTheorey): Add Coupling lemma

[yuanyi-350]

Summary

This PR formalizes a standard coupling bound on countable measurable spaces. More precisely, for a probability measure μ and measurable maps
Y Z : Ω → S with S countable, it proves the L¹ bound
∑' k : S, |(μ.map Y).real ({k} : Set S) - (μ.map Z).real ({k} : Set S)| ≤ 2 * μ.real {ω | Y ω ≠ Z ω}.

Main changes

• add tsum_restrict_preimage_singleton_eq and tsum_restrict_preimage_singleton_eq' in MeasureTheory/Measure/Restrict.lean;
• add tsum_measureReal_restrict_preimage_singleton_eq, coupling_term_bound, and coupling_lemma in MeasureTheory/Measure/Real.lean;
• include some local cleanup in MeasureTheory/Measure/Real.lean, mainly simplifying toReal-related arguments and notation.

References

• Wikipedia: https://en.wikipedia.org/wiki/Coupling_(probability)

---

[github-actions]

PR summary 2050ca5474

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ coupling_lemma
+ coupling_term_bound
+ tsum_measureReal_restrict_preimage_singleton_eq
+ tsum_restrict_preimage_singleton_eq
+ tsum_restrict_preimage_singleton_eq'

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).