Theory Zeta_Laurent_Expansion
section ‹The Laurent series expansion of $\zeta$ at 1›
theory Zeta_Laurent_Expansion
imports Zeta_Function
begin
text ‹
In this section, we shall derive the Laurent series expansion of $\zeta(s)$ at $s = 1$, which
is of the form
\[\zeta(s) = \frac{1}{s-1} + \sum_{n=0}^\infty \frac{(-1)^n\,\gamma_n}{n!} (s-1)^n\]
where the $\gamma_n$ are the ∗‹Stieltjes constants›. Notably, $\gamma_0$ is equal to
the Euler--Mascheroni constant $\gamma$.
›
subsection ‹Definition of the Stieltjes constants›
text ‹
We define the Stieltjes constants by their infinite series form, since it is fairly
easy to show the convergence of the series by the comparison test.
›
definition%important stieltjes_gamma :: "nat ⇒ 'a :: real_algebra_1" where
"stieltjes_gamma n =
of_real (∑k. ln (k+1) ^ n / (k+1) - (ln (k+2) ^ (n+1) - ln (k+1) ^ (n + 1)) / (n + 1))"
lemma stieltjes_gamma_0 [simp]: "stieltjes_gamma 0 = euler_mascheroni"
using euler_mascheroni_sum_real by (simp add: sums_iff stieltjes_gamma_def field_simps)
lemma stieltjes_gamma_summable:
"summable (λk. ln (k+1) ^ n / (k+1) - (ln (k+2) ^ (n+1) - ln (k+1) ^ (n + 1)) / (n + 1))"
(is "summable ?f")
proof (rule summable_comparison_test_bigo)
have "eventually (λx::real. ln x ^ n - ln x ^ (n+1) * (inverse (ln x) * (1 + real n)) *
inverse (real n + 1) = 0) at_top"
using eventually_gt_at_top[of 1] by eventually_elim (auto simp: field_simps)
thus "?f ∈ O(λk. k powr (-3/2))"
by real_asymp
qed (simp_all add: summable_real_powr_iff)
lemma of_real_stieltjes_gamma [simp]: "of_real (stieltjes_gamma k) = stieltjes_gamma k"
by (simp add: stieltjes_gamma_def)
lemma sums_stieltjes_gamma:
"(λk. ln (k+1) ^ n / (k+1) - (ln (k+2) ^ (n+1) - ln (k+1) ^ (n + 1)) / (n + 1))
sums stieltjes_gamma n"
using stieltjes_gamma_summable[of n] unfolding stieltjes_gamma_def by (simp add: summable_sums)
text ‹
We can now derive the alternative definition of the Stieltjes constants as a limit.
This limit can also be written in the Euler--MacLaurin-style form
\[\lim\limits_{m\to\infty} \left(\sum\limits_{k=1}^m \frac{\ln^n k}{k} -
\int_1^m \frac{\ln^n x}{x}\,\text{d}x\right)\,,\]
which is perhaps a bit more illuminating.
›
lemma stieltjes_gamma_real_limit_form:
"(λm. (∑k = 1..m. ln (real k) ^ n / real k) - ln (real m) ^ (n + 1) / real (n + 1))
⇢ stieltjes_gamma n"
proof -
have "(λm::nat. ∑k<m. ln (k+1) ^ n / (k+1) - (ln (k+2) ^ (n+1) - ln (k+1) ^ (n + 1)) / (n + 1))
⇢ stieltjes_gamma n"
using sums_stieltjes_gamma[of n] by (simp add: add_ac sums_def)
also have "(λm::nat. ∑k<m. ln (k+1) ^ n / (k+1) - (ln (k+2) ^ (n+1) - ln (k+1) ^ (n + 1)) / (n + 1)) =
(λm::nat. (∑k=1..m. ln k ^ n / k) - ln (m + 1) ^ (n + 1) / (n + 1))"
(is "?lhs = ?rhs")
proof (rule ext, goal_cases)
fix m :: nat
have "(∑k<m. ln (k+1) ^ n / (k+1) - (ln (k+2) ^ (n+1) - ln (k+1) ^ (n + 1)) / (n + 1)) =
(∑k<m. ln (k+1) ^ n / (k+1)) -
(∑k<m. ln (Suc k+1) ^ (n+1) - ln (k+1) ^ (n + 1)) / (n + 1)"
by (simp add: sum_subtractf flip: sum_divide_distrib)
also have "(∑k<m. ln (k+1) ^ n / (k+1)) = (∑k=1..m. ln k ^ n / k)"
by (rule sum.reindex_bij_witness[of _ "λk. k-1" Suc]) auto
also have "(∑k<m. ln (Suc k+1) ^ (n+1) - ln (k+1) ^ (n + 1)) = ln (m + 1) ^ (n + 1)"
by (subst sum_lessThan_telescope) simp_all
finally show "?lhs m = ?rhs m" .
qed
finally have *: "(λm. (∑k = 1..m. ln k ^ n / k) - ln (m + 1) ^ (n + 1) / (n + 1))
⇢ stieltjes_gamma n" .
have **: "(λm. ln (m + 1) ^ (n + 1) / (n + 1) - ln m ^ (n + 1) / (n + 1)) ⇢ 0"
by real_asymp
from tendsto_add[OF * **] show ?thesis by (simp add: algebra_simps)
qed
lemma stieltjes_gamma_limit_form:
"(λm. of_real ((∑k=1..m. ln (real k) ^ n / real k) - ln (real m) ^ (n + 1) / real (n + 1)))
⇢ (stieltjes_gamma n :: 'a :: real_normed_algebra_1)"
proof -
have "(λm. of_real ((∑k=1..m. ln (real k) ^ n / real k) - ln m ^ (n + 1) / real (n + 1)))
⇢ (of_real (stieltjes_gamma n) :: 'a)"
using stieltjes_gamma_real_limit_form[of n] by (intro tendsto_of_real) (auto simp: add_ac)
thus ?thesis by simp
qed
lemma stieltjes_gamma_real_altdef:
"(stieltjes_gamma n :: real) =
lim (λm. (∑k = 1..m. ln (real k) ^ n / real k) -
ln (real m) ^ (n + 1) / real (n + 1))"
by (rule sym, rule limI, rule stieltjes_gamma_real_limit_form)
subsection ‹Proof of the Laurent expansion›
text ‹
We shall follow the proof by Briggs and Chowla~\<^cite>‹"briggs55"›, which examines the entire
function $g(s) = (2^{1-s}-1)\zeta(s)$. They determine the value of $g^{(k)}(1)$ in two
different ways: First by the Dirichlet series of $g$ and then by its power series expansion
around 1. We shall do the same here.
›
context
fixes g and G1 G2 G2' G :: "complex fps" and A :: "nat ⇒ complex"
defines "g ≡ perzeta (1 / 2)"
defines "G1 ≡ fps_shift 1 (fps_exp (-ln 2 :: complex) - 1)"
defines "G2 ≡ fps_expansion (λs. (s - 1) * pre_zeta 1 s + 1) 1"
defines "G2' ≡ fps_expansion (pre_zeta 1) 1"
defines "G ≡ G1 * G2"
defines "A ≡ fps_nth G2"
begin
text ‹
@{term "G1"}, @{term "G2"}, @{term "G2'"}, and @{term "G2"} are the formal power series
expansions of functions around ‹s = 1› of the entire functions
▪ $(2^{1-s} - 1) / (s - 1)$,
▪ $(s - 1) \zeta(s)$,
▪ $\zeta(s) - \frac{1}{s-1}$,
▪ $(2^{1-s}-1) \zeta(s)$,
respectively.
Our goal is to determine the coefficients of @{term G2'}, and we shall do so
by determining the coefficients of @{term G2} (which are the same, but shifted by 1).
This in turn will be done by determining the coefficients of @{term "G = G1 * G2"}.
Note that $(2^{1-s} - 1) \zeta(s)$ is written as @{term "perzeta (1/2)"} in Isabelle
(using the periodic ‹ζ› function) and the analytic continuation of $\zeta(s) - \frac{1}{s-1}$
is written as @{term "pre_zeta 1 s"} (@{const pre_zeta} is an artefact from the definition of
@{const zeta}, which comes in useful here).
›
lemma stieltjes_gamma_aux1: "(λn. (-1)^(n+1) * ln(n+1)^k / (n+1)) sums ((-1)^k * (deriv^^k) g 1)"
proof -
define H where "H = fds_perzeta (1 / 2)"
have conv: "conv_abscissa H < 1" unfolding H_def
by (rule le_less_trans[OF conv_abscissa_perzeta']) (use fraction_not_in_ints[of 2 1] in auto)
have [simp]: "eval_fds H s = g s" if "Re s > 0" for s
unfolding H_def g_def using fraction_not_in_ints[of 2 1] that
by (subst perzeta_altdef2) auto
have ev: "eventually (λs. s ∈ {s. Re s > 0}) (nhds 1)"
by (intro eventually_nhds_in_open open_halfspace_Re_gt) auto
have [simp]: "(deriv ^^ k) (eval_fds H) 1 = (deriv ^^ k) g 1"
by (intro higher_deriv_cong_ev eventually_mono[OF ev]) auto
have "fds_converges ((fds_deriv ^^ k) H) 1"
by (intro fds_converges le_less_trans[OF conv_abscissa_higher_deriv_le])
(use conv in ‹simp add: one_ereal_def›)
hence "(λn. fds_nth ((fds_deriv ^^ k) H) (n+1) / real (n+1)) sums eval_fds ((fds_deriv ^^ k) H) 1"
by (simp add: fds_converges_altdef)
also have "eval_fds ((fds_deriv ^^ k) H) 1 = (deriv ^^ k) (eval_fds H) 1"
using conv by (intro eval_fds_higher_deriv) (auto simp: one_ereal_def)
also have "(λn. fds_nth ((fds_deriv ^^ k) H) (n+1) / real (n+1)) =
(λn. (-1)^k * (-1)^(n+1) * ln (real (n+1)) ^ k / (n+1))"
by (auto simp: fds_nth_higher_deriv algebra_simps H_def fds_perzeta_one_half Ln_Reals_eq)
finally have "(λn. (- 1) ^ k * complex_of_real ((-1)^(n+1) * ln (real (n+1)) ^ k / real (n+1))) sums
((deriv ^^ k) g 1)" by (simp add: algebra_simps)
hence "(λn. (-1)^k * ((-1)^k * complex_of_real ((-1)^(n+1) * ln (real (n+1)) ^ k / real (n+1)))) sums
((-1)^k * (deriv ^^ k) g 1)" by (intro sums_mult)
also have "(λn. (-1)^k * ((-1)^k * complex_of_real ((-1)^(n+1) * ln (real (n+1)) ^ k / real (n+1)))) =
(λn. complex_of_real ((-1)^(n+1) * ln (real (n+1)) ^ k / real (n+1)))"
by (intro ext) auto
finally show ?thesis .
qed
lemma stieltjes_gamma_aux2: "(deriv^^k) g 1 = fact k * fps_nth G k"
and stieltjes_gamma_aux3: "G2 = fps_X * G2' + 1"
proof -
have [simp]: "fps_conv_radius G1 = ∞"
using fps_conv_radius_diff[of "fps_exp (-Ln 2)" 1] by (simp add: G1_def)
have "fps_conv_radius G2 ≥ ∞"
unfolding G2_def by (intro conv_radius_fps_expansion holomorphic_intros) auto
hence [simp]: "fps_conv_radius G2 = ∞"
by simp
have "fps_conv_radius G2' ≥ ∞"
unfolding G2'_def by (intro conv_radius_fps_expansion holomorphic_intros) auto
hence [simp]: "fps_conv_radius G2' = ∞"
by simp
have [simp]: "fps_conv_radius G = ∞"
using fps_conv_radius_mult[of G1 G2] by (simp add: G_def)
have eval_G1: "eval_fps G1 (s - 1) =
(if s = 1 then -ln 2 else (2 powr (1 - s) - 1) / (s - 1))" for s
unfolding G1_def using fps_conv_radius_diff[of "fps_exp (-Ln 2)" 1]
by (subst eval_fps_shift)
(auto intro!: subdegree_geI simp: eval_fps_diff powr_def exp_diff exp_minus algebra_simps)
have eval_G2: "eval_fps G2 (s - 1) = (s - 1) * pre_zeta 1 s + 1" for s
unfolding G2_def by (subst eval_fps_expansion[where r = ∞]) (auto intro!: holomorphic_intros)
have eval_G: "eval_fps G (s - 1) = g s" for s
unfolding G_def by (simp add: eval_fps_mult eval_G1 eval_G2 g_def perzeta_one_half_left')
have eval_G': "eval_fps G s = g (1 + s)" for s
using eval_G[of "s + 1"] by (simp add: add_ac)
have eval_G2': "eval_fps G2' (s - 1) = pre_zeta 1 s" for s
unfolding G2'_def by (intro eval_fps_expansion[where r = ∞]) (auto intro!: holomorphic_intros)
show "G2 = fps_X * G2' + 1"
proof (intro eval_fps_eqD always_eventually allI)
have *: "fps_conv_radius (fps_X * G2') = ∞"
using fps_conv_radius_mult[of fps_X G2'] by simp
from * show "fps_conv_radius (fps_X * G2' + 1) > 0"
using fps_conv_radius_add[of "fps_X * G2'" 1] by auto
show "eval_fps G2 s = eval_fps (fps_X * G2' + 1) s" for s
using * eval_G2[of "1 + s"] eval_G2'[of "1 + s"]
by (simp add: eval_fps_add eval_fps_mult)
qed auto
have "G = fps_expansion g 1"
proof (rule eval_fps_eqD)
have "fps_conv_radius (fps_expansion g 1) ≥ ∞"
using fraction_not_in_ints[of 2 1]
by (intro conv_radius_fps_expansion) (auto intro!: holomorphic_intros simp: g_def)
thus "fps_conv_radius (fps_expansion g 1) > 0" by simp
next
have "eval_fps (fps_expansion g 1) z = g (1 + z)" for z
using fraction_not_in_ints[of 2 1]
by (subst eval_fps_expansion'[where r = ∞]) (auto simp: g_def intro!: holomorphic_intros)
thus "eventually (λz. eval_fps G z = eval_fps (fps_expansion g 1) z) (nhds 0)"
by (simp add: eval_G')
qed auto
thus "(deriv ^^ k) g 1 = fact k * fps_nth G k"
by (simp add: fps_eq_iff fps_expansion_def)
qed
lemma stieltjes_gamma_aux4: "fps_nth G k = (∑i=1..k+1. (-ln 2)^i * A (k-(i-1)) / fact i)"
proof -
have "fps_nth G k = (∑i≤k. fps_nth G1 i * A (k - i))"
unfolding G_def fps_mult_nth A_def by (intro sum.cong) auto
also have "… = (∑i≤k. (-ln 2)^(i+1) * A (k - i) / fact (i+1))"
by (simp add: G1_def algebra_simps)
also have "… = (∑i=1..k+1. (-ln 2)^i * A (k-(i-1)) / fact i)"
by (intro sum.reindex_bij_witness[of _ "λi. i-1" Suc]) (auto simp: Suc_diff_Suc)
finally show ?thesis .
qed
lemma stieltjes_gamma_aux5: "(∑t<k. (k choose t) * Ln 2 ^ (k - t) * stieltjes_gamma t) -
ln 2 ^ (k+1) / of_nat (k+1) = (-1) ^ k * (deriv ^^ k) g 1"
proof -
define h where "h = (λk x. (∑n=1..x. ln(real n)^k / real n) -
ln (real x)^(k+1) / real(k+1) - stieltjes_gamma k)"
have h_eq: "(∑n=1..x. ln n ^ k / n) = ln x^(k+1) / real (k+1) + stieltjes_gamma k + h k x"
for k x :: nat by (simp add: h_def)
define h' where "h' = (λx. ∑t=0..k. (k choose t) * ln 2 ^ (k - t) * h t x)"
define S1 where "S1 = (λx. (∑t=0..k. (k choose t) * ln 2 ^ (k - t) * ln x ^ (t + 1) / (t + 1)))"
define S2 where "S2 = (λx. (∑t=0..k. (k choose t) * ln 2 ^ (k - t) * ln x ^ (t + 1) / (k + 1)))"
have [THEN filterlim_compose, tendsto_intros]: "h t ⇢ 0" for t
using tendsto_diff[OF stieltjes_gamma_real_limit_form[of t] tendsto_const[of "stieltjes_gamma t"]]
by (simp add: h_def)
have eq: "(∑n=1..2 * x. (-1)^(n+1) * ln n ^ k / n) =
ln 2 ^ (k+1) / real (k+1) -
(∑t<k. (k choose t) * ln 2 ^ (k-t) * stieltjes_gamma t) + h k (2*x) - h' x"
(is "?lhs x = ?rhs x") if "x > 0" for x :: nat
proof -
have "2 * (∑n=1..x. ln (2*n)^k/(2*n)) =
(∑n=1..x. ∑t=0..k. 1/n * (k choose t) * ln 2 ^ (k-t) * ln n ^ t)"
unfolding sum_distrib_left
proof (rule sum.cong)
fix n :: nat assume n: "n ∈ {1..x}"
have "2 * (ln (2*n)^k / (2*n)) = 1/n * (ln n + ln 2) ^ k"
using n by (simp add: ln_mult add_ac)
also have "(ln n + ln 2) ^ k = (∑t=0..k. (k choose t) * ln 2 ^ (k-t) * ln n ^ t)"
by (subst binomial_ring, rule sum.cong) auto
also have "1/n * … = (∑t=0..k. 1/n * (k choose t) * ln 2 ^ (k-t) * ln n ^ t)"
by (subst sum_distrib_left) (simp add: mult_ac)
finally show "2 * (ln (2*n)^k / (2*n)) = …" .
qed auto
also have "… = (∑t=0..k. ∑n=1..x. 1/n * (k choose t) * ln 2 ^ (k-t) * ln n ^ t)"
by (rule sum.swap)
also have "… = (∑t=0..k. (k choose t) * ln 2 ^ (k - t) *
(ln x ^ (t+1) / (t+1) + stieltjes_gamma t + h t x))"
proof (rule sum.cong)
fix t :: nat assume t: "t ∈ {0..k}"
have "(∑n=1..x. 1/n * (k choose t) * ln 2 ^ (k-t) * ln n ^ t) =
(k choose t) * ln 2 ^ (k - t) * (∑n=1..x. ln n ^ t / n)"
by (subst sum_distrib_left) (simp add: mult_ac)
also have "(∑n=1..x. ln n ^ t / n) = ln x ^ (t+1) / (t+1) + stieltjes_gamma t + h t x"
using h_eq[of t] by simp
finally show "(∑n=1..x. 1/n * (k choose t) * ln 2 ^ (k-t) * ln n ^ t) =
(k choose t) * ln 2 ^ (k - t) * …" .
qed simp_all
also have "… = (∑t=0..k. (k choose t) / (t + 1) * ln 2 ^ (k - t) * ln x ^ (t + 1)) +
(∑t=0..k. (k choose t) * ln 2 ^ (k - t) * stieltjes_gamma t) + h' x"
by (simp add: ring_distribs sum.distrib h'_def)
also have "(∑t=0..k. (k choose t) / (t + 1) * ln 2 ^ (k - t) * ln x ^ (t + 1)) =
(∑t=0..k. (Suc k choose Suc t) / (k + 1) * ln 2 ^ (k - t) * ln x ^ (t + 1))"
proof (intro sum.cong refl, goal_cases)
case (1 t)
have "of_nat (k choose t) * (of_nat (k + 1) :: real) = of_nat ((k choose t) * (k + 1))"
by (simp only: of_nat_mult)
also have "(k choose t) * (k + 1) = (Suc k choose Suc t) * (t + 1)"
using Suc_times_binomial_eq[of k t] by (simp add: algebra_simps)
also have "of_nat … = of_nat (Suc k choose Suc t) * (of_nat (t + 1) :: real)"
by (simp only: of_nat_mult)
finally have *: "of_nat (k choose t) / of_nat (t + 1) =
(of_nat (Suc k choose Suc t) / (k + 1) :: real)"
by (simp add: divide_simps flip: of_nat_Suc del: binomial_Suc_Suc)
show ?case by (simp only: *)
qed
also have "… = (∑t=1..Suc k. (Suc k choose t) / (k + 1) * ln 2 ^ (Suc k - t) * ln x ^ t)"
by (intro sum.reindex_bij_witness[of _ "λt. t-1" Suc]) auto
also have "{1..Suc k} = {..Suc k} - {0}" by auto
also have "(∑t∈…. (Suc k choose t) / (k + 1) * ln 2 ^ (Suc k - t) * ln x ^ t) =
(∑t≤Suc k. (Suc k choose t) / (k + 1) * ln 2 ^ (Suc k - t) * ln x ^ t) -
ln 2 ^ Suc k / (k + 1)"
by (subst sum_diff1) auto
also have "(∑t≤Suc k. (Suc k choose t) / (k + 1) * ln 2 ^ (Suc k - t) * ln x ^ t) =
(ln x + ln 2) ^ Suc k / (k + 1)"
unfolding binomial_ring by (subst sum_divide_distrib) (auto simp: algebra_simps)
also have "ln x + ln 2 = ln (2 * x)"
using ‹x > 0› by (simp add: ln_mult)
finally have eq1: "2 * (∑n=1..x. ln (real (2*n))^k / real (2*n)) =
ln (real (2*x))^(k+1) / real (k+1) - ln 2^(k+1) / real (k+1) +
(∑t=0..k. (k choose t) * ln 2^(k - t) * stieltjes_gamma t) + h' x"
by (simp add: algebra_simps)
have eq2: "(∑n=1..2*x. ln n ^ k / n) = ln (real (2*x))^(k+1) / real (k+1) + stieltjes_gamma k + h k (2*x)"
by (simp only: h_eq)
have "(∑n=1..2*x. (-1)^(n+1) * ln n ^ k / n) =
(∑n=1..2*x. ln n ^ k / n - 2 * (if even n then ln n ^ k / n else 0))"
by (intro sum.cong) auto
also have "… = (∑n=1..2*x. ln n ^ k / n) -
2 * (∑n=1..2*x. if even n then ln n ^ k / n else 0)"
by (simp only: sum_subtractf sum_distrib_left)
also have "(∑n=1..2*x. if even n then ln n ^ k / n else 0) =
(∑n | n ∈ {1..2*x} ∧ even n. ln n ^ k / n)"
by (intro sum.mono_neutral_cong_right) auto
also have "… = (∑n=1..x. ln (real (2*n)) ^ k / real (2*n))"
by (intro sum.reindex_bij_witness[of _ "λn. 2*n" "λn. n div 2"]) auto
also have "(∑n=1..2*x. ln n ^ k / n) - 2 * … =
ln 2^(k+1) / real (k+1) -
((∑t=0..k. (k choose t) * ln 2^(k - t) * stieltjes_gamma t) - stieltjes_gamma k) +
h k (2*x) - h' x"
using arg_cong2[OF eq1 eq2, of "(-)"] by simp
also have "{0..k} = insert k {..<k}" by auto
also have "(∑t∈…. (k choose t) * ln 2^(k - t) * stieltjes_gamma t) - stieltjes_gamma k =
(∑t<k. (k choose t) * ln 2^(k - t) * stieltjes_gamma t)"
by (subst sum.insert) auto
finally show ?thesis .
qed
have "?rhs ⇢ ln 2 ^ (k+1) / real (k+1) -
(∑t<k. (k choose t) * ln 2 ^ (k-t) * stieltjes_gamma t)"
unfolding h'_def by (rule tendsto_eq_intros refl mult_nat_left_at_top filterlim_ident | simp)+
moreover have "eventually (λx. ?rhs x = ?lhs x) sequentially"
using eventually_gt_at_top[of 0] by eventually_elim (simp only: eq)
ultimately have *: "?lhs ⇢ ln 2 ^ (k+1) / real (k+1) -
(∑t<k. (k choose t) * ln 2 ^ (k-t) * stieltjes_gamma t)"
by (rule Lim_transform_eventually)
also have "(λx. ∑n=1..2*x. (-1)^(n+1) * ln (real n)^k / real n) =
(λx. ∑n<2*x. -((-1)^(n+1) * ln (real (n+1))^k / real (n+1)))"
by (intro ext sum.reindex_bij_witness[of _ Suc "λn. n - 1"]) (auto simp: power_diff)
also have "… = (λx. -(∑n<2*x. ((-1)^(n+1) * ln (real (n+1))^k / real (n+1))))"
by (subst sum_negf) auto
finally have *: "… ⇢ (ln 2 ^ (k+1) / real (k+1) -
(∑t<k. (k choose t) * ln 2 ^ (k - t) * stieltjes_gamma t))" .
have lim1: "(λx. (∑n<2*x. complex_of_real ((-1)^(n+1) * ln (real (n+1))^k / real (n+1))))
⇢ -(ln 2 ^ (k+1) / of_nat (k+1) -
(∑t<k. (k choose t) * ln 2 ^ (k - t) * stieltjes_gamma t))"
(is "?lhs' ⇢ _")
using tendsto_of_real[OF tendsto_minus[OF *], where ?'a = complex]
by (simp add: Ln_Reals_eq)
moreover have "?lhs' ⇢ ((- 1) ^ k * (deriv ^^ k) g 1)"
proof -
have **: "filterlim (λn::nat. 2 * n) sequentially sequentially" by real_asymp
have "(λx. (∑n<2*x. complex_of_real ((-1)^(n+1) * ln (real (n+1))^k / real (n+1))))
⇢ ((- 1) ^ k * (deriv ^^ k) g 1)"
by (rule filterlim_compose[OF _ **]) (use stieltjes_gamma_aux1 in ‹simp add: sums_def›)
thus ?thesis .
qed
ultimately have "-(ln 2 ^ (k+1) / of_nat (k+1) -
(∑t<k. (k choose t) * ln 2 ^ (k - t) * stieltjes_gamma t)) =
(-1) ^ k * (deriv ^^ k) g 1"
by (rule LIMSEQ_unique)
thus ?thesis by (simp add: Ln_Reals_eq)
qed
lemma stieltjes_gamma_aux6: "(∑t<k. (k choose t) * Ln 2 ^ (k - t) * stieltjes_gamma t) -
Ln 2 ^ (k + 1) / of_nat (k + 1) =
(-1)^k * fact k * (∑i=1..k+1. (-Ln 2) ^ i * A (k-(i-1)) / fact i)"
proof -
have "(∑t<k. (k choose t) * Ln 2 ^ (k - t) * stieltjes_gamma t) -
Ln 2 ^ (k + 1) / of_nat (k + 1) = (- 1) ^ k * (deriv ^^ k) g 1"
using stieltjes_gamma_aux5[of k] .
also have "(deriv ^^ k) g 1 = fact k * fps_nth G k"
by (rule stieltjes_gamma_aux2)
also have "fps_nth G k = (∑i=1..k + 1. (-Ln 2) ^ i * A (k - (i - 1)) / fact i)"
by (rule stieltjes_gamma_aux4)
finally show ?thesis by (simp add: mult_ac)
qed
theorem higher_deriv_pre_zeta_1_1: "(deriv ^^ k) (pre_zeta 1) 1 = (-1) ^ k * stieltjes_gamma k"
proof -
have eq: "A k = (if k = 0 then 1 else (-1)^(k+1) * stieltjes_gamma (k - 1) / fact (k - 1))" for k
proof (induction k rule: less_induct)
case (less k)
show ?case
proof (cases "k = 0")
case True
with stieltjes_gamma_aux6[of 0] show ?thesis by simp
next
case False
have "k * Ln 2 * stieltjes_gamma (k - 1) +
(∑t<k-1. (k choose t) * Ln 2 ^ (k - t) * stieltjes_gamma t) =
(∑t∈insert (k-1) {..<k-1}. (k choose t) * Ln 2 ^ (k - t) * stieltjes_gamma t)"
using False by (subst sum.insert) auto
also have "insert (k-1) {..<k-1} = {..<k}" using False by auto
also have "(∑t<k. of_nat (k choose t) * Ln 2 ^ (k - t) * stieltjes_gamma t) =
Ln 2 ^ (k + 1) / of_nat (k + 1) +
(- 1) ^ k * fact k * (∑i = 1..k + 1. (- Ln 2) ^ i * A (k - (i - 1)) / fact i)"
using stieltjes_gamma_aux6[of k] by (simp add: algebra_simps)
also have "{1..k+1} = {1,k+1} ∪ {2..k}" by auto
also have "(- 1) ^ k * fact k * (∑i∈…. (- Ln 2) ^ i * A (k - (i - 1)) / fact i) =
(∑i=2..k. (-1)^k * fact k * (- Ln 2) ^ i * A (k - (i - 1)) / fact i)
-Ln 2 * A k * (- 1) ^ k * fact k +
(-Ln 2)^(k+1) * A 0 / fact (k+1) * (- 1) ^ k * fact k"
using False by (subst sum.union_disjoint)
(auto simp: algebra_simps sum_distrib_left sum_distrib_right)
also have "(∑i=2..k. (-1)^k * fact k * (-Ln 2) ^ i * A (k-(i-1)) / fact i) =
(∑i<k-1. (k choose i) * Ln 2 ^ (k-i) * stieltjes_gamma i)"
using False
by (intro sum.reindex_bij_witness[of _ "λi. k - i" "λi. k - i"])
(auto simp: binomial_fact Suc_diff_le less field_simps power_neg_one_If)
finally have "k * Ln 2 * stieltjes_gamma (k - 1) =
(-1)^(k+1) * fact k * Ln 2 * A k"
using False by (simp add: less power_minus')
also have "… * (-1)^(k+1) / fact k / Ln 2 = A k"
by simp
also have "k * Ln 2 * stieltjes_gamma (k - 1) * (-1)^(k+1) / fact k / Ln 2 =
(-1)^(k+1) * stieltjes_gamma (k - 1) / fact (k - 1)"
using False by (simp add: field_simps fact_reduce)
finally have "A k = (- 1) ^ (k + 1) * stieltjes_gamma (k - 1) / fact (k - 1)" ..
thus ?thesis using False by simp
qed
qed
have "fps_nth G2' k = fps_nth G2 (Suc k)"
by (simp add: stieltjes_gamma_aux3)
also have "… = A (Suc k)"
by (simp add: A_def)
also have "… = (-1) ^ k * stieltjes_gamma k / fact k"
by (simp add: eq)
finally show "(deriv ^^ k) (pre_zeta 1) 1 = (-1) ^ k * stieltjes_gamma k"
by (simp add: G2'_def fps_eq_iff fps_expansion_def)
qed
corollary pre_zeta_1_1 [simp]: "pre_zeta 1 1 = euler_mascheroni"
using higher_deriv_pre_zeta_1_1[of 0] by simp
corollary zeta_minus_pole_limit: "(λs. zeta s - 1 / (s - 1)) ─1→ euler_mascheroni"
proof (rule Lim_transform_eventually)
show "eventually (λs. pre_zeta 1 s = zeta s - 1 / (s - 1)) (at 1)"
by (auto simp: zeta_minus_pole_eq [symmetric] eventually_at_filter)
have "isCont (pre_zeta 1) 1"
by (intro continuous_intros) auto
thus "pre_zeta 1 ─1→ euler_mascheroni"
by (simp add: isCont_def)
qed
corollary fps_expansion_pre_zeta_1_1:
"fps_expansion (pre_zeta 1) 1 = Abs_fps (λn. (-1)^n * stieltjes_gamma n / fact n)"
by (simp add: fps_expansion_def higher_deriv_pre_zeta_1_1)
end
definition fps_pre_zeta_1 :: "complex fps" where
"fps_pre_zeta_1 = Abs_fps (λn. (-1)^n * stieltjes_gamma n / fact n)"
lemma pre_zeta_1_has_fps_expansion_1 [fps_expansion_intros]:
"(λz. pre_zeta 1 (1 + z)) has_fps_expansion fps_pre_zeta_1"
proof -
have "(λz. pre_zeta 1 (1 + z)) has_fps_expansion fps_expansion (pre_zeta 1) 1"
by (intro analytic_at_imp_has_fps_expansion analytic_intros analytic_pre_zeta) auto
also have "… = fps_pre_zeta_1"
by (simp add: fps_expansion_pre_zeta_1_1 fps_pre_zeta_1_def)
finally show ?thesis .
qed
definition fls_zeta_1 :: "complex fls" where
"fls_zeta_1 = fls_X_intpow (-1) + fps_to_fls fps_pre_zeta_1"
lemma zeta_has_laurent_expansion_1 [laurent_expansion_intros]:
"(λz. zeta (1 + z)) has_laurent_expansion fls_zeta_1"
proof -
have "(λz. z powi (-1) + pre_zeta 1 (1 + z)) has_laurent_expansion fls_zeta_1"
unfolding fls_zeta_1_def
by (intro laurent_expansion_intros fps_expansion_intros has_laurent_expansion_fps)
also have "?this ⟷ ?thesis"
by (intro has_laurent_expansion_cong)
(auto simp: eventually_at_filter zeta_def hurwitz_zeta_def divide_inverse)
finally show ?thesis .
qed
end