Theory Zeta_Function
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›
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
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
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
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}"
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)
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
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
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
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
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
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
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
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