Transferring conditional uniformity across a repair

A repair changes a deterministic continuation by at most its total variation cost. If the retained marginal changes, comparing to the actual marginal costs at most the same amount once more. These bounds hold for arbitrary real weights and also for empty output alphabets.

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_uniformSecond_le_of_dist_of_same_first {Tag : Type u_1} {Out : Type u_2} [Fintype Tag] [Fintype Out] {p q : Tag × Out → ℝ} {ρ ε : ℝ} (near : weightDist p q ≤ ρ) (uniform : weightDist q (uniformSecondWeight q) ≤ ε) (same : firstWeight p = firstWeight q) : weightDist p (uniformSecondWeight p) ≤ ρ + ε

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_uniformSecond_le_of_dist {Tag : Type u_1} {Out : Type u_2} [Fintype Tag] [Fintype Out] {p q : Tag × Out → ℝ} {ρ ε : ℝ} (near : weightDist p q ≤ ρ) (uniform : weightDist q (uniformSecondWeight q) ≤ ε) : weightDist p (uniformSecondWeight p) ≤ 2 * ρ + ε

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_uniformSecond_map_le_of_dist_of_same_first {α : Type u_1} {Tag : Type u_2} {Out : Type u_3} [Fintype α] [Fintype Tag] [Fintype Out] {p q : α → ℝ} {ρ ε : ℝ} (F : α → Tag × Out) (near : weightDist p q ≤ ρ) (uniform : weightDist (mapWeight F q) (uniformSecondWeight (mapWeight F q)) ≤ ε) (same : firstWeight (mapWeight F p) = firstWeight (mapWeight F q)) : weightDist (mapWeight F p) (uniformSecondWeight (mapWeight F p)) ≤ ρ + ε

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_uniformSecond_map_le_of_dist {α : Type u_1} {Tag : Type u_2} {Out : Type u_3} [Fintype α] [Fintype Tag] [Fintype Out] {p q : α → ℝ} {ρ ε : ℝ} (F : α → Tag × Out) (near : weightDist p q ≤ ρ) (uniform : weightDist (mapWeight F q) (uniformSecondWeight (mapWeight F q)) ≤ ε) : weightDist (mapWeight F p) (uniformSecondWeight (mapWeight F p)) ≤ 2 * ρ + ε