# Theory Zeta_Library

section ‹Various preliminary material›
theory Zeta_Library
imports
"HOL-Complex_Analysis.Complex_Analysis"
"HOL-Real_Asymp.Real_Asymp"
"Dirichlet_Series.Dirichlet_Series_Analysis"
begin

subsection ‹Facts about limits›

lemma at_within_altdef:
"at x within A = (INF S∈{S. open S ∧ x ∈ S}. principal (S ∩ (A - {x})))"
unfolding at_within_def nhds_def inf_principal [symmetric]
by (subst INF_inf_distrib [symmetric]) (auto simp: INF_constant)

lemma tendsto_at_left_realI_sequentially:
fixes f :: "real ⇒ 'b::first_countable_topology"
assumes *: "⋀X. filterlim X (at_left c) sequentially ⟹ (λn. f (X n)) ⇢ y"
shows "(f ⤏ y) (at_left c)"
proof -
obtain A where A: "decseq A" "open (A n)" "y ∈ A n" "nhds y = (INF n. principal (A n))" for n
by (rule nhds_countable[of y]) (rule that)

have "∀m. ∃d<c. ∀x∈{d<..<c}. f x ∈ A m"
proof (rule ccontr)
assume "¬ (∀m. ∃d<c. ∀x∈{d<..<c}. f x ∈ A m)"
then obtain m where **: "⋀d. d < c ⟹ ∃x∈{d<..<c}. f x ∉ A m"
by auto
have "∃X. ∀n. (f (X n) ∉ A m ∧ X n < c) ∧ X (Suc n) > c - max 0 ((c - X n) / 2)"
proof (intro dependent_nat_choice, goal_cases)
case 1
from **[of "c - 1"] show ?case by auto
next
case (2 x n)
with **[of "c - max 0 (c - x) / 2"] show ?case by force
qed
then obtain X where X: "⋀n. f (X n) ∉ A m" "⋀n. X n < c" "⋀n. X (Suc n) > c - max 0 ((c - X n) / 2)"
by auto
have X_ge: "X n ≥ c - (c - X 0) / 2 ^ n" for n
proof (induction n)
case (Suc n)
have "c - (c - X 0) / 2 ^ Suc n = c - (c - (c - (c - X 0) / 2 ^ n)) / 2"
by simp
also have "c - (c - (c - (c - X 0) / 2 ^ n)) / 2 ≤ c - (c - X n) / 2"
by (intro diff_left_mono divide_right_mono Suc diff_right_mono) auto
also have "… = c - max 0 ((c - X n) / 2)"
using X[of n] by (simp add: max_def)
also have "… < X (Suc n)"
using X[of n] by simp
finally show ?case by linarith
qed auto

have "X ⇢ c"
proof (rule tendsto_sandwich)
show "eventually (λn. X n ≤ c) sequentially"
using X by (intro always_eventually) (auto intro!: less_imp_le)
show "eventually (λn. X n ≥ c - (c - X 0) / 2 ^ n) sequentially"
using X_ge by (intro always_eventually) auto
qed real_asymp+
hence "filterlim X (at_left c) sequentially"
by (rule tendsto_imp_filterlim_at_left)
(use X in ‹auto intro!: always_eventually less_imp_le›)
from topological_tendstoD[OF *[OF this] A(2, 3), of m] X(1) show False
by auto
qed

then obtain d where d: "d m < c" "x ∈ {d m<..<c} ⟹ f x ∈ A m" for m x
by metis
have ***: "at_left c = (INF S∈{S. open S ∧ c ∈ S}. principal (S ∩ {..<c}))"
by (simp add: at_within_altdef)
from d show ?thesis
unfolding *** A using A(1,2) by (intro filterlim_base[of _ "λm. {d m<..}"]) auto
qed

lemma
shows at_right_PInf [simp]: "at_right (∞ :: ereal) = bot"
and at_left_MInf [simp]: "at_left (-∞ :: ereal) = bot"
proof -
have "{(∞::ereal)<..} = {}" "{..<-(∞::ereal)} = {}"
by auto
thus "at_right (∞ :: ereal) = bot" "at_left (-∞ :: ereal) = bot"
by (simp_all add: at_within_def)
qed

lemma tendsto_at_left_erealI_sequentially:
fixes f :: "ereal ⇒ 'b::first_countable_topology"
assumes *: "⋀X. filterlim X (at_left c) sequentially ⟹ (λn. f (X n)) ⇢ y"
shows "(f ⤏ y) (at_left c)"
proof (cases c)
case [simp]: PInf
have "((λx. f (ereal x)) ⤏ y) at_top" using assms
by (intro tendsto_at_topI_sequentially assms)
(simp_all flip: ereal_tendsto_simps add: o_def filterlim_at)
thus ?thesis
by (simp add: at_left_PInf filterlim_filtermap)
next
case [simp]: MInf
thus ?thesis by auto
next
case [simp]: (real c')
have "((λx. f (ereal x)) ⤏ y) (at_left c')"
proof (intro tendsto_at_left_realI_sequentially assms)
fix X assume *: "filterlim X (at_left c') sequentially"
show "filterlim (λn. ereal (X n)) (at_left c) sequentially"
by (rule filterlim_compose[OF _ *])
(simp add: sequentially_imp_eventually_within tendsto_imp_filterlim_at_left)
qed
thus ?thesis
by (simp add: at_left_ereal filterlim_filtermap)
qed

lemma tendsto_at_right_realI_sequentially:
fixes f :: "real ⇒ 'b::first_countable_topology"
assumes *: "⋀X. filterlim X (at_right c) sequentially ⟹ (λn. f (X n)) ⇢ y"
shows "(f ⤏ y) (at_right c)"
proof -
obtain A where A: "decseq A" "open (A n)" "y ∈ A n" "nhds y = (INF n. principal (A n))" for n
by (rule nhds_countable[of y]) (rule that)

have "∀m. ∃d>c. ∀x∈{c<..<d}. f x ∈ A m"
proof (rule ccontr)
assume "¬ (∀m. ∃d>c. ∀x∈{c<..<d}. f x ∈ A m)"
then obtain m where **: "⋀d. d > c ⟹ ∃x∈{c<..<d}. f x ∉ A m"
by auto
have "∃X. ∀n. (f (X n) ∉ A m ∧ X n > c) ∧ X (Suc n) < c + max 0 ((X n - c) / 2)"
proof (intro dependent_nat_choice, goal_cases)
case 1
from **[of "c + 1"] show ?case by auto
next
case (2 x n)
with **[of "c + max 0 (x - c) / 2"] show ?case by force
qed
then obtain X where X: "⋀n. f (X n) ∉ A m" "⋀n. X n > c" "⋀n. X (Suc n) < c + max 0 ((X n - c) / 2)"
by auto
have X_le: "X n ≤ c + (X 0 - c) / 2 ^ n" for n
proof (induction n)
case (Suc n)
have "X (Suc n) < c + max 0 ((X n - c) / 2)"
by (intro X)
also have "… = c + (X n - c) / 2"
using X[of n] by (simp add: field_simps max_def)
also have "… ≤ c + (c + (X 0 - c) / 2 ^ n - c) / 2"
by (intro add_left_mono divide_right_mono Suc diff_right_mono) auto
also have "… = c + (X 0 - c) / 2 ^ Suc n"
by simp
finally show ?case by linarith
qed auto

have "X ⇢ c"
proof (rule tendsto_sandwich)
show "eventually (λn. X n ≥ c) sequentially"
using X by (intro always_eventually) (auto intro!: less_imp_le)
show "eventually (λn. X n ≤ c + (X 0 - c) / 2 ^ n) sequentially"
using X_le by (intro always_eventually) auto
qed real_asymp+
hence "filterlim X (at_right c) sequentially"
by (rule tendsto_imp_filterlim_at_right)
(use X in ‹auto intro!: always_eventually less_imp_le›)
from topological_tendstoD[OF *[OF this] A(2, 3), of m] X(1) show False
by auto
qed

then obtain d where d: "d m > c" "x ∈ {c<..<d m} ⟹ f x ∈ A m" for m x
by metis
have ***: "at_right c = (INF S∈{S. open S ∧ c ∈ S}. principal (S ∩ {c<..}))"
by (simp add: at_within_altdef)
from d show ?thesis
unfolding *** A using A(1,2) by (intro filterlim_base[of _ "λm. {..<d m}"]) auto
qed

lemma tendsto_at_right_erealI_sequentially:
fixes f :: "ereal ⇒ 'b::first_countable_topology"
assumes *: "⋀X. filterlim X (at_right c) sequentially ⟹ (λn. f (X n)) ⇢ y"
shows "(f ⤏ y) (at_right c)"
proof (cases c)
case [simp]: MInf
have "((λx. f (-ereal x)) ⤏ y) at_top" using assms
by (intro tendsto_at_topI_sequentially assms)
(simp_all flip: uminus_ereal.simps ereal_tendsto_simps add: o_def filterlim_at)
thus ?thesis
by (simp add: at_right_MInf filterlim_filtermap at_top_mirror)
next
case [simp]: PInf
thus ?thesis by auto
next
case [simp]: (real c')
have "((λx. f (ereal x)) ⤏ y) (at_right c')"
proof (intro tendsto_at_right_realI_sequentially assms)
fix X assume *: "filterlim X (at_right c') sequentially"
show "filterlim (λn. ereal (X n)) (at_right c) sequentially"
by (rule filterlim_compose[OF _ *])
(simp add: sequentially_imp_eventually_within tendsto_imp_filterlim_at_right)
qed
thus ?thesis
by (simp add: at_right_ereal filterlim_filtermap)
qed

proposition analytic_continuation':
assumes hol: "f holomorphic_on S" "g holomorphic_on S"
and "open S" and "connected S"
and "U ⊆ S" and "ξ ∈ S"
and "ξ islimpt U"
and fU0 [simp]: "⋀z. z ∈ U ⟹ f z = g z"
and "w ∈ S"
shows "f w = g w"
using analytic_continuation[OF holomorphic_on_diff[OF hol] assms(3-7) _ assms(9)] assms(8)
by simp

subsection ‹Various facts about integrals›

lemma continuous_on_imp_set_integrable_cbox:
fixes h :: "'a :: euclidean_space ⇒ 'b :: euclidean_space"
assumes "continuous_on (cbox a b) h"
shows   "set_integrable lborel (cbox a b) h"
proof -
from assms have "h absolutely_integrable_on cbox a b"
by (rule absolutely_integrable_continuous)
moreover have "(λx. indicat_real (cbox a b) x *⇩R h x) ∈ borel_measurable borel"
by (rule borel_measurable_continuous_on_indicator) (use assms in auto)
ultimately show ?thesis
unfolding set_integrable_def using assms by (subst (asm) integrable_completion) auto
qed

lemma set_nn_integral_cong:
assumes "M = M'" "A = B" "⋀x. x ∈ space M ∩ A ⟹ f x = g x"
shows   "set_nn_integral M A f = set_nn_integral M' B g"
using assms unfolding assms(1,2) by (intro nn_integral_cong) (auto simp: indicator_def)

lemma set_integrable_bound:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
and g :: "'a ⇒ 'c::{banach, second_countable_topology}"
assumes "set_integrable M A f" "set_borel_measurable M A g"
assumes "AE x in M. x ∈ A ⟶ norm (g x) ≤ norm (f x)"
shows   "set_integrable M A g"
unfolding set_integrable_def
proof (rule Bochner_Integration.integrable_bound)
from assms(1) show "integrable M (λx. indicator A x *⇩R f x)"
by (simp add: set_integrable_def)
from assms(2) show "(λx. indicat_real A x *⇩R g x) ∈ borel_measurable M"
by (simp add: set_borel_measurable_def)
from assms(3) show "AE x in M. norm (indicat_real A x *⇩R g x) ≤ norm (indicat_real A x *⇩R f x)"
by eventually_elim (simp add: indicator_def)
qed

(* TODO replace version in library. Better name? *)
lemma nn_integral_has_integral_lebesgue:
fixes f :: "'a::euclidean_space ⇒ real"
assumes nonneg: "⋀x. x ∈ Ω ⟹ 0 ≤ f x" and I: "(f has_integral I) Ω"
shows "integral⇧N lborel (λx. indicator Ω x * f x) = I"
proof -
from I have "(λx. indicator Ω x *⇩R f x) ∈ lebesgue →⇩M borel"
by (rule has_integral_implies_lebesgue_measurable)
then obtain f' :: "'a ⇒ real"
where [measurable]: "f' ∈ borel →⇩M borel" and eq: "AE x in lborel. indicator Ω x * f x = f' x"
by (auto dest: completion_ex_borel_measurable_real)

from I have "((λx. abs (indicator Ω x * f x)) has_integral I) UNIV"
using nonneg by (simp add: indicator_def of_bool_def if_distrib[of "λx. x * f y" for y] cong: if_cong)
also have "((λx. abs (indicator Ω x * f x)) has_integral I) UNIV ⟷ ((λx. abs (f' x)) has_integral I) UNIV"
using eq by (intro has_integral_AE) auto
finally have "integral⇧N lborel (λx. abs (f' x)) = I"
by (rule nn_integral_has_integral_lborel[rotated 2]) auto
also have "integral⇧N lborel (λx. abs (f' x)) = integral⇧N lborel (λx. abs (indicator Ω x * f x))"
using eq by (intro nn_integral_cong_AE) auto
also have "(λx. abs (indicator Ω x * f x)) = (λx. indicator Ω x * f x)"
using nonneg by (auto simp: indicator_def fun_eq_iff)
finally show ?thesis .
qed

subsection ‹Uniform convergence of integrals›

lemma has_absolute_integral_change_of_variables_1':
fixes f :: "real ⇒ real" and g :: "real ⇒ real"
assumes S: "S ∈ sets lebesgue"
and der_g: "⋀x. x ∈ S ⟹ (g has_field_derivative g' x) (at x within S)"
and inj: "inj_on g S"
shows "(λx. ¦g' x¦ *⇩R f(g x)) absolutely_integrable_on S ∧
integral S (λx. ¦g' x¦ *⇩R f(g x)) = b
⟷ f absolutely_integrable_on (g  S) ∧ integral (g  S) f = b"
proof -
have "(λx. ¦g' x¦ *⇩R vec (f(g x)) :: real ^ 1) absolutely_integrable_on S ∧
integral S (λx. ¦g' x¦ *⇩R vec (f(g x))) = (vec b :: real ^ 1)
⟷ (λx. vec (f x) :: real ^ 1) absolutely_integrable_on (g  S) ∧
integral (g  S) (λx. vec (f x)) = (vec b :: real ^ 1)"
using assms unfolding has_field_derivative_iff_has_vector_derivative
by (intro has_absolute_integral_change_of_variables_1 assms) auto
thus ?thesis
by (simp add: absolutely_integrable_on_1_iff integral_on_1_eq)
qed

lemma set_nn_integral_lborel_eq_integral:
fixes f::"'a::euclidean_space ⇒ real"
assumes "set_borel_measurable borel A f"
assumes "⋀x. x ∈ A ⟹ 0 ≤ f x" "(∫⇧+x∈A. f x ∂lborel) < ∞"
shows "(∫⇧+x∈A. f x ∂lborel) = integral A f"
proof -
have eq: "(∫⇧+x∈A. f x ∂lborel) = (∫⇧+x. ennreal (indicator A x * f x) ∂lborel)"
by (intro nn_integral_cong) (auto simp: indicator_def)
also have "… = integral UNIV (λx. indicator A x * f x)"
using assms eq by (intro nn_integral_lborel_eq_integral)
(auto simp: indicator_def set_borel_measurable_def)
also have "integral UNIV (λx. indicator A x * f x) = integral A (λx. indicator A x * f x)"
by (rule integral_spike_set) (auto intro: empty_imp_negligible)

also have "… = integral A f"
by (rule integral_cong) (auto simp: indicator_def)
finally show ?thesis .
qed

lemma nn_integral_has_integral_lebesgue':
fixes f :: "'a::euclidean_space ⇒ real"
assumes nonneg: "⋀x. x ∈ Ω ⟹ 0 ≤ f x" and I: "(f has_integral I) Ω"
shows "integral⇧N lborel (λx. ennreal (f x) * indicator Ω x) = ennreal I"
proof -
have "integral⇧N lborel (λx. ennreal (f x) * indicator Ω x) =
integral⇧N lborel (λx. ennreal (indicator Ω x * f x))"
by (intro nn_integral_cong) (auto simp: indicator_def)
also have "… = ennreal I"
using assms by (intro nn_integral_has_integral_lebesgue)
finally show ?thesis .
qed

lemma uniform_limit_set_lebesgue_integral:
fixes f :: "'a ⇒ 'b :: euclidean_space ⇒ 'c :: {banach, second_countable_topology}"
assumes "set_integrable lborel X' g"
assumes [measurable]: "X' ∈ sets borel"
assumes [measurable]: "⋀y. y ∈ Y ⟹ set_borel_measurable borel X' (f y)"
assumes "⋀y. y ∈ Y ⟹ (AE t∈X' in lborel. norm (f y t) ≤ g t)"
assumes "eventually (λx. X x ∈ sets borel ∧ X x ⊆ X') F"
assumes "filterlim (λx. set_lebesgue_integral lborel (X x) g)
(nhds (set_lebesgue_integral lborel X' g)) F"
shows "uniform_limit Y
(λx y. set_lebesgue_integral lborel (X x) (f y))
(λy. set_lebesgue_integral lborel X' (f y)) F"
proof (rule uniform_limitI, goal_cases)
case (1 ε)
have integrable_g: "set_integrable lborel U g"
if "U ∈ sets borel" "U ⊆ X'" for U
by (rule set_integrable_subset[OF assms(1)]) (use that in auto)
have "eventually (λx. dist (set_lebesgue_integral lborel (X x) g)
(set_lebesgue_integral lborel X' g) < ε) F"
using ‹ε > 0› assms by (auto simp: tendsto_iff)
from this show ?case using ‹eventually (λ_. _ ∧ _) F›
proof eventually_elim
case (elim x)
hence [measurable]:"X x ∈ sets borel" and "X x ⊆ X'" by auto
have integrable: "set_integrable lborel U (f y)"
if "y ∈ Y" "U ∈ sets borel" "U ⊆ X'" for y U
apply (rule set_integrable_subset)
apply (rule set_integrable_bound[OF assms(1)])
apply (use assms(3) that in ‹simp add: set_borel_measurable_def›)
using assms(4)[OF ‹y ∈ Y›] apply eventually_elim apply force
using that apply simp_all
done
show ?case
proof
fix y assume "y ∈ Y"
have "dist (set_lebesgue_integral lborel (X x) (f y))
(set_lebesgue_integral lborel X' (f y)) =
norm (set_lebesgue_integral lborel X' (f y) -
set_lebesgue_integral lborel (X x) (f y))"
by (simp add: dist_norm norm_minus_commute)
also have "set_lebesgue_integral lborel X' (f y) -
set_lebesgue_integral lborel (X x) (f y) =
set_lebesgue_integral lborel (X' - X x) (f y)"
unfolding set_lebesgue_integral_def
apply (subst Bochner_Integration.integral_diff [symmetric])
unfolding set_integrable_def [symmetric]
apply (rule integrable; (fact | simp))
apply (rule integrable; fact)
apply (intro Bochner_Integration.integral_cong)
apply (use ‹X x ⊆ X'› in ‹auto simp: indicator_def›)
done
also have "norm … ≤ (∫t∈X'-X x. norm (f y t) ∂lborel)"
by (intro set_integral_norm_bound integrable) (fact | simp)+
also have "AE t∈X' - X x in lborel. norm (f y t) ≤ g t"
using assms(4)[OF ‹y ∈ Y›] by eventually_elim auto
with ‹y ∈ Y› have "(∫t∈X'-X x. norm (f y t) ∂lborel) ≤ (∫t∈X'-X x. g t ∂lborel)"
by (intro set_integral_mono_AE set_integrable_norm integrable integrable_g) auto
also have "… = (∫t∈X'. g t ∂lborel) - (∫t∈X x. g t ∂lborel)"
unfolding set_lebesgue_integral_def
apply (subst Bochner_Integration.integral_diff [symmetric])
unfolding set_integrable_def [symmetric]
apply (rule integrable_g; (fact | simp))
apply (rule integrable_g; fact)
apply (intro Bochner_Integration.integral_cong)
apply (use ‹X x ⊆ X'› in ‹auto simp: indicator_def›)
done
also have "… ≤ dist (∫t∈X x. g t ∂lborel) (∫t∈X'. g t ∂lborel)"
by (simp add: dist_norm)
also have "… < ε" by fact
finally show "dist (set_lebesgue_integral lborel (X x) (f y))
(set_lebesgue_integral lborel X' (f y)) < ε" .
qed
qed
qed

lemma integral_dominated_convergence_at_right:
fixes s :: "real ⇒ 'a ⇒ 'b::{banach, second_countable_topology}" and w :: "'a ⇒ real"
and f :: "'a ⇒ 'b" and M and c :: real
assumes "f ∈ borel_measurable M" "⋀t. s t ∈ borel_measurable M" "integrable M w"
assumes lim: "AE x in M. ((λi. s i x) ⤏ f x) (at_right c)"
assumes bound: "∀⇩F i in at_right c. AE x in M. norm (s i x) ≤ w x"
shows "((λt. integral⇧L M (s t)) ⤏ integral⇧L M f) (at_right c)"
proof (rule tendsto_at_right_realI_sequentially)
fix X :: "nat ⇒ real" assume X: "filterlim X (at_right c) sequentially"
from filterlim_iff[THEN iffD1, OF this, rule_format, OF bound]
obtain N where w: "⋀n. N ≤ n ⟹ AE x in M. norm (s (X n) x) ≤ w x"
by (auto simp: eventually_sequentially)

show "(λn. integral⇧L M (s (X n))) ⇢ integral⇧L M f"
proof (rule LIMSEQ_offset, rule integral_dominated_convergence)
show "AE x in M. norm (s (X (n + N)) x) ≤ w x" for n
by (rule w) auto
show "AE x in M. (λn. s (X (n + N)) x) ⇢ f x"
using lim
proof eventually_elim
fix x assume "((λi. s i x) ⤏ f x) (at_right c)"
then show "(λn. s (X (n + N)) x) ⇢ f x"
by (intro LIMSEQ_ignore_initial_segment filterlim_compose[OF _ X])
qed
qed fact+
qed

lemma integral_dominated_convergence_at_left:
fixes s :: "real ⇒ 'a ⇒ 'b::{banach, second_countable_topology}" and w :: "'a ⇒ real"
and f :: "'a ⇒ 'b" and M and c :: real
assumes "f ∈ borel_measurable M" "⋀t. s t ∈ borel_measurable M" "integrable M w"
assumes lim: "AE x in M. ((λi. s i x) ⤏ f x) (at_left c)"
assumes bound: "∀⇩F i in at_left c. AE x in M. norm (s i x) ≤ w x"
shows "((λt. integral⇧L M (s t)) ⤏ integral⇧L M f) (at_left c)"
proof (rule tendsto_at_left_realI_sequentially)
fix X :: "nat ⇒ real" assume X: "filterlim X (at_left c) sequentially"
from filterlim_iff[THEN iffD1, OF this, rule_format, OF bound]
obtain N where w: "⋀n. N ≤ n ⟹ AE x in M. norm (s (X n) x) ≤ w x"
by (auto simp: eventually_sequentially)

show "(λn. integral⇧L M (s (X n))) ⇢ integral⇧L M f"
proof (rule LIMSEQ_offset, rule integral_dominated_convergence)
show "AE x in M. norm (s (X (n + N)) x) ≤ w x" for n
by (rule w) auto
show "AE x in M. (λn. s (X (n + N)) x) ⇢ f x"
using lim
proof eventually_elim
fix x assume "((λi. s i x) ⤏ f x) (at_left c)"
then show "(λn. s (X (n + N)) x) ⇢ f x"
by (intro LIMSEQ_ignore_initial_segment filterlim_compose[OF _ X])
qed
qed fact+
qed

lemma uniform_limit_interval_integral_right:
fixes f :: "'a ⇒ real ⇒ 'c :: {banach, second_countable_topology}"
assumes "interval_lebesgue_integrable lborel a b g"
assumes [measurable]: "⋀y. y ∈ Y ⟹ set_borel_measurable borel (einterval a b) (f y)"
assumes "⋀y. y ∈ Y ⟹ (AE t∈einterval a b in lborel. norm (f y t) ≤ g t)"
assumes "a < b"
shows   "uniform_limit Y (λb' y. LBINT t=a..b'. f y t) (λy. LBINT t=a..b. f y t) (at_left b)"
proof (cases "Y = {}")
case False
have g_nonneg: "AE t∈einterval a b in lborel. g t ≥ 0"
proof -
from ‹Y ≠ {}› obtain y where "y ∈ Y" by auto
from assms(3)[OF this] show ?thesis
by eventually_elim (auto elim: order.trans[rotated])
qed

have ev: "eventually (λb'. b' ∈ {a<..<b}) (at_left b)"
using ‹a < b› by (intro eventually_at_leftI)
with ‹a < b› have "?thesis ⟷ uniform_limit Y (λb' y. ∫t∈einterval a (min b b'). f y t ∂lborel)
(λy. ∫t∈einterval a b. f y t ∂lborel) (at_left b)"
by (intro filterlim_cong arg_cong2[where f = uniformly_on])
(auto simp: interval_lebesgue_integral_def fun_eq_iff min_def
intro!: eventually_mono[OF ev])
also have …
proof (rule uniform_limit_set_lebesgue_integral[where g = g], goal_cases)
show "∀⇩F b' in at_left b. einterval a (min b b') ∈ sets borel ∧
einterval a (min b b') ⊆ einterval a b"
using ev by eventually_elim (auto simp: einterval_def)
next
show "((λb'. set_lebesgue_integral lborel (einterval a (min b b')) g) ⤏
set_lebesgue_integral lborel (einterval a b) g) (at_left b)"
unfolding set_lebesgue_integral_def
proof (intro tendsto_at_left_erealI_sequentially integral_dominated_convergence)
have *: "set_borel_measurable borel (einterval a b) g"
using assms(1) less_imp_le[OF ‹a < b›]
by (simp add: interval_lebesgue_integrable_def set_integrable_def set_borel_measurable_def)
show "(λx. indicat_real (einterval a b) x *⇩R g x) ∈ borel_measurable lborel"
using * by (simp add: set_borel_measurable_def)
fix X :: "nat ⇒ ereal" and n :: nat
have "set_borel_measurable borel (einterval a (min b (X n))) g"
by (rule set_borel_measurable_subset[OF *]) (auto simp: einterval_def)
thus "(λx. indicat_real (einterval a (min b (X n))) x *⇩R g x) ∈ borel_measurable lborel"
by (simp add: set_borel_measurable_def)
next
fix X :: "nat ⇒ ereal"
assume X: "filterlim X (at_left b) sequentially"
show "AE x in lborel. (λn. indicat_real (einterval a (min b (X n))) x *⇩R g x)
⇢ indicat_real (einterval a b) x *⇩R g x"
proof (rule AE_I2)
fix x :: real
have "(λt. indicator (einterval a (min b (X t))) x :: real) ⇢
indicator (einterval a b) x"
proof (cases "x ∈ einterval a b")
case False
hence "x ∉ einterval a (min b (X t))"for t by (auto simp: einterval_def)
with False show ?thesis by (simp add: indicator_def)
next
case True
with ‹a < b› have "eventually (λt. t ∈ {max a x<..<b}) (at_left b)"
by (intro eventually_at_leftI[of "ereal x"]) (auto simp: einterval_def min_def)
from this and X have "eventually (λt. X t ∈ {max a x<..<b}) sequentially"
by (rule eventually_compose_filterlim)
hence "eventually (λt. indicator (einterval a (min b (X t))) x = (1 :: real)) sequentially"
by eventually_elim (use True in ‹auto simp: indicator_def einterval_def›)
from tendsto_eventually[OF this] and True show ?thesis
by (simp add: indicator_def)
qed
thus "(λn. indicat_real (einterval a (min b (X n))) x *⇩R g x)
⇢ indicat_real (einterval a b) x *⇩R g x" by (intro tendsto_intros)
qed
next
fix X :: "nat ⇒ ereal" and n :: nat
show "AE x in lborel. norm (indicator (einterval a (min b (X n))) x *⇩R g x) ≤
indicator (einterval a b) x *⇩R g x"
using g_nonneg by eventually_elim (auto simp: indicator_def einterval_def)
qed (use assms less_imp_le[OF ‹a < b›] in
‹auto simp: interval_lebesgue_integrable_def set_integrable_def›)
qed (use assms in ‹auto simp: interval_lebesgue_integrable_def›)
finally show ?thesis .
qed auto

lemma uniform_limit_interval_integral_left:
fixes f :: "'a ⇒ real ⇒ 'c :: {banach, second_countable_topology}"
assumes "interval_lebesgue_integrable lborel a b g"
assumes [measurable]: "⋀y. y ∈ Y ⟹ set_borel_measurable borel (einterval a b) (f y)"
assumes "⋀y. y ∈ Y ⟹ (AE t∈einterval a b in lborel. norm (f y t) ≤ g t)"
assumes "a < b"
shows   "uniform_limit Y (λa' y. LBINT t=a'..b. f y t) (λy. LBINT t=a..b. f y t) (at_right a)"
proof (cases "Y = {}")
case False
have g_nonneg: "AE t∈einterval a b in lborel. g t ≥ 0"
proof -
from ‹Y ≠ {}› obtain y where "y ∈ Y" by auto
from assms(3)[OF this] show ?thesis
by eventually_elim (auto elim: order.trans[rotated])
qed

have ev: "eventually (λb'. b' ∈ {a<..<b}) (at_right a)"
using ‹a < b› by (intro eventually_at_rightI)
with ‹a < b› have "?thesis ⟷ uniform_limit Y (λa' y. ∫t∈einterval (max a a') b. f y t ∂lborel)
(λy. ∫t∈einterval a b. f y t ∂lborel) (at_right a)"
by (intro filterlim_cong arg_cong2[where f = uniformly_on])
(auto simp: interval_lebesgue_integral_def fun_eq_iff max_def
intro!: eventually_mono[OF ev])
also have …
proof (rule uniform_limit_set_lebesgue_integral[where g = g], goal_cases)
show "∀⇩F a' in at_right a. einterval (max a a') b ∈ sets borel ∧
einterval (max a a') b ⊆ einterval a b"
using ev by eventually_elim (auto simp: einterval_def)
next
show "((λa'. set_lebesgue_integral lborel (einterval (max a a') b) g) ⤏
set_lebesgue_integral lborel (einterval a b) g) (at_right a)"
unfolding set_lebesgue_integral_def
proof (intro tendsto_at_right_erealI_sequentially integral_dominated_convergence)
have *: "set_borel_measurable borel (einterval a b) g"
using assms(1) less_imp_le[OF ‹a < b›]
by (simp add: interval_lebesgue_integrable_def set_integrable_def set_borel_measurable_def)
show "(λx. indicat_real (einterval a b) x *⇩R g x) ∈ borel_measurable lborel"
using * by (simp add: set_borel_measurable_def)
fix X :: "nat ⇒ ereal" and n :: nat
have "set_borel_measurable borel (einterval (max a (X n)) b) g"
by (rule set_borel_measurable_subset[OF *]) (auto simp: einterval_def)
thus "(λx. indicat_real (einterval (max a (X n)) b) x *⇩R g x) ∈ borel_measurable lborel"
by (simp add: set_borel_measurable_def)
next
fix X :: "nat ⇒ ereal"
assume X: "filterlim X (at_right a) sequentially"
show "AE x in lborel. (λn. indicat_real (einterval (max a (X n)) b) x *⇩R g x)
⇢ indicat_real (einterval a b) x *⇩R g x"
proof (rule AE_I2)
fix x :: real
have "(λt. indicator (einterval (max a (X t)) b) x :: real) ⇢
indicator (einterval a b) x"
proof (cases "x ∈ einterval a b")
case False
hence "x ∉ einterval (max a (X t)) b"for t by (auto simp: einterval_def)
with False show ?thesis by (simp add: indicator_def)
next
case True
with ‹a < b› have "eventually (λt. t ∈ {a<..<x}) (at_right a)"
by (intro eventually_at_rightI[of _ "ereal x"]) (auto simp: einterval_def min_def)
from this and X have "eventually (λt. X t ∈ {a<..<x}) sequentially"
by (rule eventually_compose_filterlim)
hence "eventually (λt. indicator (einterval (max a (X t)) b) x = (1 :: real)) sequentially"
by eventually_elim (use True in ‹auto simp: indicator_def einterval_def›)
from tendsto_eventually[OF this] and True show ?thesis
by (simp add: indicator_def)
qed
thus "(λn. indicat_real (einterval (max a (X n)) b) x *⇩R g x)
⇢ indicat_real (einterval a b) x *⇩R g x" by (intro tendsto_intros)
qed
next
fix X :: "nat ⇒ ereal" and n :: nat
show "AE x in lborel. norm (indicator (einterval (max a (X n)) b) x *⇩R g x) ≤
indicator (einterval a b) x *⇩R g x"
using g_nonneg by eventually_elim (auto simp: indicator_def einterval_def)
qed (use assms less_imp_le[OF ‹a < b›] in
‹auto simp: interval_lebesgue_integrable_def set_integrable_def›)
qed (use assms in ‹auto simp: interval_lebesgue_integrable_def›)
finally show ?thesis .
qed auto

lemma uniform_limit_interval_integral_sequentially:
fixes f :: "'a ⇒ real ⇒ 'c :: {banach, second_countable_topology}"
assumes "interval_lebesgue_integrable lborel a b g"
assumes [measurable]: "⋀y. y ∈ Y ⟹ set_borel_measurable borel (einterval a b) (f y)"
assumes "⋀y. y ∈ Y ⟹ (AE t∈einterval a b in lborel. norm (f y t) ≤ g t)"
assumes a': "filterlim a' (at_right a) sequentially"
assumes b': "filterlim b' (at_left b) sequentially"
assumes "a < b"
shows   "uniform_limit Y (λn y. LBINT t=a' n..b' n. f y t)
(λy. LBINT t=a..b. f y t) sequentially"
proof (cases "Y = {}")
case False
have g_nonneg: "AE t∈einterval a b in lborel. g t ≥ 0"
proof -
from ‹Y ≠ {}› obtain y where "y ∈ Y" by auto
from assms(3)[OF this] show ?thesis
by eventually_elim (auto elim: order.trans[rotated])
qed

have ev: "eventually (λn. a < a' n ∧ a' n < b' n ∧ b' n < b) sequentially"
proof -
from ereal_dense2[OF ‹a < b›] obtain t where t: "a < ereal t" "ereal t < b" by blast
from t have "eventually (λn. a' n ∈ {a<..<t}) sequentially"
by (intro eventually_compose_filterlim[OF _ a'] eventually_at_rightI[of _ "ereal t"])
moreover from t have "eventually (λn. b' n ∈ {t<..<b}) sequentially"
by (intro eventually_compose_filterlim[OF _ b'] eventually_at_leftI[of "ereal t"])
ultimately show "eventually (λn. a < a' n ∧ a' n < b' n ∧ b' n < b) sequentially"
by eventually_elim auto
qed

have "?thesis ⟷ uniform_limit Y (λn y. ∫t∈einterval (max a (a' n)) (min b (b' n)). f y t ∂lborel)
(λy. ∫t∈einterval a b. f y t ∂lborel) sequentially" using ‹a < b›
by (intro filterlim_cong arg_cong2[where f = uniformly_on])
(auto simp: interval_lebesgue_integral_def fun_eq_iff min_def max_def
intro!: eventually_mono[OF ev])
also have …
proof (rule uniform_limit_set_lebesgue_integral[where g = g], goal_cases)
show "∀⇩F n in sequentially. einterval (max a (a' n)) (min b (b' n)) ∈ sets borel ∧
einterval (max a (a' n)) (min b (b' n)) ⊆ einterval a b"
using ev by eventually_elim (auto simp: einterval_def)
next
show "((λn. set_lebesgue_integral lborel (einterval (max a (a' n)) (min b (b' n))) g) ⤏
set_lebesgue_integral lborel (einterval a b) g) sequentially"
unfolding set_lebesgue_integral_def
proof (intro integral_dominated_convergence)
have *: "set_borel_measurable borel (einterval a b) g"
using assms(1) less_imp_le[OF ‹a < b›]
by (simp add: interval_lebesgue_integrable_def set_integrable_def set_borel_measurable_def)
show "(λx. indicat_real (einterval a b) x *⇩R g x) ∈ borel_measurable lborel"
using * by (simp add: set_borel_measurable_def)
fix n :: nat
have "set_borel_measurable borel (einterval (max a (a' n)) (min b (b' n))) g"
by (rule set_borel_measurable_subset[OF *]) (auto simp: einterval_def)
thus "(λx. indicat_real (einterval (max a (a' n)) (min b (b' n))) x *⇩R g x) ∈ borel_measurable lborel"
by (simp add: set_borel_measurable_def)
next
show "AE x in lborel. (λn. indicat_real (einterval (max a (a' n)) (min b (b' n))) x *⇩R g x)
⇢ indicat_real (einterval a b) x *⇩R g x"
proof (rule AE_I2)
fix x :: real
have "(λt. indicator (einterval (max a (a' t)) (min b (b' t))) x :: real) ⇢
indicator (einterval a b) x"
proof (cases "x ∈ einterval a b")
case False
hence "x ∉ einterval (max a (a' t)) (min b (b' t))"for t
by (auto simp: einterval_def)
with False show ?thesis by (simp add: indicator_def)
next
case True
with ‹a < b› have "eventually (λt. t ∈ {a<..<x}) (at_right a)"
by (intro eventually_at_rightI[of _ "ereal x"]) (auto simp: einterval_def min_def)

have "eventually (λn. x ∈ {a' n<..<b' n}) sequentially"
proof -
have "eventually (λn. a' n ∈ {a<..<x}) sequentially" using True
by (intro eventually_compose_filterlim[OF _ a'] eventually_at_rightI[of _ "ereal x"])
(auto simp: einterval_def)
moreover have "eventually (λn. b' n ∈ {x<..<b}) sequentially" using True
by (intro eventually_compose_filterlim[OF _ b'] eventually_at_leftI[of "ereal x"])
(auto simp: einterval_def)
ultimately show "eventually (λn. x ∈ {a' n<..<b' n}) sequentially"
by eventually_elim auto
qed
hence "eventually (λt. indicator (einterval (max a (a' t)) (min b (b' t))) x = (1 :: real)) sequentially"
by eventually_elim (use True in ‹auto simp: indicator_def einterval_def›)
from tendsto_eventually[OF this] and True show ?thesis
by (simp add: indicator_def)
qed
thus "(λn. indicat_real (einterval (max a (a' n)) (min b (b' n))) x *⇩R g x)
⇢ indicat_real (einterval a b) x *⇩R g x" by (intro tendsto_intros)
qed
next
fix X :: "nat ⇒ ereal" and n :: nat
show "AE x in lborel. norm (indicator (einterval (max a (a' n)) (min b (b' n))) x *⇩R g x) ≤
indicator (einterval a b) x *⇩R g x"
using g_nonneg by eventually_elim (auto simp: indicator_def einterval_def)
qed (use assms less_imp_le[OF ‹a < b›] in
‹auto simp: interval_lebesgue_integrable_def set_integrable_def›)
qed (use assms in ‹auto simp: interval_lebesgue_integrable_def›)
finally show ?thesis .
qed auto

lemma interval_lebesgue_integrable_combine:
assumes "interval_lebesgue_integrable lborel A B f"
assumes "interval_lebesgue_integrable lborel B C f"
assumes "set_borel_measurable borel (einterval A C) f"
assumes "A ≤ B" "B ≤ C"
shows   "interval_lebesgue_integrable lborel A C f"
proof -
have meas: "set_borel_measurable borel (einterval A B ∪ einterval B C) f"
by (rule set_borel_measurable_subset[OF assms(3)]) (use assms in ‹auto simp: einterval_def›)
have "set_integrable lborel (einterval A B ∪ einterval B C) f"
using assms by (intro set_integrable_Un) (auto simp: interval_lebesgue_integrable_def)
also have "?this ⟷ set_integrable lborel (einterval A C) f"
proof (cases "B ∈ {∞, -∞}")
case True
with assms have "einterval A B ∪ einterval B C = einterval A C"
by (auto simp: einterval_def)
thus ?thesis by simp
next
case False
then obtain B' where [simp]: "B = ereal B'"
by (cases B) auto
have "indicator (einterval A C) x = (indicator (einterval A B ∪ einterval B C) x :: real)"
if "x ≠ B'" for x using assms(4,5) that
by (cases A; cases C) (auto simp: einterval_def indicator_def)
hence "{x ∈ space lborel. indicat_real (einterval A B ∪ einterval B C) x *⇩R f x ≠
indicat_real (einterval A C) x *⇩R f x} ⊆ {B'}" by force
thus ?thesis unfolding set_integrable_def using meas assms
by (intro integrable_cong_AE AE_I[of _ _ "{B'}"])
qed
also have "… ⟷ ?thesis"
using order.trans[OF assms(4,5)] by (simp add: interval_lebesgue_integrable_def)
finally show ?thesis .
qed

lemma interval_lebesgue_integrable_bigo_right:
fixes A B :: real
fixes f :: "real ⇒ real"
assumes "f ∈ O[at_left B](g)"
assumes cont: "continuous_on {A..<B} f"
assumes meas: "set_borel_measurable borel {A<..<B} f"
assumes "interval_lebesgue_integrable lborel A B g"
assumes "A < B"
shows   "interval_lebesgue_integrable lborel A B f"
proof -
from assms(1) obtain c where c: "c > 0" "eventually (λx. norm (f x) ≤ c * norm (g x)) (at_left B)"
by (elim landau_o.bigE)
then obtain B' where B': "B' < B" "⋀x. x ∈ {B'<..<B} ⟹ norm (f x) ≤ c * norm (g x)"
using ‹A < B› by (auto simp: Topological_Spaces.eventually_at_left[of A])

show ?thesis
proof (rule interval_lebesgue_integrable_combine)
show "interval_lebesgue_integrable lborel A (max A B') f"
using B' assms
by (intro interval_integrable_continuous_on continuous_on_subset[OF cont]) auto
show "set_borel_measurable borel (einterval (ereal A) (ereal B)) f"
using assms by simp
have meas': "set_borel_measurable borel {max A B'<..<B} f"
by (rule set_borel_measurable_subset[OF meas]) auto
have "set_integrable lborel {max A B'<..<B} f"
proof (rule set_integrable_bound[OF _ _ AE_I2[OF impI]])
have "set_integrable lborel {A<..<B} (λx. c * g x)"
using assms by (simp add: interval_lebesgue_integrable_def)
thus "set_integrable lborel {max A B'<..<B} (λx. c * g x)"
by (rule set_integrable_subset) auto
next
fix x assume "x ∈ {max A B'<..<B}"
hence "norm (f x) ≤ c * norm (g x)"
by (intro B') auto
also have "… ≤ norm (c * g x)"
unfolding norm_mult by (intro mult_right_mono) auto
finally show  "norm (f x) ≤ norm (c * g x)" .
qed (use meas' in ‹simp_all add: set_borel_measurable_def›)
thus "interval_lebesgue_integrable lborel (ereal (max A B')) (ereal B) f"
unfolding interval_lebesgue_integrable_def einterval_eq_Icc using ‹B' < B› assms by simp
qed (use B' assms in auto)
qed

lemma interval_lebesgue_integrable_bigo_left:
fixes A B :: real
fixes f :: "real ⇒ real"
assumes "f ∈ O[at_right A](g)"
assumes cont: "continuous_on {A<..B} f"
assumes meas: "set_borel_measurable borel {A<..<B} f"
assumes "interval_lebesgue_integrable lborel A B g"
assumes "A < B"
shows   "interval_lebesgue_integrable lborel A B f"
proof -
from assms(1) obtain c where c: "c > 0" "eventually (λx. norm (f x) ≤ c * norm (g x)) (at_right A)"
by (elim landau_o.bigE)
then obtain A' where A': "A' > A" "⋀x. x ∈ {A<..<A'} ⟹ norm (f x) ≤ c * norm (g x)"
using ‹A < B› by (auto simp: Topological_Spaces.eventually_at_right[of A])

show ?thesis
proof (rule interval_lebesgue_integrable_combine)
show "interval_lebesgue_integrable lborel (min B A') B f"
using A' assms
by (intro interval_integrable_continuous_on continuous_on_subset[OF cont]) auto
show "set_borel_measurable borel (einterval (ereal A) (ereal B)) f"
using assms by simp
have meas': "set_borel_measurable borel {A<..<min B A'} f"
by (rule set_borel_measurable_subset[OF meas]) auto
have "set_integrable lborel {A<..<min B A'} f"
proof (rule set_integrable_bound[OF _ _ AE_I2[OF impI]])
have "set_integrable lborel {A<..<B} (λx. c * g x)"
using assms by (simp add: interval_lebesgue_integrable_def)
thus "set_integrable lborel {A<..<min B A'} (λx. c * g x)"
by (rule set_integrable_subset) auto
next
fix x assume "x ∈ {A<..<min B A'}"
hence "norm (f x) ≤ c * norm (g x)"
by (intro A') auto
also have "… ≤ norm (c * g x)"
unfolding norm_mult by (intro mult_right_mono) auto
finally show  "norm (f x) ≤ norm (c * g x)" .
qed (use meas' in ‹simp_all add: set_borel_measurable_def›)
thus "interval_lebesgue_integrable lborel (ereal A) (ereal (min B A')) f"
unfolding interval_lebesgue_integrable_def einterval_eq_Icc using ‹A' > A› assms by simp
qed (use A' assms in auto)
qed

subsection ‹Other material›

(* TODO: Library *)
lemma summable_comparison_test_bigo:
fixes f :: "nat ⇒ real"
assumes "summable (λn. norm (g n))" "f ∈ O(g)"
shows   "summable f"
proof -
from ‹f ∈ O(g)› obtain C where C: "eventually (λx. norm (f x) ≤ C * norm (g x)) at_top"
by (auto elim: landau_o.bigE)
thus ?thesis
by (rule summable_comparison_test_ev) (insert assms, auto intro: summable_mult)
qed

lemma fps_expansion_cong:
assumes "eventually (λx. g x = h x) (nhds x)"
shows   "fps_expansion g x = fps_expansion h x"
proof -
have "(deriv ^^ n) g x = (deriv ^^ n) h x" for n
by (intro higher_deriv_cong_ev assms refl)
thus ?thesis by (simp add: fps_expansion_def)
qed

lemma fps_expansion_eq_zero_iff:
assumes "g holomorphic_on ball z r" "r > 0"
shows   "fps_expansion g z = 0 ⟷ (∀z∈ball z r. g z = 0)"
proof
assume *: "∀z∈ball z r. g z = 0"
have "eventually (λw. w ∈ ball z r) (nhds z)"
using assms by (intro eventually_nhds_in_open) auto
hence "eventually (λz. g z = 0) (nhds z)"
by eventually_elim (use * in auto)
hence "fps_expansion g z = fps_expansion (λ_. 0) z"
by (intro fps_expansion_cong)
thus "fps_expansion g z = 0"
by (simp add: fps_expansion_def fps_zero_def)
next
assume *: "fps_expansion g z = 0"
have "g w = 0" if "w ∈ ball z r" for w
by (rule holomorphic_fun_eq_0_on_ball[OF assms(1) that])
(use * in ‹auto simp: fps_expansion_def fps_eq_iff›)
thus "∀w∈ball z r. g w = 0" by blast
qed

lemma fds_nth_higher_deriv:
"fds_nth ((fds_deriv ^^ k) F) = (λn. (-1) ^ k * of_real (ln n) ^ k * fds_nth F n)"
by (induction k) (auto simp: fds_nth_deriv fun_eq_iff simp flip: scaleR_conv_of_real)

lemma binomial_n_n_minus_one [simp]: "n > 0 ⟹ n choose (n - Suc 0) = n"
by (cases n) auto

lemma has_field_derivative_complex_powr_right:
"w ≠ 0 ⟹ ((λz. w powr z) has_field_derivative Ln w * w powr z) (at z within A)"
by (rule DERIV_subset, rule has_field_derivative_powr_right) auto

lemmas has_field_derivative_complex_powr_right' =
has_field_derivative_complex_powr_right[THEN DERIV_chain2]

end

# Theory Zeta_Function

(*
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
begin

subsection ‹Preliminary facts›

(* TODO Move once Landau symbols are in the distribution *)
lemma holomorphic_on_extend:
assumes "f holomorphic_on S - {ξ}" "ξ ∈ interior S" "f ∈ O[at ξ](λ_. 1)"
shows   "(∃g. g holomorphic_on S ∧ (∀z∈S - {ξ}. g z = f z))"
by (subst holomorphic_on_extend_bounded) (insert assms, auto elim!: landau_o.bigE)

lemma removable_singularities:
assumes "finite X" "X ⊆ interior S" "f holomorphic_on (S - X)"
assumes "⋀z. z ∈ X ⟹ f ∈ O[at z](λ_. 1)"
shows   "∃g. g holomorphic_on S ∧ (∀z∈S-X. g z = f z)"
using assms
proof (induction arbitrary: f rule: finite_induct)
case empty
thus ?case by auto
next
case (insert z0 X f)
from insert.prems and insert.hyps have z0: "z0 ∈ interior (S - X)"
by (auto simp: interior_diff finite_imp_closed)
hence "∃g. g holomorphic_on (S - X) ∧ (∀z∈S - X - {z0}. g z = f z)"
using insert.prems insert.hyps by (intro holomorphic_on_extend) auto
then obtain g where g: "g holomorphic_on (S - X)" "∀z∈S - X - {z0}. g z = f z" by blast
have "∃h. h holomorphic_on S ∧ (∀z∈S - X. h z = g z)"
proof (rule insert.IH)
fix z0' assume z0': "z0' ∈ X"
hence "eventually (λz. z ∈ interior S - (X - {z0'}) - {z0}) (nhds z0')"
using insert.prems insert.hyps
by (intro eventually_nhds_in_open open_Diff finite_imp_closed) auto
hence ev: "eventually (λz. z ∈ S - X - {z0}) (at z0')"
unfolding eventually_at_filter
by eventually_elim (insert z0' insert.hyps interior_subset[of S], auto)
have "g ∈ Θ[at z0'](f)"
by (intro bigthetaI_cong eventually_mono[OF ev]) (insert g, auto)
also have "f ∈ O[at z0'](λ_. 1)"
using z0' by (intro insert.prems) auto
finally show "g ∈ …" .
qed (insert insert.prems g, auto)
then obtain h where "h holomorphic_on S" "∀z∈S - X. h z = g z" by blast
with g have "h holomorphic_on S" "∀z∈S - insert z0 X. h z = f z" by auto
thus ?case by blast
qed

lemma continuous_imp_bigo_1:
assumes "continuous (at x within A) f"
shows   "f ∈ O[at x within A](λ_. 1)"
proof (rule bigoI_tendsto)
from assms show "((λx. f x / 1) ⤏ f x) (at x within A)"
by (auto simp: continuous_within)
qed auto

lemma taylor_bigo_linear:
assumes "f field_differentiable at x0 within A"
shows   "(λx. f x - f x0) ∈ O[at x0 within A](λx. x - x0)"
proof -
from assms obtain f' where "(f has_field_derivative f') (at x0 within A)"
by (auto simp: field_differentiable_def)
hence "((λx. (f x - f x0) / (x - x0)) ⤏ f') (at x0 within A)"
by (auto simp: has_field_derivative_iff)
thus ?thesis by (intro bigoI_tendsto[where c = f']) (auto simp: eventually_at_filter)
qed
(* END TODO *)

(* TODO Move? *)
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

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))+)
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"
unfolding zeta_def by (rule is_pole_hurwitz_zeta) auto

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 ∈ UNIV" "w ≠ 1"
thus "hurwitz_zeta a w = (pre_zeta a w * (w - 1) + a powr (1 - w)) * (w - 1) powr (of_int (-1))"
apply (subst (1) powr_of_int)
by (auto simp add: hurwitz_zeta_def field_simps)
qed (insert assms, 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

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]
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
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 * ln k))))"
(is "?a = ?b")
proof (intro fds_eqI, goal_cases)
case (1 n)
then consider "n = 1" | "n > 1" by force
hence "fds_nth ?a n = mangoldt n / ln (real n) * (2 + (n powr (𝗂 * a) + n powr (-𝗂 * a)))"
by cases (auto simp: field_simps scaleR_conv_of_real numeral_fds)
also have "n powr (𝗂 * a) + n powr (-𝗂 * a) = 2 * cos (of_real (a * ln n))"
using 1 by (subst cos_exp_eq) (simp_all add: powr_def algebra_simps)
also have "mangoldt n / ln (real n) * (2 + …) =
of_real (2 * mangoldt n / ln n * (1 + cos (a * ln n)))"
by (subst cos_of_real) simp_all
finally show ?case by (simp add: fds_nth_fds')
qed
finally show ?thesis .
qed
― ‹It is then obvious that this logarithm series has non-negative real coefficients.›
also have "nonneg_dirichlet_series …"
proof (standard, goal_cases)
case (1 n)
from cos_ge_minus_one[of "a * ln n"] have "1 + cos (a * ln (real n)) ≥ 0" by linarith
thus ?case using 1
by (cases "n = 0")
(auto simp: complex_nonneg_Reals_iff fds_nth_fds' mangoldt_nonneg
intro!: divide_nonneg_nonneg mult_nonneg_nonneg)
qed
― ‹Therefore, the original series also has non-negative real coefficients.›
finally have nonneg: "nonneg_dirichlet_series Q_fds"
by (rule nonneg_dirichlet_series_lnD) (auto simp: Q_fds_def)

― ‹By the Pringsheim--Landau theorem, a Dirichlet series with non-negative coefficnets that
can be analytically continued to the entire complex plane must converge everywhere, i.\,e.\
its abscissa of (absolute) convergence is $-\infty$:›
have abscissa_Q_fds: "abs_conv_abscissa Q_fds ≤ 1"
unfolding Q_fds_def by (auto intro!: abs_conv_abscissa_mult_leI abs_conv_abscissa_power_leI)
with nonneg and eval_Q_fds and ‹Q' holomorphic_on UNIV›
have abscissa: "abs_conv_abscissa Q_fds = -∞"
by (intro entire_continuation_imp_abs_conv_abscissa_MInfty[where c = 1 and g = Q'])
(auto simp: one_ereal_def)

― ‹This now leads to a contradiction in a very obvious way. If @{term Q_fds} is
absolutely convergent, then the subseries corresponding to powers of 2 (\i.e.
we delete all summands $a_n / n ^ s$ where $n$ is not a power of 2 from the sum) is
also absolutely convergent. We denote this series with $R$.›
define R_fds where "R_fds = fds_primepow_subseries 2 Q_fds"
have "conv_abscissa R_fds ≤ abs_conv_abscissa R_fds" by (rule conv_le_abs_conv_abscissa)
also have "abs_conv_abscissa R_fds ≤ abs_conv_abscissa Q_fds"
unfolding R_fds_def by (rule abs_conv_abscissa_restrict)
also have "… = -∞" by (simp add: abscissa)
finally have abscissa': "conv_abscissa R_fds = -∞" by simp

― ‹Since $\zeta(s)$ and $\zeta(s \pm ia)$ have an Euler product expansion for
$\mathfrak{R}(s) > 1$, we have
$R(s) = (1 - 2^{-s})^-2 (1 - 2^{-s+ia})^{-1} (1 - 2^{-s-ia})^{-1}$
there, and since $R$ converges everywhere and the right-hand side is holomorphic for
$\mathfrak{R}(s) > 0$, the equation is also valid for all $s$ with $\mathfrak{R}(s) > 0$
by analytic continuation.›
have eval_R: "eval_fds R_fds s =
1 / ((1 - 2 powr -s) ^ 2 * (1 - 2 powr (-s + 𝗂 * a)) * (1 - 2 powr (-s - 𝗂 * a)))"
(is "_ = ?f s") if "Re s > 0" for s
proof -
show ?thesis
proof (rule analytic_continuation_open[where f = "eval_fds R_fds"])
show "?f holomorphic_on {s. Re s > 0}"
by (intro holomorphic_intros) (auto simp: powr_def exp_eq_1 Ln_Reals_eq)
next
fix z assume z: "z ∈ {s. Re s > 1}"
have [simp]: "completely_multiplicative_function (fds_nth fds_zeta)" by standard auto
thus "eval_fds R_fds z = ?f z" using z
by (simp add: R_fds_def Q_fds_def eval_fds_mult eval_fds_power fds_abs_converges_mult
fds_abs_converges_power fds_primepow_subseries_euler_product_cm divide_simps
powr_minus powr_diff powr_add fds_abs_summable_zeta)
qed (insert that abscissa', auto intro!: exI[of _ 2] convex_connected open_halfspace_Re_gt
convex_halfspace_Re_gt holomorphic_intros)
qed

― ‹We now clearly have a contradiction: $R(s)$, being entire, is continuous everywhere,
while the function on the right-hand side clearly has a pole at $0$.›
show False
proof (rule not_tendsto_and_filterlim_at_infinity)
have "((λb. (1-2 powr - b)⇧2 * (1 - 2 powr (-b+𝗂*a)) * (1 - 2 powr (-b-𝗂*a))) ⤏ 0)
(at 0 within {s. Re s > 0})"
(is "filterlim ?f' _ _") by (intro tendsto_eq_intros) (auto)
moreover have "eventually (λs. s ∈ {s. Re s > 0}) (at 0 within {s. Re s > 0})"
by (auto simp: eventually_at_filter)
hence "eventually (λs. ?f' s ≠ 0) (at 0 within {s. Re s > 0})"
by eventually_elim (auto simp: powr_def exp_eq_1 Ln_Reals_eq)
ultimately have "filterlim ?f' (at 0) (at 0 within {s. Re s > 0})" by (simp add: filterlim_at)
hence "filterlim ?f at_infinity (at 0 within {s. Re s > 0})" (is ?lim)
by (intro filterlim_divide_at_infinity[OF tendsto_const]
tendsto_mult_filterlim_at_infinity) auto
also have ev: "eventually (λs. Re s > 0) (at 0 within {s. Re s > 0})"
by (auto simp: eventually_at intro!: exI[of _ 1])
have "?lim ⟷ filterlim (eval_fds R_fds) at_infinity (at 0 within {s. Re s > 0})"
by (intro filterlim_cong refl eventually_mono[OF ev]) (auto simp: eval_R)
finally show … .
next
have "continuous (at 0 within {s. Re s > 0}) (eval_fds R_fds)"
by (intro continuous_intros) (auto simp: abscissa')
thus "((eval_fds R_fds ⤏ eval_fds R_fds 0)) (at 0 within {s. Re s > 0})"
by (auto simp: continuous_within)
next
have "0 ∈ {s. Re s ≥ 0}" by simp
also have "{s. Re s ≥ 0} = closure {s. Re s > 0}"
using closure_halfspace_gt[of "1::complex" 0] by (simp add: inner_commute)
finally have "0 ∈ …" .
thus "at 0 within {s. Re s > 0} ≠ bot"
by (subst at_within_eq_bot_iff) auto
qed
qed
qed (fact zeta_Re_gt_1_nonzero)

subsection ‹Special values of the $\zeta$ functions›

theorem hurwitz_zeta_neg_of_nat:
assumes "a > 0"
shows   "hurwitz_zeta a (-of_nat n) = -bernpoly (Suc n) a / of_nat (Suc n)"
proof -
have "-of_nat n ≠ (1::complex)" by (simp add: complex_eq_iff)
hence "hurwitz_zeta a (-of_nat n) =
pre_zeta a (-of_nat n) + a powr real (Suc n) / (-of_nat (Suc n))"
unfolding zeta_def hurwitz_zeta_def using assms by (simp add: powr_of_real [symmetric])
also have "a powr real (Suc n) / (-of_nat (Suc n)) = - (a powr real (Suc n) / of_nat (Suc n))"
by (simp add: divide_simps del: of_nat_Suc)
also have "a powr real (Suc n) = a ^ Suc n"
using assms by (intro powr_realpow)
also have "pre_zeta a (-of_nat n) = pre_zeta_aux (Suc n) a (- of_nat n)"
using assms by (intro pre_zeta_aux_eq_pre_zeta [symmetric]) auto
also have "… = of_real a powr of_nat n / 2 +
(∑i = 1..Suc n. (bernoulli (2 * i) / fact (2 * i)) *⇩R
(pochhammer (- of_nat n) (2 * i - 1) *
of_real a powr (of_nat n - of_nat (2 * i - 1)))) +
EM_remainder (Suc (2 * Suc n)) (λx. - (pochhammer (- of_nat n)
(2*n+3) * of_real (x + a) powr (- of_nat n - 3))) 0"
(is "_ = ?B + sum (λn. ?f (2 * n)) _ + _")
unfolding pre_zeta_aux_def by (simp add: add_ac eval_nat_numeral)
also have "?B = of_real (a ^ n) / 2"
using assms by (subst powr_Reals_eq) (auto simp: powr_realpow)
also have "pochhammer (-of_nat n :: complex) (2*n+3) = 0"
by (subst pochhammer_eq_0_iff) auto
finally have "hurwitz_zeta a (-of_nat n) =
- (a ^ Suc n / of_nat (Suc n)) + (a ^ n / 2 + sum (λn. ?f (2 * n)) {1..Suc n})"
by simp

also have "sum (λn. ?f (2 * n)) {1..Suc n} = sum ?f ((*) 2  {1..Suc n})"
by (intro sum.reindex_bij_witness[of _ "λi. i div 2" "λi. 2*i"]) auto
also have "… = (∑i=2..2*n+2. ?f i)"
proof (intro sum.mono_neutral_left ballI, goal_cases)
case (3 i)
hence "odd i" "i ≠ 1" by (auto elim!: evenE)
thus ?case by (simp add: bernoulli_odd_eq_0)
qed auto
also have "… = (∑i=2..Suc n. ?f i)"
proof (intro sum.mono_neutral_right ballI, goal_cases)
case (3 i)
hence "pochhammer (-of_nat n :: complex) (i - 1) = 0"
by (subst pochhammer_eq_0_iff) auto
thus ?case by simp
qed auto
also have "… = (∑i=Suc 1..Suc n. -of_real (real (Suc n choose i) * bernoulli i *
a ^ (Suc n - i)) / of_nat (Suc n))"
(is "sum ?lhs _ = sum ?f _")
proof (intro sum.cong, goal_cases)
case (2 i)
hence "of_nat n - of_nat (i - 1) = (of_nat (Suc n - i) :: complex)"
by (auto simp: of_nat_diff)
also have "of_real a powr … = of_real (a ^ (Suc n - i))"
using 2 assms by (subst powr_nat) auto
finally have A: "of_real a powr (of_nat n - of_nat (i - 1)) = …" .
have "pochhammer (-of_nat n) (i - 1) = complex_of_real (pochhammer (-real n) (i - 1))"
by (simp add: pochhammer_of_real [symmetric])
also have "pochhammer (-real n) (i - 1) = pochhammer (-of_nat (Suc n)) i / (-1 - real n)"
using 2 by (subst (2) pochhammer_rec_if) auto
also have "-1 - real n = -real (Suc n)" by simp
finally have B: "pochhammer (-of_nat n) (i - 1) =
-complex_of_real (pochhammer (-real (Suc n)) i / real (Suc n))"
by (simp del: of_nat_Suc)
have "?lhs i = -complex_of_real (bernoulli i * pochhammer (-real (Suc n)) i / fact i *
a ^ (Suc n - i)) / of_nat (Suc n)"
by (simp only: A B) (simp add: scaleR_conv_of_real)
also have "bernoulli i * pochhammer (-real (Suc n)) i / fact i =
(real (Suc n) gchoose i) * bernoulli i" using 2
by (subst gbinomial_pochhammer) (auto simp: minus_one_power_iff bernoulli_odd_eq_0)
also have "real (Suc n) gchoose i = Suc n choose i"
by (subst binomial_gbinomial) auto
finally show ?case by simp
qed auto
also have "a ^ n / 2 + sum ?f {Suc 1..Suc n} = sum ?f {1..Suc n}"
by (subst (2) sum.atLeast_Suc_atMost) (simp_all add: scaleR_conv_of_real del: of_nat_Suc)
also have "-(a ^ Suc n / of_nat (Suc n)) + sum ?f {1..Suc n} = sum ?f {0..Suc n}"
by (subst (2) sum.atLeast_Suc_atMost) (simp_all add: scaleR_conv_of_real)
also have "… = - bernpoly (Suc n) a / of_nat (Suc n)"
unfolding sum_negf sum_divide_distrib [symmetric] by (simp add: bernpoly_def atLeast0AtMost)
finally show ?thesis .
qed

lemma hurwitz_zeta_0 [simp]: "a > 0 ⟹ hurwitz_zeta a 0 = 1 / 2 - a"
using hurwitz_zeta_neg_of_nat[of a 0] by (simp add: bernpoly_def)

lemma zeta_0 [simp]: "zeta 0 = -1 / 2"
by (simp add: zeta_def)

theorem zeta_neg_of_nat:
"zeta (-of_nat n) = -of_real (bernoulli' (Suc n)) / of_nat (Suc n)"
unfolding zeta_def by (simp add: hurwitz_zeta_neg_of_nat bernpoly_1')

corollary zeta_trivial_zero:
assumes "even n" "n ≠ 0"
shows   "zeta (-of_nat n) = 0"
using zeta_neg_of_nat[of n] assms by (simp add: bernoulli'_odd_eq_0)

theorem zeta_even_nat:
"zeta (2 * of_nat n) =
of_real ((-1) ^ Suc n * bernoulli (2 * n) * (2 * pi) ^ (2 * n) / (2 * fact (2 * n)))"
proof (cases "n = 0")
case False
hence "(λk. 1 / of_nat (Suc k) ^ (2 * n)) sums zeta (of_nat (2 * n))"
by (intro sums_zeta_nat) auto
from sums_unique2 [OF this nat_even_power_sums_complex] False show ?thesis by simp
qed (insert zeta_neg_of_nat[of 0], simp_all)

corollary zeta_even_numeral:
"zeta (numeral (Num.Bit0 n)) = of_real
((- 1) ^ Suc (numeral n) * bernoulli (numeral (num.Bit0 n)) *
(2 * pi) ^ numeral (num.Bit0 n) / (2 * fact (numeral (num.Bit0 n))))" (is "_ = ?rhs")
proof -
have *: "(2 * numeral n :: nat) = numeral (Num.Bit0 n)"
by (subst numeral.numeral_Bit0, subst mult_2, rule refl)
have "numeral (Num.Bit0 n) = (2 * numeral n :: complex)"
by (subst numeral.numeral_Bit0, subst mult_2, rule refl)
also have "… = 2 * of_nat (numeral n)" by (simp only: of_nat_numeral of_nat_mult)
also have "zeta … = ?rhs" by (subst zeta_even_nat) (simp only: *)
finally show ?thesis .
qed

corollary zeta_neg_even_numeral [simp]: "zeta (-numeral (Num.Bit0 n)) = 0"
proof -
have "-numeral (Num.Bit0 n) = (-of_nat (numeral (Num.Bit0 n)) :: complex)"
by simp
also have "zeta … = 0"
proof (rule zeta_trivial_zero)
have "numeral (Num.Bit0 n) = (2 * numeral n :: nat)"
by (subst numeral.numeral_Bit0, subst mult_2, rule refl)
also have "even …" by (rule dvd_triv_left)
finally show "even (numeral (Num.Bit0 n) :: nat)" .
qed auto
finally show ?thesis .
qed

corollary zeta_neg_numeral:
"zeta (-numeral n) =
-of_real (bernoulli' (numeral (Num.inc n)) / numeral (Num.inc n))"
proof -
have "-numeral n = (- of_nat (numeral n) :: complex)"
by simp
also have "zeta … = -of_real (bernoulli' (numeral (Num.inc n)) / numeral (Num.inc n))"
by (subst zeta_neg_of_nat) (simp add: numeral_inc)
finally show ?thesis .
qed

corollary zeta_neg1: "zeta (-1) = - 1 / 12"
using zeta_neg_of_nat[of 1] by (simp add: eval_bernoulli)

corollary zeta_neg3: "zeta (-3) = 1 / 120"
by (simp add: zeta_neg_numeral)

corollary zeta_neg5: "zeta (-5) = - 1 / 252"
by (simp add: zeta_neg_numeral)

corollary zeta_2: "zeta 2 = pi ^ 2 / 6"
by (simp add: zeta_even_numeral)

corollary zeta_4: "zeta 4 = pi ^ 4 / 90"
by (simp add: zeta_even_numeral fact_num_eq_if)

corollary zeta_6: "zeta 6 = pi ^ 6 / 945"
by (simp add: zeta_even_numeral fact_num_eq_if)

corollary zeta_8: "zeta 8 = pi ^ 8 / 9450"
by (simp add: zeta_even_numeral fact_num_eq_if)

subsection ‹Integral relation between $\Gamma$ and $\zeta$ function›

lemma
assumes z: "Re z > 0" and a: "a > 0"
shows   Gamma_hurwitz_zeta_aux_integral:
"Gamma z / (of_nat n + of_real a) powr z =
(∫s∈{0<..}. (s powr (z - 1) / exp ((n+a) * s)) ∂lebesgue)"
and   Gamma_hurwitz_zeta_aux_integrable:
"set_integrable lebesgue {0<..} (λs. s powr (z - 1) / exp ((n+a) * s))"
proof -
note integrable = absolutely_integrable_Gamma_integral' [OF z]
let ?INT = "set_lebesgue_integral lebesgue {0<..} :: (real ⇒ complex) ⇒ complex"
let ?INT' = "set_lebesgue_integral lebesgue {0<..} :: (real ⇒ real) ⇒ real"

have meas1: "set_borel_measurable lebesgue {0<..}
(λx. of_real x powr (z - 1) / of_real (exp ((n+a) * x)))"
unfolding set_borel_measurable_def
by (intro measurable_completion, subst measurable_lborel2,
intro borel_measurable_continuous_on_indicator) (auto intro!: continuous_intros)
show integrable1: "set_integrable lebesgue {0<..}
(λs. s powr (z - 1) / exp ((n+a) * s))"
using assms by (intro absolutely_integrable_Gamma_integral) auto
from assms have pos: "0 < real n + a" by (simp add: add_nonneg_pos)
hence "complex_of_real 0 ≠ of_real (real n + a)" by (simp only: of_real_eq_iff)
also have "complex_of_real (real n + a) = of_nat n + of_real a" by simp
finally have nz: "… ≠ 0" by auto

have "((λt. complex_of_real t powr (z - 1) / of_real (exp t)) has_integral Gamma z) {0<..}"
by (rule Gamma_integral_complex') fact+
hence "Gamma z = ?INT (λt. t powr (z - 1) / of_real (exp t))"
using set_lebesgue_integral_eq_integral(2) [OF integrable]
by (simp add: has_integral_iff exp_of_real)
also have "lebesgue = density (distr lebesgue lebesgue (λt. (real n+a) * t))
(λx. ennreal (real n+a))"
using lebesgue_real_scale[of "real n + a"] pos by auto
also have "set_lebesgue_integral … {0<..} (λt. of_real t powr (z - 1) / of_real (exp t)) =
set_lebesgue_integral (distr lebesgue lebesgue (λt. (real n + a) * t)) {0<..}
(λt. (real n + a) * t powr (z - 1) / exp t)" using integrable pos
unfolding set_lebesgue_integral_def
by (subst integral_density) (simp_all add: exp_of_real algebra_simps scaleR_conv_of_real set_integrable_def)
also have "… = ?INT (λs. (n + a) * (of_real (n+a) * of_real s) powr (z - 1) /
of_real (exp ((n+a) * s)))"
unfolding set_lebesgue_integral_def
proof (subst integral_distr)
show "(*) (real n + a) ∈ lebesgue →⇩M lebesgue"
using lebesgue_measurable_scaling[of "real n + a", where ?'a = real]
unfolding real_scaleR_def .
next
have "(λx. (n+a) * (indicator {0<..} x *⇩R (of_real x powr (z - 1) / of_real (exp x))))
∈ lebesgue →⇩M borel"
using integrable unfolding set_integrable_def by (intro borel_measurable_times) simp_all
thus "(λx. indicator {0<..} x *⇩R
(complex_of_real (real n + a) * complex_of_real x powr (z - 1) / exp x))
∈ borel_measurable lebesgue" by simp
qed (intro Bochner_Integration.integral_cong refl, insert pos,
auto simp: indicator_def zero_less_mult_iff)
also have "… = ?INT (λs. ((n+a) powr z) * (s powr (z - 1) / exp ((n+a) * s)))" using pos
by (intro set_lebesgue_integral_cong refl allI impI, simp, subst powr_times_real)
(auto simp: powr_diff)
also have "… = (n + a) powr z * ?INT (λs. s powr (z - 1) / exp ((n+a) * s))"
unfolding set_lebesgue_integral_def
by (subst integral_mult_right_zero [symmetric]) simp_all
finally show "Gamma z / (of_nat n + of_real a) powr z =
?INT (λs. s powr (z - 1) / exp ((n+a) * s))"
using nz by (auto simp add: field_simps)
qed

lemma
assumes x: "x > 0" and "a > 0"
shows   Gamma_hurwitz_zeta_aux_integral_real:
"Gamma x / (real n + a) powr x =
set_lebesgue_integral lebesgue {0<..}
(λs. s powr (x - 1) / exp ((real n + a) * s))"
and   Gamma_hurwitz_zeta_aux_integrable_real:
"set_integrable lebesgue {0<..} (λs. s powr (x - 1) / exp ((real n + a) * s))"
proof -
show "set_integrable lebesgue {0<..} (λs. s powr (x - 1) / exp ((real n + a) * s))"
using absolutely_integrable_Gamma_integral[of "of_real x" "real n + a"]
unfolding set_integrable_def
proof (rule Bochner_Integration.integrable_bound, goal_cases)
case 3
have "set_integrable lebesgue {0<..} (λxa. complex_of_real xa powr (of_real x - 1) /
of_real (exp ((n + a) * xa)))"
using assms by (intro Gamma_hurwitz_zeta_aux_integrable) auto
also have "?this ⟷ integrable lebesgue
(λs. complex_of_real (indicator {0<..} s *⇩R (s powr (x - 1) / (exp ((n+a) * s)))))"
unfolding set_integrable_def
by (intro Bochner_Integration.integrable_cong refl) (auto simp: powr_Reals_eq indicator_def)
finally have "set_integrable lebesgue {0<..} (λs. s powr (x - 1) / exp ((n+a) * s))"
unfolding set_integrable_def complex_of_real_integrable_eq .
thus ?case
by (simp add: set_integrable_def)
qed (insert assms, auto intro!: AE_I2 simp: indicator_def norm_divide norm_powr_real_powr)
from Gamma_hurwitz_zeta_aux_integral[of "of_real x" a n] and assms
have "of_real (Gamma x / (real n + a) powr x) = set_lebesgue_integral lebesgue {0<..}
(λs. complex_of_real s powr (of_real x - 1) / of_real (exp ((n+a) * s)))" (is "_ = ?I")
by (auto simp: Gamma_complex_of_real powr_Reals_eq)
also have "?I = lebesgue_integral lebesgue
(λs. of_real (indicator {0<..} s *⇩R (s powr (x - 1) / exp ((n+a) * s))))"
unfolding set_lebesgue_integral_def
using assms by (intro Bochner_Integration.integral_cong refl)
(auto simp: indicator_def powr_Reals_eq)
also have "… = of_real (set_lebesgue_integral lebesgue {0<..}
(λs. s powr (x - 1) / exp ((n+a) * s)))"
unfolding set_lebesgue_integral_def
by (rule Bochner_Integration.integral_complex_of_real)
finally show "Gamma x / (real n + a) powr x = set_lebesgue_integral lebesgue {0<..}
(λs. s powr (x - 1) / exp ((real n + a) * s))"
by (subst (asm) of_real_eq_iff)
qed

theorem
assumes "Re z > 1" and "a > (0::real)"
shows   Gamma_times_hurwitz_zeta_integral: "Gamma z * hurwitz_zeta a z =
(∫x∈{0<..}. (of_real x powr (z - 1) * of_real (exp (-a*x) / (1 - exp (-x)))) ∂lebesgue)"
and   Gamma_times_hurwitz_zeta_integrable:
"set_integrable lebesgue {0<..}
(λx. of_real x powr (z - 1) * of_real (exp (-a*x) / (1 - exp (-x))))"
proof -
from assms have z: "Re z > 0" by simp
let ?INT = "set_lebesgue_integral lebesgue {0<..} :: (real ⇒ complex) ⇒ complex"
let ?INT' = "set_lebesgue_integral lebesgue {0<..} :: (real ⇒ real) ⇒ real"

have 1: "complex_set_integrable lebesgue {0<..}
(λx. of_real x powr (z - 1) / of_real (exp ((real n + a) * x)))" for n
by (rule Gamma_hurwitz_zeta_aux_integrable) (use assms in simp_all)
have 2: "summable (λn. norm (indicator {0<..} s *⇩R (of_real s powr (z - 1) /
of_real (exp ((n + a) * s)))))" for s
proof (cases "s > 0")
case True
hence "summable (λn. norm (of_real s powr (z - 1)) * exp (-a * s) * exp (-s) ^ n)"
using assms by (intro summable_mult summable_geometric) simp_all
with True show ?thesis
by (simp add: norm_mult norm_divide exp_add exp_diff
exp_minus field_simps exp_of_nat_mult [symmetric])
qed simp_all
have 3: "summable (λn. ∫x. norm (indicator {0<..} x *⇩R (complex_of_real x powr (z - 1) /
complex_of_real (exp ((n + a) * x)))) ∂lebesgue)"
proof -
have "summable (λn. Gamma (Re z) * (real n + a) powr -Re z)"
using assms by (intro summable_mult summable_hurwitz_zeta_real) simp_all
also have "?this ⟷ summable (λn. ?INT' (λs. norm (of_real s powr (z - 1) /
of_real (exp ((n+a) * s)))))"
proof (intro summable_cong always_eventually allI, goal_cases)
case (1 n)
have "Gamma (Re z) * (real n + a) powr -Re z = Gamma (Re z) / (real n + a) powr Re z"
by (subst powr_minus) (simp_all add: field_simps)
also from assms have "… = (∫x∈{0<..}. (x powr (Re z-1) / exp ((n+a) * x)) ∂lebesgue)"
by (subst Gamma_hurwitz_zeta_aux_integral_real) simp_all
also have "… = (∫xa∈{0<..}. norm (of_real xa powr (z-1) / of_real (exp ((n+a) * xa)))
∂lebesgue)"
unfolding set_lebesgue_integral_def
by (intro Bochner_Integration.integral_cong refl)
(auto simp: indicator_def norm_divide norm_powr_real_powr)
finally show ?case .
qed
finally show ?thesis
by (simp add: set_lebesgue_integral_def)
qed

have sum_eq: "(∑n. indicator {0<..} s *⇩R (of_real s powr (z - 1) / of_real (exp ((n+a) * s)))) =
indicator {0<..} s *⇩R (of_real s powr (z - 1) *
of_real (exp (-a * s) / (1 - exp (-s))))" for s
proof (cases "s > 0")
case True
hence "(∑n. indicator {0..} s *⇩R (of_real s powr (z - 1) / of_real (exp ((n+a) * s)))) =
(∑n. of_real s powr (z - 1) * of_real (exp (-a * s)) * of_real (exp (-s)) ^ n)"
by (intro suminf_cong)
(auto simp: exp_add exp_minus exp_of_nat_mult [symmetric] field_simps of_real_exp)
also have "(∑n. of_real s powr (z - 1) * of_real (exp (-a * s)) * of_real (exp (-s)) ^ n) =
of_real s powr (z - 1) * of_real (exp (-a * s)) * (∑n. of_real (exp (-s)) ^ n)"
using True by (intro suminf_mult summable_geometric) simp_all
also have "(∑n. complex_of_real (exp (-s)) ^ n) = 1 / (1 - of_real (exp (-s)))"
using True by (intro suminf_geometric) auto
also have "of_real s powr (z - 1) * of_real (exp (-a * s)) * … =
of_real s powr (z - 1) * of_real (exp (-a * s) / (1 - exp (-s)))" using ‹a > 0›
by (auto simp add: divide_simps exp_minus)
finally show ?thesis using True by simp
qed simp_all

show "set_integrable lebesgue {0<..}
(λx. of_real x powr (z - 1) * of_real (exp (-a*x) / (1 - exp (-x))))"
using 1 unfolding sum_eq [symmetric] set_integrable_def
by (intro integrable_suminf[OF _ AE_I2] 2 3)

have "(λn. ?INT (λs. s powr (z - 1) / exp ((n+a) * s))) sums lebesgue_integral lebesgue
(λs. ∑n. indicator {0<..} s *⇩R (s powr (z - 1) / exp ((n+a) * s)))" (is "?A sums ?B")
using 1 unfolding set_lebesgue_integral_def set_integrable_def
by (rule sums_integral[OF _ AE_I2[OF 2] 3])
also have "?A = (λn. Gamma z * (n + a) powr -z)"
using assms by (subst Gamma_hurwitz_zeta_aux_integral [symmetric])
(simp_all add: powr_minus divide_simps)
also have "?B = ?INT (λs. of_real s powr (z - 1) * of_real (exp (-a * s) / (1 - exp (-s))))"
unfolding sum_eq set_lebesgue_integral_def ..
finally have "(λn. Gamma z * (of_nat n + of_real a) powr -z) sums
?INT (λx. of_real x powr (z - 1) * of_real (exp (-a * x) / (1 - exp (-x))))"
by simp
moreover have "(λn. Gamma z * (of_nat n + of_real a) powr -z) sums (Gamma z * hurwitz_zeta a z)"
using assms by (intro sums_mult sums_hurwitz_zeta) simp_all
ultimately show "Gamma z * hurwitz_zeta a z =
(∫x∈{0<..}. (of_real x powr (z - 1) *
of_real (exp (-a * x) / (1 - exp (-x)))) ∂lebesgue)"
by (rule sums_unique2 [symmetric])
qed

corollary
assumes "Re z > 1"
shows   Gamma_times_zeta_integral: "Gamma z * zeta z =
(∫x∈{0<..}. (of_real x powr (z - 1) / of_real (exp x - 1)) ∂lebesgue)" (is ?th1)
and   Gamma_times_zeta_integrable:
"set_integrable lebesgue {0<..}
(λx. of_real x powr (z - 1) / of_real (exp x - 1))" (is ?th2)
proof -
have *: "(λx. indicator {0<..} x *⇩R (of_real x powr (z - 1) *
of_real (exp (-x) / (1 - exp (-x))))) =
(λx. indicator {0<..} x *⇩R (of_real x powr (z - 1) / of_real (exp x - 1)))"
by (intro ext) (simp add: field_simps exp_minus indicator_def)
from Gamma_times_hurwitz_zeta_integral [OF assms zero_less_one] and *
show ?th1 by (simp add: zeta_def set_lebesgue_integral_def)
from Gamma_times_hurwitz_zeta_integrable [OF assms zero_less_one] and *
show ?th2 by (simp add: zeta_def set_integrable_def)
qed

corollary hurwitz_zeta_integral_Gamma_def:
assumes "Re z > 1" "a > 0"
shows   "hurwitz_zeta a z =
rGamma z * (∫x∈{0<..}. (of_real x powr (z - 1) *
of_real (exp (-a * x) / (1 - exp (-x)))) ∂lebesgue)"
proof -
from assms have "Gamma z ≠ 0"
by (subst Gamma_eq_zero_iff) (auto elim!: nonpos_Ints_cases)
with Gamma_times_hurwitz_zeta_integral [OF assms] show ?thesis
by (simp add: rGamma_inverse_Gamma field_simps)
qed

corollary zeta_integral_Gamma_def:
assumes "Re z > 1"
shows   "zeta z =
rGamma z * (∫x∈{0<..}. (of_real x powr (z - 1) / of_real (exp x - 1)) ∂lebesgue)"
proof -
from assms have "Gamma z ≠ 0"
by (subst Gamma_eq_zero_iff) (auto elim!: nonpos_Ints_cases)
with Gamma_times_zeta_integral [OF assms] show ?thesis
by (simp add: rGamma_inverse_Gamma field_simps)
qed

lemma Gamma_times_zeta_has_integral:
assumes "Re z > 1"
shows   "((λx. x powr (z - 1) / (of_real (exp x) - 1)) has_integral (Gamma z * zeta z)) {0<..}"
(is "(?f has_integral _) _")
proof -
have "(?f has_integral set_lebesgue_integral lebesgue {0<..} ?f) {0<..}"
using Gamma_times_zeta_integrable[OF assms]
by (intro has_integral_set_lebesgue) auto
also have "set_lebesgue_integral lebesgue {0<..} ?f = Gamma z * zeta z"
using Gamma_times_zeta_integral[OF assms] by simp
finally show ?thesis .
qed

lemma Gamma_times_zeta_has_integral_real:
fixes z :: real
assumes "z > 1"
shows   "((λx. x powr (z - 1) / (exp x - 1)) has_integral (Gamma z * Re (zeta z))) {0<..}"
proof -
from assms have *: "Re (of_real z) > 1" by simp
have "((λx. Re (complex_of_real x powr (complex_of_real z - 1)) / (exp x - 1)) has_integral
Gamma z * Re (zeta (complex_of_real z))) {0<..}"
using has_integral_linear[OF Gamma_times_zeta_has_integral[OF *] bounded_linear_Re]
by (simp add: o_def Gamma_complex_of_real)
also have "?this ⟷ ?thesis"
using assms by (intro has_integral_cong) (auto simp: powr_Reals_eq)
finally show ?thesis .
qed

lemma Gamma_integral_real':
assumes x: "x > (0 :: real)"
shows   "((λt. t powr (x - 1) / exp t) has_integral Gamma x) {0<..}"
using Gamma_integral_real[OF assms] by (subst has_integral_closure [symmetric]) auto

subsection ‹An analytic proof of the infinitude of primes›

text ‹
We can now also do an analytic proof of the infinitude of primes.
›
lemma primes_infinite_analytic: "infinite {p :: nat. prime p}"
proof
― ‹Suppose the set of primes were finite.›
define P :: "nat set" where "P = {p. prime p}"
assume fin: "finite P"

― ‹Then the Euler product form of the $\zeta$ function ranges over a finite set,
and since each factor is holomorphic in the positive real half-space,
the product is, too.›
define zeta' :: "complex ⇒ complex"
where "zeta' = (λs. (∏p∈P. inverse (1 - 1 / of_nat p powr s)))"
have holo: "zeta' holomorphic_on A" if "A ⊆ {s. Re s > 0}" for A
proof -
{
fix p :: nat and s :: complex assume p: "p ∈ P" and s: "s ∈ A"
from p have p': "real p > 1"
by (subst of_nat_1 [symmetric], subst of_nat_less_iff) (simp add: prime_gt_Suc_0_nat P_def)
have "norm (of_nat p powr s) = real p powr Re s"
by (simp add: norm_powr_real_powr)
also have "… > real p powr 0" using p p' s that
by (subst powr_less_cancel_iff) (auto simp: prime_gt_1_nat)
finally have "of_nat p powr s ≠ 1" using p by (auto simp: P_def)
}
thus ?thesis by (auto simp: zeta'_def P_def intro!: holomorphic_intros)
qed

― ‹Since the Euler product expansion of $\zeta(s)$ is valid for all $s$ with
real value at least 1, and both $\zeta(s)$ and the Euler product must
be equal in the positive real half-space punctured at 1 by analytic
continuation.›
have eq: "zeta s = zeta' s" if "Re s > 0" "s ≠ 1" for s
proof (rule analytic_continuation_open[of "{s. Re s > 1}" "{s. Re s > 0} - {1}" zeta zeta'])
fix s assume s: "s ∈ {s. Re s > 1}"
let ?f = "(λn. ∏p≤n. if prime p then inverse (1 - 1 / of_nat p powr s) else 1)"
have "eventually (λn. ?f n = zeta' s) sequentially"
using eventually_ge_at_top[of "Max P"]
proof eventually_elim
case (elim n)
have "P ≠ {}" by (auto simp: P_def intro!: exI[of _ 2])
with elim have "P ⊆ {..n}" using fin by auto
thus ?case unfolding zeta'_def
by (intro prod.mono_neutral_cong_right) (auto simp: P_def)
qed
moreover from s have "?f ⇢ zeta s" by (intro euler_product_zeta) auto
ultimately have "(λ_. zeta' s) ⇢ zeta s"
by (blast intro: Lim_transform_eventually)
thus "zeta s = zeta' s" by (simp add: LIMSEQ_const_iff)
qed (auto intro!: exI[of _ 2] open_halfspace_Re_gt connected_open_delete convex_halfspace_Re_gt
holomorphic_intros holo that intro: convex_connected)

― ‹However, since the Euler product is holomorphic on the entire positive real
half-space, it cannot have a pole at 1, while $\zeta(s)$ does have a pole
at 1. Since they are equal in the punctured neighbourhood of 1, this is
have ev: "eventually (λs. s ∈ {s. Re s > 0} - {1}) (at 1)"
by (auto simp: eventually_at_filter intro!: open_halfspace_Re_gt
eventually_mono[OF eventually_nhds_in_open[of "{s. Re s > 0}"]])
have "¬is_pole zeta' 1"
by (rule not_is_pole_holomorphic [of "{s. Re s > 0}"]) (auto intro!: holo open_halfspace_Re_gt)
also have "is_pole zeta' 1 ⟷ is_pole zeta 1" unfolding is_pole_def
by (intro filterlim_cong refl eventually_mono [OF ev] eq [symmetric]) auto
finally show False using is_pole_zeta by contradiction
qed

subsection ‹The periodic zeta function›

text ‹
The periodic zeta function $F(s, q)$ (as described e.\,g.\ by Apostol~\cite{apostol1976analytic}
is related to the Hurwitz zeta function. It is periodic in ‹q› with period 1 and it can be
represented by a Dirichlet series that is absolutely convergent for $\mathfrak{R}(s) > 1$.
If ‹q ∉ ℤ›, it furthermore convergent for $\mathfrak{R}(s) > 0$.

It is clear that for integer ‹q›, we have $F(s, q) = F(s, 0) = \zeta(s)$. Moreover, for
non-integer ‹q›, $F(s, q)$ can be analytically continued to an entire function.
›
definition fds_perzeta :: "real ⇒ complex fds" where
"fds_perzeta q = fds (λm. exp (2 * pi * 𝗂 * m * q))"

text ‹
The definition of the periodic zeta function on the full domain is a bit unwieldy.
The precise reasoning for this definition will be given later, and, in any case, it
is probably more instructive to look at the derived alternative'' definitions later.
›
definition perzeta :: "real ⇒ complex ⇒ complex" where
"perzeta q' s =
(if q' ∈ ℤ then zeta s
else let q = frac q' in
if s = 0 then 𝗂 / (2 * pi) * (pre_zeta q 1 - pre_zeta (1 - q) 1 +
ln (1 - q) - ln q + pi * 𝗂)
else if s ∈ ℕ then eval_fds (fds_perzeta q) s
else complex_of_real (2 * pi) powr (s - 1) * 𝗂 * Gamma (1 - s) *
(𝗂 powr (-s) * hurwitz_zeta q (1 - s) -
𝗂 powr s * hurwitz_zeta (1 - q) (1 - s)))"

interpretation fds_perzeta: periodic_fun_simple' fds_perzeta
by standard (simp_all add: fds_perzeta_def exp_add ring_distribs exp_eq_polar
cis_mult [symmetric] cis_multiple_2pi)

interpretation perzeta: periodic_fun_simple' perzeta
proof -
have [simp]: "n + 1 ∈ ℤ ⟷ n ∈ ℤ" for n :: real
by (simp flip: frac_eq_0_iff add: frac.plus_1)
show "periodic_fun_simple' perzeta"
by standard (auto simp: fun_eq_iff perzeta_def Let_def frac.plus_1)
qed

lemma perzeta_frac [simp]: "perzeta (frac q) = perzeta q"
by (auto simp: perzeta_def fun_eq_iff Let_def)

lemma fds_perzeta_frac [simp]: "fds_perzeta (frac q) = fds_perzeta q"
using fds_perzeta.plus_of_int[of "frac q" "⌊q⌋"] by (simp add: frac_def)

lemma abs_conv_abscissa_perzeta: "abs_conv_abscissa (fds_perzeta q) ≤ 1"
proof (rule abs_conv_abscissa_leI)
fix c assume c: "ereal c > 1"
hence "summable (λn. n powr -c)"
by (simp add: summable_real_powr_iff)
also have "?this ⟷ fds_abs_converges (fds_perzeta q) (of_real c)" unfolding fds_abs_converges_def
by (intro summable_cong eventually_mono[OF eventually_gt_at_top[of 0]])
(auto simp: norm_divide norm_powr_real_powr fds_perzeta_def powr_minus field_simps)
finally show "∃s. s ∙ 1 = c ∧ fds_abs_converges (fds_perzeta q) s"
by (intro exI[of _ "of_real c"]) auto
qed

lemma conv_abscissa_perzeta: "conv_abscissa (fds_perzeta q) ≤ 1"
by (rule order.trans[OF conv_le_abs_conv_abscissa abs_conv_abscissa_perzeta])

lemma fds_perzeta__left_0 [simp]: "fds_perzeta 0 = fds_zeta"
by (simp add: fds_perzeta_def fds_zeta_def)

lemma perzeta_0_left [simp]: "perzeta 0 s = zeta s"
by (simp add: perzeta_def eval_fds_zeta)

lemma perzeta_int: "q ∈ ℤ ⟹ perzeta q = zeta"
by (simp add: perzeta_def fun_eq_iff)

lemma fds_perzeta_int: "q ∈ ℤ ⟹ fds_perzeta q = fds_zeta"
by (auto simp: fds_perzeta.of_int elim!: Ints_cases)

lemma sums_fds_perzeta:
assumes "Re s > 1"
shows   "(λm. exp (2 * pi * 𝗂 * Suc m * q) / of_nat (Suc m) powr s) sums
eval_fds (fds_perzeta q) s"
proof -
have "conv_abscissa (fds_perzeta q) ≤ 1" by (rule conv_abscissa_perzeta)
also have "… < ereal (Re s)"  using assms by (simp add: one_ereal_def)
finally have "fds_converges (fds_perzeta q) s" by (intro fds_converges) auto
hence "(λn. fds_nth (fds_perzeta q) (Suc n) / nat_power (Suc n) s) sums
eval_fds (fds_perzeta q) s" by (subst sums_Suc_iff) (auto simp: fds_converges_iff)
thus ?thesis by (simp add: fds_perzeta_def)
qed

lemma sum_tendsto_fds_perzeta:
assumes "Re s > 1"
shows   "(λn. ∑k∈{0<..n}. exp (2 * real k * pi * q * 𝗂) * of_nat k powr - s)
⇢ eval_fds (fds_perzeta q) s"
proof -
have "(λm. exp (2 * pi * 𝗂 * Suc m * q) / of_nat (Suc m) powr s) sums eval_fds (fds_perzeta q) s"
by (intro sums_fds_perzeta assms)
hence "(λn. ∑k<n. exp (2 * real (Suc k) * pi * q * 𝗂) * of_nat (Suc k) powr -s) ⇢
eval_fds (fds_perzeta q) s"
(is "filterlim ?f _ _") by (simp add: sums_def powr_minus field_simps)
also have "?f = (λn. ∑k∈{0<..n}. exp (2 * real k * pi * q * 𝗂) * of_nat k powr -s)"
by (intro ext sum.reindex_bij_betw sum.reindex_bij_witness[of _ "λn. n - 1" Suc]) auto
finally show ?thesis by simp
qed

text ‹
Using the geometric series, it is easy to see that the Dirichlet series for $F(s, q)$
has bounded partial sums for non-integer ‹q›, so it must converge for any ‹s› with
$\mathfrak{R}(s) > 0$.
›
lemma conv_abscissa_perzeta':
assumes "q ∉ ℤ"
shows   "conv_abscissa (fds_perzeta q) ≤ 0"
proof (rule conv_abscissa_leI)
fix c :: real assume c: "ereal c > 0"
have "fds_converges (fds_perzeta q) (of_real c)"
proof (rule bounded_partial_sums_imp_fps_converges)
define ω where "ω = exp (2 * pi * 𝗂 * q)"
have [simp]: "norm ω = 1" by (simp add: ω_def)
define M where "M = 2 / norm (1 - ω)"
from ‹q ∉ ℤ› have "ω ≠ 1"
by (auto simp: ω_def exp_eq_1)
hence "M > 0" by (simp add: M_def)

show "Bseq (λn. ∑k≤n. fds_nth (fds_perzeta q) k / nat_power k 0)"
unfolding Bseq_def
proof (rule exI, safe)
fix n :: nat
show "norm (∑k≤n. fds_nth (fds_perzeta q) k / nat_power k 0) ≤ M"
proof (cases "n = 0")
case False
have "(∑k≤n. fds_nth (fds_perzeta q) k / nat_power k 0) =
(∑k∈{1..1 + (n - 1)}. ω ^ k)" using False
by (intro sum.mono_neutral_cong_right)
(auto simp: fds_perzeta_def fds_nth_fds exp_of_nat_mult [symmetric] mult_ac ω_def)
also have "… = ω * (1 - ω ^ n) / (1 - ω)" using ‹ω ≠ 1› and False
by (subst sum_gp_offset) simp
also have "norm … ≤ 1 * (norm (1::complex) + norm (ω ^ n)) / norm (1 - ω)"
unfolding norm_mult norm_divide
by (intro mult_mono divide_right_mono norm_triangle_ineq4) auto
also have "… = M" by (simp add: M_def norm_power)
finally show ?thesis .
qed (use ‹M > 0› in simp_all)
qed fact+
qed (insert c, auto)
thus "∃s. s ∙ 1 = c ∧ fds_converges (fds_perzeta q) s"
by (intro exI[of _ "of_real c"]) auto
qed

lemma fds_perzeta_one_half: "fds_perzeta (1 / 2) = fds (λn. (-1) ^ n)"
using Complex.DeMoivre[of pi]
by (intro fds_eqI) (auto simp: fds_perzeta_def exp_eq_polar mult_ac)

lemma perzeta_one_half_1 [simp]: "perzeta (1 / 2) 1 = -ln 2"
proof (rule sums_unique2)
have *: "(1 / 2 :: real) ∉ ℤ"
using fraction_not_in_ints[of 2 1] by auto
have "fds_converges (fds_perzeta (1 / 2)) 1"
by (rule fds_converges, rule le_less_trans, rule conv_abscissa_perzeta') (use * in auto)
hence "(λn. (-1) ^ Suc n / Suc n) sums eval_fds (fds_perzeta (1 / 2)) 1"
unfolding fds_converges_altdef by (simp add: fds_perzeta_one_half)
also from * have "eval_fds (fds_perzeta (1 / 2)) 1 = perzeta (1 / 2) 1"
by (simp add: perzeta_def)
finally show "(λn. -complex_of_real ((-1) ^ n / Suc n)) sums perzeta (1 / 2) 1"
by simp
hence "(λn. -complex_of_real ((-1) ^ n / Suc n)) sums -of_real (ln 2)"
by (intro sums_minus sums_of_real alternating_harmonic_series_sums)
thus "(λn. -complex_of_real ((-1) ^ n / Suc n)) sums -(ln 2)"
by (simp flip: Ln_of_real)
qed

subsection ‹Hurwitz's formula›

text ‹
We now move on to prove Hurwitz's formula relating the Hurwitz zeta function and the
periodic zeta function. We mostly follow Apostol's proof, although we do make some small
changes in order to make the proof more amenable to Isabelle's complex analysis library.

The big difference is that Apostol integrates along a circle with a slit, where the two
sides of the slit lie on different branches of the integrand. This makes sense when looking
as the integrand as a Riemann surface, but we do not have a notion of Riemann surfaces in
Isabelle.

It is therefore much easier to simply cut the circle into an upper and a lower half. In fact,
the integral on the lower half can be reduced to the one on the upper half easily by
symmetry, so we really only need to handle the integral on the upper half. The integration
contour that we will use is therefore a semi-annulus in the upper half of the complex plane,
centred around the origin.

Now, first of all, we prove the existence of an important improper integral
that we will need later.
›
(* TODO: Move *)
lemma set_integrable_bigo:
fixes f g :: "real ⇒ 'a :: {banach, real_normed_field, second_countable_topology}"
assumes "f ∈ O(λx. g x)" and "set_integrable lborel {a..} g"
assumes "⋀b. b ≥ a ⟹ set_integrable lborel {a..<b} f"
assumes [measurable]: "set_borel_measurable borel {a..} f"
shows   "set_integrable lborel {a..} f"
proof -
from assms(1) obtain C x0 where C: "C > 0" "⋀x. x ≥ x0 ⟹ norm (f x) ≤ C * norm (g x)"
by (fastforce elim!: landau_o.bigE simp: eventually_at_top_linorder)
define x0' where "x0' = max a x0"

have "set_integrable lborel {a..<x0'} f"
by (intro assms) (auto simp: x0'_def)
moreover have "set_integrable lborel {x0'..} f" unfolding set_integrable_def
proof (rule Bochner_Integration.integrable_bound)
from assms(2) have "set_integrable lborel {x0'..} g"
by (rule set_integrable_subset) (auto simp: x0'_def)
thus "integrable lborel (λx. C *⇩R (indicator {x0'..} x *⇩R g x))" unfolding set_integrable_def
by (intro integrable_scaleR_right) (simp add: abs_mult norm_mult)
next
from assms(4) have "set_borel_measurable borel {x0'..} f"
by (rule set_borel_measurable_subset) (auto simp: x0'_def)
thus "(λx. indicator {x0'..} x *⇩R f x) ∈ borel_measurable lborel"
by (simp add: set_borel_measurable_def)
next
show "AE x in lborel. norm (indicator {x0'..} x *⇩R f x)
≤ norm (C *⇩R (indicator {x0'..} x *⇩R g x))"
using C by (intro AE_I2) (auto simp: abs_mult indicator_def x0'_def)
qed
ultimately have "set_integrable lborel ({a..<x0'} ∪ {x0'..}) f"
by (rule set_integrable_Un) auto
also have "{a..<x0'} ∪ {x0'..} = {a..}" by (auto simp: x0'_def)
finally show ?thesis .
qed

lemma set_integrable_Gamma_hurwitz_aux2_real:
fixes s a :: real
assumes "r > 0" and "a > 0"
shows "set_integrable lborel {r..} (λx. x powr s * (exp (-a * x)) / (1 - exp (-x)))"
(is "set_integrable _ _ ?g")
proof (rule set_integrable_bigo)
have "(λx. exp (-(a/2) * x)) integrable_on {r..}" using assms
by (intro integrable_on_exp_minus_to_infinity) auto
hence "set_integrable lebesgue {r..} (λx. exp (-(a/2) * x))"
by (intro nonnegative_absolutely_integrable) simp_all
thus "set_integrable lborel {r..} (λx. exp (-(a/2) * x))"
by (simp add: set_integrable_def integrable_completion)
next
fix y :: real
have "set_integrable lborel {r..y} ?g" using assms
by (intro borel_integrable_atLeastAtMost') (auto intro!: continuous_intros)
thus "set_integrable lborel {r..<y} ?g"
by (rule set_integrable_subset) auto
next
from assms show "?g ∈ O(λx. exp (-(a/2) * x))"
by real_asymp
qed (auto simp: set_borel_measurable_def)

lemma set_integrable_Gamma_hurwitz_aux2:
fixes s :: complex and a :: real
assumes "r > 0" and "a > 0"
shows   "set_integrable lborel {r..} (λx. x powr -s * (exp (- a * x)) / (1 - exp (- x)))"
(is "set_integrable _ _ ?g")
proof -
have "set_integrable lborel {r..} (λx. x powr -Re s * (exp (-a * x)) / (1 - exp (-x)))"
(is "set_integrable _ _ ?g'")
by (rule set_integrable_Gamma_hurwitz_aux2_real) (use assms in auto)
also have "?this ⟷ integrable lborel (λx. indicator {r..} x *⇩R ?g' x)"
by (simp add: set_integrable_def)
also have "(λx. indicator {r..} x *⇩R ?g' x) = (λx. norm (indicator {r..} x *⇩R ?g x))" using assms
by (auto simp: indicator_def norm_mult norm_divide norm_powr_real_powr fun_eq_iff
exp_of_real exp_minus norm_inverse in_Reals_norm power2_eq_square divide_simps)
finally show ?thesis unfolding set_integrable_def
by (subst (asm) integrable_norm_iff) auto
qed

lemma closed_neg_Im_slit: "closed {z. Re z = 0 ∧ Im z ≤ 0}"
proof -
have "closed ({z. Re z = 0} ∩ {z. Im z ≤ 0})"
by (intro closed_Int closed_halfspace_Re_eq closed_halfspace_Im_le)
also have "{z. Re z = 0} ∩ {z. Im z ≤ 0} = {z. Re z = 0 ∧ Im z ≤ 0}" by blast
finally show ?thesis .
qed

text ‹
We define tour semi-annulus path. When this path is mirrored into the lower half of the complex
plane and subtracted from the original path and the outer radius tends to ‹∞›, this becomes a
Hankel contour extending to ‹-∞›.
›
definition hankel_semiannulus :: "real ⇒ nat ⇒ real ⇒ complex" where
"hankel_semiannulus r N = (let R = (2 * N + 1) * pi in
part_circlepath 0 R 0 pi +++                  ―‹Big half circle›
linepath (of_real (-R)) (of_real (-r)) +++    ―‹Line on the negative real axis›
part_circlepath 0 r pi 0 +++                  ―‹Small half circle›
linepath (of_real r) (of_real R))             ―‹Line on the positive real axis›"

lemma path_hankel_semiannulus [simp, intro]: "path (hankel_semiannulus r R)"
and valid_path_hankel_semiannulus [simp, intro]: "valid_path (hankel_semiannulus r R)"
and pathfinish_hankel_semiannulus [simp, intro]:
"pathfinish (hankel_semiannulus r R) = pathstart (hankel_semiannulus r R)"
by (simp_all add: hankel_semiannulus_def Let_def)

text ‹
We set the stage for an application of the Residue Theorem. We define a function
$f(s, z) = z^{-s} \frac{\exp(az)}{1-\exp(-z)}\ ,$
which will be the integrand. However, the principal branch of $z^{-s}$ has a branch cut
along the non-positive real axis, which is bad because a part of our integration path also
lies on the non-positive real axis. We therefore choose a slightly different branch of $z^{-s}$
by moving the logarithm branch along by $90^{\circ}$ so that the branch cut lies on the
non-positive imaginary axis instead.
›
context
fixes a :: real
fixes f :: "complex ⇒ complex ⇒ complex"
and g :: "complex ⇒ real ⇒ complex"
and h :: "real ⇒ complex ⇒ real ⇒ complex"
and Res :: "complex ⇒ nat ⇒ complex"
and Ln' :: "complex ⇒ complex"
and F :: "real ⇒ complex ⇒ complex"
assumes a: "a ∈ {0<..1}"

―‹Our custom branch of the logarithm›
defines "Ln' ≡ (λz. ln (-𝗂 * z) + 𝗂 * pi / 2)"

―‹The integrand›
defines "f ≡ (λs z. exp (Ln' z * (-s) + of_real a * z) / (1 - exp z))"

―‹The integrand on the negative real axis›
defines "g ≡ (λs x. complex_of_real x powr -s * of_real (exp (-a*x)) / of_real (1 - exp (-x)))"

―‹The integrand on the circular arcs›
defines "h ≡ (λr s t. r * 𝗂 * cis t * exp (a * (r * cis t) - (ln r + 𝗂 * t) * s) /
(1 - exp (r * cis t)))"

―‹The interesting part of the residues›
defines "Res ≡ (λs k. exp (of_real (2 * real k * pi * a) * 𝗂) *
of_real (2 * real k * pi) powr (-s))"

―‹The periodic zeta function (at least on $\mathfrak{R}(s) > 1$ half-plane)›
defines "F ≡ (λq. eval_fds (fds_perzeta q))"
begin

text ‹
First, some basic properties of our custom branch of the logarithm:
›
lemma Ln'_i: "Ln' 𝗂 = 𝗂 * pi / 2"
by (simp add: Ln'_def)

lemma Ln'_of_real_pos:
assumes "x > 0"
shows   "Ln' (of_real x) = of_real (ln x)"
proof -
have "Ln' (of_real x) = Ln (of_real x * (-𝗂)) + 𝗂 * pi / 2"
by (simp add: Ln'_def mult_ac)
also have "… = of_real (ln x)" using assms
by (subst Ln_times_of_real) (auto simp: Ln_of_real)
finally show ?thesis .
qed

lemma Ln'_of_real_neg:
assumes "x < 0"
shows   "Ln' (of_real x) = of_real (ln (-x)) + 𝗂 * pi"
proof -
have "Ln' (of_real x) = Ln (of_real (-x) * 𝗂) + 𝗂 * pi / 2"
by (simp add: Ln'_def mult_ac)
also have "… = of_real (ln (-x)) + 𝗂 * pi" using assms
by (subst Ln_times_of_real) (auto simp: Ln_Reals_eq)
finally show ?thesis .
qed

lemma Ln'_times_of_real:
"Ln' (of_real x * z) = of_real (ln x) + Ln' z" if "x > 0" "z ≠ 0" for z x
proof -
have "Ln' (of_real x * z) = Ln (of_real x * (- 𝗂 * z)) + 𝗂 * pi / 2"
by (simp add: Ln'_def mult_ac)
also have "… = of_real (ln x) + Ln' z"
using that by (subst Ln_times_of_real) (auto simp: Ln'_def Ln_of_real)
finally show ?thesis .
qed

lemma Ln'_cis:
assumes "t ∈ {-pi / 2<..3 / 2 * pi}"
shows   "Ln' (cis t) = 𝗂 * t"
proof -
have "exp (𝗂 * pi / 2) = 𝗂" by (simp add: exp_eq_polar)
hence "Ln (- (𝗂 * cis t)) = 𝗂 * (t - pi / 2)" using assms
by (intro Ln_unique) (auto simp: algebra_simps exp_diff cis_conv_exp)
thus ?thesis by (simp add: Ln'_def algebra_simps)
qed

text ‹
Next, we show that the line and circle integrals are holomorphic using Leibniz's rule:
›
lemma contour_integral_part_circlepath_h:
assumes r: "r > 0"
shows   "contour_integral (part_circlepath 0 r 0 pi) (f s) = integral {0..pi} (h r s)"
proof -
have "contour_integral (part_circlepath 0 r 0 pi) (f s) =
integral {0..pi} (λt. f s (r * cis t) * r * 𝗂 * cis t)"
by (simp add: contour_integral_part_circlepath_eq)
also have "integral {0..pi} (λt. f s (r * cis t) * r * 𝗂 * cis t) = integral {0..pi} (h r s)"
proof (intro integral_cong)
fix t assume t: "t ∈ {0..pi}"
have "-(pi / 2) < 0" by simp
also have "0 ≤ t" using t by simp
finally have "t ∈ {-(pi/2)<..3/2*pi}" using t by auto
thus "f s (r * cis t) * r * 𝗂 * cis t = h r s t"
using r by (simp add: f_def Ln'_times_of_real Ln'_cis h_def Ln_Reals_eq)
qed
finally show ?thesis .
qed

lemma integral_g_holomorphic:
assumes "b > 0"
shows   "(λs. integral {b..c} (g</