Transporting uniformity through independent messages

Balanced output maps contract conditional uniformity error. Relabeling an observation and applying a transcript-dependent output bijection also contract it. An observation of the independent opposite source preserves the averaged error exactly, including null transcript rows.

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_uniformSecond_map_output_le {Z : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype Z] [Fintype X] [Fintype Y] (p : Z × X → ℝ) (f : X → Y) (balanced : mapWeight f (uniformWeight X) = uniformWeight Y) : weightDist (mapWeight (fun (zx : Z × X) => (zx.1, f zx.2)) p) (uniformSecondWeight (mapWeight (fun (zx : Z × X) => (zx.1, f zx.2)) p)) ≤ weightDist p (uniformSecondWeight p)

theorem Algebraic.Cutwidth.Extractor.Internal.observedSeedWeight_image_dist_le {Z : Type u_1} {A : Type u_2} {U : Type u_3} {X : Type u_4} {Y : Type u_5} [Fintype Z] [Fintype A] [Fintype U] [Fintype X] [Fintype Y] (w : Z → ℝ) (l : Z → A → ℝ) (u : Z → A → U) (x : Z → A → X) (f : X → Y) (balanced : mapWeight f (uniformWeight X) = uniformWeight Y) : weightDist (observedSeedWeight w l u fun (z : Z) (a : A) => f (x z a)) (uniformSecondWeight (observedSeedWeight w l u fun (z : Z) (a : A) => f (x z a))) ≤ weightDist (observedSeedWeight w l u x) (uniformSecondWeight (observedSeedWeight w l u x))

theorem Algebraic.Cutwidth.Extractor.Internal.observedSeedWeight_transform_dist_le {Z : Type u_1} {A : Type u_2} {U : Type u_3} {V : Type u_4} {X : Type u_5} {Y : Type u_6} [Fintype Z] [Fintype A] [Fintype U] [Fintype V] [Fintype X] [Fintype Y] (w : Z → ℝ) (l : Z → A → ℝ) (u : Z → A → U) (x : Z → A → X) (f : Z → U → V) (e : Z → X ≃ Y) : weightDist (observedSeedWeight w l (fun (z : Z) (a : A) => f z (u z a)) fun (z : Z) (a : A) => (e z) (x z a)) (uniformSecondWeight (observedSeedWeight w l (fun (z : Z) (a : A) => f z (u z a)) fun (z : Z) (a : A) => (e z) (x z a))) ≤ weightDist (observedSeedWeight w l u x) (uniformSecondWeight (observedSeedWeight w l u x))

theorem Algebraic.Cutwidth.Extractor.Internal.observedSeedWeight_observe_other_dist {Z : Type u_1} {A : Type u_2} {B : Type u_3} {V : Type u_4} {U : Type u_5} {X : Type u_6} [Fintype Z] [Fintype A] [Fintype B] [Fintype V] [Fintype U] [Fintype X] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (g : Z → B → V) (u : Z → A → U) (x : Z → A → X) (hw : ∀ (z : Z), 0 ≤ w z) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : weightDist (observedSeedWeight (observedTranscriptWeight w r g) (fun (zv : Z × V) => l zv.1) (fun (zv : Z × V) => u zv.1) fun (zv : Z × V) => x zv.1) (uniformSecondWeight (observedSeedWeight (observedTranscriptWeight w r g) (fun (zv : Z × V) => l zv.1) (fun (zv : Z × V) => u zv.1) fun (zv : Z × V) => x zv.1)) = weightDist (observedSeedWeight w l u x) (uniformSecondWeight (observedSeedWeight w l u x))