theorem LSeries.term_sum_apply {ι : Type u_1} [DecidableEq ι] {f : ι → ℕ → ℂ} (S : Finset ι) (s : ℂ) (n : ℕ) : LSeries.term (∑ i ∈ S, f i) s n = ∑ i ∈ S, LSeries.term (f i) s n

theorem LSeries.term_sum {ι : Type u_1} [DecidableEq ι] {f : ι → ℕ → ℂ} (S : Finset ι) (s : ℂ) : LSeries.term (∑ i ∈ S, f i) s = ∑ i ∈ S, LSeries.term (f i) s

theorem LSeriesHasSum.sum {ι : Type u_1} [DecidableEq ι] {s : ℂ} {f : ι → ℕ → ℂ} (S : Finset ι) {a : ι → ℂ} (hf : ∀ i ∈ S, LSeriesHasSum (f i) s (a i)) : LSeriesHasSum (∑ i ∈ S, f i) s (∑ i ∈ S, a i)

theorem LSeriesSummable.sum {ι : Type u_1} [DecidableEq ι] {s : ℂ} {f : ι → ℕ → ℂ} (S : Finset ι) (hf : ∀ i ∈ S, LSeriesSummable (f i) s) : LSeriesSummable (∑ i ∈ S, f i) s

@[simp]

theorem LSeries_sum {ι : Type u_1} [DecidableEq ι] {s : ℂ} {f : ι → ℕ → ℂ} (S : Finset ι) (hf : ∀ i ∈ S, LSeriesSummable (f i) s) : LSeries (∑ i ∈ S, f i) s = ∑ i ∈ S, LSeries (f i) s

theorem LSeriesHasSum.sum' {ι : Type u_1} [DecidableEq ι] {s : ℂ} {f : ι → ℕ → ℂ} [Fintype ι] {a : ι → ℂ} (hf : ∀ (i : ι), LSeriesHasSum (f i) s (a i)) : LSeriesHasSum (∑ i : ι, f i) s (∑ i : ι, a i)

The version of LSeriesHasSum.sum for Fintype.sum.

theorem LSeriesSummable.sum' {ι : Type u_1} [DecidableEq ι] {s : ℂ} {f : ι → ℕ → ℂ} [Fintype ι] (hf : ∀ (i : ι), LSeriesSummable (f i) s) : LSeriesSummable (∑ i : ι, f i) s

The version of LSeriesSummable.sum for Fintype.sum.

@[simp]

theorem LSeries_sum' {ι : Type u_1} [DecidableEq ι] {s : ℂ} {f : ι → ℕ → ℂ} [Fintype ι] (hf : ∀ (i : ι), LSeriesSummable (f i) s) : LSeries (∑ i : ι, f i) s = ∑ i : ι, LSeries (f i) s

The version of LSeries_sum for Fintype.sum.

Statement of a version of the Wiener-Ikehara Theorem

def WienerIkeharaTheorem : Prop

A version of the Wiener-Ikehara Tauberian Theorem: If f is a nonnegative arithmetic function whose L-series has a simple pole at s = 1 with residue A and otherwise extends continuously to the closed half-plane re s ≥ 1, then ∑ n < N, f n is asymptotic to A*N.

Equations

• One or more equations did not get rendered due to their size.

The L-function of a Dirichlet character does not vanish on Re(s) = 1

theorem one_lt_re_of_pos {x : ℝ} (y : ℝ) (hx : 0 < x) : 1 < (1 + ↑x).re ∧ 1 < (1 + ↑x + Complex.I * ↑y).re ∧ 1 < (1 + ↑x + 2 * Complex.I * ↑y).re

def rzeta : Lean.ParserDescr

We use ζ to denote the Riemann zeta function.

Equations

• rzeta = Lean.ParserDescr.node `rzeta 1024 (Lean.ParserDescr.symbol "ζ")

def Dchar_one' : Lean.ParserDescr

We use χ₁ to denote the (trivial) Dirichlet character modulo 1.

Equations

• Dchar_one' = Lean.ParserDescr.node `Dchar_one' 1024 (Lean.ParserDescr.symbol "χ₁")

theorem DirichletCharacter.LSeries_eulerProduct' {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) : Complex.exp (∑' (p : Nat.Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))) = LSeries (fun (n : ℕ) => χ ↑n) s

A variant of the Euler product for Dirichlet L-series.

theorem ArithmeticFunction.LSeries_zeta_eulerProduct' {s : ℂ} (hs : 1 < s.re) : Complex.exp (∑' (p : Nat.Primes), -Complex.log (1 - ↑↑p ^ (-s))) = LSeries 1 s

A variant of the Euler product for the L-series of ζ.

theorem riemannZeta_eulerProduct' {s : ℂ} (hs : 1 < s.re) : Complex.exp (∑' (p : Nat.Primes), -Complex.log (1 - ↑↑p ^ (-s))) = riemannZeta s

A variant of the Euler product for the Riemann zeta function.

theorem summable_neg_log_one_sub_char_mul_prime_cpow {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) : Summable fun (p : Nat.Primes) => -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))

theorem re_log_comb_nonneg {a : ℝ} (ha₀ : 0 ≤ a) (ha₁ : a < 1) {z : ℂ} (hz : ‖z‖ = 1) : 0 ≤ 3 * (-Complex.log (1 - ↑a)).re + 4 * (-Complex.log (1 - ↑a * z)).re + (-Complex.log (1 - ↑a * z ^ 2)).re

A technical lemma showing that a certain linear combination of real parts of logarithms is nonnegative. This is used to show non-vanishing of the Riemann zeta function and of Dirichlet L-series on the line re s = 1.

theorem DirichletCharacter.deriv_LFunction_eq_deriv_LSeries {n : ℕ} [NeZero n] (χ : DirichletCharacter ℂ n) {s : ℂ} (hs : 1 < s.re) : deriv (DirichletCharacter.LFunction χ) s = deriv (LSeries fun (n_1 : ℕ) => χ ↑n_1) s

theorem DirichletCharacter.re_log_comb_nonneg {N : ℕ} (χ : DirichletCharacter ℂ N) {n : ℕ} (hn : 2 ≤ n) {x : ℝ} {y : ℝ} (hx : 1 < x) : 0 ≤ 3 * (-Complex.log (1 - 1 ↑n * ↑n ^ (-↑x))).re + 4 * (-Complex.log (1 - χ ↑n * ↑n ^ (-(↑x + Complex.I * ↑y)))).re + (-Complex.log (1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * Complex.I * ↑y)))).re

The logarithm of an Euler factor of the product L(χ^0, x)^3 * L(χ, x+I*y)^4 * L(χ^2, x+2*I*y) has nonnegative real part when s = x + I*y has real part x > 1.

theorem DirichletCharacter.norm_LSeries_product_ge_one {N : ℕ} (χ : DirichletCharacter ℂ N) {x : ℝ} (hx : 0 < x) (y : ℝ) : ‖LSeries (fun (n : ℕ) => 1 ↑n) (1 + ↑x) ^ 3 * LSeries (fun (n : ℕ) => χ ↑n) (1 + ↑x + Complex.I * ↑y) ^ 4 * LSeries (fun (n : ℕ) => (χ ^ 2) ↑n) (1 + ↑x + 2 * Complex.I * ↑y)‖ ≥ 1

For positive x and nonzero y we have that $|L(\chi^0, x)^3 \cdot L(\chi, x+iy)^4 \cdot L(\chi^2, x+2iy)| \ge 1$.

theorem DirichletCharacter.norm_LFunction_product_ge_one {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} {x : ℝ} (hx : 0 < x) (y : ℝ) : ‖DirichletCharacter.LFunctionTrivChar N (1 + ↑x) ^ 3 * DirichletCharacter.LFunction χ (1 + ↑x + Complex.I * ↑y) ^ 4 * DirichletCharacter.LFunction (χ ^ 2) (1 + ↑x + 2 * Complex.I * ↑y)‖ ≥ 1

A variant of DirichletCharacter.norm_LSeries_product_ge_one in terms of the L-functions.

theorem DirichletCharacter.LFunction_triv_char_isBigO_near_one_horizontal {N : ℕ} [NeZero N] : (fun (x : ℝ) => DirichletCharacter.LFunctionTrivChar N (1 + ↑x)) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => 1 / ↑x

theorem DirichletCharacter.LFunction_isBigO_of_ne_one_horizontal {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} {y : ℝ} (hy : y ≠ 0 ∨ χ ≠ 1) : (fun (x : ℝ) => DirichletCharacter.LFunction χ (1 + ↑x + Complex.I * ↑y)) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => 1

theorem DirichletCharacter.LFunction_isBigO_near_root_horizontal {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} {y : ℝ} (hy : y ≠ 0 ∨ χ ≠ 1) (h : DirichletCharacter.LFunction χ (1 + Complex.I * ↑y) = 0) : (fun (x : ℝ) => DirichletCharacter.LFunction χ (1 + ↑x + Complex.I * ↑y)) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => ↑x

theorem DirichletCharacter.LFunction_ne_zero_of_re_eq_one_of_not_quadratic {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} {t : ℝ} (h : χ ^ 2 ≠ 1 ∨ t ≠ 0) : DirichletCharacter.LFunction χ (1 + Complex.I * ↑t) ≠ 0

The L function of a Dirichlet character χ does not vanish at 1 + I*t if t ≠ 0 or χ^2 ≠ 1.

theorem DirichletCharacter.Lfunction_ne_zero_of_re_eq_one {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) (t : ℝ) (hχt : χ ≠ 1 ∨ t ≠ 0) : DirichletCharacter.LFunction χ (1 + Complex.I * ↑t) ≠ 0

If χ is a Dirichlet character, then L(χ, 1 + I*t) does not vanish for t ∈ ℝ except when χ is trivial and t = 0 (then L(χ, s) has a simple pole at s = 1).

theorem DirichletCharacter.Lfunction_ne_zero_of_one_le_re {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) ⦃s : ℂ⦄ (hχs : χ ≠ 1 ∨ s ≠ 1) (hs : 1 ≤ s.re) : DirichletCharacter.LFunction χ s ≠ 0

If χ is a Dirichlet character, then L(χ, s) does not vanish for s.re ≥ 1 except when χ is trivial and s = 1 (then L(χ, s) has a simple pole at s = 1).

theorem riemannZeta_ne_zero_of_one_le_re ⦃z : ℂ⦄ (hz : z ≠ 1) (hz' : 1 ≤ z.re) : riemannZeta z ≠ 0

The Riemann Zeta Function does not vanish on the closed half-plane re z ≥ 1.

The logarithmic derivative of the L-function of a trivial character has a simple pole at s = 1 with residue -1

We show that s ↦ L'(χ) s / L(χ) s + 1 / (s - 1) (or rather, its negative, which is the function we need for the Wiener-Ikehara Theorem) is continuous outside the zeros of L(χ) when χ is a trivial Dirichlet character.

noncomputable def DirichletCharacter.LFunction_triv_char₁ (n : ℕ) [NeZero n] : ℂ → ℂ

The function obtained by "multiplying away" the pole of L(χ) for a trivial Dirichlet character χ. Its (negative) logarithmic derivative is used in the Wiener-Ikehara Theorem to prove the Prime Number Theorem version of Dirichlet's Theorem on primes in arithmetic progressions.

Equations

• DirichletCharacter.LFunction_triv_char₁ n = Function.update (fun (z : ℂ) => DirichletCharacter.LFunctionTrivChar n z * (z - 1)) 1 (∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹))

theorem DirichletCharacter.LFunction_triv_char₁_apply_of_ne_one (n : ℕ) [NeZero n] {z : ℂ} (hz : z ≠ 1) : DirichletCharacter.LFunction_triv_char₁ n z = DirichletCharacter.LFunctionTrivChar n z * (z - 1)

theorem DirichletCharacter.LFunction_triv_char₁_differentiable (n : ℕ) [NeZero n] : Differentiable ℂ (DirichletCharacter.LFunction_triv_char₁ n)

theorem DirichletCharacter.deriv_LFunction_triv_char₁_apply_of_ne_one (n : ℕ) [NeZero n] {z : ℂ} (hz : z ≠ 1) : deriv (DirichletCharacter.LFunction_triv_char₁ n) z = deriv (DirichletCharacter.LFunctionTrivChar n) z * (z - 1) + DirichletCharacter.LFunctionTrivChar n z

theorem DirichletCharacter.neg_logDeriv_LFunction_triv_char₁_eq (n : ℕ) [NeZero n] {z : ℂ} (hz₁ : z ≠ 1) (hz₂ : DirichletCharacter.LFunctionTrivChar n z ≠ 0) : -deriv (DirichletCharacter.LFunction_triv_char₁ n) z / DirichletCharacter.LFunction_triv_char₁ n z = -deriv (DirichletCharacter.LFunctionTrivChar n) z / DirichletCharacter.LFunctionTrivChar n z - 1 / (z - 1)

theorem DirichletCharacter.continuousOn_neg_logDeriv_LFunction_triv_char₁ (n : ℕ) [NeZero n] : ContinuousOn (fun (z : ℂ) => -deriv (DirichletCharacter.LFunction_triv_char₁ n) z / DirichletCharacter.LFunction_triv_char₁ n z) {z : ℂ | z = 1 ∨ DirichletCharacter.LFunctionTrivChar n z ≠ 0}

theorem DirichletCharacter.eq_one_or_LFunction_triv_char_ne_zero_of_one_le_re (n : ℕ) [NeZero n] : {s : ℂ | 1 ≤ s.re} ⊆ {s : ℂ | s = 1 ∨ DirichletCharacter.LFunction 1 s ≠ 0}

theorem DirichletCharacter.continuousOn_neg_logDeriv_LFunction_nontriv_char {n : ℕ} [NeZero n] {χ : DirichletCharacter ℂ n} (hχ : χ ≠ 1) : ContinuousOn (fun (z : ℂ) => -deriv (DirichletCharacter.LFunction χ) z / DirichletCharacter.LFunction χ z) {z : ℂ | DirichletCharacter.LFunction χ z ≠ 0}

The negative logarithmic derivative of a Dirichlet L-function is continuous away from the zeros of the L-function.

theorem DirichletCharacter.LFunction_nontriv_char_ne_zero_of_one_le_re {n : ℕ} [NeZero n] {χ : DirichletCharacter ℂ n} (hχ : χ ≠ 1) : {s : ℂ | 1 ≤ s.re} ⊆ {s : ℂ | DirichletCharacter.LFunction χ s ≠ 0}

The logarithmic derivative of ζ has a simple pole at s = 1 with residue -1

We show that s ↦ ζ' s / ζ s + 1 / (s - 1) (or rather, its negative, which is the function we need for the Wiener-Ikehara Theorem) is continuous outside the zeros of ζ.

noncomputable def ζ₁ : ℂ → ℂ

The function obtained by "multiplying away" the pole of ζ. Its (negative) logarithmic derivative is the function used in the Wiener-Ikehara Theorem to prove the Prime Number Theorem.

Equations

• ζ₁ = Function.update (fun (z : ℂ) => riemannZeta z * (z - 1)) 1 1

theorem riemannZeta_eq_LFunction_triv_char_one : riemannZeta = DirichletCharacter.LFunctionTrivChar 1

theorem ζ₁_eq_LFunction_triv_char₁_one : ζ₁ = DirichletCharacter.LFunction_triv_char₁ 1

theorem neg_logDeriv_ζ₁_eq {z : ℂ} (hz₁ : z ≠ 1) (hz₂ : riemannZeta z ≠ 0) : -deriv ζ₁ z / ζ₁ z = -deriv riemannZeta z / riemannZeta z - 1 / (z - 1)

theorem continuousOn_neg_logDeriv_ζ₁ : ContinuousOn (fun (z : ℂ) => -deriv ζ₁ z / ζ₁ z) {z : ℂ | z = 1 ∨ riemannZeta z ≠ 0}

Proof of Lemma 9

We prove Lemma 9 of Section 2 in the PNT+ Project.

theorem WeakPNT_character {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) {s : ℂ} (hs : 1 < s.re) : LSeries ({n : ℕ | ↑n = a}.indicator fun (n : ℕ) => ↑(ArithmeticFunction.vonMangoldt n)) s = -(↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * (deriv (DirichletCharacter.LFunction χ) s / DirichletCharacter.LFunction χ s)

Lemma 9 of Section 2 of PNT+: The L-series of the von Mangoldt function restricted to the prime residue class a mod q as a linear combination of logarithmic derivatives of L functions of the Dirichlet characters mod q.

noncomputable def weakDirichlet_auxFun (q : ℕ) [NeZero q] (a : ZMod q) (s : ℂ) : ℂ

The function F used in the Wiener-Ikehara Theorem to prove Dirichlet's Theorem.

Equations

• One or more equations did not get rendered due to their size.

theorem weakDirichlet_auxFun_prop {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) : Set.EqOn (weakDirichlet_auxFun q a) (fun (s : ℂ) => LSeries ({n : ℕ | ↑n = a}.indicator fun (n : ℕ) => ↑(ArithmeticFunction.vonMangoldt n)) s - (↑q.totient)⁻¹ / (s - 1)) {s : ℂ | 1 < s.re}

theorem continuousOn_weakDirichlet_auxFun {q : ℕ} [NeZero q] {a : ZMod q} : ContinuousOn (weakDirichlet_auxFun q a) {s : ℂ | 1 ≤ s.re}

(A version of) Proposition 2 of Section 2 of PNT+: the L-series of the von Mangoldt function restricted to the prime residue class a mod q is continuous on s.re ≥ 1 except for a single pole at s = 1 with residue (q.totient)⁻¹.

Derivation of the Prime Number Theorem and Dirichlet's Theorem from the Wiener-Ikehara Theorem

theorem Dirichlet_vonMangoldt (WIT : WienerIkeharaTheorem) {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) : Filter.Tendsto (fun (N : ℕ) => (Finset.filter (fun (n : ℕ) => ↑n = a) (Finset.range N)).sum ⇑ArithmeticFunction.vonMangoldt / ↑N) Filter.atTop (nhds (↑q.totient)⁻¹)

The Wiener-Ikehara Theorem implies Dirichlet's Theorem in the form that ψ x ∼ q.totient⁻¹ * x, where ψ x = ∑ n < x ∧ n ≡ a mod q, Λ n and Λ is the von Mangoldt function.

This is Theorem 2 in Section 2 of PNT+ (but using the WIT stub defined here).

theorem PNT_vonMangoldt (WIT : WienerIkeharaTheorem) : Filter.Tendsto (fun (N : ℕ) => (Finset.range N).sum ⇑ArithmeticFunction.vonMangoldt / ↑N) Filter.atTop (nhds 1)

The Wiener-Ikehara Theorem implies the Prime Number Theorem in the form that ψ x ∼ x, where ψ x = ∑ n < x, Λ n and Λ is the von Mangoldt function.