2.4 Total variation distance
Lean: MeasureTheory.tvDistReal
For finite Borel measures \(P, Q\) on \(\alpha \),
where the supremum is over measurable \(A \subseteq \alpha \). This is the half-sup / metric convention, chosen so that Pinsker reads as \(\mathrm{TV}(P,Q) \le \sqrt{\mathrm{KL}(P\| Q)/2}\) [ 4 , § 3 ] , [ 24 , Ch. 1 ] .
Lean: MeasureTheory.tvDistReal_set_nonempty
The set \(\{ |P(A).\mathrm{toReal} - Q(A).\mathrm{toReal}| : A \text{ measurable} \} \) is nonempty (witnessed by \(A = \emptyset \)).
Lean: MeasureTheory.tvDistReal_set_bddAbove
The same set is bounded above by \(P(\alpha ).\mathrm{toReal} + Q(\alpha ).\mathrm{toReal}\).
The repository also contains a second total-variation object, \(\mathrm{FintypePMF.tvDistance}\, p\, q = \sum _a |p\, a - q\, a|\) (the \(L^1\) convention, see Chapter 4); the two conventions differ by a factor of \(2\) on discrete supports. Downstream consumers should not compose them without inserting the factor-of-\(\tfrac {1}{2}\) correction.