Twisted divisor sums

This file defines the twisted divisor sum

sigma e psi phi n = sum_{d | n} psi (n / d) * phi d * d ^ e

attached to two Dirichlet characters. These sums are the nonconstant Fourier coefficients of Eisenstein series with character: the weight-k coefficient uses exponent e = k - 1.

The definition is expressed as a Dirichlet convolution of multiplicative arithmetic functions. The resulting API includes its divisor-sum formula, multiplicativity, and its values at prime powers. For characters of level one it specializes to Mathlib's ordinary divisor sum ArithmeticFunction.sigma.

Main declarations

• DirichletCharacter.twistedDivisorSum: the arithmetic function of twisted divisor sums;
• DirichletCharacter.isMultiplicative_twistedDivisorSum: its multiplicativity;
• DirichletCharacter.twistedDivisorSum_apply_prime_pow: its prime-power formula;
• DirichletCharacter.twistedDivisorSum_apply_prime_pow_of_dvd_left_level: its bad-level specialization;
• DirichletCharacter.twistedDivisorSum_modOne_eq_sigma: its reduction to the ordinary divisor sum.

The convention follows Diamond--Shurman, A First Course in Modular Forms, Chapter 4 (especially Sections 4.5--4.8).

def DirichletCharacter.twistedDivisorSum {R : Type u_1} [CommSemiring R] {u v : ℕ} (e : ℕ) (psi : DirichletCharacter R u) (phi : DirichletCharacter R v) : ArithmeticFunction R

The twisted divisor sum attached to psi, phi, and the exponent e.

At a positive integer n its value is sum_{d | n} psi (n / d) * phi d * d ^ e. It is packaged as an arithmetic function so that Dirichlet convolution supplies its multiplicativity.

Equations

• DirichletCharacter.twistedDivisorSum e psi phi = (toArithmeticFunction fun (x : ℕ) => psi ↑x) * (toArithmeticFunction fun (x : ℕ) => phi ↑x).pmul ↑(ArithmeticFunction.pow e)

theorem DirichletCharacter.twistedDivisorSum_apply {R : Type u_1} [CommSemiring R] {u v : ℕ} (e : ℕ) (psi : DirichletCharacter R u) (phi : DirichletCharacter R v) (n : ℕ) : (twistedDivisorSum e psi phi) n = ∑ d ∈ n.divisors, psi ↑(n / d) * phi ↑d * ↑d ^ e

The defining divisor-sum formula for twistedDivisorSum.

theorem DirichletCharacter.isMultiplicative_twistedDivisorSum {R : Type u_1} [CommSemiring R] {u v : ℕ} (e : ℕ) (psi : DirichletCharacter R u) (phi : DirichletCharacter R v) : (twistedDivisorSum e psi phi).IsMultiplicative

Twisted divisor sums are multiplicative arithmetic functions.

@[simp]

theorem DirichletCharacter.twistedDivisorSum_one {R : Type u_1} [CommSemiring R] {u v : ℕ} (e : ℕ) (psi : DirichletCharacter R u) (phi : DirichletCharacter R v) : (twistedDivisorSum e psi phi) 1 = 1

The twisted divisor sum at 1 is 1.

theorem DirichletCharacter.twistedDivisorSum_apply_prime_pow {R : Type u_1} [CommSemiring R] {u v : ℕ} (e : ℕ) (psi : DirichletCharacter R u) (phi : DirichletCharacter R v) (r : ℕ) {p : ℕ} (hp : Nat.Prime p) : (twistedDivisorSum e psi phi) (p ^ r) = ∑ j ∈ Finset.range (r + 1), psi ↑p ^ (r - j) * phi ↑p ^ j * ↑p ^ (j * e)

The twisted divisor sum on a prime power is a finite geometric-type sum.

theorem DirichletCharacter.twistedDivisorSum_apply_prime {R : Type u_1} [CommSemiring R] {u v : ℕ} (e : ℕ) (psi : DirichletCharacter R u) (phi : DirichletCharacter R v) {p : ℕ} (hp : Nat.Prime p) : (twistedDivisorSum e psi phi) p = psi ↑p + phi ↑p * ↑p ^ e

At a prime, the twisted divisor sum has its two expected Euler-factor terms.

theorem DirichletCharacter.twistedDivisorSum_apply_prime_pow_of_dvd_left_level {R : Type u_1} [CommSemiring R] {u v : ℕ} (e : ℕ) (psi : DirichletCharacter R u) (phi : DirichletCharacter R v) (r : ℕ) {p : ℕ} (hp : Nat.Prime p) (hpu : p ∣ u) : (twistedDivisorSum e psi phi) (p ^ r) = phi ↑p ^ r * ↑p ^ (r * e)

If p divides the level of the left character, only the right-character term remains in the value at p ^ r.

theorem DirichletCharacter.twistedDivisorSum_apply_prime_of_dvd_left_level {R : Type u_1} [CommSemiring R] {u v : ℕ} (e : ℕ) (psi : DirichletCharacter R u) (phi : DirichletCharacter R v) {p : ℕ} (hp : Nat.Prime p) (hpu : p ∣ u) : (twistedDivisorSum e psi phi) p = phi ↑p * ↑p ^ e

If p divides the level of the left character, only the right-character term remains in the value at p.

theorem DirichletCharacter.twistedDivisorSum_apply_prime_pow_of_dvd_right_level {R : Type u_1} [CommSemiring R] {u v : ℕ} (e : ℕ) (psi : DirichletCharacter R u) (phi : DirichletCharacter R v) (r : ℕ) {p : ℕ} (hp : Nat.Prime p) (hpv : p ∣ v) : (twistedDivisorSum e psi phi) (p ^ r) = psi ↑p ^ r

If p divides the level of the right character, only the left-character term remains in the value at p ^ r.

theorem DirichletCharacter.twistedDivisorSum_apply_prime_of_dvd_right_level {R : Type u_1} [CommSemiring R] {u v : ℕ} (e : ℕ) (psi : DirichletCharacter R u) (phi : DirichletCharacter R v) {p : ℕ} (hp : Nat.Prime p) (hpv : p ∣ v) : (twistedDivisorSum e psi phi) p = psi ↑p

If p divides the level of the right character, only the left-character term remains in the value at p.

@[simp]

theorem DirichletCharacter.twistedDivisorSum_modOne_eq_sigma {R : Type u_1} [CommSemiring R] (e : ℕ) (psi phi : DirichletCharacter R 1) : twistedDivisorSum e psi phi = ↑(ArithmeticFunction.sigma e)

With both characters of level one, the twisted divisor sum is Mathlib's ordinary divisor sum ArithmeticFunction.sigma.