Numerical parameters for the Bombieri--Stepanov argument

The sharp parameter choice in Tao's exposition uses a floor. The BGS application only needs a universal bidegree multiple of the square-root error, so it is cleaner to use

ell = s - 1, m = s + 2 * g

when the square-root field size s is at least (g + 1) * (g + 2). These parameters satisfy the three inequalities needed by the one-point Riemann-space argument, and give the same O(g * s) error term.

def BGS.HasseWeil.stepanovEll (s : ℕ) : ℕ

The slightly non-sharp parameters used in the formal Stepanov argument.

Equations

• BGS.HasseWeil.stepanovEll s = s - 1

def BGS.HasseWeil.stepanovM (g s : ℕ) : ℕ

The second tensor-factor parameter used in the formal Stepanov argument.

Equations

• BGS.HasseWeil.stepanovM g s = s + 2 * g

theorem BGS.HasseWeil.stepanovEll_lt {g s : ℕ} (hlarge : (g + 1) * (g + 2) ≤ s) : stepanovEll s < s

The first parameter is strictly smaller than the Frobenius scale.

theorem BGS.HasseWeil.stepanov_genus_le_parameters {g s : ℕ} (hlarge : (g + 1) * (g + 2) ≤ s) : g ≤ stepanovEll s + 1 ∧ g ≤ stepanovM g s + 1

Both tensor factors are large enough for Riemann's inequality.

theorem BGS.HasseWeil.stepanov_dimension_inequality {g s : ℕ} (hlarge : (g + 1) * (g + 2) ≤ s) : (stepanovEll s + 1 - g) * (stepanovM g s + 1 - g) > stepanovEll s * s + stepanovM g s + 1

The tensor-product dimension lower bound is strictly larger than the dimension upper bound for the second Frobenius restriction map.

theorem BGS.HasseWeil.stepanov_zero_bound {g s : ℕ} (hs : 0 < s) : stepanovEll s + stepanovM g s * s ≤ s ^ 2 + (2 * g + 1) * s

The resulting zero-count bound is at most s^2 + (2g+1)s; this is the weak Hasse--Weil upper bound needed later.