Total variation, overlap, and shift distance

Adapted for Lean Pool by changing module paths and selecting explicit imports.

Komlos.tvDist P Q is half the sum of |P x - Q x|. Komlos.overlap P Q is the sum of min (P x) (Q x). Komlos.shiftDist P u is the total variation distance between P and its translate by u.

For probability distributions, overlap equals 1 - tvDist P Q.

noncomputable def Komlos.tvDist {E : Type u_1} (P Q : E →₀ ℝ) : ℝ

Half the sum of absolute differences of the weights of two finitely supported functions.

Equations

• Komlos.tvDist P Q = 2⁻¹ * (P - Q).sum fun (x : E) (r : ℝ) => |r|

noncomputable def Komlos.overlap {E : Type u_1} (P Q : E →₀ ℝ) : ℝ

Total common weight, computed by taking the pointwise minimum.

Equations

• Komlos.overlap P Q = Komlos.mass (P ⊓ Q)

noncomputable def Komlos.shiftDist {E : Type u_1} [AddCommGroup E] (P : E →₀ ℝ) (u : E) : ℝ

Total variation distance between a finitely supported function and its translate by u.

Equations

• Komlos.shiftDist P u = Komlos.tvDist P (Komlos.tr u P)

theorem Komlos.tvDist_nonneg {E : Type u_1} (P Q : E →₀ ℝ) : 0 ≤ tvDist P Q

theorem Komlos.tvDist_eq_sum {E : Type u_1} {P Q : E →₀ ℝ} {s : Finset E} (hP : P.support ⊆ s) (hQ : Q.support ⊆ s) : tvDist P Q = 2⁻¹ * ∑ x ∈ s, |P x - Q x|

theorem Komlos.overlap_eq_sum {E : Type u_1} {P Q : E →₀ ℝ} {s : Finset E} (hP : P.support ⊆ s) (hQ : Q.support ⊆ s) : overlap P Q = ∑ x ∈ s, min (P x) (Q x)

theorem Komlos.overlap_tr {E : Type u_1} [AddCommGroup E] (u : E) (P Q : E →₀ ℝ) : overlap (tr u P) (tr u Q) = overlap P Q

theorem Komlos.mass_le_overlap {E : Type u_1} {P Q R : E →₀ ℝ} (hP : R ≤ P) (hQ : R ≤ Q) : mass R ≤ overlap P Q

theorem Komlos.overlap_eq_one_sub_tvDist {E : Type u_1} {P Q : E →₀ ℝ} (hP : IsDist P) (hQ : IsDist Q) : overlap P Q = 1 - tvDist P Q

theorem Komlos.shiftDist_eq_one_sub_overlap {E : Type u_1} [AddCommGroup E] {P : E →₀ ℝ} (hP : IsDist P) (u : E) : shiftDist P u = 1 - overlap P (tr u P)