Factored-law lifts and exact distance averages

Keeping the left kernel normalized makes the distance between two factored laws exactly the weighted average of their right-kernel distances. No individual transcript row needs positive transcript mass.

theorem Algebraic.Cutwidth.Extractor.Internal.rightCoordinateLift_probability {Z : Type u_1} {B : Type u_2} {Q : Type u_3} [Fintype B] [Fintype Q] (r : Z → B → ℝ) (q : Z → B → Q) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (z : Z) : IsProbabilityWeight (rightCoordinateLift r q z)

theorem Algebraic.Cutwidth.Extractor.Internal.rightCoordinateLift_fst {Z : Type u_1} {B : Type u_2} {Q : Type u_3} [Fintype B] [Fintype Q] (r : Z → B → ℝ) (q : Z → B → Q) (z : Z) : mapWeight Prod.fst (rightCoordinateLift r q z) = r z

theorem Algebraic.Cutwidth.Extractor.Internal.rightCoordinateLift_snd {Z : Type u_1} {B : Type u_2} {Q : Type u_3} [Fintype B] [Fintype Q] (r : Z → B → ℝ) (q : Z → B → Q) (z : Z) : mapWeight Prod.snd (rightCoordinateLift r q z) = mapWeight (q z) (r z)

theorem Algebraic.Cutwidth.Extractor.Internal.factoredWeight_map_right {Z : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Fintype Z] [Fintype A] [Fintype B] [Fintype C] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (f : Z → B → C) : mapWeight (fun (p : (Z × B) × A) => ((p.1.1, f p.1.1 p.1.2), p.2)) (factoredWeight w l r) = factoredWeight w l fun (z : Z) => mapWeight (f z) (r z)

theorem Algebraic.Cutwidth.Extractor.Internal.factoredWeight_rightCoordinateLift {Z : Type u_1} {A : Type u_2} {B : Type u_3} {Q : Type u_4} [Fintype Z] [Fintype A] [Fintype B] [Fintype Q] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (q : Z → B → Q) : factoredWeight w l (rightCoordinateLift r q) = mapWeight (fun (p : (Z × B) × A) => ((p.1.1, p.1.2, q p.1.1 p.1.2), p.2)) (factoredWeight w l r)

theorem Algebraic.Cutwidth.Extractor.Internal.factoredWeight_dist_right {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r r' : Z → B → ℝ) (nonnegative : ∀ (z : Z), 0 ≤ w z) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) : weightDist (factoredWeight w l r) (factoredWeight w l r') = ∑ z : Z, w z * weightDist (r z) (r' z)

theorem Algebraic.Cutwidth.Extractor.Internal.retainedSeedWeight_dist_eq_sum {Z : Type u_1} {B : Type u_2} {Q : Type u_3} [Fintype Z] [Fintype B] [Fintype Q] (w : Z → ℝ) (r : Z → B → ℝ) (q : Z → B → Q) (nonnegative : ∀ (z : Z), 0 ≤ w z) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : weightDist (retainedSeedWeight w r q) (uniformSecondWeight (retainedSeedWeight w r q)) = ∑ z : Z, w z * weightDist (mapWeight (q z) (r z)) (uniformWeight Q)

theorem Algebraic.Cutwidth.Extractor.Internal.rightCoordinateRepair_source_eq {Z : Type u_1} {B : Type u_2} {Q : Type u_3} {X : Type u_4} [Fintype B] [Fintype Q] (w : Z → ℝ) (r : Z → B → ℝ) (r' : Z → B × Q → ℝ) (same : ∀ (z : Z) (b : B), w z * mapWeight Prod.fst (r' z) b = w z * r z b) (x : Z → B → X) (z : Z) (x₀ : X) : w z * mapWeight (fun (bq : B × Q) => x z bq.1) (r' z) x₀ = w z * mapWeight (x z) (r z) x₀

theorem Algebraic.Cutwidth.Extractor.Internal.factoredWeight_forget_right_eq {Z : Type u_1} {A : Type u_2} {B : Type u_3} {Q : Type u_4} [Fintype Z] [Fintype A] [Fintype B] [Fintype Q] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (r' : Z → B × Q → ℝ) (same : ∀ (z : Z) (b : B), w z * mapWeight Prod.fst (r' z) b = w z * r z b) : mapWeight (fun (p : (Z × B × Q) × A) => ((p.1.1, p.1.2.1), p.2)) (factoredWeight w l r') = factoredWeight w l r