Coupling conditionally on an external transcript

Couple each normalized transcript row and average using the unchanged transcript marginal. Null rows contribute zero. The coupling's kernel identity survives this scaling without a positivity premise on any row.

theorem Algebraic.Cutwidth.Extractor.Internal.conditionalCoupling_factor {Z : Type u_1} {A : Type u_2} [Fintype Z] [Fintype A] {p : Z × A → ℝ} (hp : IsProbabilityWeight p) : (fun (za : Z × A) => firstWeight p za.1 * conditionalWeight p za.1 za.2) = p

theorem Algebraic.Cutwidth.Extractor.Internal.conditionalCoupling_first_factor {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] {p : Z × A × B → ℝ} (hp : IsProbabilityWeight p) : mapWeight (fun (zab : Z × A × B) => (zab.1, zab.2.1)) p = fun (za : Z × A) => firstWeight p za.1 * firstWeight (conditionalWeight p za.1) za.2

theorem Algebraic.Cutwidth.Extractor.Internal.conditionalCoupling_dist_eq {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] {p : Z × A × B → ℝ} {q : Z × A → ℝ} (hp : IsProbabilityWeight p) (hq : IsProbabilityWeight q) (same : firstWeight p = firstWeight q) : weightDist (mapWeight (fun (zab : Z × A × B) => (zab.1, zab.2.1)) p) q = ∑ z : Z, firstWeight p z * weightDist (firstWeight (conditionalWeight p z)) (conditionalWeight q z)

theorem Algebraic.Cutwidth.Extractor.Internal.exists_conditional_marginal_replacement_kernel {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] {p : Z × A × B → ℝ} {q : Z × A → ℝ} (hp : IsProbabilityWeight p) (hq : IsProbabilityWeight q) (same : firstWeight p = firstWeight q) : ∃ (ρ : (Z × A × B) × A → ℝ), IsProbabilityWeight ρ ∧ (∀ (zab : Z × A × B), ∑ a' : A, ρ (zab, a') = p zab) ∧ (∀ (z : Z) (a' : A), ∑ ab : A × B, ρ ((z, ab), a') = q (z, a')) ∧ ∑ t : (Z × A × B) × A with t.1.2.1 ≠ t.2, ρ t = weightDist (mapWeight (fun (zab : Z × A × B) => (zab.1, zab.2.1)) p) q ∧ ∀ (z : Z) (a : A) (b : B) (a' : A), (∑ b' : B, p (z, a, b')) * ρ ((z, a, b), a') = p (z, a, b) * ∑ b' : B, ρ ((z, a, b'), a')

theorem Algebraic.Cutwidth.Extractor.Internal.exists_conditional_joint_marginal_replacement {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] {p : Z × A × B → ℝ} {q : Z × A → ℝ} (hp : IsProbabilityWeight p) (hq : IsProbabilityWeight q) (same : firstWeight p = firstWeight q) : ∃ (p' : Z × A × B → ℝ), IsProbabilityWeight p' ∧ mapWeight (fun (zab : Z × A × B) => (zab.1, zab.2.1)) p' = q ∧ (∀ (z : Z) (b : B), ∑ a : A, p' (z, a, b) = ∑ a : A, p (z, a, b)) ∧ weightDist p p' = weightDist (mapWeight (fun (zab : Z × A × B) => (zab.1, zab.2.1)) p) q