3.3. The first generalised Bernoulli number
The case n = 1 is the one that appears in the analytic formula for \hminus; we
record three forms used throughout.
Intermediate form for B_{1,\chi}. Let R be an integral domain and
\chi : (\mathbb{Z}/N\mathbb{Z}) \to R a non-trivial Dirichlet character. Then
B_{1,\chi} \;=\; \sum_{a \in \mathbb{Z}/N\mathbb{Z}} \chi(a)\,\frac{a}{N}.
Lean code for Lemma3.3.1●1 theorem
Associated Lean declarations
-
theoremdefined in BernoulliRegular/BernoulliGeneralized.leancomplete
theorem BernoulliRegular.BernoulliGen_one_of_ne_one.{u_1} {N : ℕ} {R : Type u_1} [CommRing R] [Algebra ℚ R] [IsDomain R] [NeZero N] {χ : DirichletCharacter R N} (hχ : χ ≠ 1) : BernoulliRegular.BernoulliGen χ 1 = ∑ a, χ a * (algebraMap ℚ R) (↑a.val / ↑N)
theorem BernoulliRegular.BernoulliGen_one_of_ne_one.{u_1} {N : ℕ} {R : Type u_1} [CommRing R] [Algebra ℚ R] [IsDomain R] [NeZero N] {χ : DirichletCharacter R N} (hχ : χ ≠ 1) : BernoulliRegular.BernoulliGen χ 1 = ∑ a, χ a * (algebraMap ℚ R) (↑a.val / ↑N)
Intermediate form (T006): for a non-trivial Dirichlet character `χ`, the `1/2` constant term in `B_1(a/N) = a/N - 1/2` does not contribute after summing, because `∑ χ(a) = 0`.
Since B_1(X) = X - \tfrac12 and the exponent 1 - 1 = 0 in the definition makes
the leading N^{n-1} factor equal to 1,
B_{1,\chi} = \sum_a \chi(a) \cdot \frac{a}{N} - \sum_a \chi(a) \cdot \frac{1}{2}.
The second sum equals \tfrac12 \cdot \sum_a \chi(a), which is zero for non-trivial
\chi by the character-sum identity used in Proposition 3.2.1.
Cleared form of B_{1,\chi}. For \chi as in the previous lemma,
N \cdot B_{1,\chi} \;=\; \sum_{a \in \mathbb{Z}/N\mathbb{Z}} \chi(a)\,a,
an identity valid in any commutative \mathbb{Q}-algebra (denominators have been
cleared).
Lean code for Lemma3.3.2●1 theorem
Associated Lean declarations
-
theoremdefined in BernoulliRegular/BernoulliGeneralized.leancomplete
theorem BernoulliRegular.natCast_mul_BernoulliGen_one_of_ne_one.{u_1} {N : ℕ} {R : Type u_1} [CommRing R] [Algebra ℚ R] [IsDomain R] [NeZero N] {χ : DirichletCharacter R N} (hχ : χ ≠ 1) : ↑N * BernoulliRegular.BernoulliGen χ 1 = ∑ a, χ a * ↑a.val
theorem BernoulliRegular.natCast_mul_BernoulliGen_one_of_ne_one.{u_1} {N : ℕ} {R : Type u_1} [CommRing R] [Algebra ℚ R] [IsDomain R] [NeZero N] {χ : DirichletCharacter R N} (hχ : χ ≠ 1) : ↑N * BernoulliRegular.BernoulliGen χ 1 = ∑ a, χ a * ↑a.val
**Diekmann eq. 24/27** (T006), cleared form: `N · B_{1, χ} = ∑_a χ(a) · a` for non-trivial `χ`. Cleared of denominators so it holds in any commutative `ℚ`-algebra.
Multiply the previous identity through by N and use that the algebra map
\mathbb{Q} \to R commutes with multiplication by N \in \mathbb{N}.
Parity vanishing at n = 1. Let R be an integral domain in which
2 \ne 0 and let \chi be a non-trivial even Dirichlet character modulo
N > 1 valued in R, with N invertible in R. Then B_{1,\chi} = 0.
Lean code for Proposition3.3.3●1 theorem
Associated Lean declarations
-
theoremdefined in BernoulliRegular/BernoulliGeneralized.leancomplete
theorem BernoulliRegular.BernoulliGen_one_eq_zero_of_even_ne_one.{u_1} {N : ℕ} {R : Type u_1} [CommRing R] [Algebra ℚ R] [IsDomain R] [NeZero 2] [NeZero N] [Fact (1 < N)] (hN : ↑N ≠ 0) {χ : DirichletCharacter R N} (hχ_ne_one : χ ≠ 1) (hχ_even : χ.Even) : BernoulliRegular.BernoulliGen χ 1 = 0
theorem BernoulliRegular.BernoulliGen_one_eq_zero_of_even_ne_one.{u_1} {N : ℕ} {R : Type u_1} [CommRing R] [Algebra ℚ R] [IsDomain R] [NeZero 2] [NeZero N] [Fact (1 < N)] (hN : ↑N ≠ 0) {χ : DirichletCharacter R N} (hχ_ne_one : χ ≠ 1) (hχ_even : χ.Even) : BernoulliRegular.BernoulliGen χ 1 = 0
**Diekmann Lemma 29** (T009): for a non-trivial even Dirichlet character `χ` of level `N > 1` over a `ℚ`-algebra domain `R` where `(2 : R) ≠ 0` and `(N : R) ≠ 0`, `B_{1, χ} = 0`.
Reindexing the sum in Lemma 3.3.2 by a \mapsto -a
and using \chi(-a) = \chi(-1) \chi(a) = \chi(a) (because \chi is even),
\sum_a \chi(a)\,a \;=\; \sum_a \chi(a)\,(-a).\mathrm{val},
where (-a).\mathrm{val} denotes the canonical representative in \{0,\dots,N-1\}.
Adding the two expressions,
2 \sum_a \chi(a)\,a \;=\; \sum_a \chi(a)\,\bigl(a + (-a).\mathrm{val}\bigr).
The pairing identity in \mathbb{Z}/N\mathbb{Z} states that
a.\mathrm{val} + (-a).\mathrm{val} equals 0 when a = 0 and N otherwise.
Substituting,
2 \sum_a \chi(a)\,a \;=\; N \cdot \sum_{a \ne 0} \chi(a) \;=\; N \cdot \Bigl(\sum_a \chi(a) - \chi(0)\Bigr) \;=\; 0,
because \chi(0) = 0 and \sum_a \chi(a) = 0 for non-trivial \chi. Since
2 \ne 0 in R, the sum vanishes, and then N \ne 0 forces B_{1,\chi} = 0
via Lemma 3.3.2.
This is the special case at n = 1 of the general parity phenomenon. For a
non-trivial Dirichlet character \chi and n \ge 1 one has B_{n,\chi} = 0
unless \chi(-1) = (-1)^n. Indeed, using the defining sum and reindexing by
a\mapsto -a, the Bernoulli polynomials satisfy B_n(1-X)=(-1)^n B_n(X), and the
character contributes the scalar \chi(-1); hence
B_{n,\chi}=\chi(-1)(-1)^n B_{n,\chi}. If \chi(-1)\ne (-1)^n, the scalar
multiplying B_{n,\chi} is not 1, so B_{n,\chi}=0.
In particular: if \chi is odd, B_{n,\chi} can be non-zero only for odd n; if
\chi is even, only for even n. Downstream this is used in two places: (i) the
cleared form of the analytic formula for \hminus runs only over odd characters,
because their B_{1,\chi} are the only non-vanishing terms; and (ii) the odd
special-value formula depends on the same parity constraint.