Spectral bounds from even power-sum asymptotics

This file formalizes the elementary Corvaja--Zannier/Tao step that turns an even-extension point-count asymptotic into the Riemann-hypothesis bound for each Frobenius parameter.

Repeated squared parameters must first be grouped. Their coefficients are the positive cardinalities of their fibers, so the weighted power-sum lemma from BGS.HasseWeil.PowerSum applies without an injectivity assumption on the original family of parameters.

noncomputable def BGS.HasseWeil.squaredBaseSet {N : ℕ} (alpha : Fin N → ℂ) : Finset ℂ

The finite set of distinct squared values occurring in alpha.

Equations

• BGS.HasseWeil.squaredBaseSet alpha = Finset.image (fun (i : Fin N) => alpha i ^ 2) Finset.univ

noncomputable def BGS.HasseWeil.squaredBaseMultiplicity {N : ℕ} (alpha : Fin N → ℂ) (z : ℂ) : ℂ

The complex-valued multiplicity of a squared value occurring in alpha.

Equations

• BGS.HasseWeil.squaredBaseMultiplicity alpha z = ↑{i : Fin N | alpha i ^ 2 = z}.card

theorem BGS.HasseWeil.squaredBaseMultiplicity_ne_zero_of_mem {N : ℕ} {alpha : Fin N → ℂ} {z : ℂ} (hz : z ∈ squaredBaseSet alpha) : squaredBaseMultiplicity alpha z ≠ 0

Every squared value in squaredBaseSet alpha has positive, hence nonzero, multiplicity.

theorem BGS.HasseWeil.weightedPowerSum_squaredBaseMultiplicity {N : ℕ} (alpha : Fin N → ℂ) (n : ℕ) : weightedPowerSum (squaredBaseSet alpha) (squaredBaseMultiplicity alpha) n = ∑ i : Fin N, alpha i ^ (2 * n)

Grouping repeated squared values with their multiplicities recovers the original even power sum.

theorem BGS.HasseWeil.spectral_norm_le_sqrt_of_evenPowerSum_isBigO {N : ℕ} {q : ℝ} (alpha : Fin N → ℂ) (hq : 0 ≤ q) (hO : (fun (n : ℕ) => ∑ i : Fin N, alpha i ^ (2 * n)) =O[Filter.atTop] fun (n : ℕ) => q ^ n) (i : Fin N) : ‖alpha i‖ ≤ √q

An O(q ^ n) bound for all even power sums forces every spectral parameter to have norm at most sqrt q.

The IsBigO hypothesis already allows an arbitrary fixed multiplicative constant.

theorem BGS.HasseWeil.spectral_norm_le_sqrt_of_divisibleEvenPowerSum_isBigO {N δ : ℕ} {q : ℝ} (alpha : Fin N → ℂ) (hq : 0 < q) (hδ : 0 < δ) (hO : (fun (n : ℕ) => ∑ i : Fin N, alpha i ^ (2 * δ * n)) =O[Filter.atTop] fun (n : ℕ) => (q ^ δ) ^ n) (i : Fin N) : ‖alpha i‖ ≤ √q

It is enough to control the even power sums along any fixed positive divisible subsequence.

theorem BGS.HasseWeil.abs_pointCount_sub_card_sub_one_le_of_evenPowerSum_isBigO (q g pointCount : ℕ) (alpha : Fin (2 * g) → ℂ) (hformula : HasPointCountSpectralFormula q g pointCount alpha) (hO : (fun (n : ℕ) => ∑ i : Fin (2 * g), alpha i ^ (2 * n)) =O[Filter.atTop] fun (n : ℕ) => ↑q ^ n) : |↑pointCount - ↑q - 1| ≤ 2 * ↑g * √↑q

The Hasse point-count inequality obtained from a spectral point-count formula and the even-power-sum asymptotic.

theorem BGS.HasseWeil.abs_pointCount_sub_card_sub_one_le_of_divisibleEvenPowerSum_isBigO (q g pointCount δ : ℕ) (alpha : Fin (2 * g) → ℂ) (hq : 0 < q) (hδ : 0 < δ) (hformula : HasPointCountSpectralFormula q g pointCount alpha) (hO : (fun (n : ℕ) => ∑ i : Fin (2 * g), alpha i ^ (2 * δ * n)) =O[Filter.atTop] fun (n : ℕ) => (↑q ^ δ) ^ n) : |↑pointCount - ↑q - 1| ≤ 2 * ↑g * √↑q

The degree-one Hasse bound follows from a power-sum estimate on any fixed positive divisible-even subsequence.