theorem card_antidiagonalTuple (k n : ℕ) : (Finset.Nat.antidiagonalTuple k n).card = k.multichoose n

The cardinality of Fin k → ℕ tuples summing to n equals multichoose k n.

theorem Nat.card_antidiagonal_tuple_choose (n d : ℕ) : (Finset.Nat.antidiagonalTuple (n + 1) d).card = (n + d).choose d

Closed form for the cardinality of Fin (n + 1) → ℕ tuples summing to d: it equals (n + d) choose d.

def growthFun_polyring (d n : ℕ) : ℕ

The growth (Hilbert) function of the polynomial ring k[x_0, …, x_{d-1}] in degree n: (n + d choose d).

theorem pow_le_ascFactorial_succ' (n d : ℕ) : n ^ d ≤ (n + 1).ascFactorial d

Auxiliary bound: n^d ≤ (n + 1).ascFactorial d for the growth function analysis.

theorem growthFun_lower_bound (n d : ℕ) : n ^ d ≤ d.factorial * growthFun_polyring d n

Lower bound on the polynomial growth function: n^d ≤ d! · growthFun_polyring d n.

theorem growthFun_upper_bound (n d : ℕ) (hnd : d ≤ n) : growthFun_polyring d n ≤ 2 ^ d * n ^ d

Upper bound on the polynomial growth function: growthFun_polyring d n ≤ 2^d · n^d for d ≤ n.

noncomputable def generatorFiltration' {k : Type u_1} [Field k] {A : Type u_2} [CommRing A] [Algebra k A] {m : ℕ} (f : MvPolynomial (Fin m) k →ₐ[k] A) (n : ℕ) : Submodule k A

Filtration of a finitely-generated algebra by total-degree truncation: the image under a presentation f of polynomials of total degree ≤ n.

noncomputable def growthFun {k : Type u_1} [Field k] {A : Type u_2} [CommRing A] [Algebra k A] {m : ℕ} (f : MvPolynomial (Fin m) k →ₐ[k] A) (n : ℕ) : ℕ

Growth function of a finitely-generated algebra A along a presentation f: the k-dimension of the degree-n filtration piece.

theorem noether_normalization_growth_comparison' (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k A] (d : ℕ) (hd : ringKrullDim A = ↑d) (m : ℕ) (f : MvPolynomial (Fin m) k →ₐ[k] A) (hf : Function.Surjective ⇑f) : ∃ (C : ℕ), 0 < C ∧ (∀ (n : ℕ), growthFun_polyring d n ≤ growthFun f n) ∧ ∀ (n : ℕ), growthFun f n ≤ C * growthFun_polyring d n

Noether normalization growth comparison: the growth function of A is sandwiched between the polynomial growth function growthFun_polyring d and a uniform multiple of it.

theorem proposition_11 (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k A] (d : ℕ) (hd : ringKrullDim A = ↑d) (m : ℕ) (f : MvPolynomial (Fin m) k →ₐ[k] A) (hf : Function.Surjective ⇑f) : ∃ (c' : ℕ) (c : ℕ), 0 < c' ∧ 0 < c ∧ (∀ (n : ℕ), n ^ d ≤ c' * growthFun f n) ∧ ∀ (n : ℕ), d ≤ n → growthFun f n ≤ c * n ^ d

Proposition 11 (separatedness/growth criterion): for a finitely-generated k-algebra A of Krull dimension d, the growth function satisfies n^d ≲ growthFun f n ≲ n^d.