Finite mass identities and total variation bounds

Normalization is preserved by marginals and deterministic maps. Total variation contracts under deterministic maps and bounds every finite test. For equal total mass, the positive-difference test attains the distance.

theorem Algebraic.Cutwidth.Extractor.Internal.probabilityWeight_exists_pos {α : Type u_1} [Fintype α] {p : α → ℝ} (hp : IsProbabilityWeight p) : ∃ (x : α), 0 < p x

theorem Algebraic.Cutwidth.Extractor.Internal.probabilityWeight_le_one {α : Type u_1} [Fintype α] {p : α → ℝ} (hp : IsProbabilityWeight p) (x : α) : p x ≤ 1

theorem Algebraic.Cutwidth.Extractor.Internal.probabilityWeight_first {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {p : α × β → ℝ} (hp : IsProbabilityWeight p) : IsProbabilityWeight (firstWeight p)

theorem Algebraic.Cutwidth.Extractor.Internal.probabilityWeight_map {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {p : α → ℝ} (hp : IsProbabilityWeight p) (f : α → β) : IsProbabilityWeight (mapWeight f p)

theorem Algebraic.Cutwidth.Extractor.Internal.probabilityWeight_uniform (α : Type u_1) [Fintype α] [Nonempty α] : IsProbabilityWeight (uniformWeight α)

theorem Algebraic.Cutwidth.Extractor.Internal.mapWeight_id {α : Type u_1} [Fintype α] (p : α → ℝ) : mapWeight id p = p

theorem Algebraic.Cutwidth.Extractor.Internal.mapWeight_equiv_apply {α : Type u_1} {β : Type u_2} [Fintype α] (e : α ≃ β) (p : α → ℝ) (y : β) : mapWeight (⇑e) p y = p (e.symm y)

theorem Algebraic.Cutwidth.Extractor.Internal.mapWeight_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] (p : α → ℝ) (f : α → β) (g : β → γ) : mapWeight g (mapWeight f p) = mapWeight (fun (x : α) => g (f x)) p

theorem Algebraic.Cutwidth.Extractor.Internal.mapWeight_fst {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (p : α × β → ℝ) : mapWeight Prod.fst p = firstWeight p

theorem Algebraic.Cutwidth.Extractor.Internal.mapWeight_snd_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (p : α × β → ℝ) (b : β) : mapWeight Prod.snd p b = ∑ a : α, p (a, b)

theorem Algebraic.Cutwidth.Extractor.Internal.cappedWeight_card_le {α : Type u_1} [Fintype α] {p : α → ℝ} {K : ℕ} (hp : IsProbabilityWeight p) (cap : CappedWeight p K) : K ≤ Fintype.card α

theorem Algebraic.Cutwidth.Extractor.Internal.cappedWeight_eq_uniform {α : Type u_1} [Fintype α] {p : α → ℝ} (cap : CappedWeight p (Fintype.card α)) (hp : IsProbabilityWeight p) : p = uniformWeight α

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_nonneg {α : Type u_1} [Fintype α] (p q : α → ℝ) : 0 ≤ weightDist p q

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_self {α : Type u_1} [Fintype α] (p : α → ℝ) : weightDist p p = 0

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_comm {α : Type u_1} [Fintype α] (p q : α → ℝ) : weightDist p q = weightDist q p

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_triangle {α : Type u_1} [Fintype α] (p q r : α → ℝ) : weightDist p r ≤ weightDist p q + weightDist q r

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_eq_zero_iff {α : Type u_1} [Fintype α] (p q : α → ℝ) : weightDist p q = 0 ↔ p = q

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_le_one {α : Type u_1} [Fintype α] {p q : α → ℝ} (hp : IsProbabilityWeight p) (hq : IsProbabilityWeight q) : weightDist p q ≤ 1

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_map_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (p q : α → ℝ) (f : α → β) : weightDist (mapWeight f p) (mapWeight f q) ≤ weightDist p q

theorem Algebraic.Cutwidth.Extractor.Internal.weightTestProb_sub_le_dist {α : Type u_1} [Fintype α] (p q : α → ℝ) (mass : ∑ x : α, p x = ∑ x : α, q x) (T : Finset α) : |weightTestProb p T - weightTestProb q T| ≤ weightDist p q

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_le_iff_tests {α : Type u_1} [Fintype α] (p q : α → ℝ) (mass : ∑ x : α, p x = ∑ x : α, q x) {ε : ℝ} : weightDist p q ≤ ε ↔ ∀ (T : Finset α), |weightTestProb p T - weightTestProb q T| ≤ ε

theorem Algebraic.Cutwidth.Extractor.Internal.weightTestProb_map {α : Type u_1} {β : Type u_2} [Fintype α] (p : α → ℝ) (f : α → β) (T : Finset β) : weightTestProb (mapWeight f p) T = ∑ x : α, if f x ∈ T then p x else 0

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_map_map_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {p : α → ℝ} (hp : IsProbabilityWeight p) (f g : α → β) : weightDist (mapWeight f p) (mapWeight g p) ≤ ∑ x : α with f x ≠ g x, p x