Source indexedtheorem · leanprover/lean4:v4.32.0

ZetaAppendix.lemma_abadeulmac'

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:1752 to 1819

Source documentation

\subsection{Approximating zeta(s)} We start with an application of Euler-Maclaurin.

Exact Lean statement

@[blueprint
  "lem:abadeulmac'"
  (title := "Identity for a partial sum of zeta(s) for integer b")
  (statement := /--
Let $b>0$, $b\in \mathbb{Z}$.
Then, for all $s\in \mathbb{C}\setminus \{1\}$ with $\Re s > 0$,
\begin{equation}\label{eq:abak1'}
  \sum_{n \leq b} \frac{1}{n^s} = \zeta(s) + \frac{b^{1-s}}{1-s} + \frac{b^{-s}}{2}
  + s \int_b^\infty \left(\{y\}-\frac{1}{2}\right) \frac{dy}{y^{s+1}}.
\end{equation}
-/)
  (proof := /--
Assume first that $\Re s > 1$. By first-order Euler-Maclaurin,
\[\sum_{n > b}\frac{1}{n^s} = \int_b^\infty \frac{dy}{y^s} + \int_b^\infty
 \left(\{y\}-\frac{1}{2}\right) d\left(\frac{1}{y^s}\right).
\]
Here $\int_b^\infty \frac{dy}{y^s} = -\frac{b^{1-s}}{1-s}$ and
$d\left(\frac{1}{y^s}\right) = - \frac{s}{y^{s+1}} dy$.
Hence, by $\sum_{n\leq b} \frac{1}{n^s} = \zeta(s) - \sum_{n>b} \frac{1}{n^s}$
for $\Re s > 1$,
$$\sum_{n\leq b} \frac{1}{n^s} = \zeta(s) + \frac{b^{1-s}}{1-s} +
\int_b^\infty \left(\{y\}-\frac{1}{2}\right) \frac{s}{y^{s+1}} dy.$$
Since the integral converges absolutely for $\Re s > 0$, both sides extend holomorphically
to $\{s\in \mathbb{C}: \Re s>0, s\ne 1\}$; thus, the equation holds throughout that region.
-/)
  (latexEnv := "lemma")
  (discussion := 566)]
theorem lemma_abadeulmac' {b : ℕ} (hb : 0 < b) {s : ℂ}
    (hs1 : s ≠ 1) (hsigma : 0 < s.re) :
    ∑ n ∈ Icc 1 b, (n : ℂ) ^ (-s) =
      riemannZeta s + (b ^ (1 - s) : ℂ) / (1 - s) + (b ^ (-s) : ℂ) / (2) +
      s * ∫ y in Set.Ioi (b : ℝ), (Int.fract y - 1 / 2) * ((y : ℂ) ^ (-(s + 1)))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "lem:abadeulmac'"  (title := "Identity for a partial sum of zeta(s) for integer b")  (statement := /--Let $b>0$, $b\in \mathbb{Z}$.Then, for all $s\in \mathbb{C}\setminus \{1\}$ with $\Re s > 0$,\begin{equation}\label{eq:abak1'}  \sum_{n \leq b} \frac{1}{n^s} = \zeta(s) + \frac{b^{1-s}}{1-s} + \frac{b^{-s}}{2}  + s \int_b^\infty \left(\{y\}-\frac{1}{2}\right) \frac{dy}{y^{s+1}}.\end{equation}-/)  (proof := /--Assume first that $\Re s > 1$. By first-order Euler-Maclaurin,\[\sum_{n > b}\frac{1}{n^s} = \int_b^\infty \frac{dy}{y^s} + \int_b^\infty \left(\{y\}-\frac{1}{2}\right) d\left(\frac{1}{y^s}\right).\]Here $\int_b^\infty \frac{dy}{y^s} = -\frac{b^{1-s}}{1-s}$ and$d\left(\frac{1}{y^s}\right) = - \frac{s}{y^{s+1}} dy$.Hence, by $\sum_{n\leq b} \frac{1}{n^s} = \zeta(s) - \sum_{n>b} \frac{1}{n^s}$for $\Re s > 1$,$$\sum_{n\leq b} \frac{1}{n^s} = \zeta(s) + \frac{b^{1-s}}{1-s} +\int_b^\infty \left(\{y\}-\frac{1}{2}\right) \frac{s}{y^{s+1}} dy.$$Since the integral converges absolutely for $\Re s > 0$, both sides extend holomorphicallyto $\{s\in \mathbb{C}: \Re s>0, s\ne 1\}$; thus, the equation holds throughout that region.-/)  (latexEnv := "lemma")  (discussion := 566)]theorem lemma_abadeulmac' {b : ℕ} (hb : 0 < b) {s : ℂ}    (hs1 : s ≠ 1) (hsigma : 0 < s.re) :    ∑ n ∈ Icc 1 b, (n : ℂ) ^ (-s) =      riemannZeta s + (b ^ (1 - s) : ℂ) / (1 - s) + (b ^ (-s) : ℂ) / (2) +      s * ∫ y in Set.Ioi (b : ℝ), (Int.fract y - 1 / 2) * ((y : ℂ) ^ (-(s + 1))) := by  rw [← Zeta0EqZeta hb (by linarith) hs1]  unfold riemannZeta0  rw [show ∑ n ∈ Icc 1 b, (n : ℂ) ^ (-s) = (∑ n ∈ Icc 1 b, (n : ℂ) ^ (-s)) + 0 by ring]  rw [show ∑ n ∈ range (b + 1), 1 / (n : ℂ) ^ s = ∑ n ∈ Icc 1 b, (n : ℂ) ^ (-s) by    rw [range_eq_Ico]    rw [sum_eq_sum_Ico_succ_bot (by linarith)]    norm_cast    rw [zero_cpow (by aesop)]    simp only [div_zero, zero_add, one_div]    rw [← Finset.Ico_succ_right_eq_Icc]    congr    ext x    rw [cpow_neg]]  rw [show (∑ n ∈ Icc 1 b, (n : ℂ) ^ (-s) + -(b : ℂ) ^ (1 - s) / (1 - s) + -(b : ℂ) ^ (-s) / 2 +          s * ∫ (x : ℝ) in Set.Ioi ↑b, (⌊x⌋ + 1 / 2 - x : ℂ) / (x : ℂ) ^ (s + 1)) +        (b : ℂ) ^ (1 - s) / (1 - s) +      (b : ℂ) ^ (-s) / 2 +    s * ∫ (y : ℝ) in Set.Ioi ↑b, ((Int.fract y) - 1 / 2) * (y : ℂ) ^ (-(s + 1)) =      ∑ n ∈ Icc 1 b, (n : ℂ) ^ (-s) + (          s * (∫ (x : ℝ) in Set.Ioi ↑b, (⌊x⌋ + 1 / 2 - x : ℂ) / (x : ℂ) ^ (s + 1))   +    s * ∫ (y : ℝ) in Set.Ioi ↑b, ((Int.fract y) - 1 / 2) * (y : ℂ) ^ (-(s + 1))) by ring]  congr! 1  suffices h : ∫ (x : ℝ) in Set.Ioi ↑b, (⌊x⌋ + 1 / 2 - x : ℂ) / ↑x ^ (s + 1) =             -∫ (y : ℝ) in Set.Ioi ↑b, ((Int.fract y) - 1 / 2 : ℂ) * ↑y ^ (-(s + 1)) by    rw [h]; ring  rw [← MeasureTheory.integral_neg]  congr 1  ext x  unfold Int.fract  rw [show (x : ℂ) ^ (-(s + 1)) = 1 / (↑x : ℂ) ^ (s + 1) by    rw [cpow_neg, one_div]]  rw [mul_one_div, ← neg_div]  congr  ring_nf  push_cast  ring_nf