5.1. The value at s = 0🔗

For an odd Dirichlet character \chi modulo p one has the finite Hurwitz expansion L(s,\chi) = \sum_{a\in \mathbb{Z}/p\mathbb{Z}}\chi(a)\,\zeta_H^{-}\!\left(\frac{a}{p},s\right), where \zeta_H^{-}(x,s) denotes the odd Hurwitz zeta function. The functional equation for \zeta_H^{-}, evaluated at s=0, gives \zeta_H^{-}(x,0) = \frac12 - x \qquad (0<x<1). Substituting this identity immediately yields the desired special value.

Theorem5.1.1

Statement uses 2

Statement dependency previews

Preview

Proposition 3.2.1

Loading preview

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

used by 1✓L∃∀N

Special value at zero. Let p be an odd prime and let \chi be a non-trivial odd Dirichlet character modulo p. Then L(0,\chi) = -B_{1,\chi}.

Lemma 3.3.1 Proposition 3.2.1

Lean code for Theorem5.1.1●1 theorem

theoremdefined in BernoulliRegular/LValueAtOne/Odd.lean

complete

theorem BernoulliRegular.odd_LFunction_zero_eq_neg_BernoulliGen_one (p : ℕ)
  [hp : Fact (Nat.Prime p)] {χ : DirichletCharacter ℂ p}
  (hχ_odd : χ.Odd) (hχ_ne_one : χ ≠ 1) :
  DirichletCharacter.LFunction χ 0 = -BernoulliRegular.BernoulliGen χ 1

theorem BernoulliRegular.odd_LFunction_zero_eq_neg_BernoulliGen_one
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {χ : DirichletCharacter ℂ p}
  (hχ_odd : χ.Odd) (hχ_ne_one : χ ≠ 1) :
  DirichletCharacter.LFunction χ 0 =
    -BernoulliRegular.BernoulliGen χ 1

**T021b / T021b1**: Odd special value `L(0, χ) = -BernoulliGen χ 1` for
odd nontrivial Dirichlet characters modulo `p`, packaged independently of the
endpoint scaffolding by feeding the endpoint identity
`sinZeta_toAddCircle_one_eq_boundary` into the generic reduction lemma.

Proof for Theorem 5.1.1

uses 0

Using the Hurwitz expansion and the value of \zeta_H^{-}(x,0), we obtain L(0,\chi) = \sum_{a\in \mathbb{Z}/p\mathbb{Z}}\chi(a)\left(\frac12-\frac{a}{p}\right) = \frac12\sum_a \chi(a) - \sum_a \chi(a)\frac{a}{p}. The first sum vanishes because \chi is non-trivial. The second sum is the expression for B_{1,\chi} given by Lemma 3.3.1. Hence L(0,\chi) = -B_{1,\chi}.