A lower set of exponent vectors is a finite disjoint union of translated coordinate orthants. Dickson's lemma supplies a threshold above which each coordinate is either fixed or unrestricted.

def CCDN.clampExponent {σ : Type u_1} (B : ℕ) (a : σ → ℕ) : σ → ℕ

Truncate every coordinate of the exponent vector a at B, giving i ↦ min (a i) B.

Equations

• CCDN.clampExponent B a i = min (a i) B

theorem CCDN.lowerSet_clamp_stabilizes {σ : Type u_1} [Finite σ] (S : Set (σ → ℕ)) (hS : IsLowerSet S) : ∃ (B : ℕ), 0 < B ∧ ∀ (a : σ → ℕ), a ∈ S ↔ clampExponent B a ∈ S

Membership in a lower exponent set is determined by a finite box.

@[reducible, inline]

abbrev CCDN.orthantFree {σ : Type u_1} {B : ℕ} (b : σ → Fin (B + 1)) : Type u_1

A truncated coordinate pattern, with value B marking its free coordinates.

Equations

• CCDN.orthantFree b = { i : σ // ↑(b i) = B }

def CCDN.orthantBaseDegree {σ : Type u_1} [Fintype σ] {B : ℕ} (b : σ → Fin (B + 1)) : ℕ

The total degree ∑ i, b i of the base point of the orthant with truncated coordinate pattern b.

Equations

• CCDN.orthantBaseDegree b = ∑ i : σ, ↑(b i)

def CCDN.orthantExpand {σ : Type u_1} {B : ℕ} (b : σ → Fin (B + 1)) (c : orthantFree b → ℕ) : σ → ℕ

The point of the orthant with truncated pattern b obtained by adding c to the base point b in the free coordinates (those where b i = B).

Equations

• CCDN.orthantExpand b c i = ↑(b i) + if h : ↑(b i) = B then c ⟨i, h⟩ else 0

theorem CCDN.clamp_orthantExpand {σ : Type u_1} {B : ℕ} (b : σ → Fin (B + 1)) (c : orthantFree b → ℕ) : clampExponent B (orthantExpand b c) = fun (i : σ) => ↑(b i)

Every point of the orthant with truncated pattern b truncates back to b.

theorem CCDN.orthantExpand_sum {σ : Type u_1} [Fintype σ] {B : ℕ} (b : σ → Fin (B + 1)) (c : orthantFree b → ℕ) : ∑ i : σ, orthantExpand b c i = orthantBaseDegree b + ∑ j : orthantFree b, c j

The total degree of a point of the orthant with pattern b is the base degree of b plus the total of the added free coordinates.

def CCDN.orthantExpandEquiv {σ : Type u_1} {B : ℕ} (b : σ → Fin (B + 1)) : (orthantFree b → ℕ) ≃ { a : σ → ℕ // clampExponent B a = fun (i : σ) => ↑(b i) }

Every cell of the truncation map is a coordinate orthant.

Equations

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

def CCDN.exponentPattern {σ : Type u_1} (B : ℕ) (a : σ → ℕ) : σ → Fin (B + 1)

Truncation gives the unique cell containing any exponent vector.

Equations

• CCDN.exponentPattern B a i = ⟨min (a i) B, ⋯⟩

noncomputable def CCDN.boundedOrthantEquiv {σ : Type u_1} [Fintype σ] {B N : ℕ} (b : σ → Fin (B + 1)) (hN : orthantBaseDegree b ≤ N) : { c : orthantFree b → ℕ // ∑ i : orthantFree b, c i ≤ N - orthantBaseDegree b } ≃ { a : σ → ℕ // (clampExponent B a = fun (i : σ) => ↑(b i)) ∧ ∑ i : σ, a i ≤ N }

A bounded slice of an orthant is a bounded exponent simplex in its free coordinates.

Equations

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