Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.ZetaExtensionTrace

Extension point counts and the zeta spectral formula #

This file packages the elementary interface between rationality of a curve's zeta function and the even-extension estimate produced by the Bombieri--Stepanov/Galois-averaging argument. The geometric construction of the zeta function remains a separate preceding stage.

source
def BGS.HasseWeil.HasExtensionPointCountSpectralFormula (q g : ℕ) (pointCount : ℕ → ℕ) (alpha : Fin (2 * g) → ℂ) :
Prop

A compatible spectral formula for every positive extension degree.

Equations
Instances For
    source
    theorem BGS.HasseWeil.HasExtensionPointCountSpectralFormula.at_one {q g : ℕ} {pointCount : ℕ → ℕ} {alpha : Fin (2 * g) → ℂ} (h : HasExtensionPointCountSpectralFormula q g pointCount alpha) :
    HasPointCountSpectralFormula q g (pointCount 1) alpha

    The extension formula at degree one is the single spectral formula used in the final Hasse inequality.

    source
    theorem BGS.HasseWeil.evenPowerSum_isBigO_of_extensionPointCountError_isBigO {q g : ℕ} {pointCount : ℕ → ℕ} {alpha : Fin (2 * g) → ℂ} (hformula : HasExtensionPointCountSpectralFormula q g pointCount alpha) (herror : (fun (n : ℕ) => ↑(pointCount (2 * n)) - ↑q ^ (2 * n) - 1) =O[Filter.atTop] fun (n : ℕ) => ↑q ^ n) :
    (fun (n : ℕ) => ∑ i : Fin (2 * g), alpha i ^ (2 * n)) =O[Filter.atTop] fun (n : ℕ) => ↑q ^ n

    An even-extension point-count error of order q ^ n is exactly the power-sum estimate needed to bound the Frobenius parameters.

    source
    theorem BGS.HasseWeil.abs_pointCount_sub_card_sub_one_le_of_extensionFormula_and_evenError_isBigO (q g : ℕ) (pointCount : ℕ → ℕ) (alpha : Fin (2 * g) → ℂ) (hformula : HasExtensionPointCountSpectralFormula q g pointCount alpha) (herror : (fun (n : ℕ) => ↑(pointCount (2 * n)) - ↑q ^ (2 * n) - 1) =O[Filter.atTop] fun (n : ℕ) => ↑q ^ n) :
    |↑(pointCount 1) - ↑q - 1| ≤ 2 * ↑g * √↑q

    The complete analytic last step: a zeta spectral formula together with the two-sided even-extension asymptotic gives Hasse--Weil at the base field.