Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Extractor.Strong.Block.Splitting.Defs

Repairing the second block while preserving the first marginal #

Rows of mass below K*μ are replaced by a uniform row of the same mass. All other rows are retained. If the original point masses are at most μ, the retained rows already satisfy the desired conditional cap. The formula is total, including zero-mass rows and empty finite second-coordinate types.

noncomputable def Algebraic.Cutwidth.Extractor.twoBlockRepair {α : Type u_1} {β : Type u_2} [Fintype β] (p : α × β → ℝ) (K : ℕ) (μ : ℝ) (ab : α × β) :

Uniformize only rows below the mass needed for the conditional point cap.

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