Formal logarithmic derivatives of zeta functions

Recover point-count coefficients from logarithmic derivatives of formal zeta series and their linear factors.

noncomputable def BGS.HasseWeil.negativeXLogDerivative (f : PowerSeries ℂ) : PowerSeries ℂ

The negative logarithmic derivative of a formal power series.

Equations

• BGS.HasseWeil.negativeXLogDerivative f = -PowerSeries.X * PowerSeries.derivative f * f⁻¹

noncomputable def BGS.HasseWeil.linearPowerSeriesFactor (a : ℂ) : PowerSeries ℂ

The linear formal power-series factor associated with a complex coefficient.

Equations

• BGS.HasseWeil.linearPowerSeriesFactor a = 1 - PowerSeries.C a * PowerSeries.X

@[simp]

theorem BGS.HasseWeil.constantCoeff_linearPowerSeriesFactor (a : ℂ) : PowerSeries.constantCoeff (linearPowerSeriesFactor a) = 1

theorem BGS.HasseWeil.linearPowerSeriesFactor_inv (a : ℂ) : (linearPowerSeriesFactor a)⁻¹ = (PowerSeries.rescale a) (PowerSeries.mk 1)

theorem BGS.HasseWeil.derivative_linearPowerSeriesFactor (a : ℂ) : PowerSeries.derivative (linearPowerSeriesFactor a) = -PowerSeries.C a

@[simp]

theorem BGS.HasseWeil.coeff_negativeXLogDerivative_linearPowerSeriesFactor (a : ℂ) (n : ℕ) : (PowerSeries.coeff (n + 1)) (negativeXLogDerivative (linearPowerSeriesFactor a)) = a ^ (n + 1)

theorem BGS.HasseWeil.inverse_mul_of_constantCoeff_ne_zero (f g : PowerSeries ℂ) (hf : PowerSeries.constantCoeff f ≠ 0) (hg : PowerSeries.constantCoeff g ≠ 0) : (f * g)⁻¹ = f⁻¹ * g⁻¹

theorem BGS.HasseWeil.negativeXLogDerivative_mul (f g : PowerSeries ℂ) (hf : PowerSeries.constantCoeff f ≠ 0) (hg : PowerSeries.constantCoeff g ≠ 0) : negativeXLogDerivative (f * g) = negativeXLogDerivative f + negativeXLogDerivative g

theorem BGS.HasseWeil.negativeXLogDerivative_prod_linearPowerSeriesFactor {I : Type u_1} [Fintype I] (a : I → ℂ) : negativeXLogDerivative (∏ i : I, linearPowerSeriesFactor (a i)) = ∑ i : I, negativeXLogDerivative (linearPowerSeriesFactor (a i))

theorem BGS.HasseWeil.coeff_negativeXLogDerivative_prod_linearPowerSeriesFactor {I : Type u_1} [Fintype I] (a : I → ℂ) (n : ℕ) : (PowerSeries.coeff (n + 1)) (negativeXLogDerivative (∏ i : I, linearPowerSeriesFactor (a i))) = ∑ i : I, a i ^ (n + 1)

def BGS.HasseWeil.pointCountDerivativeSeries (pointCount : ℕ → ℕ) : PowerSeries ℂ

The formal series whose coefficient at n is the point count over the extension of degree n + 1.

Equations

• BGS.HasseWeil.pointCountDerivativeSeries pointCount = PowerSeries.mk fun (n : ℕ) => ↑(pointCount (n + 1))

def BGS.HasseWeil.HasFormalZetaPointCountDerivative (Z : PowerSeries ℂ) (pointCount : ℕ → ℕ) : Prop

Euler's logarithmic-derivative identity for a point-count zeta series.

Equations

• BGS.HasseWeil.HasFormalZetaPointCountDerivative Z pointCount = (PowerSeries.derivative Z = Z * BGS.HasseWeil.pointCountDerivativeSeries pointCount)

noncomputable def BGS.HasseWeil.pointCountLogSeries (pointCount : ℕ → ℕ) : PowerSeries ℂ

The formal logarithm ∑ₙ Nₙ Tⁿ/n attached to extension point counts.

Equations

• BGS.HasseWeil.pointCountLogSeries pointCount = PowerSeries.mk fun (n : ℕ) => if n = 0 then 0 else ↑(pointCount n) / ↑n

@[simp]

theorem BGS.HasseWeil.constantCoeff_pointCountLogSeries (pointCount : ℕ → ℕ) : PowerSeries.constantCoeff (pointCountLogSeries pointCount) = 0

theorem BGS.HasseWeil.pointCountLogSeries_hasSubst (pointCount : ℕ → ℕ) : PowerSeries.HasSubst (pointCountLogSeries pointCount)

noncomputable def BGS.HasseWeil.formalPointCountZeta (pointCount : ℕ → ℕ) : PowerSeries ℂ

The formal exponential definition exp(∑ₙ Nₙ Tⁿ/n) of the point-count zeta series.

Equations

• BGS.HasseWeil.formalPointCountZeta pointCount = PowerSeries.subst (BGS.HasseWeil.pointCountLogSeries pointCount) (PowerSeries.exp ℂ)

theorem BGS.HasseWeil.derivative_pointCountLogSeries (pointCount : ℕ → ℕ) : PowerSeries.derivative (pointCountLogSeries pointCount) = pointCountDerivativeSeries pointCount

theorem BGS.HasseWeil.formalPointCountZeta_hasPointCountDerivative (pointCount : ℕ → ℕ) : HasFormalZetaPointCountDerivative (formalPointCountZeta pointCount) pointCount

noncomputable def BGS.HasseWeil.curveZetaDenominator (q : ℕ) : PowerSeries ℂ

The denominator (1 - T)(1 - qT) of the zeta function of a curve over the field with q elements.

Equations

• BGS.HasseWeil.curveZetaDenominator q = BGS.HasseWeil.linearPowerSeriesFactor 1 * BGS.HasseWeil.linearPowerSeriesFactor ↑q

@[simp]

theorem BGS.HasseWeil.constantCoeff_curveZetaDenominator (q : ℕ) : PowerSeries.constantCoeff (curveZetaDenominator q) = 1

def BGS.HasseWeil.HasCurveZetaRationalForm (Z : PowerSeries ℂ) (q : ℕ) (P : Polynomial ℂ) : Prop

Rationality in the normalized curve form.

Equations

• BGS.HasseWeil.HasCurveZetaRationalForm Z q P = (Z * BGS.HasseWeil.curveZetaDenominator q = ↑P)

theorem BGS.HasseWeil.coeff_negativeXLogDerivative_polynomial (P : Polynomial ℂ) (hP0 : P.coeff 0 = 1) (n : ℕ) : (PowerSeries.coeff (n + 1)) (negativeXLogDerivative ↑P) = ∑ i : Fin P.natDegree, reciprocalRootParameter P i ^ (n + 1)

theorem BGS.HasseWeil.coeff_negativeXLogDerivative_curveZetaDenominator (q n : ℕ) : (PowerSeries.coeff (n + 1)) (negativeXLogDerivative (curveZetaDenominator q)) = 1 + ↑q ^ (n + 1)

theorem BGS.HasseWeil.coeff_negativeXLogDerivative_of_pointCountDerivative (Z : PowerSeries ℂ) (pointCount : ℕ → ℕ) (hZ0 : PowerSeries.constantCoeff Z = 1) (htrace : HasFormalZetaPointCountDerivative Z pointCount) (n : ℕ) : (PowerSeries.coeff (n + 1)) (negativeXLogDerivative Z) = -↑(pointCount (n + 1))

theorem BGS.HasseWeil.hasZetaNumeratorPointCountFormula_of_formalZeta (q : ℕ) (pointCount : ℕ → ℕ) (Z : PowerSeries ℂ) (P : Polynomial ℂ) (hP0 : P.coeff 0 = 1) (htrace : HasFormalZetaPointCountDerivative Z pointCount) (hrational : HasCurveZetaRationalForm Z q P) : HasZetaNumeratorPointCountFormula q pointCount P

A normalized rational zeta series satisfying Euler's derivative identity produces the reciprocal-root extension point-count formula.

theorem BGS.HasseWeil.hasZetaNumeratorPointCountFormula_of_formalPointCountZeta_rational (q : ℕ) (pointCount : ℕ → ℕ) (P : Polynomial ℂ) (hP0 : P.coeff 0 = 1) (hrational : HasCurveZetaRationalForm (formalPointCountZeta pointCount) q P) : HasZetaNumeratorPointCountFormula q pointCount P

For the canonical exponential point-count zeta series, rationality in curve form is the only remaining premise needed for the numerator trace formula.