The coupling inequality

Two functions of one sample are at statistical distance at most the probability that they differ (Cslib.Probability.PMF.dist_map_map_le). The sample space may be infinite; only the common codomain is finite.

Main results

• Cslib.Probability.PMF.dist_map_map_le: the coupling inequality.

theorem Cslib.Probability.PMF.dist_map_map_le {α : Type u_1} {β : Type u_2} [Fintype β] (p : PMF α) (f g : α → β) : dist (PMF.map f p) (PMF.map g p) ≤ (p.toOuterMeasure {a : α | f a ≠ g a}).toReal

Coupling inequality. Two functions of the same sample are at statistical distance at most the probability that they differ.