The factorial and coefficient-count logarithms in the determinant comparison cost only a dimension constant times s^(1+1/r).

theorem CCDN.hypersurface_rank_ge_degree_parameter {r d M s : ℕ} (hrpos : 0 < r) (hd : 0 < d) (hdM : d ≤ M) (hr : s + (r + 1 + (M - d)).choose (M - d) = (r + 1 + M).choose M) : M ≤ s

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), is at least M when 0 < r and 0 < d ≤ M.

theorem CCDN.log_le_dimension_root {r : ℕ} (hr : 0 < r) {s : ℝ} (hs : 0 < s) : Real.log s ≤ ↑r * s ^ (1 / ↑r)

For 0 < r and positive real s, log s ≤ r * s ^ (1/r).

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

The dimension constant ((r + 2) r + (r + 1)) / 2 bounding the archimedean logarithmic terms of the determinant comparison by a multiple of s ^ (1 + 1/r).

Equations

• CCDN.hypersurfaceArchimedeanError r = ((↑r + 2) * ↑r + (↑r + 1)) / 2

theorem CCDN.hypersurface_rank_archimedean_error {r d M s : ℕ} (hrpos : 0 < r) (hd : 0 < d) (hdM : d ≤ M) (hr : s + (r + 1 + (M - d)).choose (M - d) = (r + 1 + M).choose M) : Real.log ↑s.factorial / 2 + ↑s / 2 * Real.log ↑((r + 1 + M).choose M) ≤ hypersurfaceArchimedeanError r * ↑s ^ (1 + 1 / ↑r)

The two archimedean logarithmic terms have the exact scale of the main rank term and cost only an explicit dimension constant.