The small-height numerical auxiliary-degree bound, with exact box and coefficient exponents and a constant depending only on dimension.
The additive error term, depending only on the dimension r and the constant E, in the
small-height logarithmic bound on the auxiliary degree M.
Equations
- CCDN.hypersurfaceSmallHeightError r E = (E + CCDN.hypersurfaceRankLogError r + 4 * (↑r + 1) ^ 2) / ↑r
Instances For
theorem
CCDN.hypersurface_small_height_log_degree_bound
{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)
(B L A E : ℝ)
(hB : 1 ≤ B)
(hL : 1 ≤ L)
(hheight : Real.log L ≤ 2 * ↑d * (↑r + 1) * Real.log B)
(hscale : ↑d * Real.log B ≤ ↑d ^ (1 / ↑r) * ↑M)
(hcomparison :
↑r.factorial ^ (1 / ↑r) * ↑s ^ (1 / ↑r) / ((↑r + 1) * ↑M) * (Real.log ↑s - ↑r * (4 * Real.log ↑d + Real.log A) - E) ≤ Real.log B - ↑((r + 1 + (M - d)).choose (M - d)) / (↑M * ↑s) * Real.log L)
:
Solve the normalized exact-rank inequality in the small-height range.
theorem
CCDN.hypersurface_degree_bound_of_log_bound
{r d M : ℕ}
{B L A C : ℝ}
(hd : 0 < d)
(hM : 0 < M)
(hB : 0 < B)
(hL : 0 < L)
(hA : 0 < A)
(hlog :
Real.log ↑M ≤ C + (4 - 1 / ↑r) * Real.log ↑d + Real.log A + (↑r + 1) / (↑r * ↑d ^ (1 / ↑r)) * Real.log B - Real.log L / (↑r * ↑d * ↑d ^ (1 / ↑r)))
:
Exponentiating retains all exponents in CCDN's coefficient-sensitive auxiliary bound.