Documentation

LeanPool.CCDN.AuxiliaryPolynomial.HypersurfaceRankProfile

Uniform bounds for the exact homogeneous hypersurface Hilbert rank. The factorial leading coefficient is retained in both directions.

theorem CCDN.hypersurface_rank_binomial_bounds {r d M s : ℕ} (hdM : d ≤ M) (hr : s + (r + 1 + (M - d)).choose (M - d) = (r + 1 + M).choose M) :
d * (r + (M - d)).choose r ≤ s ∧ s ≤ d * (r + M).choose r

The Hilbert function s of a degree-d hypersurface in r + 2 homogeneous variables, given by s + C(r + 1 + (M - d), M - d) = C(r + 1 + M, M), satisfies d * C(r + (M - d), r) ≤ s ≤ d * C(r + M, r).

theorem CCDN.hypersurface_rank_power_bounds {r d M s : ℕ} (hdM : d ≤ M) (hr : s + (r + 1 + (M - d)).choose (M - d) = (r + 1 + M).choose M) :
↑d * (↑M - ↑d + 1) ^ r / ↑r.factorial ≤ ↑s ∧ ↑s ≤ ↑d * (↑M + ↑r) ^ r / ↑r.factorial

Uniform power bounds with exact leading coefficient d/r!. The error is controlled by shifts of at most d and r in the degree M.