Total variation distance between FintypePMFs (L1 form)

tvDistance p q = ∑ a, |p.prob a - q.prob a|. This is the L1 form of total variation; the probabilists' normalised TV is half this quantity. The L1 form is what the transfer principle composes with directly.

def ProbabilityTheory.FintypePMF.tvDistance {α : Type u_1} [Fintype α] (p q : FintypePMF α) : ℝ

L1 total variation distance between two FintypePMFs.

Equations

• p.tvDistance q = ∑ a : α, |p.prob a - q.prob a|

theorem ProbabilityTheory.FintypePMF.tvDistance_nonneg {α : Type u_1} [Fintype α] (p q : FintypePMF α) : 0 ≤ p.tvDistance q

theorem ProbabilityTheory.FintypePMF.tvDistance_comm {α : Type u_1} [Fintype α] (p q : FintypePMF α) : p.tvDistance q = q.tvDistance p

theorem ProbabilityTheory.FintypePMF.tvDistance_self {α : Type u_1} [Fintype α] (p : FintypePMF α) : p.tvDistance p = 0