Construction of L-functions

This file constructs L-functions as formal Dirichlet series.

Main definitions

• ArithmeticFunction.ofPowerSeries q f: L-function f(q⁻ˢ) obtained from a power series f(T).
• ArithmeticFunction.eulerProduct f: the Euler product of a family f i of Dirichlet series.

Implementation notes

We take the following route from polynomials to L-functions:

• Starting from a polynomial in T, PowerSeries.invOfUnit gives the reciporical power series.
• ofPowerSeries gives the local Euler factor as a formal Dirichlet series on powers of q.
• eulerProduct gives the L-function as the formal product of these local Euler factors.
• LSeries gives the L-function as an analytic function on the right half-plane of convergence.

For example, the Riemann zeta function ζ(s) corresponds to taking 1 - T at each prime p.

For context, here is a diagram of the possible routes from polynomials to L-functions:

               T=q⁻ˢ                     s ∈ ℂ

[polynomials in T] ----> [polynomials in q⁻ˢ] ----> [analytic function in s] | | | | (reciprocal) | (reciprocal) | (reciprocal) v T=q⁻ˢ V s ∈ ℂ V [power series in T] ----> [power series in q⁻ˢ] ----> [analytic function in s] (the Euler factor) | | | | (product) | (product) | (product) v T=q⁻ˢ V s ∈ ℂ V [multivariate power series] ----> [Dirichlet series] ----> [L-function in s] (the Euler product)

TODO

• If each q is a prime power, then ArithmeticFunction.ofPowerSeries q f is multiplicative.

noncomputable def ArithmeticFunction.ofPowerSeries {R : Type u_1} [CommSemiring R] (q : ℕ) : PowerSeries R →ₐ[R] ArithmeticFunction R

The arithmetic function corresponding to the Dirichlet series f(q⁻ˢ). For example, if f = 1 + X + X² + ... and q = p, then f(q⁻ˢ) = 1 + p⁻ˢ + p⁻²ˢ + ....

If q ≤ 1 then k ↦ q ^ k is not injective, so we use the junk value f.constantCoeff.

Equations

• One or more equations did not get rendered due to their size.

theorem ArithmeticFunction.ofPowerSeries_apply {R : Type u_1} [CommSemiring R] {q : ℕ} (hq : 1 < q) (f : PowerSeries R) (n : ℕ) : ((ofPowerSeries q) f) n = Function.extend (fun (x : ℕ) => q ^ x) (fun (x : ℕ) => (PowerSeries.coeff x) f) 0 n

theorem ArithmeticFunction.ofPowerSeries_apply_pow {R : Type u_1} [CommSemiring R] {q : ℕ} (hq : 1 < q) (f : PowerSeries R) (k : ℕ) : ((ofPowerSeries q) f) (q ^ k) = (PowerSeries.coeff k) f

theorem ArithmeticFunction.ofPowerSeries_apply_zero {R : Type u_1} [CommSemiring R] (q : ℕ) (f : PowerSeries R) : ((ofPowerSeries q) f) 0 = 0

@[simp]

theorem ArithmeticFunction.ofPowerSeries_apply_one {R : Type u_1} [CommSemiring R] (q : ℕ) (f : PowerSeries R) : ((ofPowerSeries q) f) 1 = PowerSeries.constantCoeff f

@[implicit_reducible]

def ArithmeticFunction.uniformSpace {R : Type u_2} [CommSemiring R] : UniformSpace (ArithmeticFunction R)

A private uniform space instance on ArithmeticFunction R in order to define eulerProduct as a tprod. If R is viewed as having the discrete topology, then the resulting topology on ArithmeticFunction R is the topology of pointwise convergence (see tendsto_iff).

See tendsTo_eulerProduct_of_tendsTo for the outward facing eulerProduct API.

Equations

• ArithmeticFunction.uniformSpace = UniformSpace.comap DFunLike.coe inferInstance

theorem ArithmeticFunction.instCompleteSpace {R : Type u_2} [CommSemiring R] : CompleteSpace (ArithmeticFunction R)

The uniform space structure on arithmetic functions is complete. See tendsTo_eulerProduct_of_tendsTo for the outward facing eulerProduct API.

noncomputable def ArithmeticFunction.eulerProduct {ι : Type u_1} {R : Type u_2} [CommSemiring R] (f : ι → ArithmeticFunction R) : ArithmeticFunction R

The Euler product of a family of arithmetic functions. Defined as a tprod, but see tendsTo_eulerProduct_of_tendsTo for the outward facing eulerProduct API.

Equations

• ArithmeticFunction.eulerProduct f = ∏' (i : ι), f i

theorem ArithmeticFunction.tendsTo_eulerProduct_of_tendsTo {ι : Type u_1} {R : Type u_2} [CommSemiring R] (f : ι → ArithmeticFunction R) (hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in Filter.cofinite, (f i) n = 1 n) (n : ℕ) : ∀ᶠ (s : Finset ι) in Filter.atTop, (∏ i ∈ s, f i) n = (eulerProduct f) n

If arithmetic functions f i converges to 1 pointwise, then the partial products ∏ i ∈ s, f i converge to eulerProduct f pointwise.

theorem ArithmeticFunction.isMultiplicative_eulerProduct {ι : Type u_1} {R : Type u_2} [CommSemiring R] (f : ι → ArithmeticFunction R) (hf : ∀ (i : ι), (f i).IsMultiplicative) : (eulerProduct f).IsMultiplicative