Conditioning finite sources without discarding zero-mass rows

Every row is normalized, with a uniform completion at null events. Exact factorization recovers the original joint law. Total variation from a fresh uniform output equals the average conditional distance, retaining the actual first marginal. These identities support finite leakage and independence merging without a pointwise conditional entropy assumption.

theorem Algebraic.Cutwidth.Extractor.conditionalWeight_factor {α : Type u_1} {β : Type u_2} [Fintype β] (p : α × β → ℝ) (nonnegative : ∀ (ab : α × β), 0 ≤ p ab) (a : α) (b : β) : firstWeight p a * conditionalWeight p a b = p (a, b)

Multiplying a conditional row by its marginal recovers each original point mass.

theorem Algebraic.Cutwidth.Extractor.IsProbabilityWeight.conditionalWeight {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [Nonempty β] {p : α × β → ℝ} (probability : IsProbabilityWeight p) (a : α) : IsProbabilityWeight (Extractor.conditionalWeight p a)

Every conditional row of a probability law is normalized, including null rows.

theorem Algebraic.Cutwidth.Extractor.IsProbabilityWeight.uniformExtension {α : Type u_1} [Fintype α] {w : α → ℝ} (probability : IsProbabilityWeight w) (β : Type u_2) [Fintype β] [Nonempty β] : IsProbabilityWeight (uniformExtensionWeight β w)

Appending an independent uniform coordinate preserves normalization.

theorem Algebraic.Cutwidth.Extractor.firstWeight_uniformExtension {α : Type u_1} {β : Type u_2} [Fintype β] [Nonempty β] (w : α → ℝ) : firstWeight (uniformExtensionWeight β w) = w

Uniform extension preserves its supplied first-coordinate weighting exactly.

theorem Algebraic.Cutwidth.Extractor.IsProbabilityWeight.uniformSecond {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [Nonempty β] {p : α × β → ℝ} (probability : IsProbabilityWeight p) : IsProbabilityWeight (uniformSecondWeight p)

Replacing the second coordinate by fresh uniform randomness preserves probability.

theorem Algebraic.Cutwidth.Extractor.weightDist_uniformSecond_eq {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {p : α × β → ℝ} (probability : IsProbabilityWeight p) : weightDist p (uniformSecondWeight p) = ∑ a : α, firstWeight p a * weightDist (conditionalWeight p a) (uniformWeight β)

Distance from a conditionally uniform output averages the exact row distances.

theorem Algebraic.Cutwidth.Extractor.firstWeight_map_fiber {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β → ℝ) (f : α → β → γ) : firstWeight (mapWeight (fun (ab : α × β) => (ab.1, f ab.1 ab.2)) p) = firstWeight p

Processing the second coordinate separately on each row preserves the first marginal.

theorem Algebraic.Cutwidth.Extractor.weightDist_uniformSecond_tagged {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype ι] [Fintype α] [Fintype β] (w : ι → ℝ) (p : ι → α × β → ℝ) (nonnegative : ∀ (i : ι), 0 ≤ w i) : weightDist (fun (iab : (ι × α) × β) => w iab.1.1 * p iab.1.1 (iab.1.2, iab.2)) (uniformSecondWeight fun (iab : (ι × α) × β) => w iab.1.1 * p iab.1.1 (iab.1.2, iab.2)) = ∑ i : ι, w i * weightDist (p i) (uniformSecondWeight (p i))

Retaining a nonnegative mixture tag averages distance from conditionally uniform output.

theorem Algebraic.Cutwidth.Extractor.firstWeight_map_first {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β → ℝ) (f : α → γ) : firstWeight (mapWeight (fun (ab : α × β) => (f ab.1, ab.2)) p) = mapWeight f (firstWeight p)

A deterministic observation of the first coordinate pushes forward its marginal.

theorem Algebraic.Cutwidth.Extractor.mapWeight_uniformExtension {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] (w : α → ℝ) (f : α → γ) : mapWeight (fun (ab : α × β) => (f ab.1, ab.2)) (uniformExtensionWeight β w) = uniformExtensionWeight β (mapWeight f w)

Observing the first coordinate commutes with adding independent uniform randomness.

theorem Algebraic.Cutwidth.Extractor.uniformSecondWeight_map_first {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β → ℝ) (f : α → γ) : mapWeight (fun (ab : α × β) => (f ab.1, ab.2)) (uniformSecondWeight p) = uniformSecondWeight (mapWeight (fun (ab : α × β) => (f ab.1, ab.2)) p)

Uniformizing an output commutes with every deterministic observation of its side information.

theorem Algebraic.Cutwidth.Extractor.weightDist_uniformSecond_map_first_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β → ℝ) (f : α → γ) : weightDist (mapWeight (fun (ab : α × β) => (f ab.1, ab.2)) p) (uniformSecondWeight (mapWeight (fun (ab : α × β) => (f ab.1, ab.2)) p)) ≤ weightDist p (uniformSecondWeight p)

Forgetting side information cannot increase the distance from an independent uniform output.