Total variation distance on pmf

Stream: Is there code for X?

[Bolton Bailey]

measure_theory.probability_mass_function.basic has the type pmf of discrete probability measures. Do we have the total variation metric on this type?

[Kalle Kytölä]

It was discussed as one among the reasonable topologies on probability measures (and finite measures) here, but to my knowledge has not been implemented in mathlib yet.

I think the total variation metric should be defined on docs#measure_theory.finite_measure and docs#measure_theory.probability_measure. (But it should not be recorded as an instance, since the outcome of the discussions above was that the topology instance on these types should be that of convergence in distribution.) It will be essentially the dual norm in for example the dual of the space of continuous functions on a compact space, so very natural in the generality of finite_measures. In this route, it would be a theorem that for probability measures determined by pmfs (for example on finite sample spaces), the total variation distance is half the sum of the absolute differences of the values of the pmfs (half their $\ell^1$ distance), as in <https://en.wikipedia.org/wiki/Total_variation_distance_of_probability_measures>.

By the way, $\ell^1$ distance exists (docs#lp), so that can probably be used for (twice) the total variation distance right away.