Common mass and zero-mass fibers

The positive residual after removing pointwise common mass equals total variation distance. Nonnegative zero-mass fibers vanish pointwise, making the normalized residual and conditional-kernel formulas valid at zero mass.

theorem Algebraic.Cutwidth.Extractor.Internal.nonnegWeight_eq_zero_of_mass_zero {α : Type u_1} [Fintype α] {p : α → ℝ} (nonnegative : ∀ (x : α), 0 ≤ p x) (mass : ∑ x : α, p x = 0) (x : α) : p x = 0

theorem Algebraic.Cutwidth.Extractor.Internal.nonnegWeight_mul_mass_div {α : Type u_1} [Fintype α] (p : α → ℝ) (nonnegative : ∀ (x : α), 0 ≤ p x) (x : α) : (p x * ∑ y : α, p y) / ∑ y : α, p y = p x

theorem Algebraic.Cutwidth.Extractor.Internal.sum_common_residual_eq_weightDist {α : Type u_1} [Fintype α] {p q : α → ℝ} (hp : IsProbabilityWeight p) (hq : IsProbabilityWeight q) : ∑ x : α, (p x - min (p x) (q x)) = weightDist p q

theorem Algebraic.Cutwidth.Extractor.Internal.common_residual_mul_self_eq_zero (a b : ℝ) : (a - min a b) * (b - min a b) = 0