The weighted half sum of an odd Dirichlet character

For f odd and χ an odd Dirichlet character modulo f with values in a field of characteristic 0, the weighted half sum ∑_{c=1}^{(f-1)/2} c χ(c) is (f/2) B_{1,χ} (χ(2)⁻¹ − 1) (a classical identity, found in Kanemitsu–Kuzumaki and in Kučera). The proof reduces to the ring identities DigitosII.diag.

Main results

• DiagKK.thm_diag: ∑_{c=1}^{(f-1)/2} c χ(c) = (f/2) B_{1,χ} (χ(2)⁻¹ − 1), with B_{1,χ} = f⁻¹ ∑_{a ∈ ZMod f} χ(a) a.val (ConjeturaC.B1).
• DiagKK.thm_diag_half: the unweighted sum, ∑_{c ≤ (f-1)/2} χ(c) = (χ(2)⁻¹ − 2) B_{1,χ}.
• DiagKK.thm_diag_iff: if B_{1,χ} ≠ 0, the weighted half sum vanishes iff χ(2) = 1.

B_{1,χ} ≠ 0 for primitive χ (it is −L(0, χ)) is a hypothesis here: at the pinned commit Mathlib has no value of a Dirichlet L-function at s = 0 for odd χ (hurwitzZeta_neg_nat excludes k = 0).

References

• C. Marín, Zeros of weighted partial sums of completely multiplicative functions: Dirichlet characters, the Euler factor at 2 and Conrey's sine series, Zenodo (2026), doi:10.5281/zenodo.22847374.

The sums C, T, Tq and the ring identities DigitosII.diag are those of Formalizations.NumberTheory.WeightedCharacterSums.DigitCorollaries.

The Dirichlet-character statement

theorem DiagKK.bridge {K : Type u_1} [Field K] (c : ℕ) (χ : DirichletCharacter K (2 * c + 1)) (hodd : χ.Odd) : have χn := fun (n : ℕ) => χ ↑n; (∀ (a b : ℕ), χn (a * b) = χn a * χn b) ∧ (∀ (j r : ℕ), 1 ≤ r → r < 2 * c + 1 → χn (j * (2 * c + 1) + r) = χn r) ∧ χn (2 * c) = -1 ∧ DigitosII.Tq χn (2 * c + 1) = ∑ a : ZMod (2 * c + 1), χ a * ↑a.val

The bridge: the hypotheses of diag for n ↦ χ(n mod f), and T_f = f B_{1,χ}.

theorem DiagKK.chi_two_ne_zero {K : Type u_1} [Field K] (c : ℕ) (χ : DirichletCharacter K (2 * c + 1)) : χ 2 ≠ 0

χ(2) ≠ 0 for f odd.

theorem DiagKK.diag_char {K : Type u_1} [Field K] [CharZero K] (c : ℕ) (χ : DirichletCharacter K (2 * c + 1)) (hχ : χ.Odd) : ∑ n ∈ Finset.Icc 1 c, ↑n * χ ↑n = ↑(2 * c + 1) / 2 * ConjeturaC.B1 χ * ((χ 2)⁻¹ - 1) ∧ ∑ n ∈ Finset.Icc 1 c, χ ↑n = ((χ 2)⁻¹ - 2) * ConjeturaC.B1 χ

The three identities of the proof, for an odd Dirichlet character modulo f = 2c+1.

theorem DiagKK.thm_diag {K : Type u_1} [Field K] [CharZero K] {f : ℕ} [NeZero f] (hf : Odd f) (χ : DirichletCharacter K f) (hχ : χ.Odd) : ∑ n ∈ Finset.Icc 1 ((f - 1) / 2), ↑n * χ ↑n = ↑f / 2 * ConjeturaC.B1 χ * ((χ 2)⁻¹ - 1)

thm:diag (4.2), the displayed formula. f odd, χ an odd Dirichlet character modulo f with values in a field of characteristic 0: ∑_{c=1}^{(f-1)/2} c χ(c) = (f/2) B_{1,χ} (χ(2)⁻¹ - 1).

theorem DiagKK.thm_diag_half {K : Type u_1} [Field K] [CharZero K] {f : ℕ} [NeZero f] (hf : Odd f) (χ : DirichletCharacter K f) (hχ : χ.Odd) : ∑ n ∈ Finset.Icc 1 ((f - 1) / 2), χ ↑n = ((χ 2)⁻¹ - 2) * ConjeturaC.B1 χ

The unweighted twin from the proof of thm:diag: ∑_{c=1}^{(f-1)/2} χ(c) = (χ(2)⁻¹ - 2) B_{1,χ}.

theorem DiagKK.thm_diag_iff {K : Type u_1} [Field K] [CharZero K] {f : ℕ} [NeZero f] (hf : Odd f) (χ : DirichletCharacter K f) (hχ : χ.Odd) (hB : ConjeturaC.B1 χ ≠ 0) : ∑ n ∈ Finset.Icc 1 ((f - 1) / 2), ↑n * χ ↑n = 0 ↔ χ 2 = 1

thm:diag (4.2), second sentence, with B_{1,χ} ≠ 0 as hypothesis (the paper obtains it from primitivity, B_{1,χ} = -L(0,χ) ≠ 0; not formalized): the weighted half sum vanishes iff χ(2) = 1.