5.2. The value at s = 1🔗

For a primitive odd character \chi modulo p, define the completed L-function by \Lambda(s,\chi) := \left(\frac{p}{\pi}\right)^{(s+1)/2} \Gamma\!\left(\frac{s+1}{2}\right)L(s,\chi). Its functional equation is \Lambda(1-s,\chi) = \frac{\tau(\chi)}{i\sqrt p}\,\Lambda(s,\chi^{-1}), where \tau(\chi)=\sum_{a\in \mathbb{Z}/p\mathbb{Z}}\chi(a)e^{2\pi i a/p} is the Gauss sum of \chi.

Proposition5.2.1

Statement uses 3

Statement dependency previews

Preview

Definition 2.3.1

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Let p be an odd prime and let \chi be a primitive odd Dirichlet character modulo p. If L(0,\chi^{-1}) = -B_{1,\chi^{-1}}, then L(1,\chi) = \frac{\pi i\,\tau(\chi)}{p}\,B_{1,\chi^{-1}}.

Definition 4.1.1 Definition 3.1.1 Definition 2.3.1

Lean code for Proposition5.2.1●1 theorem

theoremdefined in BernoulliRegular/LValueAtOne/Defs.lean

complete

theorem BernoulliRegular.odd_LFunction_one_eq_oddLValueRhs_of_LFunction_inv_zero
  (p : ℕ) [hp : Fact (Nat.Prime p)] {χ : DirichletCharacter ℂ p}
  (hχ_prim : χ.IsPrimitive) (hχ_odd : χ.Odd)
  (hχ0 :
    DirichletCharacter.LFunction χ⁻¹ 0 =
      -BernoulliRegular.BernoulliGen χ⁻¹ 1) :
  DirichletCharacter.LFunction χ 1 = BernoulliRegular.oddLValueRhs p χ

theorem BernoulliRegular.odd_LFunction_one_eq_oddLValueRhs_of_LFunction_inv_zero
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {χ : DirichletCharacter ℂ p}
  (hχ_prim : χ.IsPrimitive)
  (hχ_odd : χ.Odd)
  (hχ0 :
    DirichletCharacter.LFunction χ⁻¹ 0 =
      -BernoulliRegular.BernoulliGen χ⁻¹
          1) :
  DirichletCharacter.LFunction χ 1 =
    BernoulliRegular.oddLValueRhs p χ

Functional-equation reduction of the odd `L(1, χ)` formula to the special
value formula for `L(0, χ⁻¹)`.

Proof for Proposition 5.2.1

uses 0

Set s=0 in the functional equation. Since \Lambda(1,\chi)=\frac{p}{\pi}L(1,\chi) and \Lambda(0,\chi^{-1}) = \left(\frac{p}{\pi}\right)^{1/2}\Gamma\!\left(\frac12\right)L(0,\chi^{-1}) = \sqrt p\,L(0,\chi^{-1}), we get \frac{p}{\pi}L(1,\chi) = \frac{\tau(\chi)}{i\sqrt p}\cdot \sqrt p\,L(0,\chi^{-1}) = -i\,\tau(\chi)L(0,\chi^{-1}). Substituting the hypothesis L(0,\chi^{-1})=-B_{1,\chi^{-1}} gives the stated formula.

Corollary5.2.2

Statement uses 2

Statement dependency previews

Preview

Theorem 5.1.1

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Odd character formula at s=1. Let p be an odd prime and let \chi be a non-trivial odd Dirichlet character modulo p. Then L(1,\chi) = \frac{\pi i\,\tau(\chi)}{p}\,B_{1,\chi^{-1}}.

Theorem 5.1.1 Proposition 5.2.1

Lean code for Corollary5.2.2●1 theorem

theoremdefined in BernoulliRegular/LValueAtOne/Odd.lean

complete

theorem BernoulliRegular.odd_LFunction_one_eq_oddLValueRhs (p : ℕ)
  [hp : Fact (Nat.Prime p)] {χ : DirichletCharacter ℂ p}
  (hχ_prim : χ.IsPrimitive) (hχ_odd : χ.Odd) (hχ_ne_one : χ ≠ 1) :
  DirichletCharacter.LFunction χ 1 = BernoulliRegular.oddLValueRhs p χ

theorem BernoulliRegular.odd_LFunction_one_eq_oddLValueRhs
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {χ : DirichletCharacter ℂ p}
  (hχ_prim : χ.IsPrimitive)
  (hχ_odd : χ.Odd) (hχ_ne_one : χ ≠ 1) :
  DirichletCharacter.LFunction χ 1 =
    BernoulliRegular.oddLValueRhs p χ

**T021 / T021c / T021c1**: `L(1, χ)` for odd primitive characters
modulo `p`. Closes the full odd-side formula by applying the functional-equation
reduction `odd_LFunction_one_eq_oddLValueRhs_of_LFunction_inv_zero` to the
packaged odd special-value theorem at `χ⁻¹`.

Proof for Corollary 5.2.2

uses 0

Because p is prime, every non-trivial character modulo p is primitive. Applying Proposition 5.2.1 and then Theorem 5.1.1 to \chi^{-1} gives the result.

This is the form of the special-value formula needed in the proof of the analytic class number formula for \hminus.