Tag-dependent output bijections preserve conditional uniformity #
For arbitrary finite real weights, changing the output by a bijection that depends on the retained tag commutes with replacing the output by independent uniform randomness. The exact total variation distance is preserved.
Adding a tag-dependent mask is a special case for finite additive groups. The tag retains its actual marginal; normalization, positivity, commutativity, and nonempty-type assumptions are unnecessary for these identities.
theorem
Algebraic.Cutwidth.Extractor.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)
A tag-dependent output equivalence preserves the exact distance from conditional uniformity.
theorem
Algebraic.Cutwidth.Extractor.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)
A tag-dependent additive mask preserves the exact distance from conditional uniformity.