|
| 1 | +/- |
| 2 | +Copyright (c) 2024 David Loeffler. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: David Loeffler |
| 5 | +-/ |
| 6 | + |
| 7 | +import Mathlib.NumberTheory.LSeries.HurwitzZetaEven |
| 8 | +import Mathlib.NumberTheory.LSeries.HurwitzZetaOdd |
| 9 | +import Mathlib.Analysis.SpecialFunctions.Gamma.Beta |
| 10 | + |
| 11 | +/-! |
| 12 | +# The Hurwitz zeta function |
| 13 | +
|
| 14 | +This file gives the definition and properties of the following two functions: |
| 15 | +
|
| 16 | +* The **Hurwitz zeta function**, which is the meromorphic continuation to all `s ∈ ℂ` of the |
| 17 | + function defined for `1 < re s` by the series |
| 18 | +
|
| 19 | + `∑' n, 1 / (n + a) ^ s` |
| 20 | +
|
| 21 | + for a parameter `a ∈ ℝ`, with the sum taken over all `n` such that `n + a > 0`; |
| 22 | +
|
| 23 | +* the related sum, which we call the "**exponential zeta function**" (does it have a standard name?) |
| 24 | +
|
| 25 | + `∑' n : ℕ, exp (2 * π * I * n * a) / n ^ s`. |
| 26 | +
|
| 27 | +## Main definitions and results |
| 28 | +
|
| 29 | +* `hurwitzZeta`: the Hurwitz zeta function (defined to be periodic in `a` with period 1) |
| 30 | +* `expZeta`: the exponential zeta function |
| 31 | +* `hasSum_nat_hurwitzZeta_of_mem_Icc` and `hasSum_expZeta_of_one_lt_re`: |
| 32 | + relation to Dirichlet series for `1 < re s` |
| 33 | +* ` hurwitzZeta_residue_one` shows that the residue at `s = 1` equals `1` |
| 34 | +* `differentiableAt_hurwitzZeta` and `differentiableAt_expZeta`: analyticity away from `s = 1` |
| 35 | +* `hurwitzZeta_one_sub` and `expZeta_one_sub`: functional equations `s ↔ 1 - s`. |
| 36 | +-/ |
| 37 | + |
| 38 | +open Set Real Complex Filter Topology |
| 39 | + |
| 40 | +/-! |
| 41 | +## The Hurwitz zeta function |
| 42 | +-/ |
| 43 | + |
| 44 | +/-- The Hurwitz zeta function, which is the meromorphic continuation of |
| 45 | +`∑ (n : ℕ), 1 / (n + a) ^ s` if `0 ≤ a ≤ 1`. See `hasSum_hurwitzZeta_of_one_lt_re` for the relation |
| 46 | +to the Dirichlet series in the convergence range. -/ |
| 47 | +noncomputable def hurwitzZeta (a : UnitAddCircle) (s : ℂ) := |
| 48 | + hurwitzZetaEven a s + hurwitzZetaOdd a s |
| 49 | + |
| 50 | +lemma hurwitzZetaEven_eq (a : UnitAddCircle) (s : ℂ) : |
| 51 | + hurwitzZetaEven a s = (hurwitzZeta a s + hurwitzZeta (-a) s) / 2 := by |
| 52 | + simp only [hurwitzZeta, hurwitzZetaEven_neg, hurwitzZetaOdd_neg] |
| 53 | + ring_nf |
| 54 | + |
| 55 | +lemma hurwitzZetaOdd_eq (a : UnitAddCircle) (s : ℂ) : |
| 56 | + hurwitzZetaOdd a s = (hurwitzZeta a s - hurwitzZeta (-a) s) / 2 := by |
| 57 | + simp only [hurwitzZeta, hurwitzZetaEven_neg, hurwitzZetaOdd_neg] |
| 58 | + ring_nf |
| 59 | + |
| 60 | +/-- The Hurwitz zeta function is differentiable away from `s = 1`. -/ |
| 61 | +lemma differentiableAt_hurwitzZeta (a : UnitAddCircle) {s : ℂ} (hs : s ≠ 1) : |
| 62 | + DifferentiableAt ℂ (hurwitzZeta a) s := |
| 63 | + (differentiableAt_hurwitzZetaEven a hs).add (differentiable_hurwitzZetaOdd a s) |
| 64 | + |
| 65 | +/-- Formula for `hurwitzZeta s` as a Dirichlet series in the convergence range. We |
| 66 | +restrict to `a ∈ Icc 0 1` to simplify the statement. -/ |
| 67 | +lemma hasSum_hurwitzZeta_of_one_lt_re {a : ℝ} (ha : a ∈ Icc 0 1) {s : ℂ} (hs : 1 < re s) : |
| 68 | + HasSum (fun n : ℕ ↦ 1 / (n + a : ℂ) ^ s) (hurwitzZeta a s) := by |
| 69 | + convert (hasSum_nat_hurwitzZetaEven_of_mem_Icc ha hs).add |
| 70 | + (hasSum_nat_hurwitzZetaOdd_of_mem_Icc ha hs) using 1 |
| 71 | + ext1 n |
| 72 | + -- plain `ring_nf` works here, but the following is faster: |
| 73 | + apply show ∀ (x y : ℂ), x = (x + y) / 2 + (x - y) / 2 by intros; ring |
| 74 | + |
| 75 | +/-- The residue of the Hurwitz zeta function at `s = 1` is `1`. -/ |
| 76 | +lemma hurwitzZeta_residue_one (a : UnitAddCircle) : |
| 77 | + Tendsto (fun s ↦ (s - 1) * hurwitzZeta a s) (𝓝[≠] 1) (𝓝 1) := by |
| 78 | + simp only [hurwitzZeta, mul_add, (by simp : 𝓝 (1 : ℂ) = 𝓝 (1 + (1 - 1) * hurwitzZetaOdd a 1))] |
| 79 | + refine (hurwitzZetaEven_residue_one a).add ((Tendsto.mul ?_ ?_).mono_left nhdsWithin_le_nhds) |
| 80 | + exacts [tendsto_id.sub_const _, (differentiable_hurwitzZetaOdd a).continuous.tendsto _] |
| 81 | + |
| 82 | +lemma differentiableAt_hurwitzZeta_sub_one_div (a : UnitAddCircle) : |
| 83 | + DifferentiableAt ℂ (fun s ↦ hurwitzZeta a s - 1 / (s - 1) / Gammaℝ s) 1 := by |
| 84 | + simp only [hurwitzZeta, add_sub_right_comm] |
| 85 | + exact (differentiableAt_hurwitzZetaEven_sub_one_div a).add (differentiable_hurwitzZetaOdd a 1) |
| 86 | + |
| 87 | +/-- Expression for `hurwitzZeta a 1` as a limit. (Mathematically `hurwitzZeta a 1` is |
| 88 | +undefined, but our construction assigns some value to it; this lemma is mostly of interest for |
| 89 | +determining what that value is). -/ |
| 90 | +lemma tendsto_hurwitzZeta_sub_one_div_nhds_one (a : UnitAddCircle) : |
| 91 | + Tendsto (fun s ↦ hurwitzZeta a s - 1 / (s - 1) / Gammaℝ s) (𝓝 1) (𝓝 (hurwitzZeta a 1)) := by |
| 92 | + simp only [hurwitzZeta, add_sub_right_comm] |
| 93 | + refine (tendsto_hurwitzZetaEven_sub_one_div_nhds_one a).add ?_ |
| 94 | + exact (differentiable_hurwitzZetaOdd a 1).continuousAt.tendsto |
| 95 | + |
| 96 | +/-- The difference of two Hurwitz zeta functions is differentiable everywhere. -/ |
| 97 | +lemma differentiable_hurwitzZeta_sub_hurwitzZeta (a b : UnitAddCircle) : |
| 98 | + Differentiable ℂ (fun s ↦ hurwitzZeta a s - hurwitzZeta b s) := by |
| 99 | + simp only [hurwitzZeta, add_sub_add_comm] |
| 100 | + refine (differentiable_hurwitzZetaEven_sub_hurwitzZetaEven a b).add (Differentiable.sub ?_ ?_) |
| 101 | + all_goals apply differentiable_hurwitzZetaOdd |
| 102 | + |
| 103 | +/-! |
| 104 | +## The exponential zeta function |
| 105 | +-/ |
| 106 | + |
| 107 | +/-- Meromorphic continuation of the series `∑' (n : ℕ), exp (2 * π * I * a * n) / n ^ s`. See |
| 108 | +`hasSum_expZeta_of_one_lt_re` for the relation to the Dirichlet series. -/ |
| 109 | +noncomputable def expZeta (a : UnitAddCircle) (s : ℂ) := |
| 110 | + cosZeta a s + I * sinZeta a s |
| 111 | + |
| 112 | +lemma cosZeta_eq (a : UnitAddCircle) (s : ℂ) : |
| 113 | + cosZeta a s = (expZeta a s + expZeta (-a) s) / 2 := by |
| 114 | + rw [expZeta, expZeta, cosZeta_neg, sinZeta_neg] |
| 115 | + ring_nf |
| 116 | + |
| 117 | +lemma sinZeta_eq (a : UnitAddCircle) (s : ℂ) : |
| 118 | + sinZeta a s = (expZeta a s - expZeta (-a) s) / (2 * I) := by |
| 119 | + rw [expZeta, expZeta, cosZeta_neg, sinZeta_neg] |
| 120 | + field_simp |
| 121 | + ring_nf |
| 122 | + |
| 123 | +lemma hasSum_expZeta_of_one_lt_re (a : ℝ) {s : ℂ} (hs : 1 < re s) : |
| 124 | + HasSum (fun n : ℕ ↦ cexp (2 * π * I * a * n) / n ^ s) (expZeta a s) := by |
| 125 | + convert (hasSum_nat_cosZeta a hs).add ((hasSum_nat_sinZeta a hs).mul_left I) using 1 |
| 126 | + ext1 n |
| 127 | + simp only [mul_right_comm _ I, ← cos_add_sin_I, push_cast] |
| 128 | + rw [add_div, mul_div, mul_comm _ I] |
| 129 | + |
| 130 | +lemma differentiableAt_expZeta (a : UnitAddCircle) (s : ℂ) (hs : s ≠ 1 ∨ a ≠ 0) : |
| 131 | + DifferentiableAt ℂ (expZeta a) s := by |
| 132 | + apply DifferentiableAt.add |
| 133 | + · exact differentiableAt_cosZeta a hs |
| 134 | + · apply (differentiableAt_const _).mul (differentiableAt_sinZeta a s) |
| 135 | + |
| 136 | +/-- If `a ≠ 0` then the exponential zeta function is analytic everywhere. -/ |
| 137 | +lemma differentiable_expZeta_of_ne_zero {a : UnitAddCircle} (ha : a ≠ 0) : |
| 138 | + Differentiable ℂ (expZeta a) := |
| 139 | + (differentiableAt_expZeta a · (Or.inr ha)) |
| 140 | + |
| 141 | +/-- Reformulation of `hasSum_expZeta_of_one_lt_re` using `LSeriesHasSum`. -/ |
| 142 | +lemma LSeriesHasSum_exp (a : ℝ) {s : ℂ} (hs : 1 < re s) : |
| 143 | + LSeriesHasSum (cexp <| 2 * π * I * a * ·) s (expZeta a s) := by |
| 144 | + refine (hasSum_expZeta_of_one_lt_re a hs).congr_fun (fun n ↦ ?_) |
| 145 | + rcases eq_or_ne n 0 with rfl | hn |
| 146 | + · rw [LSeries.term_zero, Nat.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs), div_zero] |
| 147 | + · apply LSeries.term_of_ne_zero hn |
| 148 | + |
| 149 | +/-! |
| 150 | +## The functional equation |
| 151 | +-/ |
| 152 | + |
| 153 | +lemma hurwitzZeta_one_sub (a : UnitAddCircle) {s : ℂ} |
| 154 | + (hs : ∀ (n : ℕ), s ≠ -n) (hs' : a ≠ 0 ∨ s ≠ 1) : |
| 155 | + hurwitzZeta a (1 - s) = (2 * π) ^ (-s) * Gamma s * |
| 156 | + (exp (-π * I * s / 2) * expZeta a s + exp (π * I * s / 2) * expZeta (-a) s) := by |
| 157 | + rw [hurwitzZeta, hurwitzZetaEven_one_sub a hs hs', hurwitzZetaOdd_one_sub a hs, |
| 158 | + expZeta, expZeta, Complex.cos, Complex.sin, sinZeta_neg, cosZeta_neg] |
| 159 | + rw [show ↑π * I * s / 2 = ↑π * s / 2 * I by ring, |
| 160 | + show -↑π * I * s / 2 = -(↑π * s / 2) * I by ring] |
| 161 | + -- these `generalize` commands are not strictly needed for the `ring_nf` call to succeed, but |
| 162 | + -- make it run faster: |
| 163 | + generalize (2 * π : ℂ) ^ (-s) = x |
| 164 | + generalize (↑π * s / 2 * I).exp = y |
| 165 | + generalize (-(↑π * s / 2) * I).exp = z |
| 166 | + ring_nf |
| 167 | + |
| 168 | +/-- Functional equation for the exponential zeta function. -/ |
| 169 | +lemma expZeta_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ 1 - n) : |
| 170 | + expZeta a (1 - s) = (2 * π) ^ (-s) * Gamma s * |
| 171 | + (exp (π * I * s / 2) * hurwitzZeta a s + exp (-π * I * s / 2) * hurwitzZeta (-a) s) := by |
| 172 | + have hs' (n : ℕ) : s ≠ -↑n := by |
| 173 | + convert hs (n + 1) using 1 |
| 174 | + push_cast |
| 175 | + ring |
| 176 | + rw [expZeta, cosZeta_one_sub a hs, sinZeta_one_sub a hs', hurwitzZeta, hurwitzZeta, |
| 177 | + hurwitzZetaEven_neg, hurwitzZetaOdd_neg, Complex.cos, Complex.sin] |
| 178 | + rw [show ↑π * I * s / 2 = ↑π * s / 2 * I by ring, |
| 179 | + show -↑π * I * s / 2 = -(↑π * s / 2) * I by ring] |
| 180 | + -- these `generalize` commands are not strictly needed for the `ring_nf` call to succeed, but |
| 181 | + -- make it run faster: |
| 182 | + generalize (2 * π : ℂ) ^ (-s) = x |
| 183 | + generalize (↑π * s / 2 * I).exp = y |
| 184 | + generalize (-(↑π * s / 2) * I).exp = z |
| 185 | + ring_nf |
| 186 | + rw [I_sq] |
| 187 | + ring_nf |
0 commit comments