Documentation

LeanPool.CCDN.Surface.SmallDegreeSurfaceCurveCount

Nonlinear initial curves whose degrees are at most logarithmic in the box radius. The full affine curve theorem and the strict surface exponent gap give a linear bound in every surface degree at least five.

theorem CCDN.logarithmic_degree_curve_union_bound (k : ℕ) :
∃ (C : ℝ), 0 < C ∧ ∀ (S : Finset (Ideal (CoordinatePolynomial 3))) (δ : Ideal (CoordinatePolynomial 3) → ℕ) (d : ℕ), 5 ≤ d → ∀ (A D B : ℝ), 0 ≤ A → 0 ≤ D → 1 ≤ B → (∀ P ∈ S, P.IsPrime ∧ 2 ≤ δ P ∧ HasAffineCurveDegree P (δ P)) → (∀ P ∈ S, ↑(δ P) ≤ D * (Real.log B + 1)) → ∑ P ∈ S, ↑(δ P) ≤ A * B ^ (1 / √↑d) * (Real.log B + 1) ^ k → ↑(count (⋃ P ∈ S, idealZeroLocus P) B) ≤ C * A * D ^ 2 * (D + 1) * B

For each k, there is a constant C such that, for d ≥ 5 and a finite family of integral affine curves of degree at least two, each of degree at most D (log B + 1) and of total degree at most A B^(1/√d) (log B + 1)^k, the union of the curves has at most C A D² (D + 1) B integral points of height at most B.