# Documentation

Mathlib.NumberTheory.EulerProduct.Basic

# Euler Products #

The main result in this file is EulerProduct.eulerProduct, which says that if f : ℕ → R is norm-summable, where R is a complete normed commutative ring and f is multiplicative on coprime arguments with f 0 = 0, then ∏ p in primesBelow N, ∑' e : ℕ, f (p^e) tends to ∑' n, f n as N tends to infinity. Nat.ArithmeticFunction.IsMultiplicative.eulerProduct is a version of EulerProduct.eulerProduct for multiplicative arithmetic functions in the sense of Nat.ArithmeticFunction.IsMultiplicative.

There is also a version EulerProduct.eulerProduct_completely_multiplicative, which states that ∏ p in primesBelow N, (1 - f p)⁻¹ tends to ∑' n, f n as N tends to infinity, when f is completely multiplicative with values in a complete normed field F (implemented as f : ℕ →*₀ F).

An intermediate step is EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum (and its variant EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum_geometric), which relates the finite product over primes to the sum of f n over N-smooth n.

## Tags #

Euler product

theorem Summable.norm_lt_one {F : Type u_1} [] [] {f : →* F} (hsum : Summable f) {p : } (hp : 1 < p) :
f p < 1

If f is multiplicative and summable, then its values at natural numbers > 1 have norm strictly less than 1.

### General Euler Products #

In this section we consider multiplicative (on coprime arguments) functions f : ℕ → R, where R is a complete normed commutative ring. The main result is EulerProduct.eulerProduct.

theorem EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum {R : Type u_1} [] [] {f : R} (hf₁ : f 1 = 1) (hmul : ∀ {m n : }, f (m * n) = f m * f n) (hsum : ∀ {p : }, Summable fun (n : ) => f (p ^ n)) (N : ) :
(Summable fun (m : ) => f m) HasSum (fun (m : ) => f m) (Finset.prod () fun (p : ) => ∑' (n : ), f (p ^ n))

We relate a finite product over primes to an infinite sum over smooth numbers.

theorem EulerProduct.prod_primesBelow_tsum_eq_tsum_smoothNumbers {R : Type u_1} [] [] {f : R} (hf₁ : f 1 = 1) (hmul : ∀ {m n : }, f (m * n) = f m * f n) (hsum : Summable fun (x : ) => f x) (N : ) :
(Finset.prod () fun (p : ) => ∑' (n : ), f (p ^ n)) = ∑' (m : ), f m

A version of EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum in terms of the value of the series.

theorem EulerProduct.norm_tsum_smoothNumbers_sub_tsum_lt {R : Type u_1} [] [] {f : R} (hsum : ) (hf₀ : f 0 = 0) {ε : } (εpos : 0 < ε) :
∃ (N₀ : ), NN₀, ∑' (m : ), f m - ∑' (m : ), f m < ε

The following statement says that summing over N-smooth numbers for large enough N gets us arbitrarily close to the sum over all natural numbers (assuming f is norm-summable and f 0 = 0; the latter since 0 is not smooth).

theorem EulerProduct.eulerProduct {R : Type u_1} [] [] {f : R} (hf₁ : f 1 = 1) (hmul : ∀ {m n : }, f (m * n) = f m * f n) (hsum : Summable fun (x : ) => f x) (hf₀ : f 0 = 0) :
Filter.Tendsto (fun (n : ) => Finset.prod () fun (p : ) => ∑' (e : ), f (p ^ e)) Filter.atTop (nhds (∑' (n : ), f n))

The Euler Product for multiplicative (on coprime arguments) functions. If f : ℕ → R, where R is a complete normed commutative ring, f 0 = 0, f 1 = 1, f is multiplicative on coprime arguments, and ‖f ·‖ is summable, then ∏' p : {p : ℕ | p.Prime}, ∑' e, f (p ^ e) = ∑' n, f n. Since there are no infinite products yet in Mathlib, we state it in the form of convergence of finite partial products.

theorem Nat.ArithmeticFunction.IsMultiplicative.eulerProduct {R : Type u_1} [] [] {f : } (hsum : Summable fun (x : ) => f x) :
Filter.Tendsto (fun (n : ) => Finset.prod () fun (p : ) => ∑' (e : ), f (p ^ e)) Filter.atTop (nhds (∑' (n : ), f n))

The Euler Product for a multiplicative arithmetic function f with values in a complete normed commutative ring R: if ‖f ·‖ is summable, then ∏' p : {p : ℕ | p.Prime}, ∑' e, f (p ^ e) = ∑' n, f n. Since there are no infinite products yet in Mathlib, we state it in the form of convergence of finite partial products.

### Euler Products for completely multiplicative functions #

We now assume that f is completely multiplicative and has values in a complete normed field F. Then we can use the formula for geometric series to simplify the statement. This leads to EulerProduct.eulerProduct_completely_multiplicative.

theorem EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric {F : Type u_1} [] [] {f : →* F} (h : ∀ {p : }, f p < 1) (N : ) :
(Summable fun (m : ) => f m) HasSum (fun (m : ) => f m) (Finset.prod () fun (p : ) => (1 - f p)⁻¹)

Given a (completely) multiplicative function f : ℕ → F, where F is a normed field, such that ‖f p‖ < 1 for all primes p, we can express the sum of f n over all N-smooth positive integers n as a product of (1 - f p)⁻¹ over the primes p < N. At the same time, we show that the sum involved converges absolutely.

theorem EulerProduct.prod_primesBelow_geometric_eq_tsum_smoothNumbers {F : Type u_1} [] [] {f : →* F} (hsum : Summable f) (N : ) :
(Finset.prod () fun (p : ) => (1 - f p)⁻¹) = ∑' (m : ), f m

A version of EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric in terms of the value of the series.

theorem EulerProduct.eulerProduct_completely_multiplicative {F : Type u_1} [] [] {f : →*₀ F} (hsum : Summable fun (x : ) => f x) :
Filter.Tendsto (fun (n : ) => Finset.prod () fun (p : ) => (1 - f p)⁻¹) Filter.atTop (nhds (∑' (n : ), f n))

The Euler Product for completely multiplicative functions. If f : ℕ →*₀ F, where F is a complete normed field and ‖f ·‖ is summable, then ∏' p : {p : ℕ | p.Prime}, (1 - f p)⁻¹ = ∑' n, f n. Since there are no infinite products yet in Mathlib, we state it in the form of convergence of finite partial products.