Documentation

LeanPool.CCDN.Curve.ProjectiveHilbertCurveGrowth

The plane curve estimate gives a smaller degree exponent for curves specified by their filtered Hilbert polynomial. The construction of the finite birational projection and its integer matrix is internal.

theorem CCDN.projective_hilbert_curve_dimension_growth (n : ℕ) (hn : 1 ≤ n) :
∃ (C : ℝ), 0 < C ∧ ∀ (I : Ideal (MvPolynomial (Fin (n + 1)) ℚ)), I.IsPrime → IsHomogeneousIdeal I → ∀ (d : ℕ), 5 ≤ d → HasProjectiveDimensionDegree I 1 d → ∀ (B : ℝ), 1 ≤ B → ↑(projectiveCount (projectiveIdealZeroLocus I) B) ≤ C * ↑d ^ (3 * (n + 1) + 4) * B

Dimension growth for projective curves in ℙⁿ over ℚ, specified by their Hilbert polynomial: there is a constant C > 0, depending only on n ≥ 1, such that every homogeneous prime ideal I of projective dimension 1 and degree d ≥ 5 has at most C * d ^ (3 * (n + 1) + 4) * B rational points of height at most B for all B ≥ 1.