(* File: Zeta_Function.thy Author: Manuel Eberl, TU München *) section ‹The Hurwitz and Riemann $\zeta$ functions› theory Zeta_Function imports "Euler_MacLaurin.Euler_MacLaurin" "Bernoulli.Bernoulli_Zeta" "Dirichlet_Series.Dirichlet_Series_Analysis" "Winding_Number_Eval.Winding_Number_Eval" "HOL-Real_Asymp.Real_Asymp" Zeta_Library "Pure-ex.Guess" begin subsection ‹Preliminary facts› (* TODO Move? *) lemma powr_add_minus_powr_asymptotics: fixes a z :: complex shows "((λz. ((1 + z) powr a - 1) / z) ⤏ a) (at 0)" proof (rule Lim_transform_eventually) have "eventually (λz::complex. z ∈ ball 0 1 - {0}) (at 0)" using eventually_at_ball'[of 1 "0::complex" UNIV] by (simp add: dist_norm) thus "eventually (λz. (∑n. (a gchoose (Suc n)) * z ^ n) = ((1 + z) powr a - 1) / z) (at 0)" proof eventually_elim case (elim z) hence "(λn. (a gchoose n) * z ^ n) sums (1 + z) powr a" by (intro gen_binomial_complex) auto hence "(λn. (a gchoose (Suc n)) * z ^ (Suc n)) sums ((1 + z) powr a - 1)" by (subst sums_Suc_iff) simp_all also have "(λn. (a gchoose (Suc n)) * z ^ (Suc n)) = (λn. z * ((a gchoose (Suc n)) * z ^ n))" by (simp add: algebra_simps) finally have "(λn. (a gchoose (Suc n)) * z ^ n) sums (((1 + z) powr a - 1) / z)" by (rule sums_mult_D) (use elim in auto) thus ?case by (simp add: sums_iff) qed next have "conv_radius (λn. a gchoose (n + 1)) = conv_radius (λn. a gchoose n)" using conv_radius_shift[of "λn. a gchoose n" 1] by simp hence "continuous_on (cball 0 (1/2)) (λz. ∑n. (a gchoose (Suc n)) * (z - 0) ^ n)" using conv_radius_gchoose[of a] by (intro powser_continuous_suminf) (simp_all) hence "isCont (λz. ∑n. (a gchoose (Suc n)) * z ^ n) 0" by (auto intro: continuous_on_interior) thus "(λz. ∑n. (a gchoose Suc n) * z ^ n) ─0→ a" by (auto simp: isCont_def) qed lemma complex_powr_add_minus_powr_asymptotics: fixes s :: complex assumes a: "a > 0" and s: "Re s < 1" shows "filterlim (λx. of_real (x + a) powr s - of_real x powr s) (nhds 0) at_top" proof (rule Lim_transform_eventually) show "eventually (λx. ((1 + of_real (a / x)) powr s - 1) / of_real (a / x) * of_real x powr (s - 1) * a = of_real (x + a) powr s - of_real x powr s) at_top" (is "eventually (λx. ?f x / ?g x * ?h x * _ = _) _") using eventually_gt_at_top[of a] proof eventually_elim case (elim x) have "?f x / ?g x * ?h x * a = ?f x * (a * ?h x / ?g x)" by simp also have "a * ?h x / ?g x = of_real x powr s" using elim a by (simp add: powr_diff) also have "?f x * … = of_real (x + a) powr s - of_real x powr s" using a elim by (simp add: algebra_simps powr_times_real [symmetric]) finally show ?case . qed have "filterlim (λx. complex_of_real (a / x)) (nhds (complex_of_real 0)) at_top" by (intro tendsto_of_real real_tendsto_divide_at_top[OF tendsto_const] filterlim_ident) hence "filterlim (λx. complex_of_real (a / x)) (at 0) at_top" using a by (intro filterlim_atI) auto hence "((λx. ?f x / ?g x * ?h x * a) ⤏ s * 0 * a) at_top" using s by (intro tendsto_mult filterlim_compose[OF powr_add_minus_powr_asymptotics] tendsto_const tendsto_neg_powr_complex_of_real filterlim_ident) auto thus "((λx. ?f x / ?g x * ?h x * a) ⤏ 0) at_top" by simp qed (* END TODO *) lemma summable_zeta: assumes "Re s > 1" shows "summable (λn. of_nat (Suc n) powr -s)" proof - have "summable (λn. exp (complex_of_real (ln (real (Suc n))) * - s))" (is "summable ?f") by (subst summable_Suc_iff, rule summable_complex_powr_iff) (use assms in auto) also have "?f = (λn. of_nat (Suc n) powr -s)" by (simp add: powr_def algebra_simps del: of_nat_Suc) finally show ?thesis . qed lemma summable_zeta_real: assumes "x > 1" shows "summable (λn. real (Suc n) powr -x)" proof - have "summable (λn. of_nat (Suc n) powr -complex_of_real x)" using assms by (intro summable_zeta) simp_all also have "(λn. of_nat (Suc n) powr -complex_of_real x) = (λn. of_real (real (Suc n) powr -x))" by (subst powr_Reals_eq) simp_all finally show ?thesis by (subst (asm) summable_complex_of_real) qed lemma summable_hurwitz_zeta: assumes "Re s > 1" "a > 0" shows "summable (λn. (of_nat n + of_real a) powr -s)" proof - have "summable (λn. (of_nat (Suc n) + of_real a) powr -s)" proof (rule summable_comparison_test' [OF summable_zeta_real [OF assms(1)]] ) fix n :: nat have "norm ((of_nat (Suc n) + of_real a) powr -s) = (real (Suc n) + a) powr - Re s" (is "?N = _") using assms by (simp add: norm_powr_real_powr) also have "… ≤ real (Suc n) powr -Re s" using assms by (intro powr_mono2') auto finally show "?N ≤ …" . qed thus ?thesis by (subst (asm) summable_Suc_iff) qed lemma summable_hurwitz_zeta_real: assumes "x > 1" "a > 0" shows "summable (λn. (real n + a) powr -x)" proof - have "summable (λn. (of_nat n + of_real a) powr -complex_of_real x)" using assms by (intro summable_hurwitz_zeta) simp_all also have "(λn. (of_nat n + of_real a) powr -complex_of_real x) = (λn. of_real ((real n + a) powr -x))" using assms by (subst powr_Reals_eq) simp_all finally show ?thesis by (subst (asm) summable_complex_of_real) qed subsection ‹Definitions› text ‹ We use the Euler--MacLaurin summation formula to express $\zeta(s,a) - \frac{a^{1-s}}{s-1}$ as a polynomial plus some remainder term, which is an integral over a function of order $O(-1-2n-\mathfrak{R}(s))$. It is then clear that this integral converges uniformly to an analytic function in $s$ for all $s$ with $\mathfrak{R}(s) > -2n$. › definition pre_zeta_aux :: "nat ⇒ real ⇒ complex ⇒ complex" where "pre_zeta_aux N a s = a powr - s / 2 + (∑i=1..N. (bernoulli (2 * i) / fact (2 * i)) *⇩_{R}(pochhammer s (2*i - 1) * of_real a powr (- s - of_nat (2*i - 1)))) + EM_remainder (Suc (2*N)) (λx. -(pochhammer s (Suc (2*N)) * of_real (x + a) powr (- 1 - 2*N - s))) 0" text ‹ By iterating the above construction long enough, we can extend this to the entire complex plane. › definition pre_zeta :: "real ⇒ complex ⇒ complex" where "pre_zeta a s = pre_zeta_aux (nat (1 - ⌈Re s / 2⌉)) a s" text ‹ We can then obtain the Hurwitz $\zeta$ function by adding back the pole at 1. Note that it is not necessary to trust that this somewhat complicated definition is, in fact, the correct one, since we will later show that this Hurwitz zeta function fulfils \[\zeta(s,a) = \sum_{n=0}^\infty \frac{1}{(n + a)^s}\] and is analytic on $\mathbb{C}\setminus \{1\}$, which uniquely defines the function due to analytic continuation. It is therefore obvious that any alternative definition that is analytic on $\mathbb{C}\setminus \{1\}$ and satisfies the above equation must be equal to our Hurwitz $\zeta$ function. › definition hurwitz_zeta :: "real ⇒ complex ⇒ complex" where "hurwitz_zeta a s = (if s = 1 then 0 else pre_zeta a s + of_real a powr (1 - s) / (s - 1))" text ‹ The Riemann $\zeta$ function is simply the Hurwitz $\zeta$ function with $a = 1$. › definition zeta :: "complex ⇒ complex" where "zeta = hurwitz_zeta 1" text ‹ We define the $\zeta$ functions as 0 at their poles. To avoid confusion, these facts are not added as simplification rules by default. › lemma hurwitz_zeta_1: "hurwitz_zeta c 1 = 0" by (simp add: hurwitz_zeta_def) lemma zeta_1: "zeta 1 = 0" by (simp add: zeta_def hurwitz_zeta_1) lemma zeta_minus_pole_eq: "s ≠ 1 ⟹ zeta s - 1 / (s - 1) = pre_zeta 1 s" by (simp add: zeta_def hurwitz_zeta_def) context begin private lemma holomorphic_pre_zeta_aux': assumes "a > 0" "bounded U" "open U" "U ⊆ {s. Re s > σ}" and σ: "σ > - 2 * real n" shows "pre_zeta_aux n a holomorphic_on U" unfolding pre_zeta_aux_def proof (intro holomorphic_intros) define C :: real where "C = max 0 (Sup ((λs. norm (pochhammer s (Suc (2 * n)))) ` closure U))" have "compact (closure U)" using assms by (auto simp: compact_eq_bounded_closed) hence "compact ((λs. norm (pochhammer s (Suc (2 * n)))) ` closure U)" by (rule compact_continuous_image [rotated]) (auto intro!: continuous_intros) hence "bounded ((λs. norm (pochhammer s (Suc (2 * n)))) ` closure U)" by (simp add: compact_eq_bounded_closed) hence C: "cmod (pochhammer s (Suc (2 * n))) ≤ C" if "s ∈ U" for s using that closure_subset[of U] unfolding C_def by (intro max.coboundedI2 cSup_upper bounded_imp_bdd_above) (auto simp: image_iff) have C' [simp]: "C ≥ 0" by (simp add: C_def) let ?g = "λ(x::real). C * (x + a) powr (- 1 - 2 * of_nat n - σ)" let ?G = "λ(x::real). C / (- 2 * of_nat n - σ) * (x + a) powr (- 2 * of_nat n - σ)" define poch' where "poch' = deriv (λz::complex. pochhammer z (Suc (2 * n)))" have [derivative_intros]: "((λz. pochhammer z (Suc (2 * n))) has_field_derivative poch' z) (at z within A)" for z :: complex and A unfolding poch'_def by (rule holomorphic_derivI [OF holomorphic_pochhammer [of _ UNIV]]) auto have A: "continuous_on A poch'" for A unfolding poch'_def by (rule continuous_on_subset[OF _ subset_UNIV], intro holomorphic_on_imp_continuous_on holomorphic_deriv) (auto intro: holomorphic_pochhammer) note [continuous_intros] = continuous_on_compose2[OF this _ subset_UNIV] define f' where "f' = (λz t. - (poch' z * complex_of_real (t + a) powr (- 1 - 2 * of_nat n - z) - Ln (complex_of_real (t + a)) * complex_of_real (t + a) powr (- 1 - 2 * of_nat n - z) * pochhammer z (Suc (2 * n))))" show "(λz. EM_remainder (Suc (2 * n)) (λx. - (pochhammer z (Suc (2 * n)) * complex_of_real (x + a) powr (- 1 - 2 * of_nat n - z))) 0) holomorphic_on U" unfolding pre_zeta_aux_def proof (rule holomorphic_EM_remainder[of _ ?G ?g _ _ f'], goal_cases) case (1 x) show ?case by (insert 1 σ ‹a > 0›, rule derivative_eq_intros refl | simp)+ (auto simp: field_simps powr_diff powr_add powr_minus) next case (2 z t x) note [derivative_intros] = has_field_derivative_powr_right [THEN DERIV_chain2] show ?case by (insert 2 σ ‹a > 0›, (rule derivative_eq_intros refl | (simp add: add_eq_0_iff; fail))+) (simp add: f'_def) next case 3 hence *: "complex_of_real x + complex_of_real a ∉ ℝ⇩_{≤}⇩_{0}" if "x ≥ 0" for x using nonpos_Reals_of_real_iff[of "x+a", unfolded of_real_add] that ‹a > 0› by auto show ?case using ‹a > 0› and * unfolding f'_def by (auto simp: case_prod_unfold add_eq_0_iff intro!: continuous_intros) next case (4 b c z e) have "- 2 * real n < σ" by (fact σ) also from 4 assms have "σ < Re z" by auto finally show ?case using assms 4 by (intro integrable_continuous_real continuous_intros) (auto simp: add_eq_0_iff) next case (5 t x s) thus ?case using ‹a > 0› by (intro integrable_EM_remainder') (auto intro!: continuous_intros simp: add_eq_0_iff) next case 6 from σ have "(λy. C / (-2 * real n - σ) * (a + y) powr (-2 * real n - σ)) ⇢ 0" by (intro tendsto_mult_right_zero tendsto_neg_powr filterlim_real_sequentially filterlim_tendsto_add_at_top [OF tendsto_const]) auto thus ?case unfolding convergent_def by (auto simp: add_ac) next case 7 show ?case proof (intro eventually_mono [OF eventually_ge_at_top[of 1]] ballI) fix x :: real and s :: complex assume x: "x ≥ 1" and s: "s ∈ U" have "norm (- (pochhammer s (Suc (2 * n)) * of_real (x + a) powr (- 1 - 2 * of_nat n - s))) = norm (pochhammer s (Suc (2 * n))) * (x + a) powr (-1 - 2 * of_nat n - Re s)" (is "?N = _") using 7 ‹a > 0› x by (simp add: norm_mult norm_powr_real_powr) also have "… ≤ ?g x" using 7 assms x s ‹a > 0› by (intro mult_mono C powr_mono) auto finally show "?N ≤ ?g x" . qed qed (insert assms, auto) qed (insert assms, auto) lemma analytic_pre_zeta_aux: assumes "a > 0" shows "pre_zeta_aux n a analytic_on {s. Re s > - 2 * real n}" unfolding analytic_on_def proof fix s assume s: "s ∈ {s. Re s > - 2 * real n}" define σ where "σ = (Re s - 2 * real n) / 2" with s have σ: "σ > - 2 * real n" by (simp add: σ_def field_simps) from s have s': "s ∈ {s. Re s > σ}" by (auto simp: σ_def field_simps) have "open {s. Re s > σ}" by (rule open_halfspace_Re_gt) with s' obtain ε where "ε > 0" "ball s ε ⊆ {s. Re s > σ}" unfolding open_contains_ball by blast with σ have "pre_zeta_aux n a holomorphic_on ball s ε" by (intro holomorphic_pre_zeta_aux' [OF assms, of _ σ]) auto with ‹ε > 0› show "∃e>0. pre_zeta_aux n a holomorphic_on ball s e" by blast qed end context fixes s :: complex and N :: nat and ζ :: "complex ⇒ complex" and a :: real assumes s: "Re s > 1" and a: "a > 0" defines "ζ ≡ (λs. ∑n. (of_nat n + of_real a) powr -s)" begin interpretation ζ: euler_maclaurin_nat' "λx. of_real (x + a) powr (1 - s) / (1 - s)" "λx. of_real (x + a) powr -s" "λn x. (-1) ^ n * pochhammer s n * of_real (x + a) powr -(s + n)" 0 N "ζ s" "{}" proof (standard, goal_cases) case 2 show ?case by (simp add: powr_minus field_simps) next case (3 k) have "complex_of_real x + complex_of_real a = 0 ⟷ x = -a" for x by (simp only: of_real_add [symmetric] of_real_eq_0_iff add_eq_0_iff2) with a s show ?case by (intro continuous_intros) (auto simp: add_nonneg_nonneg) next case (4 k x) with a have "0 < x + a" by simp hence *: "complex_of_real x + complex_of_real a ∉ ℝ⇩_{≤}⇩_{0}" using nonpos_Reals_of_real_iff[of "x+a", unfolded of_real_add] by auto have **: "pochhammer z (Suc n) = - pochhammer z n * (-z - of_nat n :: complex)" for z n by (simp add: pochhammer_rec' field_simps) show "((λx. (- 1) ^ k * pochhammer s k * of_real (x + a) powr - (s + of_nat k)) has_vector_derivative (- 1) ^ Suc k * pochhammer s (Suc k) * of_real (x + a) powr - (s + of_nat (Suc k))) (at x)" by (insert 4 *, (rule has_vector_derivative_real_field derivative_eq_intros refl | simp)+) (auto simp: divide_simps powr_add powr_diff powr_minus **) next case 5 with s a show ?case by (auto intro!: continuous_intros simp: minus_equation_iff add_eq_0_iff) next case (6 x) with a have "0 < x + a" by simp hence *: "complex_of_real x + complex_of_real a ∉ ℝ⇩_{≤}⇩_{0}" using nonpos_Reals_of_real_iff[of "x+a", unfolded of_real_add] by auto show ?case unfolding of_real_add by (insert 6 s *, (rule has_vector_derivative_real_field derivative_eq_intros refl | force simp add: minus_equation_iff)+) next case 7 from s a have "(λk. (of_nat k + of_real a) powr -s) sums ζ s" unfolding ζ_def by (intro summable_sums summable_hurwitz_zeta) auto hence 1: "(λb. (∑k=0..b. (of_nat k + of_real a) powr -s)) ⇢ ζ s" by (simp add: sums_def') { fix z assume "Re z < 0" hence "((λb. (a + real b) powr Re z) ⤏ 0) at_top" by (intro tendsto_neg_powr filterlim_tendsto_add_at_top filterlim_real_sequentially) auto also have "(λb. (a + real b) powr Re z) = (λb. norm ((of_nat b + a) powr z))" using a by (subst norm_powr_real_powr) (auto simp: add_ac) finally have "((λb. (of_nat b + a) powr z) ⤏ 0) at_top" by (subst (asm) tendsto_norm_zero_iff) simp } note * = this have "(λb. (of_nat b + a) powr (1 - s) / (1 - s)) ⇢ 0 / (1 - s)" using s by (intro tendsto_divide tendsto_const *) auto hence 2: "(λb. (of_nat b + a) powr (1 - s) / (1 - s)) ⇢ 0" by simp have "(λb. (∑i<2 * N + 1. (bernoulli' (Suc i) / fact (Suc i)) *⇩_{R}((- 1) ^ i * pochhammer s i * (of_nat b + a) powr -(s + of_nat i)))) ⇢ (∑i<2 * N + 1. (bernoulli' (Suc i) / fact (Suc i)) *⇩_{R}((- 1) ^ i * pochhammer s i * 0))" using s by (intro tendsto_intros *) auto hence 3: "(λb. (∑i<2 * N + 1. (bernoulli' (Suc i) / fact (Suc i)) *⇩_{R}((- 1) ^ i * pochhammer s i * (of_nat b + a) powr -(s + of_nat i)))) ⇢ 0" by simp from tendsto_diff[OF tendsto_diff[OF 1 2] 3] show ?case by simp qed simp_all text ‹ The pre-$\zeta$ functions agree with the infinite sum that is used to define the $\zeta$ function for $\mathfrak{R}(s)>1$. › lemma pre_zeta_aux_conv_zeta: "pre_zeta_aux N a s = ζ s + a powr (1 - s) / (1 - s)" proof - let ?R = "(∑i=1..N. ((bernoulli (2*i) / fact (2*i)) *⇩_{R}pochhammer s (2*i - 1) * of_real a powr (-s - (2*i-1))))" let ?S = "EM_remainder (Suc (2 * N)) (λx. - (pochhammer s (Suc (2*N)) * of_real (x + a) powr (- 1 - 2 * of_nat N - s))) 0" from ζ.euler_maclaurin_strong_nat'[OF le_refl, simplified] have "of_real a powr -s = a powr (1 - s) / (1 - s) + ζ s + a powr -s / 2 + (-?R) - ?S" unfolding sum_negf [symmetric] by (simp add: scaleR_conv_of_real pre_zeta_aux_def mult_ac) thus ?thesis unfolding pre_zeta_aux_def (* TODO: Field_as_Ring causes some problems with field_simps vs. div_mult_self *) by (simp add: field_simps del: div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1) qed end text ‹ Since all of the partial pre-$\zeta$ functions are analytic and agree in the halfspace with $\mathfrak R(s)>0$, they must agree in their entire domain. › lemma pre_zeta_aux_eq: assumes "m ≤ n" "a > 0" "Re s > -2 * real m" shows "pre_zeta_aux m a s = pre_zeta_aux n a s" proof - have "pre_zeta_aux n a s - pre_zeta_aux m a s = 0" proof (rule analytic_continuation[of "λs. pre_zeta_aux n a s - pre_zeta_aux m a s"]) show "(λs. pre_zeta_aux n a s - pre_zeta_aux m a s) holomorphic_on {s. Re s > -2 * real m}" using assms by (intro holomorphic_intros analytic_imp_holomorphic analytic_on_subset[OF analytic_pre_zeta_aux]) auto next fix s assume "s ∈ {s. Re s > 1}" with ‹a > 0› show "pre_zeta_aux n a s - pre_zeta_aux m a s = 0" by (simp add: pre_zeta_aux_conv_zeta) next have "2 ∈ {s. Re s > 1}" by simp also have "… = interior …" by (intro interior_open [symmetric] open_halfspace_Re_gt) finally show "2 islimpt {s. Re s > 1}" by (rule interior_limit_point) next show "connected {s. Re s > -2 * real m}" using convex_halfspace_gt[of "-2 * real m" "1::complex"] by (intro convex_connected) auto qed (insert assms, auto simp: open_halfspace_Re_gt) thus ?thesis by simp qed lemma pre_zeta_aux_eq': assumes "a > 0" "Re s > -2 * real m" "Re s > -2 * real n" shows "pre_zeta_aux m a s = pre_zeta_aux n a s" proof (cases m n rule: linorder_cases) case less with assms show ?thesis by (intro pre_zeta_aux_eq) auto next case greater with assms show ?thesis by (subst eq_commute, intro pre_zeta_aux_eq) auto qed auto lemma pre_zeta_aux_eq_pre_zeta: assumes "Re s > -2 * real n" and "a > 0" shows "pre_zeta_aux n a s = pre_zeta a s" unfolding pre_zeta_def proof (intro pre_zeta_aux_eq') from assms show "- 2 * real (nat (1 - ⌈Re s / 2⌉)) < Re s" by linarith qed (insert assms, simp_all) text ‹ This means that the idea of iterating that construction infinitely does yield a well-defined entire function. › lemma analytic_pre_zeta: assumes "a > 0" shows "pre_zeta a analytic_on A" unfolding analytic_on_def proof fix s assume "s ∈ A" let ?B = "{s'. Re s' > of_int ⌊Re s⌋ - 1}" have s: "s ∈ ?B" by simp linarith? moreover have "open ?B" by (rule open_halfspace_Re_gt) ultimately obtain ε where ε: "ε > 0" "ball s ε ⊆ ?B" unfolding open_contains_ball by blast define C where "C = ball s ε" note analytic = analytic_on_subset[OF analytic_pre_zeta_aux] have "pre_zeta_aux (nat ⌈- Re s⌉ + 2) a holomorphic_on C" proof (intro analytic_imp_holomorphic analytic subsetI assms, goal_cases) case (1 w) with ε have "w ∈ ?B" by (auto simp: C_def) thus ?case by (auto simp: ceiling_minus) qed also have "?this ⟷ pre_zeta a holomorphic_on C" proof (intro holomorphic_cong refl pre_zeta_aux_eq_pre_zeta assms) fix w assume "w ∈ C" with ε have w: "w ∈ ?B" by (auto simp: C_def) thus " - 2 * real (nat ⌈- Re s⌉ + 2) < Re w" by (simp add: ceiling_minus) qed finally show "∃e>0. pre_zeta a holomorphic_on ball s e" using ‹ε > 0› unfolding C_def by blast qed lemma holomorphic_pre_zeta [holomorphic_intros]: "f holomorphic_on A ⟹ a > 0 ⟹ (λz. pre_zeta a (f z)) holomorphic_on A" using holomorphic_on_compose [OF _ analytic_imp_holomorphic [OF analytic_pre_zeta], of f] by (simp add: o_def) corollary continuous_on_pre_zeta: "a > 0 ⟹ continuous_on A (pre_zeta a)" by (intro holomorphic_on_imp_continuous_on holomorphic_intros) auto corollary continuous_on_pre_zeta' [continuous_intros]: "continuous_on A f ⟹ a > 0 ⟹ continuous_on A (λx. pre_zeta a (f x))" using continuous_on_compose2 [OF continuous_on_pre_zeta, of a A f "f ` A"] by (auto simp: image_iff) corollary continuous_pre_zeta [continuous_intros]: "a > 0 ⟹ continuous (at s within A) (pre_zeta a)" by (rule continuous_within_subset[of _ UNIV]) (insert continuous_on_pre_zeta[of a UNIV], auto simp: continuous_on_eq_continuous_at open_Compl) corollary continuous_pre_zeta' [continuous_intros]: "a > 0 ⟹ continuous (at s within A) f ⟹ continuous (at s within A) (λs. pre_zeta a (f s))" using continuous_within_compose3[OF continuous_pre_zeta, of a s A f] by auto text ‹ It is now obvious that $\zeta$ is holomorphic everywhere except 1, where it has a simple pole with residue 1, which we can simply read off. › theorem holomorphic_hurwitz_zeta: assumes "a > 0" "1 ∉ A" shows "hurwitz_zeta a holomorphic_on A" proof - have "(λs. pre_zeta a s + complex_of_real a powr (1 - s) / (s - 1)) holomorphic_on A" using assms by (auto intro!: holomorphic_intros) also from assms have "?this ⟷ ?thesis" by (intro holomorphic_cong) (auto simp: hurwitz_zeta_def) finally show ?thesis . qed corollary holomorphic_hurwitz_zeta' [holomorphic_intros]: assumes "f holomorphic_on A" and "a > 0" and "⋀z. z ∈ A ⟹ f z ≠ 1" shows "(λx. hurwitz_zeta a (f x)) holomorphic_on A" proof - have "hurwitz_zeta a ∘ f holomorphic_on A" using assms by (intro holomorphic_on_compose_gen[of _ _ _ "f ` A"] holomorphic_hurwitz_zeta assms) auto thus ?thesis by (simp add: o_def) qed theorem holomorphic_zeta: "1 ∉ A⟹ zeta holomorphic_on A" unfolding zeta_def by (auto intro: holomorphic_intros) corollary holomorphic_zeta' [holomorphic_intros]: assumes "f holomorphic_on A" and "⋀z. z ∈ A ⟹ f z ≠ 1" shows "(λx. zeta (f x)) holomorphic_on A" using assms unfolding zeta_def by (auto intro: holomorphic_intros) corollary analytic_hurwitz_zeta: assumes "a > 0" "1 ∉ A" shows "hurwitz_zeta a analytic_on A" proof - from assms(1) have "hurwitz_zeta a holomorphic_on -{1}" by (rule holomorphic_hurwitz_zeta) auto also have "?this ⟷ hurwitz_zeta a analytic_on -{1}" by (intro analytic_on_open [symmetric]) auto finally show ?thesis by (rule analytic_on_subset) (insert assms, auto) qed corollary analytic_zeta: "1 ∉ A ⟹ zeta analytic_on A" unfolding zeta_def by (rule analytic_hurwitz_zeta) auto corollary continuous_on_hurwitz_zeta: "a > 0 ⟹ 1 ∉ A ⟹ continuous_on A (hurwitz_zeta a)" by (intro holomorphic_on_imp_continuous_on holomorphic_intros) auto corollary continuous_on_hurwitz_zeta' [continuous_intros]: "continuous_on A f ⟹ a > 0 ⟹ (⋀x. x ∈ A ⟹ f x ≠ 1) ⟹ continuous_on A (λx. hurwitz_zeta a (f x))" using continuous_on_compose2 [OF continuous_on_hurwitz_zeta, of a "f ` A" A f] by (auto simp: image_iff) corollary continuous_on_zeta: "1 ∉ A ⟹ continuous_on A zeta" by (intro holomorphic_on_imp_continuous_on holomorphic_intros) auto corollary continuous_on_zeta' [continuous_intros]: "continuous_on A f ⟹ (⋀x. x ∈ A ⟹ f x ≠ 1) ⟹ continuous_on A (λx. zeta (f x))" using continuous_on_compose2 [OF continuous_on_zeta, of "f ` A" A f] by (auto simp: image_iff) corollary continuous_hurwitz_zeta [continuous_intros]: "a > 0 ⟹ s ≠ 1 ⟹ continuous (at s within A) (hurwitz_zeta a)" by (rule continuous_within_subset[of _ UNIV]) (insert continuous_on_hurwitz_zeta[of a "-{1}"], auto simp: continuous_on_eq_continuous_at open_Compl) corollary continuous_hurwitz_zeta' [continuous_intros]: "a > 0 ⟹ f s ≠ 1 ⟹ continuous (at s within A) f ⟹ continuous (at s within A) (λs. hurwitz_zeta a (f s))" using continuous_within_compose3[OF continuous_hurwitz_zeta, of a f s A] by auto corollary continuous_zeta [continuous_intros]: "s ≠ 1 ⟹ continuous (at s within A) zeta" unfolding zeta_def by (intro continuous_intros) auto corollary continuous_zeta' [continuous_intros]: "f s ≠ 1 ⟹ continuous (at s within A) f ⟹ continuous (at s within A) (λs. zeta (f s))" unfolding zeta_def by (intro continuous_intros) auto corollary field_differentiable_at_zeta: assumes "s ≠ 1" shows "zeta field_differentiable at s" proof - have "zeta holomorphic_on (- {1})" using holomorphic_zeta by force moreover have "open (-{1} :: complex set)" by (intro open_Compl) auto ultimately show ?thesis using assms by (auto simp add: holomorphic_on_open open_halfspace_Re_gt open_Diff field_differentiable_def) qed theorem is_pole_hurwitz_zeta: assumes "a > 0" shows "is_pole (hurwitz_zeta a) 1" proof - from assms have "continuous_on UNIV (pre_zeta a)" by (intro holomorphic_on_imp_continuous_on analytic_imp_holomorphic analytic_pre_zeta) hence "isCont (pre_zeta a) 1" by (auto simp: continuous_on_eq_continuous_at) hence *: "pre_zeta a ─1→ pre_zeta a 1" by (simp add: isCont_def) from assms have "isCont (λs. complex_of_real a powr (1 - s)) 1" by (intro isCont_powr_complex) auto with assms have **: "(λs. complex_of_real a powr (1 - s)) ─1→ 1" by (simp add: isCont_def) have "(λs::complex. s - 1) ─1→ 1 - 1" by (intro tendsto_intros) hence "filterlim (λs::complex. s - 1) (at 0) (at 1)" by (auto simp: filterlim_at eventually_at_filter) hence ***: "filterlim (λs :: complex. a powr (1 - s) / (s - 1)) at_infinity (at 1)" by (intro filterlim_divide_at_infinity [OF **]) auto have "is_pole (λs. pre_zeta a s + complex_of_real a powr (1 - s) / (s - 1)) 1" unfolding is_pole_def hurwitz_zeta_def by (rule tendsto_add_filterlim_at_infinity * ***)+ also have "?this ⟷ ?thesis" unfolding is_pole_def by (intro filterlim_cong refl) (auto simp: eventually_at_filter hurwitz_zeta_def) finally show ?thesis . qed corollary is_pole_zeta: "is_pole zeta 1" by (simp add: is_pole_hurwitz_zeta zeta_def) theorem zorder_hurwitz_zeta: assumes "a > 0" shows "zorder (hurwitz_zeta a) 1 = -1" proof (rule zorder_eqI[of UNIV]) fix w :: complex assume "w ≠ 1" thus "hurwitz_zeta a w = (pre_zeta a w * (w - 1) + a powr (1 - w)) * (w - 1) powi -1" by (auto simp add: hurwitz_zeta_def field_simps) qed (use assms in ‹auto intro!: holomorphic_intros›) corollary zorder_zeta: "zorder zeta 1 = - 1" unfolding zeta_def by (rule zorder_hurwitz_zeta) auto theorem residue_hurwitz_zeta: assumes "a > 0" shows "residue (hurwitz_zeta a) 1 = 1" proof - note holo = analytic_imp_holomorphic[OF analytic_pre_zeta] have "residue (hurwitz_zeta a) 1 = residue (λz. pre_zeta a z + a powr (1 - z) / (z - 1)) 1" by (intro residue_cong) (auto simp: eventually_at_filter hurwitz_zeta_def) also have "… = residue (λz. a powr (1 - z) / (z - 1)) 1" using assms by (subst residue_add [of UNIV]) (auto intro!: holomorphic_intros holo intro: residue_holo[of UNIV, OF _ _ holo]) also have "… = complex_of_real a powr (1 - 1)" using assms by (intro residue_simple [of UNIV]) (auto intro!: holomorphic_intros) also from assms have "… = 1" by simp finally show ?thesis . qed corollary residue_zeta: "residue zeta 1 = 1" unfolding zeta_def by (rule residue_hurwitz_zeta) auto lemma zeta_bigo_at_1: "zeta ∈ O[at 1 within A](λx. 1 / (x - 1))" proof - have "zeta ∈ Θ[at 1 within A](λs. pre_zeta 1 s + 1 / (s - 1))" by (intro bigthetaI_cong) (auto simp: eventually_at_filter zeta_def hurwitz_zeta_def) also have "(λs. pre_zeta 1 s + 1 / (s - 1)) ∈ O[at 1 within A](λs. 1 / (s - 1))" proof (rule sum_in_bigo) have "continuous_on UNIV (pre_zeta 1)" by (intro holomorphic_on_imp_continuous_on holomorphic_intros) auto hence "isCont (pre_zeta 1) 1" by (auto simp: continuous_on_eq_continuous_at) hence "continuous (at 1 within A) (pre_zeta 1)" by (rule continuous_within_subset) auto hence "pre_zeta 1 ∈ O[at 1 within A](λ_. 1)" by (intro continuous_imp_bigo_1) auto also have ev: "eventually (λs. s ∈ ball 1 1 ∧ s ≠ 1 ∧ s ∈ A) (at 1 within A)" by (intro eventually_at_ball') auto have "(λ_. 1) ∈ O[at 1 within A](λs. 1 / (s - 1))" by (intro landau_o.bigI[of 1] eventually_mono[OF ev]) (auto simp: eventually_at_filter norm_divide dist_norm norm_minus_commute field_simps) finally show "pre_zeta 1 ∈ O[at 1 within A](λs. 1 / (s - 1))" . qed simp_all finally show ?thesis . qed theorem assumes "a > 0" "Re s > 1" shows hurwitz_zeta_conv_suminf: "hurwitz_zeta a s = (∑n. (of_nat n + of_real a) powr -s)" and sums_hurwitz_zeta: "(λn. (of_nat n + of_real a) powr -s) sums hurwitz_zeta a s" proof - from assms have [simp]: "s ≠ 1" by auto from assms have "hurwitz_zeta a s = pre_zeta_aux 0 a s + of_real a powr (1 - s) / (s - 1)" by (simp add: hurwitz_zeta_def pre_zeta_def) also from assms have "pre_zeta_aux 0 a s = (∑n. (of_nat n + of_real a) powr -s) + of_real a powr (1 - s) / (1 - s)" by (intro pre_zeta_aux_conv_zeta) also have "… + a powr (1 - s) / (s - 1) = (∑n. (of_nat n + of_real a) powr -s) + a powr (1 - s) * (1 / (1 - s) + 1 / (s - 1))" by (simp add: algebra_simps) also have "1 / (1 - s) + 1 / (s - 1) = 0" by (simp add: divide_simps) finally show "hurwitz_zeta a s = (∑n. (of_nat n + of_real a) powr -s)" by simp moreover have "(λn. (of_nat n + of_real a) powr -s) sums (∑n. (of_nat n + of_real a) powr -s)" by (intro summable_sums summable_hurwitz_zeta assms) ultimately show "(λn. (of_nat n + of_real a) powr -s) sums hurwitz_zeta a s" by simp qed corollary assumes "Re s > 1" shows zeta_conv_suminf: "zeta s = (∑n. of_nat (Suc n) powr -s)" and sums_zeta: "(λn. of_nat (Suc n) powr -s) sums zeta s" using hurwitz_zeta_conv_suminf[of 1 s] sums_hurwitz_zeta[of 1 s] assms by (simp_all add: zeta_def add_ac) corollary assumes "n > 1" shows zeta_nat_conv_suminf: "zeta (of_nat n) = (∑k. 1 / of_nat (Suc k) ^ n)" and sums_zeta_nat: "(λk. 1 / of_nat (Suc k) ^ n) sums zeta (of_nat n)" proof - have "(λk. of_nat (Suc k) powr -of_nat n) sums zeta (of_nat n)" using assms by (intro sums_zeta) auto also have "(λk. of_nat (Suc k) powr -of_nat n) = (λk. 1 / of_nat (Suc k) ^ n :: complex)" by (simp add: powr_minus divide_simps del: of_nat_Suc) finally show "(λk. 1 / of_nat (Suc k) ^ n) sums zeta (of_nat n)" . thus "zeta (of_nat n) = (∑k. 1 / of_nat (Suc k) ^ n)" by (simp add: sums_iff) qed lemma pre_zeta_aux_cnj [simp]: assumes "a > 0" shows "pre_zeta_aux n a (cnj z) = cnj (pre_zeta_aux n a z)" proof - have "cnj (pre_zeta_aux n a z) = of_real a powr -cnj z / 2 + (∑x=1..n. (bernoulli (2 * x) / fact (2 * x)) *⇩_{R}a powr (-cnj z - (2*x-1)) * pochhammer (cnj z) (2*x-1)) + EM_remainder (2*n+1) (λx. -(pochhammer (cnj z) (Suc (2 * n)) * cnj (of_real (x + a) powr (-1 - 2 * of_nat n - z)))) 0" (is "_ = _ + ?A + ?B") unfolding pre_zeta_aux_def complex_cnj_add using assms by (subst EM_remainder_cnj [symmetric]) (auto intro!: continuous_intros simp: cnj_powr add_eq_0_iff mult_ac) also have "?B = EM_remainder (2*n+1) (λx. -(pochhammer (cnj z) (Suc (2 * n)) * of_real (x + a) powr (-1 - 2 * of_nat n - cnj z))) 0" using assms by (intro EM_remainder_cong) (auto simp: cnj_powr) also have "of_real a powr -cnj z / 2 + ?A + … = pre_zeta_aux n a (cnj z)" by (simp add: pre_zeta_aux_def mult_ac) finally show ?thesis .. qed lemma pre_zeta_cnj [simp]: "a > 0 ⟹ pre_zeta a (cnj z) = cnj (pre_zeta a z)" by (simp add: pre_zeta_def) lemma hurwitz_zeta_cnj [simp]: "a > 0 ⟹ hurwitz_zeta a (cnj z) = cnj (hurwitz_zeta a z)" proof - assume "a > 0" moreover have "cnj z = 1 ⟷ z = 1" by (simp add: complex_eq_iff) ultimately show ?thesis by (auto simp: hurwitz_zeta_def cnj_powr) qed lemma zeta_cnj [simp]: "zeta (cnj z) = cnj (zeta z)" by (simp add: zeta_def) corollary hurwitz_zeta_real: "a > 0 ⟹ hurwitz_zeta a (of_real x) ∈ ℝ" using hurwitz_zeta_cnj [of a "of_real x"] by (simp add: Reals_cnj_iff del: zeta_cnj) corollary zeta_real: "zeta (of_real x) ∈ ℝ" unfolding zeta_def by (rule hurwitz_zeta_real) auto corollary zeta_real': "z ∈ ℝ ⟹ zeta z ∈ ℝ" by (elim Reals_cases) (auto simp: zeta_real) subsection ‹Connection to Dirichlet series› lemma eval_fds_zeta: "Re s > 1 ⟹ eval_fds fds_zeta s = zeta s" using sums_zeta [of s] by (intro eval_fds_eqI) (auto simp: powr_minus divide_simps) theorem euler_product_zeta: assumes "Re s > 1" shows "(λn. ∏p≤n. if prime p then inverse (1 - 1 / of_nat p powr s) else 1) ⇢ zeta s" using euler_product_fds_zeta[of s] assms unfolding nat_power_complex_def by (simp add: eval_fds_zeta) corollary euler_product_zeta': assumes "Re s > 1" shows "(λn. ∏p | prime p ∧ p ≤ n. inverse (1 - 1 / of_nat p powr s)) ⇢ zeta s" proof - note euler_product_zeta [OF assms] also have "(λn. ∏p≤n. if prime p then inverse (1 - 1 / of_nat p powr s) else 1) = (λn. ∏p | prime p ∧ p ≤ n. inverse (1 - 1 / of_nat p powr s))" by (intro ext prod.mono_neutral_cong_right refl) auto finally show ?thesis . qed theorem zeta_Re_gt_1_nonzero: "Re s > 1 ⟹ zeta s ≠ 0" using eval_fds_zeta_nonzero[of s] by (simp add: eval_fds_zeta) theorem tendsto_zeta_Re_going_to_at_top: "(zeta ⤏ 1) (Re going_to at_top)" proof (rule Lim_transform_eventually) have "eventually (λx::real. x > 1) at_top" by (rule eventually_gt_at_top) hence "eventually (λs. Re s > 1) (Re going_to at_top)" by blast thus "eventually (λz. eval_fds fds_zeta z = zeta z) (Re going_to at_top)" by eventually_elim (simp add: eval_fds_zeta) next have "conv_abscissa (fds_zeta :: complex fds) ≤ 1" proof (rule conv_abscissa_leI) fix c' assume "ereal c' > 1" thus "∃s. s ∙ 1 = c' ∧ fds_converges fds_zeta (s::complex)" by (auto intro!: exI[of _ "of_real c'"]) qed hence "(eval_fds fds_zeta ⤏ fds_nth fds_zeta 1) (Re going_to at_top)" by (intro tendsto_eval_fds_Re_going_to_at_top') auto thus "(eval_fds fds_zeta ⤏ 1) (Re going_to at_top)" by simp qed lemma conv_abscissa_zeta [simp]: "conv_abscissa (fds_zeta :: complex fds) = 1" and abs_conv_abscissa_zeta [simp]: "abs_conv_abscissa (fds_zeta :: complex fds) = 1" proof - let ?z = "fds_zeta :: complex fds" have A: "conv_abscissa ?z ≥ 1" proof (intro conv_abscissa_geI) fix c' assume "ereal c' < 1" hence "¬summable (λn. real n powr -c')" by (subst summable_real_powr_iff) auto hence "¬summable (λn. of_real (real n powr -c') :: complex)" by (subst summable_of_real_iff) also have "summable (λn. of_real (real n powr -c') :: complex) ⟷ fds_converges fds_zeta (of_real c' :: complex)" unfolding fds_converges_def by (intro summable_cong eventually_mono [OF eventually_gt_at_top[of 0]]) (simp add: fds_nth_zeta powr_Reals_eq powr_minus divide_simps) finally show "∃s::complex. s ∙ 1 = c' ∧ ¬fds_converges fds_zeta s" by (intro exI[of _ "of_real c'"]) auto qed have B: "abs_conv_abscissa ?z ≤ 1" proof (intro abs_conv_abscissa_leI) fix c' assume "1 < ereal c'" thus "∃s::complex. s ∙ 1 = c' ∧ fds_abs_converges fds_zeta s" by (intro exI[of _ "of_real c'"]) auto qed have "conv_abscissa ?z ≤ abs_conv_abscissa ?z" by (rule conv_le_abs_conv_abscissa) also note B finally show "conv_abscissa ?z = 1" using A by (intro antisym) note A also have "conv_abscissa ?z ≤ abs_conv_abscissa ?z" by (rule conv_le_abs_conv_abscissa) finally show "abs_conv_abscissa ?z = 1" using B by (intro antisym) qed theorem deriv_zeta_sums: assumes s: "Re s > 1" shows "(λn. -of_real (ln (real (Suc n))) / of_nat (Suc n) powr s) sums deriv zeta s" proof - from s have "fds_converges (fds_deriv fds_zeta) s" by (intro fds_converges_deriv) simp_all with s have "(λn. -of_real (ln (real (Suc n))) / of_nat (Suc n) powr s) sums deriv (eval_fds fds_zeta) s" unfolding fds_converges_altdef by (simp add: fds_nth_deriv scaleR_conv_of_real eval_fds_deriv eval_fds_zeta) also from s have "eventually (λs. s ∈ {s. Re s > 1}) (nhds s)" by (intro eventually_nhds_in_open) (auto simp: open_halfspace_Re_gt) hence "eventually (λs. eval_fds fds_zeta s = zeta s) (nhds s)" by eventually_elim (auto simp: eval_fds_zeta) hence "deriv (eval_fds fds_zeta) s = deriv zeta s" by (intro deriv_cong_ev refl) finally show ?thesis . qed theorem inverse_zeta_sums: assumes s: "Re s > 1" shows "(λn. moebius_mu (Suc n) / of_nat (Suc n) powr s) sums inverse (zeta s)" proof - have "fds_converges (fds moebius_mu) s" using assms by (auto intro!: fds_abs_converges_moebius_mu) hence "(λn. moebius_mu (Suc n) / of_nat (Suc n) powr s) sums eval_fds (fds moebius_mu) s" by (simp add: fds_converges_altdef) also have "fds moebius_mu = inverse (fds_zeta :: complex fds)" by (rule fds_moebius_inverse_zeta) also from s have "eval_fds … s = inverse (zeta s)" by (subst eval_fds_inverse) (auto simp: fds_moebius_inverse_zeta [symmetric] eval_fds_zeta intro!: fds_abs_converges_moebius_mu) finally show ?thesis . qed text ‹ The following gives an extension of the $\zeta$ functions to the critical strip. › lemma hurwitz_zeta_critical_strip: fixes s :: complex and a :: real defines "S ≡ (λn. ∑i<n. (of_nat i + a) powr - s)" defines "I' ≡ (λn. of_nat n powr (1 - s) / (1 - s))" assumes "Re s > 0" "s ≠ 1" and "a > 0" shows "(λn. S n - I' n) ⇢ hurwitz_zeta a s" proof - from assms have [simp]: "s ≠ 1" by auto let ?f = "λx. of_real (x + a) powr -s" let ?fs = "λn x. (-1) ^ n * pochhammer s n * of_real (x + a) powr (-s - of_nat n)" have minus_commute: "-a - b = -b - a" for a b :: complex by (simp add: algebra_simps) define I where "I = (λn. (of_nat n + a) powr (1 - s) / (1 - s))" define R where "R = (λn. EM_remainder' 1 (?fs 1) (real 0) (real n))" define R_lim where "R_lim = EM_remainder 1 (?fs 1) 0" define C where "C = - (a powr -s / 2)" define D where "D = (λn. (1/2) * (of_real (a + real n) powr - s))" define D' where "D' = (λn. of_real (a + real n) powr - s)" define C' where "C' = a powr (1 - s) / (1 - s)" define C'' where "C'' = of_real a powr - s" { fix n :: nat assume n: "n > 0" have "((λx. of_real (x + a) powr -s) has_integral (of_real (real n + a) powr (1-s) / (1 - s) - of_real (0 + a) powr (1 - s) / (1 - s))) {0..real n}" using n assms by (intro fundamental_theorem_of_calculus) (auto intro!: continuous_intros has_vector_derivative_real_field derivative_eq_intros simp: complex_nonpos_Reals_iff) hence I: "((λx. of_real (x + a) powr -s) has_integral (I n - C')) {0..n}" by (auto simp: divide_simps C'_def I_def) have "(∑i∈{0<..n}. ?f (real i)) - integral {real 0..real n} ?f = (∑k<1. (bernoulli' (Suc k) / fact (Suc k)) *⇩_{R}(?fs k (real n) - ?fs k (real 0))) + R n" using n assms unfolding R_def by (intro euler_maclaurin_strong_raw_nat[where Y = "{0}"]) (auto intro!: continuous_intros derivative_eq_intros has_vector_derivative_real_field simp: pochhammer_rec' algebra_simps complex_nonpos_Reals_iff add_eq_0_iff) also have "(∑k<1. (bernoulli' (Suc k) / fact (Suc k)) *⇩_{R}(?fs k (real n) - ?fs k (real 0))) = ((n + a) powr - s - a powr - s) / 2" by (simp add: lessThan_nat_numeral scaleR_conv_of_real numeral_2_eq_2 [symmetric]) also have "… = C + D n" by (simp add: C_def D_def field_simps) also have "integral {real 0..real n} (λx. complex_of_real (x + a) powr - s) = I n - C'" using I by (simp add: has_integral_iff) also have "(∑i∈{0<..n}. of_real (real i + a) powr - s) = (∑i=0..n. of_real (real i + a) powr - s) - of_real a powr -s" using assms by (subst sum.head) auto also have "(∑i=0..n. of_real (real i + a) powr - s) = S n + of_real (real n + a) powr -s" unfolding S_def by (subst sum.last_plus) (auto simp: atLeast0LessThan) finally have "C - C' + C'' - D' n + D n + R n + (I n - I' n) = S n - I' n" by (simp add: algebra_simps S_def D'_def C''_def) } hence ev: "eventually (λn. C - C' + C'' - D' n + D n + R n + (I n - I' n) = S n - I' n) at_top" by (intro eventually_mono[OF eventually_gt_at_top[of 0]]) auto have [simp]: "-1 - s = -s - 1" by simp { let ?C = "norm (pochhammer s 1)" have "R ⇢ R_lim" unfolding R_def R_lim_def of_nat_0 proof (subst of_int_0 [symmetric], rule tendsto_EM_remainder) show "eventually (λx. norm (?fs 1 x) ≤ ?C * (x + a) powr (-Re s - 1)) at_top" using eventually_ge_at_top[of 0] by eventually_elim (insert assms, auto simp: norm_mult norm_powr_real_powr) next fix x assume x: "x ≥ real_of_int 0" have [simp]: "-numeral n - (x :: real) = -x - numeral n" for x n by (simp add: algebra_simps) show "((λx. ?C / (-Re s) * (x + a) powr (-Re s)) has_real_derivative ?C * (x + a) powr (- Re s - 1)) (at x within {real_of_int 0..})" using assms x by (auto intro!: derivative_eq_intros) next have "(λy. ?C / (- Re s) * (a + real y) powr (- Re s)) ⇢ 0" by (intro tendsto_mult_right_zero tendsto_neg_powr filterlim_real_sequentially filterlim_tendsto_add_at_top[OF tendsto_const]) (use assms in auto) thus "convergent (λy. ?C / (- Re s) * (real y + a) powr (- Re s))" by (auto simp: add_ac convergent_def) qed (intro integrable_EM_remainder' continuous_intros, insert assms, auto simp: add_eq_0_iff) } moreover have "(λn. I n - I' n) ⇢ 0" proof - have "(λn. (complex_of_real (real n + a) powr (1 - s) - of_real (real n) powr (1 - s)) / (1 - s)) ⇢ 0 / (1 - s)" using assms(3-5) by (intro filterlim_compose[OF _ filterlim_real_sequentially] tendsto_divide complex_powr_add_minus_powr_asymptotics) auto thus "(λn. I n - I' n) ⇢ 0" by (simp add: I_def I'_def divide_simps) qed ultimately have "(λn. C - C' + C'' - D' n + D n + R n + (I n - I' n)) ⇢ C - C' + C'' - 0 + 0 + R_lim + 0" unfolding D_def D'_def using assms by (intro tendsto_add tendsto_diff tendsto_const tendsto_mult_right_zero tendsto_neg_powr_complex_of_real filterlim_tendsto_add_at_top filterlim_real_sequentially) auto also have "C - C' + C'' - 0 + 0 + R_lim + 0 = (a powr - s / 2) + a powr (1 - s) / (s - 1) + R_lim" by (simp add: C_def C'_def C''_def field_simps) also have "… = hurwitz_zeta a s" using assms by (simp add: hurwitz_zeta_def pre_zeta_def pre_zeta_aux_def R_lim_def scaleR_conv_of_real) finally have "(λn. C - C' + C'' - D' n + D n + R n + (I n - I' n)) ⇢ hurwitz_zeta a s" . with ev show ?thesis by (blast intro: Lim_transform_eventually) qed lemma zeta_critical_strip: fixes s :: complex and a :: real defines "S ≡ (λn. ∑i=1..n. (of_nat i) powr - s)" defines "I ≡ (λn. of_nat n powr (1 - s) / (1 - s))" assumes s: "Re s > 0" "s ≠ 1" shows "(λn. S n - I n) ⇢ zeta s" proof - from hurwitz_zeta_critical_strip[OF s zero_less_one] have "(λn. (∑i<n. complex_of_real (Suc i) powr - s) - of_nat n powr (1 - s) / (1 - s)) ⇢ hurwitz_zeta 1 s" by (simp add: add_ac) also have "(λn. (∑i<n. complex_of_real (Suc i) powr -s)) = (λn. (∑i=1..n. of_nat i powr -s))" by (intro ext sum.reindex_bij_witness[of _ "λx. x - 1" Suc]) auto finally show ?thesis by (simp add: zeta_def S_def I_def) qed subsection ‹The non-vanishing of $\zeta$ for $\mathfrak{R}(s) \geq 1$› text ‹ This proof is based on a sketch by Newman~\<^cite>‹"newman1998analytic"›, which was previously formalised in HOL Light by Harrison~\<^cite>‹"harrison2009pnt"›, albeit in a much more concrete and low-level style. Our aim here is to reproduce Newman's proof idea cleanly and on the same high level of abstraction. › theorem zeta_Re_ge_1_nonzero: fixes s assumes "Re s ≥ 1" "s ≠ 1" shows "zeta s ≠ 0" proof (cases "Re s > 1") case False define a where "a = -Im s" from False assms have s [simp]: "s = 1 - 𝗂 * a" and a: "a ≠ 0" by (auto simp: complex_eq_iff a_def) show ?thesis proof assume "zeta s = 0" hence zero: "zeta (1 - 𝗂 * a) = 0" by simp with zeta_cnj[of "1 - 𝗂 * a"] have zero': "zeta (1 + 𝗂 * a) = 0" by simp ― ‹We define the function $Q(s) = \zeta(s)^2\zeta(s+ia)\zeta(s-ia)$ and its Dirichlet series. The objective will be to show that this function is entire and its Dirichlet series converges everywhere. Of course, $Q(s)$ has singularities at $1$ and $1\pm ia$, so we need to show they can be removed.› define Q Q_fds where "Q = (λs. zeta s ^ 2 * zeta (s + 𝗂 * a) * zeta (s - 𝗂 * a))" and "Q_fds = fds_zeta ^ 2 * fds_shift (𝗂 * a) fds_zeta * fds_shift (-𝗂 * a) fds_zeta" let ?sings = "{1, 1 + 𝗂 * a, 1 - 𝗂 * a}" ― ‹We show that @{term Q} is locally bounded everywhere. This is the case because the poles of $\zeta(s)$ cancel with the zeros of $\zeta(s\pm ia)$ and vice versa. This boundedness is then enough to show that @{term Q} has only removable singularities.› have Q_bigo_1: "Q ∈ O[at s](λ_. 1)" for s proof - have Q_eq: "Q = (λs. (zeta s * zeta (s + 𝗂 * a)) * (zeta s * zeta (s - 𝗂 * a)))" by (simp add: Q_def power2_eq_square mult_ac) ― ‹The singularity of $\zeta(s)$ at 1 gets cancelled by the zero of $\zeta(s-ia)$:› have bigo1: "(λs. zeta s * zeta (s - 𝗂 * a)) ∈ O[at 1](λ_. 1)" if "zeta (1 - 𝗂 * a) = 0" "a ≠ 0" for a :: real proof - have "(λs. zeta (s - 𝗂 * a) - zeta (1 - 𝗂 * a)) ∈ O[at 1](λs. s - 1)" using that by (intro taylor_bigo_linear holomorphic_on_imp_differentiable_at[of _ "-{1 + 𝗂 * a}"] holomorphic_intros) (auto simp: complex_eq_iff) hence "(λs. zeta s * zeta (s - 𝗂 * a)) ∈ O[at 1](λs. 1 / (s - 1) * (s - 1))" using that by (intro landau_o.big.mult zeta_bigo_at_1) simp_all also have "(λs. 1 / (s - 1) * (s - 1)) ∈ Θ[at 1](λ_. 1)" by (intro bigthetaI_cong) (auto simp: eventually_at_filter) finally show ?thesis . qed ― ‹The analogous result for $\zeta(s) \zeta(s+ia)$:› have bigo1': "(λs. zeta s * zeta (s + 𝗂 * a)) ∈ O[at 1](λ_. 1)" if "zeta (1 - 𝗂 * a) = 0" "a ≠ 0" for a :: real using bigo1[of "-a"] that zeta_cnj[of "1 - 𝗂 * a"] by simp ― ‹The singularity of $\zeta(s-ia)$ gets cancelled by the zero of $\zeta(s)$:› have bigo2: "(λs. zeta s * zeta (s - 𝗂 * a)) ∈ O[at (1 + 𝗂 * a)](λ_. 1)" if "zeta (1 - 𝗂 * a) = 0" "a ≠ 0" for a :: real proof - have "(λs. zeta s * zeta (s - 𝗂 * a)) ∈ O[filtermap (λs. s + 𝗂 * a) (at 1)](λ_. 1)" using bigo1'[of a] that by (simp add: mult.commute landau_o.big.in_filtermap_iff) also have "filtermap (λs. s + 𝗂 * a) (at 1) = at (1 + 𝗂 * a)" using filtermap_at_shift[of "-𝗂 * a" 1] by simp finally show ?thesis . qed ― ‹Again, the analogous result for $\zeta(s) \zeta(s+ia)$:› have bigo2': "(λs. zeta s * zeta (s + 𝗂 * a)) ∈ O[at (1 - 𝗂 * a)](λ_. 1)" if "zeta (1 - 𝗂 * a) = 0" "a ≠ 0" for a :: real using bigo2[of "-a"] that zeta_cnj[of "1 - 𝗂 * a"] by simp ― ‹Now the final case distinction to show $Q(s)\in O(1)$ for all $s\in\mathbb{C}$:› consider "s = 1" | "s = 1 + 𝗂 * a" | "s = 1 - 𝗂 * a" | "s ∉ ?sings" by blast thus ?thesis proof cases case 1 thus ?thesis unfolding Q_eq using zero zero' a by (auto intro: bigo1 bigo1' landau_o.big.mult_in_1) next case 2 from a have "isCont (λs. zeta s * zeta (s + 𝗂 * a)) (1 + 𝗂 * a)" by (auto intro!: continuous_intros) with 2 show ?thesis unfolding Q_eq using zero zero' a by (auto intro: bigo2 landau_o.big.mult_in_1 continuous_imp_bigo_1) next case 3 from a have "isCont (λs. zeta s * zeta (s - 𝗂 * a)) (1 - 𝗂 * a)" by (auto intro!: continuous_intros) with 3 show ?thesis unfolding Q_eq using zero zero' a by (auto intro: bigo2' landau_o.big.mult_in_1 continuous_imp_bigo_1) qed (auto intro!: continuous_imp_bigo_1 continuous_intros simp: Q_def complex_eq_iff) qed ― ‹Thus, we can remove the singularities from @{term Q} and extend it to an entire function.› have "∃Q'. Q' holomorphic_on UNIV ∧ (∀z∈UNIV - ?sings. Q' z = Q z)" by (intro removable_singularities Q_bigo_1) (auto simp: Q_def complex_eq_iff intro!: holomorphic_intros) then obtain Q' where Q': "Q' holomorphic_on UNIV" "⋀z. z ∉ ?sings ⟹ Q' z = Q z" by blast ― ‹@{term Q'} constitutes an analytic continuation of the Dirichlet series of @{term Q}.› have eval_Q_fds: "eval_fds Q_fds s = Q' s" if "Re s > 1" for s proof - have "eval_fds Q_fds s = Q s" using that by (simp add: Q_fds_def Q_def eval_fds_mult eval_fds_power fds_abs_converges_mult fds_abs_converges_power eval_fds_zeta) also from that have "… = Q' s" by (subst Q') auto finally show ?thesis . qed ― ‹Since $\zeta(s)$ and $\zeta(s\pm ia)$ are completely multiplicative Dirichlet series, the logarithm of their product can be rewritten into the following nice form:› have ln_Q_fds_eq: "fds_ln 0 Q_fds = fds (λk. of_real (2 * mangoldt k / ln k * (1 + cos (a * ln k))))" proof - note simps = fds_ln_mult[where l' = 0 and l'' = 0] fds_ln_power[where l' = 0] fds_ln_prod[where l' = "λ_. 0"] have "fds_ln 0 Q_fds = 2 * fds_ln 0 fds_zeta + fds_shift (𝗂 * a) (fds_ln 0 fds_zeta) + fds_shift (-𝗂 * a) (fds_ln 0 fds_zeta)" by (auto simp: Q_fds_def simps) also have "completely_multiplicative_function (fds_nth (fds_zeta :: complex fds))" by standard auto hence "fds_ln (0 :: complex) fds_zeta = fds (λn. mangoldt n /⇩_{R}ln (real n))" by (subst fds_ln_completely_multiplicative) (auto simp: fds_eq_iff) also have "2 * … + fds_shift (𝗂 * a) … + fds_shift (-𝗂 * a) … = fds (λk. of_real (2 * mangoldt k / ln k * (1 + cos (a