Transporting conditional uniformity through fiber equivalences

A bijection of each output fiber preserves its uniform law and the retained marginal. The resulting map on the tagged product is itself a bijection, so its total variation distance is unchanged. These identities hold for signed weights and empty alphabets as well as for probability laws.

theorem Algebraic.Cutwidth.Extractor.Internal.mapWeight_uniformSecond_fiberEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β → ℝ) (e : α → β ≃ γ) : mapWeight (fun (ab : α × β) => (ab.1, (e ab.1) ab.2)) (uniformSecondWeight p) = uniformSecondWeight (mapWeight (fun (ab : α × β) => (ab.1, (e ab.1) ab.2)) p)

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_uniformSecond_fiberEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β → ℝ) (e : α → β ≃ γ) : weightDist (mapWeight (fun (ab : α × β) => (ab.1, (e ab.1) ab.2)) p) (uniformSecondWeight (mapWeight (fun (ab : α × β) => (ab.1, (e ab.1) ab.2)) p)) = weightDist p (uniformSecondWeight p)

theorem Algebraic.Cutwidth.Extractor.Internal.mapWeight_uniformSecond_add_right {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [AddGroup β] (p : α × β → ℝ) (mask : α → β) : mapWeight (fun (ab : α × β) => (ab.1, ab.2 + mask ab.1)) (uniformSecondWeight p) = uniformSecondWeight (mapWeight (fun (ab : α × β) => (ab.1, ab.2 + mask ab.1)) p)

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_uniformSecond_add_right {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [AddGroup β] (p : α × β → ℝ) (mask : α → β) : weightDist (mapWeight (fun (ab : α × β) => (ab.1, ab.2 + mask ab.1)) p) (uniformSecondWeight (mapWeight (fun (ab : α × β) => (ab.1, ab.2 + mask ab.1)) p)) = weightDist p (uniformSecondWeight p)