Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Gaussian.Layout.Internal.Grid

Prefix cuts of a score order through a threshold grid #

A real score on a finite type orders it lexicographically by the score and then by a fixed enumeration. scoreKey X v is the number of elements strictly below v in this order, an injective natural-number key whose prefixes are lower sets for the score.

Every prefix of the score order lies between two consecutive threshold sets {X < a + i δ}, or inside one of the two tails. With maximum degree three, its cut is therefore at most the cut of the lower threshold set plus three times the number of scores in the window, or three times the size of a tail.

source
noncomputable def Algebraic.Cutwidth.Gaussian.Internal.scoreRank {W : Type} [Fintype W] (X : W → ℝ) (v : W) :
Lex (ℝ × ℕ)

The lexicographic position of a vertex: its score, then its enumeration index.

Equations
Instances For
    source
    noncomputable def Algebraic.Cutwidth.Gaussian.Internal.scoreKey {W : Type} [Fintype W] (X : W → ℝ) (v : W) :
    ℕ

    The number of vertices strictly below v in the lexicographic score order.

    Equations
    Instances For
      source
      theorem Algebraic.Cutwidth.Gaussian.Internal.scoreRank_injective {W : Type} [Fintype W] (X : W → ℝ) :
      Function.Injective (scoreRank X)
      source
      theorem Algebraic.Cutwidth.Gaussian.Internal.scoreKey_lt_of_scoreRank_lt {W : Type} [Fintype W] {X : W → ℝ} {u v : W} (h : scoreRank X u < scoreRank X v) :
      scoreKey X u < scoreKey X v
      source
      theorem Algebraic.Cutwidth.Gaussian.Internal.scoreKey_injective {W : Type} [Fintype W] (X : W → ℝ) :
      Function.Injective (scoreKey X)
      source
      theorem Algebraic.Cutwidth.Gaussian.Internal.scoreKey_lt_of_lt {W : Type} [Fintype W] {X : W → ℝ} {u v : W} (h : X u < X v) :
      scoreKey X u < scoreKey X v
      source
      theorem Algebraic.Cutwidth.Gaussian.Internal.card_cutFinset_le_three_mul {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (degree : ∀ (v : W), H.degree v ≤ 3) (S : Finset W) :
      (H.cutFinset S).card ≤ 3 * S.card

      A cut has at most three edges per vertex of the side.

      source
      theorem Algebraic.Cutwidth.Gaussian.Internal.card_cutFinset_le_of_subset {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (degree : ∀ (v : W), H.degree v ≤ 3) {S T : Finset W} (hST : S ⊆ T) :
      (H.cutFinset T).card ≤ (H.cutFinset S).card + 3 * (T \ S).card

      Enlarging a side changes its cut by at most three edges per added vertex.

      source
      theorem Algebraic.Cutwidth.Gaussian.Internal.card_cutFinset_scoreKey_le {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (degree : ∀ (v : W), H.degree v ≤ 3) (X : W → ℝ) {a δ : ℝ} (hδ : 0 < δ) (M : ℕ) {B : ℝ} (low : 3 * ↑{v : W | X v < a}.card ≤ B) (high : 3 * ↑{v : W | a + ↑M * δ ≤ X v}.card ≤ B) (mid : ∀ i < M, ↑(H.cutFinset {v : W | X v < a + ↑i * δ}).card + 3 * ↑{v : W | a + ↑i * δ ≤ X v ∧ X v < a + (↑i + 1) * δ}.card ≤ B) (t : ℕ) :
      ↑(H.cutFinset {w : W | scoreKey X w < t}).card ≤ B

      Grid bound for score prefixes. Fix thresholds a + i δ for i ≤ M. If both tails are small and each threshold cut plus three times its window is at most B, then every prefix of the score order has at most B crossing edges.