Documentation

Mathlib.NumberTheory.EulerProduct.Basic

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 nf (m * n) = f m * f n) (hsum : ∀ {p : }, Nat.Prime pSummable fun (n : ) => f (p ^ n)) (s : Finset ) :
(Summable fun (m : (Nat.factoredNumbers s)) => f m) HasSum (fun (m : (Nat.factoredNumbers s)) => f m) (∏ pFinset.filter Nat.Prime 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 nf (m * n) = f m * f n) (hsum : Summable fun (x : ) => f x) (s : Finset ) :
pFinset.filter Nat.Prime 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 nf (m * n) = f m * f n) (hsum : ∀ {p : }, Nat.Prime pSummable fun (n : ) => f (p ^ n)) (N : ) :
(Summable fun (m : N.smoothNumbers) => f m) HasSum (fun (m : N.smoothNumbers) => f m) (∏ pN.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 nf (m * n) = f m * f n) (hsum : Summable fun (x : ) => f x) (N : ) :
pN.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₀ : ), NN₀, ∑' (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 nf (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 nf (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 nf (m * n) = f m * f n) (hsum : Summable fun (x : ) => f x) (hf₀ : f 0 = 0) :
Filter.Tendsto (fun (n : ) => pn.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 nf (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 : ) => pn.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 pf p < 1) (s : Finset ) :
(Summable fun (m : (Nat.factoredNumbers s)) => f m) HasSum (fun (m : (Nat.factoredNumbers s)) => f m) (∏ pFinset.filter Nat.Prime 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 ) :
pFinset.filter Nat.Prime 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 pf p < 1) (N : ) :
(Summable fun (m : N.smoothNumbers) => f m) HasSum (fun (m : N.smoothNumbers) => f m) (∏ pN.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 : ) :
pN.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 : ) => pn.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.