3.1. Definition
We follow Washington's explicit formula (Washington (4.1), Diekmann Prop. 45) rather
than the generating-function description: the explicit form is what is used
throughout, and it makes the dependence on the polynomial B_n(X) manifest. Recall
that B_n(X) \in \mathbb{Q}[X] denotes the n-th Bernoulli polynomial.
Generalised Bernoulli number. Let N \ge 1, let R be a commutative
\mathbb{Q}-algebra and let \chi : (\mathbb{Z}/N\mathbb{Z}) \to R be a Dirichlet
character (with \chi(0) = 0). The generalised Bernoulli number attached to
\chi in degree n \in \mathbb{N} is
B_{n,\chi} \;:=\; N^{\,n-1}\,\sum_{a \in \mathbb{Z}/N\mathbb{Z}} \chi(a)\,B_n\!\left(\frac{a}{N}\right) \;\in\; R,
where a is identified with its representative in \{0,1,\dots,N-1\}, and
B_n(a/N) \in \mathbb{Q} is sent to R along \mathbb{Q} \to R. For the trivial
character one recovers the classical Bernoulli number: B_{n,\mathbf{1}} = B_n.
Lean code for Definition3.1.1●1 definition
Associated Lean declarations
-
BernoulliRegular.BernoulliGen[complete]
-
BernoulliRegular.BernoulliGen[complete]
-
defdefined in BernoulliRegular/BernoulliGeneralized.leancomplete
def BernoulliRegular.BernoulliGen.{u_1} {N : ℕ} {R : Type u_1} [CommRing R] [Algebra ℚ R] [NeZero N] (χ : DirichletCharacter R N) (n : ℕ) : R
def BernoulliRegular.BernoulliGen.{u_1} {N : ℕ} {R : Type u_1} [CommRing R] [Algebra ℚ R] [NeZero N] (χ : DirichletCharacter R N) (n : ℕ) : R
The generalized Bernoulli number `B_{n, χ}`, defined by the explicit formula `B_{n, χ} = N^{n-1} · ∑_{a : ZMod N} χ(a) · B_n(a/N)`, where `B_n` is the `n`-th Bernoulli polynomial over `ℚ`, base-changed to `R` via `algebraMap ℚ R`, and `a/N` is evaluated in `ℚ` using `ZMod.val a : ℕ`. For non-trivial `χ` the `a = 0` summand vanishes because `χ(0) = 0`, and `BernoulliGen_zero_of_ne_one` shows the whole sum vanishes when `n = 0`.