The Dedekind zeta function of a number field

In this file, we define and prove results about the Dedekind zeta function of a number field.

Main definitions and results

• NumberField.dedekindZeta: the Dedekind zeta function.
• NumberField.dedekindZeta_residue: the value of the residue at s = 1 of the Dedekind zeta function.
• NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT: Dirichlet class number formula computation of the residue of the Dedekind zeta function at s = 1, see Chap. 7 of D. Marcus, Number Fields

TODO

Generalize the construction of the Dedekind zeta function.

def NumberField.dedekindZeta (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : ℂ

The Dedekind zeta function of a number field. It is defined as the L-series with coefficients the number of integral ideals of norm n.

Equations

• NumberField.dedekindZeta K s = LSeries (fun (n : ℕ) => ↑(Nat.card { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = n })) s

def NumberField.dedekindZeta_residue (K : Type u_1) [Field K] [NumberField K] : ℝ

The value of the residue at s = 1 of the Dedekind zeta function, see NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.dedekindZeta_residue_def (K : Type u_1) [Field K] [NumberField K] : dedekindZeta_residue K = 2 ^ InfinitePlace.nrRealPlaces K * (2 * Real.pi) ^ InfinitePlace.nrComplexPlaces K * Units.regulator K * ↑(classNumber K) / (↑(Units.torsionOrder K) * √|↑(discr K)|)

theorem NumberField.dedekindZeta_residue_pos (K : Type u_1) [Field K] [NumberField K] : 0 < dedekindZeta_residue K

theorem NumberField.dedekindZeta_residue_ne_zero (K : Type u_1) [Field K] [NumberField K] : dedekindZeta_residue K ≠ 0

theorem NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT (K : Type u_1) [Field K] [NumberField K] : Filter.Tendsto (fun (s : ℝ) => (↑s - 1) * dedekindZeta K ↑s) (nhdsWithin 1 (Set.Ioi 1)) (nhds ↑(dedekindZeta_residue K))

Dirichlet class number formula