Finite probability weights and statistical distance

Probability weights remain normalized under marginalization and deterministic maps. Their total variation distance lies in [0,1], obeys the triangle inequality, and contracts under deterministic maps. For equal total mass, a distance bound is equivalent to the same bound on every finite test. These results connect weighted conditional-source arguments to the existing extractor contracts phrased using tests.

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

A normalized nonnegative weighting has a point of positive mass.

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

No point of a finite probability distribution has mass greater than one.

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

Taking the first marginal preserves finite probability weights.

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

A deterministic image counts all source occurrences and preserves normalization.

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

Uniform weights on a nonempty finite type form a probability distribution.

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

The identity map preserves every finite weighting.

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

An equivalence transports each point mass to its unique image.

theorem Algebraic.Cutwidth.Extractor.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

Deterministic pushforwards compose, including when either map identifies points.

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

The first marginal is the deterministic image under the first projection.

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

The second marginal sums over every first-coordinate occurrence.

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

A point-mass cap cannot exceed the size of the finite sampling space.

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

A normalized source with full possible min-entropy is exactly uniform.

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

Total variation is nonnegative, including for unnormalized weights.

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

A weighting has zero distance from itself.

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

Finite total variation is symmetric.

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

Successive repairs add their total variation errors.

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

Zero total variation means equality at every point.

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

Two finite probability distributions have total variation at most one.

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

Deterministic processing cannot increase total variation.

theorem Algebraic.Cutwidth.Extractor.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

Equal-mass weights differ on any finite test by at most their total variation.

theorem Algebraic.Cutwidth.Extractor.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| ≤ ε

For equal total mass, the finite-test and total-variation bounds are equivalent.

theorem Algebraic.Cutwidth.Extractor.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

Testing a deterministic image is the same as testing its preimage.

theorem Algebraic.Cutwidth.Extractor.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

Two deterministic observations differ in total variation by at most their disagreement probability under the same source.