Construction of L-functions

This file constructs L-functions as formal Dirichlet series.

Main definitions

• ArithmeticFunction.eulerProduct f: the Euler product of a family f i of Dirichlet series.

TODO

• If each f i is multiplicative, then ArithmeticFunction.eulerProduct f is multiplicative.

@[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.