Euler Products

The main result in this file is EulerProduct.eulerProduct_hasProd, 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 : Primes, ∑' e : ℕ, f (p^e) converges to ∑' n, f n.

ArithmeticFunction.IsMultiplicative.eulerProduct_hasProd is a version for multiplicative arithmetic functions in the sense of ArithmeticFunction.IsMultiplicative.

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

There are variants stating the equality of the infinite product and the infinite sum (EulerProduct.eulerProduct_tprod, ArithmeticFunction.IsMultiplicative.eulerProduct_tprod, EulerProduct.eulerProduct_completely_multiplicative_tprod) and also variants stating the convergence of the sequence of partial products over primes < n (EulerProduct.eulerProduct, ArithmeticFunction.IsMultiplicative.eulerProduct, EulerProduct.eulerProduct_completely_multiplicative.)

An intermediate step is EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum (and its variant EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric), which relates the finite product over primes p ∈ s to the sum of f n over s-factored n, for s : Finset ℕ.

Tags

Euler product, multiplicative function

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_factoredNumbers_prod_filter_prime_tsum {R : Type u_1} [NormedCommRing R] {f : ℕ → R} [CompleteSpace R] (hf₁ : f 1 = 1) (hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) (hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun (n : ℕ) => ‖f (p ^ n)‖) (s : Finset ℕ) : (Summable fun (m : ↑(Nat.factoredNumbers s)) => ‖f ↑m‖) ∧ HasSum (fun (m : ↑(Nat.factoredNumbers s)) => f ↑m) (∏ p ∈ Finset.filter (fun (p : ℕ) => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))

We relate a finite product over primes in s to an infinite sum over s-factored numbers.

theorem EulerProduct.prod_filter_prime_tsum_eq_tsum_factoredNumbers {R : Type u_1} [NormedCommRing R] {f : ℕ → R} [CompleteSpace R] (hf₁ : f 1 = 1) (hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) (hsum : Summable fun (x : ℕ) => ‖f x‖) (s : Finset ℕ) : ∏ p ∈ Finset.filter (fun (p : ℕ) => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n) = ∑' (m : ↑(Nat.factoredNumbers s)), f ↑m

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

theorem EulerProduct.norm_tsum_factoredNumbers_sub_tsum_lt {R : Type u_1} [NormedCommRing R] {f : ℕ → R} [CompleteSpace R] (hsum : Summable f) (hf₀ : f 0 = 0) {ε : ℝ} (εpos : 0 < ε) : ∃ (N : ℕ), ∀ (s : Finset ℕ), N.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(Nat.factoredNumbers s)), f ↑m‖ < ε

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

theorem EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum {R : Type u_1} [NormedCommRing R] {f : ℕ → R} [CompleteSpace R] (hf₁ : f 1 = 1) (hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) (hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun (n : ℕ) => ‖f (p ^ n)‖) (N : ℕ) : (Summable fun (m : ↑N.smoothNumbers) => ‖f ↑m‖) ∧ HasSum (fun (m : ↑N.smoothNumbers) => f ↑m) (∏ p ∈ N.primesBelow, ∑' (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] {f : ℕ → R} [CompleteSpace R] (hf₁ : f 1 = 1) (hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) (hsum : Summable fun (x : ℕ) => ‖f x‖) (N : ℕ) : ∏ p ∈ N.primesBelow, ∑' (n : ℕ), f (p ^ n) = ∑' (m : ↑N.smoothNumbers), 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] {f : ℕ → R} [CompleteSpace R] (hsum : Summable f) (hf₀ : f 0 = 0) {ε : ℝ} (εpos : 0 < ε) : ∃ (N₀ : ℕ), ∀ N ≥ N₀, ‖∑' (m : ℕ), f m - ∑' (m : ↑N.smoothNumbers), 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_hasProd {R : Type u_1} [NormedCommRing R] {f : ℕ → R} [CompleteSpace R] (hf₁ : f 1 = 1) (hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) (hsum : Summable fun (x : ℕ) => ‖f x‖) (hf₀ : f 0 = 0) : HasProd (fun (p : Nat.Primes) => ∑' (e : ℕ), f (↑p ^ e)) (∑' (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 : Nat.Primes, ∑' e, f (p ^ e) = ∑' n, f n. This version is stated using HasProd.

theorem EulerProduct.eulerProduct_hasProd_mulIndicator {R : Type u_1} [NormedCommRing R] {f : ℕ → R} [CompleteSpace R] (hf₁ : f 1 = 1) (hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) (hsum : Summable fun (x : ℕ) => ‖f x‖) (hf₀ : f 0 = 0) : HasProd ({p : ℕ | Nat.Prime p}.mulIndicator fun (p : ℕ) => ∑' (e : ℕ), f (p ^ e)) (∑' (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 i multiplicative on coprime arguments, and ‖f ·‖ is summable, then ∏' p : ℕ, if p.Prime then ∑' e, f (p ^ e) else 1 = ∑' n, f n. This version is stated using HasProd and Set.mulIndicator.

theorem EulerProduct.eulerProduct {R : Type u_1} [NormedCommRing R] {f : ℕ → R} [CompleteSpace R] (hf₁ : f 1 = 1) (hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) (hsum : Summable fun (x : ℕ) => ‖f x‖) (hf₀ : f 0 = 0) : Filter.Tendsto (fun (n : ℕ) => ∏ p ∈ n.primesBelow, ∑' (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. This is a version using convergence of finite partial products.

theorem EulerProduct.eulerProduct_tprod {R : Type u_1} [NormedCommRing R] {f : ℕ → R} [CompleteSpace R] (hf₁ : f 1 = 1) (hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) (hsum : Summable fun (x : ℕ) => ‖f x‖) (hf₀ : f 0 = 0) : ∏' (p : Nat.Primes), ∑' (e : ℕ), f (↑p ^ e) = ∑' (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.

Versions for arithmetic functions

theorem ArithmeticFunction.IsMultiplicative.eulerProduct_hasProd {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) (hsum : Summable fun (x : ℕ) => ‖f x‖) : HasProd (fun (p : Nat.Primes) => ∑' (e : ℕ), f (↑p ^ e)) (∑' (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 : Nat.Primes, ∑' e, f (p ^ e) = ∑' n, f n. This version is stated in terms of HasProd.

theorem ArithmeticFunction.IsMultiplicative.eulerProduct {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) (hsum : Summable fun (x : ℕ) => ‖f x‖) : Filter.Tendsto (fun (n : ℕ) => ∏ p ∈ n.primesBelow, ∑' (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 : Nat.Primes, ∑' e, f (p ^ e) = ∑' n, f n. This version is stated in the form of convergence of finite partial products.

theorem ArithmeticFunction.IsMultiplicative.eulerProduct_tprod {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) (hsum : Summable fun (x : ℕ) => ‖f x‖) : ∏' (p : Nat.Primes), ∑' (e : ℕ), f (↑p ^ e) = ∑' (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 : Nat.Primes, ∑' e, f (p ^ e) = ∑' n, f n.

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_hasProd and variants.

theorem EulerProduct.one_sub_inv_eq_geometric_of_summable_norm {F : Type u_1} [NormedField F] [CompleteSpace F] {f : ℕ →*₀ F} {p : ℕ} (hp : Nat.Prime p) (hsum : Summable fun (x : ℕ) => ‖f x‖) : (1 - f p)⁻¹ = ∑' (e : ℕ), f (p ^ e)

theorem EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric {F : Type u_1} [NormedField F] [CompleteSpace F] {f : ℕ →* F} (h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1) (s : Finset ℕ) : (Summable fun (m : ↑(Nat.factoredNumbers s)) => ‖f ↑m‖) ∧ HasSum (fun (m : ↑(Nat.factoredNumbers s)) => f ↑m) (∏ p ∈ Finset.filter (fun (p : ℕ) => Nat.Prime p) s, (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 s-factored positive integers n as a product of (1 - f p)⁻¹ over the primes p ∈ s. At the same time, we show that the sum involved converges absolutely.

theorem EulerProduct.prod_filter_prime_geometric_eq_tsum_factoredNumbers {F : Type u_1} [NormedField F] [CompleteSpace F] {f : ℕ →* F} (hsum : Summable ⇑f) (s : Finset ℕ) : ∏ p ∈ Finset.filter (fun (p : ℕ) => Nat.Prime p) s, (1 - f p)⁻¹ = ∑' (m : ↑(Nat.factoredNumbers s)), f ↑m

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

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 : ↑N.smoothNumbers) => ‖f ↑m‖) ∧ HasSum (fun (m : ↑N.smoothNumbers) => f ↑m) (∏ p ∈ N.primesBelow, (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 : ℕ) : ∏ p ∈ N.primesBelow, (1 - f p)⁻¹ = ∑' (m : ↑N.smoothNumbers), 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_hasProd {F : Type u_1} [NormedField F] [CompleteSpace F] {f : ℕ →*₀ F} (hsum : Summable fun (x : ℕ) => ‖f x‖) : HasProd (fun (p : Nat.Primes) => (1 - f ↑p)⁻¹) (∑' (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 : Nat.Primes, (1 - f p)⁻¹ = ∑' n, f n. This version is stated in terms of HasProd.

theorem EulerProduct.eulerProduct_completely_multiplicative_tprod {F : Type u_1} [NormedField F] [CompleteSpace F] {f : ℕ →*₀ F} (hsum : Summable fun (x : ℕ) => ‖f x‖) : ∏' (p : Nat.Primes), (1 - f ↑p)⁻¹ = ∑' (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 : Nat.Primes, (1 - f p)⁻¹ = ∑' n, f n.

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 : ℕ) => ∏ p ∈ n.primesBelow, (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 : Nat.Primes, (1 - f p)⁻¹ = ∑' n, f n. This version is stated in the form of convergence of finite partial products.