Normalized rows and total variation with retained conditioning

Nonnegative zero-mass rows vanish pointwise, making row factorization exact even on null events. Tagged mixture distance then identifies conditional distance with its average against the unchanged first marginal.

theorem Algebraic.Cutwidth.Extractor.Internal.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)

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

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

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

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

theorem Algebraic.Cutwidth.Extractor.Internal.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 β)

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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))

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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)