Binomial profiles for hypersurface local layers in all dimensions. The cumulative bound retains the leading coefficient μ/n! needed for the sharp determinant exponent.

def CCDN.hypersurfaceLayerBound (n μ k : ℕ) : ℕ

The degree-k Hilbert function of a homogeneous hypersurface of degree μ in n+1 variables, including the degrees below μ.

Equations

• CCDN.hypersurfaceLayerBound n μ k = (n + k).choose n - if μ ≤ k then (n + (k - μ)).choose n else 0

theorem CCDN.hypersurfaceLayerBound_succ_zero (n μ : ℕ) : hypersurfaceLayerBound n (μ + 1) 0 = 1

For positive degree μ, the Hilbert function hypersurfaceLayerBound n μ takes the value 1 in degree zero.

theorem CCDN.hypersurfaceLayerBound_succ_succ (n μ k : ℕ) : hypersurfaceLayerBound (n + 1) (μ + 1) (k + 1) = (n + (k + 1)).choose n + hypersurfaceLayerBound (n + 1) μ k

Recursion for the Hilbert function of a hypersurface: hypersurfaceLayerBound (n + 1) (μ + 1) in degree k + 1 equals (n + (k + 1)).choose n plus hypersurfaceLayerBound (n + 1) μ in degree k.

theorem CCDN.hypersurfaceLayerBound_le_mul_choose (n μ k : ℕ) : hypersurfaceLayerBound (n + 1) μ k ≤ μ * (n + k).choose n

A uniform shifted bound with the exact leading coefficient. The dimension is n+1; unlike the sharper error in CCDN 2.1, the lower terms here may contain μ.

theorem CCDN.originLayer_cumulative_le {K : Type u_1} [Field K] {n μ : ℕ} (f : MvPolynomial (Fin (n + 2)) K) (hf : f ∈ MvPolynomial.idealOfVars (Fin (n + 2)) K ^ μ) (hμ : (MvPolynomial.homogeneousComponent μ) f ≠ 0) (k : ℕ) : ∑ j : Fin (k + 1), Module.finrank K ↥(originLayer f ↑j) ≤ μ * (n + k + 1).choose (n + 1)

The cumulative local Hilbert function has this bound.