noncomputable def totalVariationDist {Ω : Type u_1} [MeasurableSpace Ω] (μ ν : MeasureTheory.Measure Ω) : ℝ

The total variation distance between two measures μ and ν, defined as ‖μ - ν‖ = sup_B |μ(B) - ν(B)| where the supremum runs over all measurable sets B.