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

Helper: n^d ≤ (n+1)·(n+2)···(n+d) (the ascending factorial).

theorem pow_le_factorial_mul_choose_add (n d : ℕ) : n ^ d ≤ d.factorial * (n + d).choose d

Helper polynomial-growth lower bound: n^d ≤ d! · C(n+d, d).

theorem choose_add_le_two_pow_mul_pow (n d : ℕ) (hnd : d ≤ n) : (n + d).choose d ≤ 2 ^ d * n ^ d

Helper polynomial-growth upper bound: for d ≤ n, C(n+d, d) ≤ 2^d · n^d.

def polyDimFun (d n : ℕ) : ℕ

The Hilbert function n ↦ C(n+d, d) of the polynomial ring in d variables; the prototypical reference for Θ(n^d) growth.

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 on A induced by an algebra surjection f: the n-th piece is the image of polynomials of total degree ≤ n under f.

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

The Hilbert function D_V(n) for the filtration generatorFiltration f: the k-dimension of its n-th 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 : ℕ), polyDimFun d n ≤ dimFun f n) ∧ ∀ (n : ℕ), dimFun f n ≤ C * polyDimFun d n

Comparison via Noether normalization: the Hilbert function dimFun f is sandwiched between polyDimFun d and a constant multiple of it, where d is the Krull dimension.

theorem HilbertFunctionGrowth.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' * dimFun f n) ∧ ∀ (n : ℕ), d ≤ n → dimFun f n ≤ c * n ^ d

Hilbert function growth (Prop 11, Lec 8): for a finitely generated domain A over a field k of Krull dimension d, the Hilbert function satisfies D_V(n) = Θ(n^d).

theorem hilbert_function_eventually_polynomial (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) : ∃ (P : Polynomial ℚ) (N₀ : ℕ), (∀ (n : ℕ), N₀ ≤ n → ↑(dimFun f n) = Polynomial.eval (↑n) P) ∧ P.natDegree = d

Eventually polynomial form of the Hilbert function: there is a rational polynomial P of degree d such that dimFun f n = P(n) for all sufficiently large n.