diff --git a/thys/Zeta_Function/Zeta_Laurent_Expansion.thy b/thys/Zeta_Function/Zeta_Laurent_Expansion.thy --- a/thys/Zeta_Function/Zeta_Laurent_Expansion.thy +++ b/thys/Zeta_Function/Zeta_Laurent_Expansion.thy @@ -1,481 +1,509 @@ 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 \<^emph>\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) (* TODO: good real_asymp example *) (* TODO: investigate how to make this more automatic *) 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 stieltjes_gamma n" using sums_stieltjes_gamma[of n] by (simp add: add_ac sums_def) also have "(\m::nat. \km::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 "(\kkkkk=1..m. ln k ^ n / k)" by (rule sum.reindex_bij_witness[of _ "\k. k-1" Suc]) auto also have "(\km. (\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 \<^item> $(2^{1-s} - 1) / (s - 1)$, \<^item> $(s - 1) \zeta(s)$, \<^item> $\zeta(s) - \frac{1}{s-1}$, \<^item> $(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: "(\tk 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 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 {..t\\. (k choose t) * ln 2^(k - t) * stieltjes_gamma t) - stieltjes_gamma k = (\t ln 2 ^ (k+1) / real (k+1) - (\tx. ?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) - (\tx. \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) - (\tx. (\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 _") 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) - (\tti=1..k+1. (-Ln 2) ^ i * A (k-(i-1)) / fact i)" proof - have "(\ti=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) + (\tt\insert (k-1) {..ti = 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) = (\ii. 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 \ No newline at end of file