Lifting a marginal coupling through a correlated joint law

Given the old joint weight on (a,b) and a coupling of its first marginal with a new a, retain the conditional distribution of b given the old a. The resulting triple law keeps the entire original joint law and has the requested new marginal. No independence between a and b is needed. Zero-mass old fibers contribute zero and require no conditional distribution. The replacement depends on the old first coordinate through a kernel; a division-free identity records the resulting conditional independence.

theorem Algebraic.Cutwidth.Extractor.Internal.exists_marginal_replacement_kernel {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {p : α × β → ℝ} {q : α → ℝ} (hp : IsProbabilityWeight p) (hq : IsProbabilityWeight q) : ∃ (ρ : (α × β) × α → ℝ), IsProbabilityWeight ρ ∧ (∀ (z : α × β), ∑ a' : α, ρ (z, a') = p z) ∧ (∀ (a' : α), ∑ z : α × β, ρ (z, a') = q a') ∧ ∑ z : (α × β) × α with z.1.1 ≠ z.2, ρ z = weightDist (firstWeight p) q ∧ ∀ (a : α) (b : β) (a' : α), firstWeight p a * ρ ((a, b), a') = p (a, b) * ∑ b' : β, ρ ((a, b'), a')

theorem Algebraic.Cutwidth.Extractor.Internal.exists_marginal_replacement_coupling {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {p : α × β → ℝ} {q : α → ℝ} (hp : IsProbabilityWeight p) (hq : IsProbabilityWeight q) : ∃ (ρ : (α × β) × α → ℝ), IsProbabilityWeight ρ ∧ (∀ (z : α × β), ∑ a' : α, ρ (z, a') = p z) ∧ (∀ (a' : α), ∑ z : α × β, ρ (z, a') = q a') ∧ ∑ z : (α × β) × α with z.1.1 ≠ z.2, ρ z = weightDist (firstWeight p) q