Conditional finite weights and independent uniform extension

A conditional row divides by its first marginal. Zero-mass rows use the uniform distribution, so every row of a probability law is normalized when the second alphabet is nonempty. Uniform extension retains an arbitrary first-coordinate law and samples a fresh independent second coordinate. Uniformizing a joint law means keeping its actual first marginal.

noncomputable def Algebraic.Cutwidth.Extractor.conditionalWeight {α : Type u_1} {β : Type u_2} [Fintype β] (p : α × β → ℝ) (a : α) (b : β) : ℝ

Normalize a row, completing zero-mass rows by the uniform weighting.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Extractor.uniformExtensionWeight (β : Type u_1) [Fintype β] {α : Type u_2} (w : α → ℝ) (ab : α × β) : ℝ

Append an independent uniform second coordinate to a supplied first-coordinate weighting.

Equations

• Algebraic.Cutwidth.Extractor.uniformExtensionWeight β w ab = w ab.1 * Algebraic.Cutwidth.Extractor.uniformWeight β ab.2

noncomputable def Algebraic.Cutwidth.Extractor.uniformSecondWeight {α : Type u_1} {β : Type u_2} [Fintype β] (p : α × β → ℝ) : α × β → ℝ

Keep the actual first marginal of a joint weighting and uniformize the second coordinate.

Equations

• Algebraic.Cutwidth.Extractor.uniformSecondWeight p = Algebraic.Cutwidth.Extractor.uniformExtensionWeight β (Algebraic.Cutwidth.Extractor.firstWeight p)