The logarithm of the exact hypersurface rank has the uniform leading term log(d)+r*log(M), with an explicit error depending only on dimension.

noncomputable def CCDN.hypersurfaceRankLogError (r : ℕ) : ℝ

The dimension constant r log 2 + log r! + r log (r + 1) bounding the deviation of the logarithm of the hypersurface Hilbert function from log d + r log M.

Equations

• CCDN.hypersurfaceRankLogError r = ↑r * Real.log 2 + Real.log ↑r.factorial + ↑r * Real.log (↑r + 1)

theorem CCDN.hypersurface_rank_log_error {r d M s : ℕ} (hrpos : 0 < r) (hd : 0 < d) (hM : 2 * d ≤ M) (hr : s + (r + 1 + (M - d)).choose (M - d) = (r + 1 + M).choose M) : |Real.log ↑s - (Real.log ↑d + ↑r * Real.log ↑M)| ≤ hypersurfaceRankLogError r

The rank logarithm loses only a dimension constant once M>=2d.