EulerProduct.eulerProduct_completely_multiplicative
theorem EulerProduct.eulerProduct_completely_multiplicative :
∀ {F : Type u_1} [inst : NormedField F] [inst_1 : CompleteSpace F] {f : ℕ →*₀ F},
(Summable fun x => ‖f x‖) →
Filter.Tendsto (fun n => n.primesBelow.prod fun p => (1 - f p)⁻¹) Filter.atTop (nhds (∑' (n : ℕ), f n))
This theorem is known as the *Euler Product* for completely multiplicative functions. If you have a completely multiplicative function `f` from natural numbers to a complete normed field `F`, and the norm of `f` is summable (i.e., the series of the norms of `f` converges), then the product over all prime numbers `p` of `(1 - f p)⁻¹` converges to the sum over all natural numbers `n` of `f n`. Concretely, this says the infinite product `∏' p : Nat.Primes, (1 - f p)⁻¹` equals the infinite sum `∑' n, f n`. This theorem is stated in the form of convergence of finite partial products, meaning that as you consider more and more terms in the product, the value of the product gets closer and closer to the value of the infinite sum.
More concisely: If `f` is a completely multiplicative function from natural numbers to a complete normed field with summable norm, then the product of `(1 - f p)⁻¹` over all prime numbers `p` converges to the sum of `fn` over all natural numbers `n`.
|
EulerProduct.eulerProduct
theorem EulerProduct.eulerProduct :
∀ {R : Type u_1} [inst : NormedCommRing R] [inst_1 : CompleteSpace R] {f : ℕ → R},
f 1 = 1 →
(∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) →
(Summable fun x => ‖f x‖) →
f 0 = 0 →
Filter.Tendsto (fun n => n.primesBelow.prod fun p => ∑' (e : ℕ), f (p ^ e)) Filter.atTop
(nhds (∑' (n : ℕ), f n))
This theorem is called the *Euler Product* for multiplicative functions on coprime arguments. It states that given a function `f` from natural numbers to a complete normed commutative ring `R` with properties that `f 0 = 0`, `f 1 = 1`, and `f` is multiplicative on coprime arguments. If the norm of `f` is summable, then the infinite product over all prime numbers `p` of the infinite sum over all natural numbers `e` of `f` applied to `p` to the power of `e`, tends to the infinite sum over all natural numbers of `f n` as `n` goes to infinity. This is a version of the Euler Product using convergence of finite partial products.
More concisely: Given a multiplicative function `f` from natural numbers to a complete normed commutative ring with `f 0 = 0`, `f 1 = 1`, and summable norm, the Euler product ∏p=p∞ ∑e=0∞ f(p)pe converges to ∑n=0∞ fn as n goes to infinity.
|
EulerProduct.prod_primesBelow_geometric_eq_tsum_smoothNumbers
theorem EulerProduct.prod_primesBelow_geometric_eq_tsum_smoothNumbers :
∀ {F : Type u_1} [inst : NormedField F] [inst_1 : CompleteSpace F] {f : ℕ →* F},
Summable ⇑f → ∀ (N : ℕ), (N.primesBelow.prod fun p => (1 - f p)⁻¹) = ∑' (m : ↑N.smoothNumbers), f ↑m
The theorem `EulerProduct.prod_primesBelow_geometric_eq_tsum_smoothNumbers` states that for any normed field `F` that is also a complete space, and any function `f` from natural numbers to `F` that is summable, for any natural number `N`, the product of `(1 - f p)⁻¹`, taken over all prime numbers less than `N`, is equal to the sum of `f m` over all `m` in the smooth numbers of `N`. Here, the symbol `∑'` stands for `tsum`, which is used to denote an infinite sum in Lean 4.
More concisely: For any complete normed field `F` and summable `F`-valued function `f` on natural numbers, the product of `(1 - f p)⁻¹` over primes `p` less than `N` equals the sum of `f m` over smooth numbers `m` of `N`, denoted as `∑' f m`.
|
EulerProduct.prod_primesBelow_tsum_eq_tsum_smoothNumbers
theorem EulerProduct.prod_primesBelow_tsum_eq_tsum_smoothNumbers :
∀ {R : Type u_1} [inst : NormedCommRing R] [inst_1 : CompleteSpace R] {f : ℕ → R},
f 1 = 1 →
(∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) →
(Summable fun x => ‖f x‖) →
∀ (N : ℕ), (N.primesBelow.prod fun p => ∑' (n : ℕ), f (p ^ n)) = ∑' (m : ↑N.smoothNumbers), f ↑m
This theorem, `EulerProduct.prod_primesBelow_tsum_eq_tsum_smoothNumbers`, states that for any normed commutative ring `R` that is also a complete space, for any function `f` from natural numbers to `R`, if `f` applied to 1 equals 1, and for every pair of natural numbers `m` and `n` that are coprime, `f` applied to the product of `m` and `n` equals the product of `f` applied to `m` and `f` applied to `n`, and if the infinite sum of the norms of `f` applied to natural numbers is finite (summable), then for an arbitrary natural number `N`, the infinite sum of `f` applied to each power of each prime number less than `N`, multiplied together, equals the infinite sum of `f` applied to each `N`-smooth number.
In mathematical terms, it's equivalent to saying: For a given function `f` that satisfies \[f(1) = 1\] and \[f(m * n) = f(m) * f(n)\] for all coprime `m` and `n`, and such that \[\sum_{x=1}^{\infty} \|f(x)\|\] is finite, then for any `N`, we have \[\prod_{p \in \text{primesBelow}(N)} \sum_{n=0}^{\infty} f(p^n) = \sum_{m \in \text{N.smoothNumbers}} f(m).\]
More concisely: For a normed commutative ring `R` that is complete, if `f : ℕ → R` satisfies `f 1 = 1`, `f (m * n) = f m * f n` for coprime `m` and `n`, and the series `∑x=1^∞ �� Situ f x` converges, then `∑p∈primesBelow(N) �� Situ (f p^n) = ∑m∈N.smoothNumbers f m` for all `N`.
|
EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum
theorem EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum :
∀ {R : Type u_1} [inst : NormedCommRing R] [inst_1 : CompleteSpace R] {f : ℕ → R},
f 1 = 1 →
(∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) →
(∀ {p : ℕ}, p.Prime → Summable fun n => ‖f (p ^ n)‖) →
∀ (N : ℕ),
(Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (N.primesBelow.prod fun p => ∑' (n : ℕ), f (p ^ n))
This theorem states that for any type `R` that has the structure of a normed commutative ring and is also a complete space, and for any function `f` from the natural numbers to `R`, given certain conditions on `f`, we can relate a finite product over primes to an infinite sum over smooth numbers. The conditions on `f` are: `f` of 1 equals 1, `f` is multiplicative for coprime arguments, and the sequence `f` of the power of any prime number is summable. Then, for any natural number `N`, there exists a summable sequence with the norm of `f` of m (for each natural number m), and the sum of the values of `f` over each natural number m equals the product of the infinite sums of `f` of the power of each prime number below `N`.
More concisely: For any normed commutative ring `R` that is complete, and any multiplicative function `f` from natural numbers to `R` with `f 1 = 1`, such that the sequence `(f p^n)` is summable for each prime `p`, there exists a summable sequence `s` in `R` such that `s.sum = prod (sum (f p^n) over primes `p < N)`.
|
EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric
theorem EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric :
∀ {F : Type u_1} [inst : NormedField F] [inst_1 : CompleteSpace F] {f : ℕ →* F},
(∀ {p : ℕ}, p.Prime → ‖f p‖ < 1) →
∀ (N : ℕ), (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (N.primesBelow.prod fun p => (1 - f p)⁻¹)
This theorem, called `EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric`, states the following: Given a completely multiplicative function `f` that maps from natural numbers to a normed field `F` (where `F` also forms a complete space), and given that the norm of `f(p)` is less than 1 for all prime `p`, we can express the sum of `f(n)` over all `N`-smooth positive integers `n` as a product of `(1 - f p)^(-1)` over the primes `p` less than `N`. Along with this, the theorem also asserts that the sum in question absolutely converges. The concept of `N`-smooth numbers refers to those positive integers whose all prime factors are less than or equal to `N`.
More concisely: Given a completely multiplicative function `f` from natural numbers to a normed field `F` with norms less than 1 for all primes, the sum of `f(n)` over all `N`-smooth positive integers `n` is equal to the product of `(1 - f p)^(-1)` over all primes `p` less than `N`, and this sum absolutely converges.
|
Summable.norm_lt_one
theorem Summable.norm_lt_one :
∀ {F : Type u_1} [inst : NormedField F] [inst_1 : CompleteSpace F] {f : ℕ →* F},
Summable ⇑f → ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
The theorem `Summable.norm_lt_one` states that for any function `f` from natural numbers to a complete normed field `F`, if `f` is a multiplicative function and it is summable (i.e., the series of its values has a finite sum), then the norm of `f(p)` is strictly less than `1` for all natural numbers `p > 1`. Here, the norm ‖f p‖ refers to the absolute value of `f(p)` in the field `F`.
More concisely: For any multiplicative, summable function `f` from natural numbers to a complete normed field `F`, the norm of `f(p)` strictly less than 1 holds for all `p > 1`.
|
EulerProduct.norm_tsum_smoothNumbers_sub_tsum_lt
theorem EulerProduct.norm_tsum_smoothNumbers_sub_tsum_lt :
∀ {R : Type u_1} [inst : NormedCommRing R] [inst_1 : CompleteSpace R] {f : ℕ → R},
Summable f →
f 0 = 0 → ∀ {ε : ℝ}, 0 < ε → ∃ N₀, ∀ N ≥ N₀, ‖∑' (m : ℕ), f m - ∑' (m : ↑N.smoothNumbers), f ↑m‖ < ε
The theorem `EulerProduct.norm_tsum_smoothNumbers_sub_tsum_lt` states that for any normed commutative ring `R` that is also a complete space, for any function `f` from natural numbers to `R`, if `f` is summable and `f(0)` is zero, then for any positive real number `ε`, there exists a natural number `N₀` such that for all `N` greater than or equal to `N₀`, the norm of the difference between the infinite sum of `f` over all natural numbers and the infinite sum of `f` over the `N`-smooth numbers is less than `ε`. In layman's terms, it says that the sum of `f` over `N`-smooth numbers can get arbitrarily close to the sum over all natural numbers, as `N` becomes large enough.
More concisely: For any normed complete commutative ring `R` and summable function `f` from natural numbers to `R` with `f(0) = 0`, given any positive real `ε`, there exists a natural number `N₀` such that the norm of `f`'s difference between the sum over all natural numbers and the sum over `N`-smooth numbers is less than `ε` for all `N` greater than or equal to `N₀`.
|