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. ArithmeticFunction.IsMultiplicative.eulerProduct is a version of EulerProduct.eulerProduct for multiplicative arithmetic functions in the sense of 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} [NormedField F] [CompleteSpace F] {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} [NormedCommRing R] [CompleteSpace R] {f : ℕ → R} (hf₁ : f 1 = 1) (hmul : ∀ {m n : ℕ}, Nat.Coprime m n → f (m * n) = f m * f n) (hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun (n : ℕ) => ‖f (p ^ n)‖) (N : ℕ) : (Summable fun (m : ↑(Nat.smoothNumbers N)) => ‖f ↑m‖) ∧ HasSum (fun (m : ↑(Nat.smoothNumbers N)) => f ↑m) (Finset.prod (Nat.primesBelow N) 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} [NormedCommRing R] [CompleteSpace R] {f : ℕ → R} (hf₁ : f 1 = 1) (hmul : ∀ {m n : ℕ}, Nat.Coprime m n → f (m * n) = f m * f n) (hsum : Summable fun (x : ℕ) => ‖f x‖) (N : ℕ) : (Finset.prod (Nat.primesBelow N) fun (p : ℕ) => ∑' (n : ℕ), f (p ^ n)) = ∑' (m : ↑(Nat.smoothNumbers N)), 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} [NormedCommRing R] [CompleteSpace R] {f : ℕ → R} (hsum : Summable f) (hf₀ : f 0 = 0) {ε : ℝ} (εpos : 0 < ε) : ∃ (N₀ : ℕ), ∀ N ≥ N₀, ‖∑' (m : ℕ), f m - ∑' (m : ↑(Nat.smoothNumbers N)), 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} [NormedCommRing R] [CompleteSpace R] {f : ℕ → R} (hf₁ : f 1 = 1) (hmul : ∀ {m n : ℕ}, Nat.Coprime 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 (Nat.primesBelow n) 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 ArithmeticFunction.IsMultiplicative.eulerProduct {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {f : ArithmeticFunction R} (hf : ArithmeticFunction.IsMultiplicative f) (hsum : Summable fun (x : ℕ) => ‖f x‖) : Filter.Tendsto (fun (n : ℕ) => Finset.prod (Nat.primesBelow n) 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} [NormedField F] [CompleteSpace F] {f : ℕ →* F} (h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1) (N : ℕ) : (Summable fun (m : ↑(Nat.smoothNumbers N)) => ‖f ↑m‖) ∧ HasSum (fun (m : ↑(Nat.smoothNumbers N)) => f ↑m) (Finset.prod (Nat.primesBelow N) 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} [NormedField F] [CompleteSpace F] {f : ℕ →* F} (hsum : Summable ⇑f) (N : ℕ) : (Finset.prod (Nat.primesBelow N) fun (p : ℕ) => (1 - f p)⁻¹) = ∑' (m : ↑(Nat.smoothNumbers N)), 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} [NormedField F] [CompleteSpace F] {f : ℕ →*₀ F} (hsum : Summable fun (x : ℕ) => ‖f x‖) : Filter.Tendsto (fun (n : ℕ) => Finset.prod (Nat.primesBelow n) 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.