summable_riemannZetaSummand
theorem summable_riemannZetaSummand : ∀ {s : ℂ} (hs : 1 < s.re), Summable fun n => ‖(riemannZetaSummandHom ⋯) n‖ := by
sorry
The theorem `summable_riemannZetaSummand` states that for any complex number `s` with its real part greater than 1, the function mapping each natural number `n` to the norm of `n` raised to the power of `-s` (as defined by the `riemannZetaSummandHom` function) is summmable. In other words, the series $\sum_{n=1}^\infty \|n^{-s}\|$ converges when the real part of `s` is greater than one.
More concisely: For complex numbers `s` with real part greater than 1, the series $\sum\_{n=1}^\infty \|n^{-s}\|$ converges.
|
summable_dirichletSummand
theorem summable_dirichletSummand :
∀ {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re), Summable fun n => ‖(dirichletSummandHom χ ⋯) n‖
The theorem `summable_dirichletSummand` states that for any complex number `s` and natural number `N`, given a Dirichlet character `χ` of level `N` and the condition that the real part of `s` is greater than 1, the function mapping each natural number `n` to the norm of the product of the value of the Dirichlet character at `n` and `n` raised to the power of `-s` is summable. In other words, the sequence given by the norms of these terms has a finite sum.
More concisely: For any complex number `s` with real part greater than 1 and Dirichlet character `χ` of level `N`, the function mapping each natural number `n` to the norm of `χ(n) * n^(-s)` is summable.
|
riemannZeta_eulerProduct
theorem riemannZeta_eulerProduct :
∀ {s : ℂ},
1 < s.re →
Filter.Tendsto (fun n => n.primesBelow.prod fun p => (1 - ↑p ^ (-s))⁻¹) Filter.atTop (nhds (riemannZeta s))
This theorem states that the Euler product formula for the Riemann zeta function holds for complex numbers `s` with real part greater than 1. More specifically, it asserts that as `n` tends to infinity, the product over the primes less than or equal to `n` of the terms `(1 - p^(-s))^(-1)` tends to the value of the Riemann zeta function at `s`. This is essentially the statement of the Euler product formula for the Riemann zeta function in the region where it is absolutely convergent.
More concisely: The Riemann Zeta function's Euler product converges and equals its value for complex numbers `s` with real part greater than 1.
|
dirichletLSeries_eulerProduct
theorem dirichletLSeries_eulerProduct :
∀ {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re),
Filter.Tendsto (fun n => n.primesBelow.prod fun p => (1 - χ ↑p * ↑p ^ (-s))⁻¹) Filter.atTop
(nhds (∑' (n : ℕ), (dirichletSummandHom χ ⋯) n))
The theorem `dirichletLSeries_eulerProduct` states that for any complex number `s` and any natural number `N`, if `s` has real part greater than 1 and `χ` is a Dirichlet character with level `N`, then as `n` goes to infinity, the product over all primes less than `n` of the term `(1 - χ p * p^(-s))^(-1)` converges to the sum of the terms `(dirichletSummandHom χ ⋯) n` for all natural numbers `n`. This is commonly known as the Euler product formula for Dirichlet L-series.
More concisely: For any complex number `s` with real part > 1 and Dirichlet character `χ` of level `N`, the Euler product `∏_(p < ∞, p prime) (1 - χ p * p^(-s))^(-1)` converges to the sum `∑_(n) (dirichletSummandHom χ ...) n` as `n` goes to infinity.
|