feat(Probability/ProbabilityMassFunction): add Total Variation distance

[BoltonBailey]

Adds the statistical distance/total variation distance.

This PR was authored with the support of Claude opus 4.5

---

Note: Perhaps a good thing to do before this PR would be to change the return type of the funlike instance for PMF into a (subtype of) the reals, see #33689.

Zulip https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/total.20variation.20distance.20between.20two.20PMFs

[github-actions]

PR summary db90f79240

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Probability.ProbabilityMassFunction.Distance (new file)	1255

---

Declarations diff

+ PMF.dist_summable
+ PMF.summable_toReal_abs
+ StatisticalDistance

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.

---

No changes to technical debt.

You can run this locally as

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