Non-vanishing of L(χ, 1) for nontrivial quadratic characters χ

structure BadChar (N : ℕ) [NeZero N] : Type

The object we're trying to show doesn't exist.

• χ : DirichletCharacter ℂ N
• χ_ne : self.χ ≠ 1
• χ_sq : self.χ ^ 2 = 1
• hχ : self.χ.LFunction 1 = 0

theorem BadChar.χ_ne {N : ℕ} [NeZero N] (self : BadChar N) : self.χ ≠ 1

theorem BadChar.χ_sq {N : ℕ} [NeZero N] (self : BadChar N) : self.χ ^ 2 = 1

theorem BadChar.hχ {N : ℕ} [NeZero N] (self : BadChar N) : self.χ.LFunction 1 = 0

theorem BadChar.χ_apply_eq {N : ℕ} [NeZero N] (B : BadChar N) (x : ZMod N) : B.χ x = 0 ∨ B.χ x = 1 ∨ B.χ x = -1

The associated character is quadratic.

def BadChar.F {N : ℕ} [NeZero N] (B : BadChar N) : ℂ → ℂ

The auxiliary function F: s ↦ ζ s * L B.χ s.

Equations

• B.F = Function.update (fun (s : ℂ) => riemannZeta s * B.χ.LFunction s) 1 (deriv B.χ.LFunction 1)

theorem BadChar.F_differentiableAt_of_ne {N : ℕ} [NeZero N] (B : BadChar N) {s : ℂ} (hs : s ≠ 1) : DifferentiableAt ℂ B.F s

theorem BadChar.F_differentiable {N : ℕ} [NeZero N] (B : BadChar N) : Differentiable ℂ B.F

theorem BadChar.F_neg_two {N : ℕ} [NeZero N] (B : BadChar N) : B.F (-2) = 0

The trivial zero at s = -2 of the zeta function gives that F (-2) = 0. This is used later to obtain a contradction.

def BadChar.e {N : ℕ} [NeZero N] (B : BadChar N) : ArithmeticFunction ℂ

The complex-valued arithmetic function whose L-series is B.F.

Equations

• B.e = ↑ArithmeticFunction.zeta * toArithmeticFunction fun (x : ℕ) => B.χ ↑x

theorem BadChar.e_summable {N : ℕ} [NeZero N] (B : BadChar N) {s : ℂ} (hs : 1 < s.re) : LSeriesSummable (fun (x : ℕ) => B.e x) s

theorem BadChar.abscissa {N : ℕ} [NeZero N] (B : BadChar N) : LSeries.abscissaOfAbsConv ⇑B.e < ↑2

theorem BadChar.F_eq_LSeries {N : ℕ} [NeZero N] (B : BadChar N) {s : ℂ} (hs : 1 < s.re) : B.F s = LSeries (⇑B.e) s

B.F agrees with the L-series of B.e on 1 < s.re.

theorem BadChar.mult_e {N : ℕ} [NeZero N] (B : BadChar N) : B.e.IsMultiplicative

theorem BadChar.e_prime_pow {N : ℕ} [NeZero N] (B : BadChar N) {p : ℕ} (hp : Nat.Prime p) (k : ℕ) : 0 ≤ B.e (p ^ k)

theorem BadChar.e_nonneg {N : ℕ} [NeZero N] (B : BadChar N) (n : ℕ) : 0 ≤ B.e n

B.e takes nonnegative real values.

theorem BadChar.e_one_eq_one {N : ℕ} [NeZero N] (B : BadChar N) : B.e 1 = 1

theorem BadChar.F_two_pos {N : ℕ} [NeZero N] (B : BadChar N) : 0 < B.F 2

theorem BadChar.elim {N : ℕ} [NeZero N] (B : BadChar N) : False

The goal: bad characters do not exist.