diff --git a/thys/Dirichlet_Series/Dirichlet_Series_Analysis.thy b/thys/Dirichlet_Series/Dirichlet_Series_Analysis.thy --- a/thys/Dirichlet_Series/Dirichlet_Series_Analysis.thy +++ b/thys/Dirichlet_Series/Dirichlet_Series_Analysis.thy @@ -1,3087 +1,3087 @@ (* File: Dirichlet_Series_Analysis.thy Author: Manuel Eberl, TU München *) section \Analytic properties of Dirichlet series\ theory Dirichlet_Series_Analysis imports "HOL-Analysis.Analysis" "HOL-Library.Going_To_Filter" "HOL-Real_Asymp.Real_Asymp" Dirichlet_Series Moebius_Mu Partial_Summation Euler_Products begin (* TODO Move *) lemma frequently_eventually_frequently: "frequently P F \ eventually Q F \ frequently (\x. P x \ Q x) F" by (erule frequently_rev_mp, erule eventually_mono) auto text \ The following illustrates a concept we will need later on: A property holds for \f\ going to \F\ if we can find e.\,g.\ a sequence that tends to \F\ and whose elements eventually satisfy \P\. \ lemma frequently_going_toI: assumes "filterlim (\n. f (g n)) F G" assumes "eventually (\n. P (g n)) G" assumes "eventually (\n. g n \ A) G" assumes "G \ bot" shows "frequently P (f going_to F within A)" unfolding frequently_def proof assume "eventually (\x. \P x) (f going_to F within A)" hence "eventually (\x. \P x) (inf (filtercomap f F) (principal A))" by (simp add: going_to_within_def) moreover have "filterlim (\n. g n) (inf (filtercomap f F) (principal A)) G" using assms unfolding filterlim_inf filterlim_principal by (auto simp add: filterlim_iff_le_filtercomap filtercomap_filtercomap) ultimately have "eventually (\n. \P (g n)) G" by (rule eventually_compose_filterlim) with assms(2) have "eventually (\_. False) G" by eventually_elim auto with assms(4) show False by simp qed lemma frequently_filtercomapI: assumes "filterlim (\n. f (g n)) F G" assumes "eventually (\n. P (g n)) G" assumes "G \ bot" shows "frequently P (filtercomap f F)" using frequently_going_toI[of f g F G P UNIV] assms by (simp add: going_to_def) lemma frequently_going_to_at_topE: fixes f :: "'a \ real" assumes "frequently P (f going_to at_top)" obtains g where "\n. P (g n)" and "filterlim (\n. f (g n)) at_top sequentially" proof - from assms have "\k. \x. f x \ real k \ P x" by (auto simp: frequently_def eventually_going_to_at_top_linorder) hence "\g. \k. f (g k) \ real k \ P (g k)" by metis then obtain g where g: "\k. f (g k) \ real k" "\k. P (g k)" by blast have "filterlim (\n. f (g n)) at_top sequentially" by (rule filterlim_at_top_mono[OF filterlim_real_sequentially]) (use g in auto) from g(2) and this show ?thesis using that[of g] by blast qed text \ Apostol often uses statements like `$P(s_k)$ for all $k$ in an infinite sequence $s_k$ such that $\mathfrak{R}(s_k)\longrightarrow\infty$ as $k\to\infty$'. Instead, we write @{prop "frequently P (Re going_to at_top)"}. This lemma shows that our statement is equivalent to his. \ lemma frequently_going_to_at_top_iff: "frequently P (f going_to (at_top :: real filter)) \ (\g. \n. P (g n) \ filterlim (\n. f (g n)) at_top sequentially)" by (auto intro: frequently_going_toI elim!: frequently_going_to_at_topE) (* END TODO *) lemma surj_bullet_1: "surj (\s::'a::{real_normed_algebra_1, real_inner}. s \ 1)" proof (rule surjI) fix x :: real show "(x *\<^sub>R 1) \ (1 :: 'a) = x" by (simp add: dot_square_norm) qed lemma bullet_1_going_to_at_top_neq_bot [simp]: "((\s::'a::{real_normed_algebra_1, real_inner}. s \ 1) going_to at_top) \ bot" unfolding going_to_def by (rule filtercomap_neq_bot_surj[OF _ surj_bullet_1]) auto lemma fds_abs_converges_altdef: "fds_abs_converges f s \ (\n. fds_nth f n / nat_power n s) abs_summable_on {1..}" by (auto simp add: fds_abs_converges_def abs_summable_on_nat_iff intro!: summable_cong eventually_mono[OF eventually_gt_at_top[of 0]]) lemma fds_abs_converges_altdef': "fds_abs_converges f s \ (\n. fds_nth f n / nat_power n s) abs_summable_on UNIV" by (subst fds_abs_converges_altdef, rule abs_summable_on_cong_neutral) (auto simp: Suc_le_eq) lemma eval_fds_altdef: assumes "fds_abs_converges f s" shows "eval_fds f s = (\\<^sub>an. fds_nth f n / nat_power n s)" proof - have "fds_abs_converges f s \ (\n. fds_nth f n / nat_power n s) abs_summable_on UNIV" unfolding fds_abs_converges_altdef by (intro abs_summable_on_cong_neutral) (auto simp: Suc_le_eq) with assms show ?thesis unfolding eval_fds_def fds_abs_converges_altdef by (intro infsetsum_nat' [symmetric]) simp_all qed lemma multiplicative_function_divide_nat_power: fixes f :: "nat \ 'a :: {nat_power, field}" assumes "multiplicative_function f" shows "multiplicative_function (\n. f n / nat_power n s)" proof interpret f: multiplicative_function f by fact show "f 0 / nat_power 0 s = 0" "f 1 / nat_power 1 s = 1" by simp_all fix a b :: nat assume "a > 1" "b > 1" "coprime a b" thus "f (a * b) / nat_power (a * b) s = f a / nat_power a s * (f b / nat_power b s)" by (simp_all add: f.mult_coprime nat_power_mult_distrib) qed lemma completely_multiplicative_function_divide_nat_power: fixes f :: "nat \ 'a :: {nat_power, field}" assumes "completely_multiplicative_function f" shows "completely_multiplicative_function (\n. f n / nat_power n s)" proof interpret f: completely_multiplicative_function f by fact show "f 0 / nat_power 0 s = 0" "f (Suc 0) / nat_power (Suc 0) s = 1" by simp_all fix a b :: nat assume "a > 1" "b > 1" thus "f (a * b) / nat_power (a * b) s = f a / nat_power a s * (f b / nat_power b s)" by (simp_all add: f.mult nat_power_mult_distrib) qed subsection \Convergence and absolute convergence\ class nat_power_normed_field = nat_power_field + real_normed_field + real_inner + real_algebra_1 + fixes real_power :: "real \ 'a \ 'a" assumes real_power_nat_power: "n > 0 \ real_power (real n) c = nat_power n c" assumes real_power_1_right_aux: "d > 0 \ real_power d 1 = d *\<^sub>R 1" assumes real_power_add: "d > 0 \ real_power d (a + b) = real_power d a * real_power d b" assumes real_power_nonzero [simp]: "d > 0 \ real_power d a \ 0" assumes norm_real_power: "x > 0 \ norm (real_power x c) = x powr (c \ 1)" assumes nat_power_of_real_aux: "nat_power n (x *\<^sub>R 1) = ((real n powr x) *\<^sub>R 1)" assumes has_field_derivative_nat_power_aux: "\x::'a. n > 0 \ LIM y inf_class.inf (Inf (principal ` {S. open S \ x \ S})) (principal (UNIV - {x})). (nat_power n y - nat_power n x - ln (real n) *\<^sub>R nat_power n x * (y - x)) /\<^sub>R norm (y - x) :> Inf (principal ` {S. open S \ 0 \ S})" assumes has_vector_derivative_real_power_aux: "x > 0 \ filterlim (\y. (real_power y c - real_power x (c :: 'a) - (y - x) *\<^sub>R (c * real_power x (c - 1))) /\<^sub>R norm (y - x)) (INF S\{S. open S \ 0 \ S}. principal S) (at x)" assumes norm_nat_power: "n > 0 \ norm (nat_power n y) = real n powr (y \ 1)" begin lemma real_power_diff: "d > 0 \ real_power d (a - b) = real_power d a / real_power d b" using real_power_add[of d b "a - b"] by (simp add: field_simps) end lemma real_power_1_right [simp]: "d > 0 \ real_power d 1 = of_real d" using real_power_1_right_aux[of d] by (simp add: scaleR_conv_of_real) lemma has_vector_derivative_real_power [derivative_intros]: "x > 0 \ ((\y. real_power y c) has_vector_derivative c * real_power x (c - 1)) (at x within A)" by (rule has_vector_derivative_at_within) (insert has_vector_derivative_real_power_aux[of x c], simp add: has_vector_derivative_def has_derivative_def nhds_def bounded_linear_scaleR_left) lemma has_field_derivative_nat_power [derivative_intros]: "n > 0 \ ((\y. nat_power n y) has_field_derivative ln (real n) *\<^sub>R nat_power n x) (at (x :: 'a :: nat_power_normed_field) within A)" by (rule has_field_derivative_at_within) (insert has_field_derivative_nat_power_aux[of n x], simp only: has_field_derivative_def has_derivative_def netlimit_at, simp add: nhds_def at_within_def bounded_linear_mult_right) lemma continuous_on_real_power [continuous_intros]: "A \ {0<..} \ continuous_on A (\x. real_power x s)" by (rule continuous_on_vector_derivative has_vector_derivative_real_power)+ auto instantiation real :: nat_power_normed_field begin definition real_power_real :: "real \ real \ real" where [simp]: "real_power_real = (powr)" instance proof (standard, goal_cases) case (7 n x) hence "((\x. nat_power n x) has_field_derivative ln (real n) *\<^sub>R nat_power n x) (at x)" by (auto intro!: derivative_eq_intros simp: powr_def) thus ?case unfolding has_field_derivative_def netlimit_at has_derivative_def by (simp add: nhds_def at_within_def) next case (8 x c) hence "((\y. real_power y c) has_vector_derivative c * real_power x (c - 1)) (at x)" by (auto intro!: derivative_eq_intros simp: has_field_derivative_iff_has_vector_derivative [symmetric]) thus ?case by (simp add: has_vector_derivative_def has_derivative_def nhds_def) qed (simp_all add: powr_add) end instantiation complex :: nat_power_normed_field begin definition nat_power_complex :: "nat \ complex \ complex" where [simp]: "nat_power_complex n z = of_nat n powr z" definition real_power_complex :: "real \ complex \ complex" where [simp]: "real_power_complex = (\x y. of_real x powr y)" instance proof fix m n :: nat and z :: complex assume "m > 0" "n > 0" thus "nat_power (m * n) z = nat_power m z * nat_power n z" unfolding nat_power_complex_def of_nat_mult by (subst powr_times_real) simp_all next fix n :: nat and z :: complex assume "n > 0" show "norm (nat_power n z) = real n powr (z \ 1)" unfolding nat_power_complex_def using norm_powr_real_powr[of "of_nat n" z] by simp next fix n :: nat and x :: complex assume n: "n > 0" hence "((\x. nat_power n x) has_field_derivative ln (real n) *\<^sub>R nat_power n x) (at x)" by (auto intro!: derivative_eq_intros simp: powr_def scaleR_conv_of_real mult_ac) thus "LIM y inf_class.inf (Inf (principal ` {S. open S \ x \ S})) (principal (UNIV - {x})). (nat_power n y - nat_power n x - ln (real n) *\<^sub>R nat_power n x * (y - x)) /\<^sub>R cmod (y - x) :> (Inf (principal ` {S. open S \ 0 \ S}))" unfolding has_field_derivative_def netlimit_at has_derivative_def by (simp add: nhds_def at_within_def) next fix x :: real and c :: complex assume "x > 0" hence "((\y. real_power y c) has_vector_derivative c * real_power x (c - 1)) (at x)" - by (auto intro!: derivative_eq_intros has_vector_derivative_real_complex) + by (auto intro!: derivative_eq_intros has_vector_derivative_real_field) thus "LIM y at x. (real_power y c - real_power x c - (y - x) *\<^sub>R (c * real_power x (c - 1))) /\<^sub>R norm (y - x) :> INF S\{S. open S \ 0 \ S}. principal S" by (simp add: has_vector_derivative_def has_derivative_def nhds_def) next fix n :: nat and x :: real show "nat_power n (x *\<^sub>R 1 :: complex) = (real n powr x) *\<^sub>R 1" by (simp add: powr_Reals_eq scaleR_conv_of_real) qed (auto simp: powr_def exp_add exp_of_nat_mult [symmetric] algebra_simps scaleR_conv_of_real simp del: Ln_of_nat) end lemma nat_power_of_real [simp]: "nat_power n (of_real x :: 'a :: nat_power_normed_field) = of_real (real n powr x)" using nat_power_of_real_aux[of n x] by (simp add: scaleR_conv_of_real) lemma fds_abs_converges_of_real [simp]: "fds_abs_converges (fds_of_real f) (of_real s :: 'a :: {nat_power_normed_field,banach}) \ fds_abs_converges f s" unfolding fds_abs_converges_def by (subst (1 2) summable_Suc_iff [symmetric]) (simp add: norm_divide norm_nat_power) lemma eval_fds_of_real [simp]: assumes "fds_converges f s" shows "eval_fds (fds_of_real f) (of_real s :: 'a :: {nat_power_normed_field,banach}) = of_real (eval_fds f s)" using assms unfolding eval_fds_def by (auto simp: fds_converges_def suminf_of_real) lemma fds_abs_summable_zeta_iff [simp]: fixes s :: "'a :: {banach, nat_power_normed_field}" shows "fds_abs_converges fds_zeta s \ s \ 1 > (1 :: real)" proof - have "fds_abs_converges fds_zeta s \ summable (\n. real n powr -(s \ 1))" unfolding fds_abs_converges_def by (intro summable_cong always_eventually) (auto simp: norm_divide fds_nth_zeta powr_minus norm_nat_power divide_simps) also have "\ \ s \ 1 > 1" by (simp add: summable_real_powr_iff) finally show ?thesis . qed lemma fds_abs_summable_zeta: "(s :: 'a :: {banach, nat_power_normed_field}) \ 1 > 1 \ fds_abs_converges fds_zeta s" by simp lemma fds_abs_converges_moebius_mu: fixes s :: "'a :: {banach,nat_power_normed_field}" assumes "s \ 1 > 1" shows "fds_abs_converges (fds moebius_mu) s" unfolding fds_abs_converges_def proof (rule summable_comparison_test, intro exI allI impI) fix n :: nat show "norm (norm (fds_nth (fds moebius_mu) n / nat_power n s)) \ real n powr (-s \ 1)" by (auto simp: powr_minus divide_simps abs_moebius_mu_le norm_nat_power norm_divide moebius_mu_def norm_power) next from assms show "summable (\n. real n powr (-s \ 1))" by (simp add: summable_real_powr_iff) qed definition conv_abscissa :: "'a :: {nat_power,banach,real_normed_field, real_inner} fds \ ereal" where "conv_abscissa f = (INF s\{s. fds_converges f s}. ereal (s \ 1))" definition abs_conv_abscissa :: "'a :: {nat_power,banach,real_normed_field, real_inner} fds \ ereal" where "abs_conv_abscissa f = (INF s\{s. fds_abs_converges f s}. ereal (s \ 1))" lemma conv_abscissa_mono: assumes "\s. fds_converges g s \ fds_converges f s" shows "conv_abscissa f \ conv_abscissa g" unfolding conv_abscissa_def by (rule INF_mono) (use assms in auto) lemma abs_conv_abscissa_mono: assumes "\s. fds_abs_converges g s \ fds_abs_converges f s" shows "abs_conv_abscissa f \ abs_conv_abscissa g" unfolding abs_conv_abscissa_def by (rule INF_mono) (use assms in auto) class dirichlet_series = euclidean_space + real_normed_field + nat_power_normed_field + assumes one_in_Basis: "1 \ Basis" instance real :: dirichlet_series by standard simp_all instance complex :: dirichlet_series by standard (simp_all add: Basis_complex_def) context assumes "SORT_CONSTRAINT('a :: dirichlet_series)" begin lemma fds_abs_converges_Re_le: fixes f :: "'a fds" assumes "fds_abs_converges f z" "z \ 1 \ z' \ 1" shows "fds_abs_converges f z'" unfolding fds_abs_converges_def proof (rule summable_comparison_test, intro exI allI impI) fix n :: nat assume n: "n \ 1" thus "norm (norm (fds_nth f n / nat_power n z')) \ norm (fds_nth f n / nat_power n z)" using assms(2) by (simp add: norm_divide norm_nat_power divide_simps powr_mono mult_left_mono) qed (insert assms(1), simp add: fds_abs_converges_def) lemma fds_abs_converges: assumes "s \ 1 > abs_conv_abscissa (f :: 'a fds)" shows "fds_abs_converges f s" proof - from assms obtain s0 where "fds_abs_converges f s0" "s0 \ 1 < s \ 1" by (auto simp: INF_less_iff abs_conv_abscissa_def) with fds_abs_converges_Re_le[OF this(1), of s] this(2) show ?thesis by simp qed lemma fds_abs_diverges: assumes "s \ 1 < abs_conv_abscissa (f :: 'a fds)" shows "\fds_abs_converges f s" proof assume "fds_abs_converges f s" hence "abs_conv_abscissa f \ s \ 1" unfolding abs_conv_abscissa_def by (intro INF_lower) auto with assms show False by simp qed lemma uniformly_Cauchy_eval_fds_aux: fixes s0 :: "'a :: dirichlet_series" assumes bounded: "Bseq (\n. \k\n. fds_nth f k / nat_power k s0)" assumes B: "compact B" "\z. z \ B \ z \ 1 > s0 \ 1" shows "uniformly_Cauchy_on B (\N z. \n\N. fds_nth f n / nat_power n z)" proof (cases "B = {}") case False show ?thesis proof (rule uniformly_Cauchy_onI', goal_cases) case (1 \) define \ where "\ = Inf ((\s. s \ 1) ` B)" have \_le: "s \ 1 \ \" if "s \ B" for s unfolding \_def using that by (intro cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded B) auto have "\ \ ((\s. s \ 1) ` B)" unfolding \_def using B \B \ {}\ by (intro closed_contains_Inf bounded_inner_imp_bdd_below compact_imp_bounded B compact_imp_closed compact_continuous_image continuous_intros) auto with B(2) have \_gt: "\ > s0 \ 1" by auto define \ where "\ = \ - s0 \ 1" have "bounded B" by (rule compact_imp_bounded) fact then obtain norm_B_aux where norm_B_aux: "\s. s \ B \ norm s \ norm_B_aux" by (auto simp: bounded_iff) define norm_B where "norm_B = norm_B_aux + norm s0" from norm_B_aux have norm_B: "norm (s - s0) \ norm_B" if "s \ B" for s using norm_triangle_ineq4[of s s0] norm_B_aux[OF that] by (simp add: norm_B_def) define A where "A = sum_upto (\k. fds_nth f k / nat_power k s0)" from bounded obtain C_aux where C_aux: "\n. norm (\k\n. fds_nth f k / nat_power k s0) \ C_aux" by (auto simp: Bseq_def) define C where "C = max C_aux 1" have C_pos: "C > 0" by (simp add: C_def) have C: "norm (A x) \ C" for x proof - have "A x = (\k\nat \x\. fds_nth f k / nat_power k s0)" unfolding A_def sum_upto_altdef by (intro sum.mono_neutral_left) auto also have "norm \ \ C_aux" by (rule C_aux) also have "\ \ C" by (simp add: C_def) finally show ?thesis . qed have "(\m. 2 * C * (1 + norm_B / \) * real m powr (-\)) \ 0" unfolding \_def using \_gt by (intro tendsto_mult_right_zero tendsto_neg_powr filterlim_real_sequentially) simp_all from order_tendstoD(2)[OF this \\ > 0\] obtain M where M: "\m. m \ M \ 2 * C * (1 + norm_B / \) * real m powr - \ < \" by (auto simp: eventually_at_top_linorder) show ?case proof (intro exI[of _ "max M 1"] ballI allI impI, goal_cases) case (1 s m n) from 1 have s: "s \ 1 > s0 \ 1" using B(2)[of s] by simp have mn: "m \ M" "m < n" "m > 0" "n > 0" using 1 by (simp_all add: ) have "dist (\n\m. fds_nth f n / nat_power n s) (\n\n. fds_nth f n / nat_power n s) = dist (\n\n. fds_nth f n / nat_power n s) (\n\m. fds_nth f n / nat_power n s)" by (simp add: dist_commute) also from 1 have "\ = norm (\k\{..n}-{..m}. fds_nth f k / nat_power k s)" by (subst Groups_Big.sum_diff) (simp_all add: dist_norm) also from 1 have "{..n} - {..m} = real -` {real m<..real n}" by auto also have "(\k\\. fds_nth f k / nat_power k s) = (\k\\. fds_nth f k / nat_power k s0 * real_power (real k) (s0 - s))" (is "_ = ?S") by (intro sum.cong refl) (simp_all add: nat_power_diff real_power_nat_power) also have *: "((\t. A t * ((s0 - s) * real_power t (s0 - s - 1))) has_integral (A (real n) * real_power n (s0 - s) - A (real m) * real_power m (s0 - s) - ?S)) {real m..real n}" (is "(?h has_integral _) _") unfolding A_def using mn by (intro partial_summation_strong[of "{}"]) (auto intro!: derivative_eq_intros continuous_intros) hence "?S = A (real n) * nat_power n (s0 - s) - A (real m) * nat_power m (s0 - s) - integral {real m..real n} ?h" using mn by (simp add: has_integral_iff real_power_nat_power) also have "norm \ \ norm (A (real n) * nat_power n (s0 - s)) + norm (A (real m) * nat_power m (s0 - s)) + norm (integral {real m..real n} ?h)" by (intro order.trans[OF norm_triangle_ineq4] add_right_mono order.refl) also have "norm (A (real n) * nat_power n (s0 - s)) \ C * nat_power m ((s0 - s) \ 1)" using mn \s \ B\ C_pos s by (auto simp: norm_mult norm_nat_power algebra_simps intro!: mult_mono C powr_mono2') also have "norm (A (real m) * nat_power m (s0 - s)) \ C * nat_power m ((s0 - s) \ 1)" using mn by (auto simp: norm_mult norm_nat_power intro!: mult_mono C) also have "norm (integral {real m..real n} ?h) \ integral {real m..real n} (\t. C * (norm (s0 - s) * t powr ((s0 - s) \ 1 - 1)))" proof (intro integral_norm_bound_integral ballI, goal_cases) case 1 with * show ?case by (simp add: has_integral_iff) next case 2 from mn show ?case by (auto intro!: integrable_continuous_real continuous_intros) next case (3 t) thus ?case unfolding norm_mult using C_pos mn by (intro mult_mono C) (auto simp: norm_real_power dot_square_norm algebra_simps) qed also have "\ = C * norm (s0 - s) * integral {real m..real n} (\t. t powr ((s0 - s) \ 1 - 1))" by (simp add: algebra_simps dot_square_norm) also { have "((\t. t powr ((s0 - s) \ 1 - 1)) has_integral (real n powr ((s0 - s) \ 1) / ((s0 - s) \ 1) - real m powr ((s0 - s) \ 1) / ((s0 - s) \ 1))) {m..n}" (is "(?l has_integral ?I) _") using mn s by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros simp: has_field_derivative_iff_has_vector_derivative [symmetric] inner_diff_left) hence "integral {real m..real n} ?l = ?I" by (simp add: has_integral_iff) also have "\ \ -(real m powr ((s0 - s) \ 1) / ((s0 - s) \ 1))" using s mn by (simp add: divide_simps inner_diff_left) also have "\ = 1 * (real m powr ((s0 - s) \ 1) / ((s - s0) \ 1))" using s by (simp add: field_simps inner_diff_left) also have "\ \ 2 * (real m powr ((s0 - s) \ 1) / ((s - s0) \ 1))" using mn s by (intro mult_right_mono divide_nonneg_pos) (simp_all add: inner_diff_left) finally have "integral {m..n} ?l \ \" . } hence "C * norm (s0 - s) * integral {real m..real n} (\t. t powr ((s0 - s) \ 1 - 1)) \ C * norm (s0 - s) * (2 * (real m powr ((s0 - s) \ 1) / ((s - s0) \ 1)))" using C_pos mn by (intro mult_mono mult_nonneg_nonneg integral_nonneg integrable_continuous_real continuous_intros) auto also have "C * nat_power m ((s0 - s) \ 1) + C * nat_power m ((s0 - s) \ 1) + \ = 2 * C * nat_power m ((s0 - s) \ 1) * (1 + norm (s - s0) / ((s - s0) \ 1))" by (simp add: algebra_simps norm_minus_commute) also have "\ \ 2 * C * nat_power m (-\) * (1 + norm_B / \)" using C_pos s mn \_le[of s] \s \ B\ \_gt unfolding nat_power_real_def by (intro mult_mono mult_nonneg_nonneg powr_mono frac_le add_mono norm_B) (simp_all add: inner_diff_left \_def) also have "\ = 2 * C * (1 + norm_B / \) * real m powr (-\)" by simp also from \m \ M\ have "\ < \" by (rule M) finally show ?case by - simp_all qed qed qed (auto simp: uniformly_Cauchy_on_def) lemma uniformly_convergent_eval_fds_aux: assumes "Bseq (\n. \k\n. fds_nth f k / nat_power k (s0 :: 'a))" assumes B: "compact B" "\z. z \ B \ z \ 1 > s0 \ 1" shows "uniformly_convergent_on B (\N z. \n\N. fds_nth f n / nat_power n z)" by (rule Cauchy_uniformly_convergent uniformly_Cauchy_eval_fds_aux assms)+ lemma uniformly_convergent_eval_fds_aux': assumes conv: "fds_converges f (s0 :: 'a)" assumes B: "compact B" "\z. z \ B \ z \ 1 > s0 \ 1" shows "uniformly_convergent_on B (\N z. \n\N. fds_nth f n / nat_power n z)" proof (rule uniformly_convergent_eval_fds_aux) from conv have "convergent (\n. \k\n. fds_nth f k / nat_power k s0)" by (simp add: fds_converges_def summable_iff_convergent') thus "Bseq (\n. \k\n. fds_nth f k / nat_power k s0)" by (rule convergent_imp_Bseq) qed (insert assms, auto) lemma bounded_partial_sums_imp_fps_converges: fixes s0 :: "'a :: dirichlet_series" assumes "Bseq (\n. \k\n. fds_nth f k / nat_power k s0)" and "s \ 1 > s0 \ 1" shows "fds_converges f s" proof - have "uniformly_convergent_on {s} (\N z. \n\N. fds_nth f n / nat_power n z)" using assms(2) by (intro uniformly_convergent_eval_fds_aux[OF assms(1)]) auto thus ?thesis by (auto simp: fds_converges_def summable_iff_convergent' dest: uniformly_convergent_imp_convergent) qed theorem fds_converges_Re_le: assumes "fds_converges f (s0 :: 'a)" "s \ 1 > s0 \ 1" shows "fds_converges f s" proof - have "uniformly_convergent_on {s} (\N z. \n\N. fds_nth f n / nat_power n z)" by (rule uniformly_convergent_eval_fds_aux' assms)+ (insert assms(2), auto) then obtain l where "uniform_limit {s} (\N z. \n\N. fds_nth f n / nat_power n z) l at_top" by (auto simp: uniformly_convergent_on_def) from tendsto_uniform_limitI[OF this, of s] have "(\n. fds_nth f n / nat_power n s) sums l s" unfolding sums_def' by (simp add: atLeast0AtMost) thus ?thesis by (simp add: fds_converges_def sums_iff) qed lemma fds_converges: assumes "s \ 1 > conv_abscissa (f :: 'a fds)" shows "fds_converges f s" proof - from assms obtain s0 where "fds_converges f s0" "s0 \ 1 < s \ 1" by (auto simp: INF_less_iff conv_abscissa_def) with fds_converges_Re_le[OF this(1), of s] this(2) show ?thesis by simp qed lemma fds_diverges: assumes "s \ 1 < conv_abscissa (f :: 'a fds)" shows "\fds_converges f s" proof assume "fds_converges f s" hence "conv_abscissa f \ s \ 1" unfolding conv_abscissa_def by (intro INF_lower) auto with assms show False by simp qed theorem fds_converges_imp_abs_converges: assumes "fds_converges (f :: 'a fds) s" "s' \ 1 > s \ 1 + 1" shows "fds_abs_converges f s'" unfolding fds_abs_converges_def proof (rule summable_comparison_test_ev) from assms(2) show "summable (\n. real n powr ((s - s') \ 1))" by (subst summable_real_powr_iff) (simp_all add: inner_diff_left) next from assms(1) have "(\n. fds_nth f n / nat_power n s) \ 0" unfolding fds_converges_def by (rule summable_LIMSEQ_zero) from tendsto_norm[OF this] have "(\n. norm (fds_nth f n / nat_power n s)) \ 0" by simp hence "eventually (\n. norm (fds_nth f n / nat_power n s) < 1) at_top" by (rule order_tendstoD) simp_all thus "eventually (\n. norm (norm (fds_nth f n / nat_power n s')) \ real n powr ((s - s') \ 1)) at_top" proof eventually_elim case (elim n) thus ?case proof (cases "n = 0") case False have "norm (fds_nth f n / nat_power n s') = norm (fds_nth f n) / real n powr (s' \ 1)" using False by (simp add: norm_divide norm_nat_power) also have "\ = norm (fds_nth f n / nat_power n s) / real n powr ((s' - s) \ 1)" using False by (simp add: norm_divide norm_nat_power inner_diff_left powr_diff) also have "\ \ 1 / real n powr ((s' - s) \ 1)" using elim by (intro divide_right_mono elim) simp_all also have "\ = real n powr ((s - s') \ 1)" using False by (simp add: field_simps inner_diff_left powr_diff) finally show ?thesis by simp qed simp_all qed qed lemma conv_le_abs_conv_abscissa: "conv_abscissa f \ abs_conv_abscissa f" unfolding conv_abscissa_def abs_conv_abscissa_def by (intro INF_superset_mono) auto lemma conv_abscissa_PInf_iff: "conv_abscissa f = \ \ (\s. \fds_converges f s)" unfolding conv_abscissa_def by (subst Inf_eq_PInfty) auto lemma conv_abscissa_PInfI [intro]: "(\s. \fds_converges f s) \ conv_abscissa f = \" by (subst conv_abscissa_PInf_iff) auto lemma conv_abscissa_MInf_iff: "conv_abscissa (f :: 'a fds) = -\ \ (\s. fds_converges f s)" proof safe assume *: "\s. fds_converges f s" have "conv_abscissa f \ B" for B :: real using spec[OF *, of "of_real B"] fds_diverges[of "of_real B" f] by (cases "conv_abscissa f \ B") simp_all thus "conv_abscissa f = -\" by (rule ereal_bot) qed (auto intro: fds_converges) lemma conv_abscissa_MInfI [intro]: "(\s. fds_converges (f::'a fds) s) \ conv_abscissa f = -\" by (subst conv_abscissa_MInf_iff) auto lemma abs_conv_abscissa_PInf_iff: "abs_conv_abscissa f = \ \ (\s. \fds_abs_converges f s)" unfolding abs_conv_abscissa_def by (subst Inf_eq_PInfty) auto lemma abs_conv_abscissa_PInfI [intro]: "(\s. \fds_converges f s) \ abs_conv_abscissa f = \" by (subst abs_conv_abscissa_PInf_iff) auto lemma abs_conv_abscissa_MInf_iff: "abs_conv_abscissa (f :: 'a fds) = -\ \ (\s. fds_abs_converges f s)" proof safe assume *: "\s. fds_abs_converges f s" have "abs_conv_abscissa f \ B" for B :: real using spec[OF *, of "of_real B"] fds_abs_diverges[of "of_real B" f] by (cases "abs_conv_abscissa f \ B") simp_all thus "abs_conv_abscissa f = -\" by (rule ereal_bot) qed (auto intro: fds_abs_converges) lemma abs_conv_abscissa_MInfI [intro]: "(\s. fds_abs_converges (f::'a fds) s) \ abs_conv_abscissa f = -\" by (subst abs_conv_abscissa_MInf_iff) auto lemma conv_abscissa_geI: assumes "\c'. ereal c' < c \ \s. s \ 1 = c' \ \fds_converges f s" shows "conv_abscissa (f :: 'a fds) \ c" proof (rule ccontr) assume "\conv_abscissa f \ c" hence "c > conv_abscissa f" by simp from ereal_dense2[OF this] obtain c' where "c > ereal c'" "c' > conv_abscissa f" by auto moreover from assms[OF this(1)] obtain s where "s \ 1 = c'" "\fds_converges f s" by blast ultimately show False using fds_converges[of f s] by auto qed lemma conv_abscissa_leI: assumes "\c'. ereal c' > c \ \s. s \ 1 = c' \ fds_converges f s" shows "conv_abscissa (f :: 'a fds) \ c" proof (rule ccontr) assume "\conv_abscissa f \ c" hence "c < conv_abscissa f" by simp from ereal_dense2[OF this] obtain c' where "c < ereal c'" "c' < conv_abscissa f" by auto moreover from assms[OF this(1)] obtain s where "s \ 1 = c'" "fds_converges f s" by blast ultimately show False using fds_diverges[of s f] by auto qed lemma abs_conv_abscissa_geI: assumes "\c'. ereal c' < c \ \s. s \ 1 = c' \ \fds_abs_converges f s" shows "abs_conv_abscissa (f :: 'a fds) \ c" proof (rule ccontr) assume "\abs_conv_abscissa f \ c" hence "c > abs_conv_abscissa f" by simp from ereal_dense2[OF this] obtain c' where "c > ereal c'" "c' > abs_conv_abscissa f" by auto moreover from assms[OF this(1)] obtain s where "s \ 1 = c'" "\fds_abs_converges f s" by blast ultimately show False using fds_abs_converges[of f s] by auto qed lemma abs_conv_abscissa_leI: assumes "\c'. ereal c' > c \ \s. s \ 1 = c' \ fds_abs_converges f s" shows "abs_conv_abscissa (f :: 'a fds) \ c" proof (rule ccontr) assume "\abs_conv_abscissa f \ c" hence "c < abs_conv_abscissa f" by simp from ereal_dense2[OF this] obtain c' where "c < ereal c'" "c' < abs_conv_abscissa f" by auto moreover from assms[OF this(1)] obtain s where "s \ 1 = c'" "fds_abs_converges f s" by blast ultimately show False using fds_abs_diverges[of s f] by auto qed lemma conv_abscissa_leI_weak: assumes "\x. ereal x > d \ fds_converges f (of_real x)" shows "conv_abscissa (f :: 'a fds) \ d" proof (rule conv_abscissa_leI) fix x assume "d < ereal x" from assms[OF this] show "\s. s \ 1 = x \ fds_converges f s" by (intro exI[of _ "of_real x"]) auto qed lemma abs_conv_abscissa_leI_weak: assumes "\x. ereal x > d \ fds_abs_converges f (of_real x)" shows "abs_conv_abscissa (f :: 'a fds) \ d" proof (rule abs_conv_abscissa_leI) fix x assume "d < ereal x" from assms[OF this] show "\s. s \ 1 = x \ fds_abs_converges f s" by (intro exI[of _ "of_real x"]) auto qed lemma conv_abscissa_truncate [simp]: "conv_abscissa (fds_truncate m (f :: 'a fds)) = -\" by (auto simp: conv_abscissa_MInf_iff) lemma abs_conv_abscissa_truncate [simp]: "abs_conv_abscissa (fds_truncate m (f :: 'a fds)) = -\" by (auto simp: abs_conv_abscissa_MInf_iff) theorem abs_conv_le_conv_abscissa_plus_1: "abs_conv_abscissa (f :: 'a fds) \ conv_abscissa f + 1" proof (rule abs_conv_abscissa_leI) fix c assume less: "conv_abscissa f + 1 < ereal c" define c' where "c' = (if conv_abscissa f = -\ then c - 2 else (c - 1 + real_of_ereal (conv_abscissa f)) / 2)" from less have c': "conv_abscissa f < ereal c' \ c' < c - 1" by (cases "conv_abscissa f") (simp_all add: c'_def field_simps) from c' have "fds_converges f (of_real c')" by (intro fds_converges) (simp_all add: inner_diff_left dot_square_norm) hence "fds_abs_converges f (of_real c)" by (rule fds_converges_imp_abs_converges) (insert c', simp_all) thus "\s. s \ 1 = c \ fds_abs_converges f s" by (intro exI[of _ "of_real c"]) auto qed lemma uniformly_convergent_eval_fds: assumes B: "compact B" "\z. z \ B \ z \ 1 > conv_abscissa (f :: 'a fds)" shows "uniformly_convergent_on B (\N z. \n\N. fds_nth f n / nat_power n z)" proof (cases "B = {}") case False define \ where "\ = Inf ((\s. s \ 1) ` B)" have \_le: "s \ 1 \ \" if "s \ B" for s unfolding \_def using that by (intro cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded B) auto have "\ \ ((\s. s \ 1) ` B)" unfolding \_def using B \B \ {}\ by (intro closed_contains_Inf bounded_inner_imp_bdd_below compact_imp_bounded B compact_imp_closed compact_continuous_image continuous_intros) auto with B(2) have \_gt: "\ > conv_abscissa f" by auto define s where "s = (if conv_abscissa f = -\ then \ - 1 else (\ + real_of_ereal (conv_abscissa f)) / 2)" from \_gt have s: "conv_abscissa f < s \ s < \" by (cases "conv_abscissa f") (auto simp: s_def) show ?thesis using s \compact B\ by (intro uniformly_convergent_eval_fds_aux'[of f "of_real s"] fds_converges) (auto dest: \_le) qed auto corollary uniformly_convergent_eval_fds': assumes B: "compact B" "\z. z \ B \ z \ 1 > conv_abscissa (f :: 'a fds)" shows "uniformly_convergent_on B (\N z. \nN z. \n\N. fds_nth f n / nat_power n z) l at_top" by (auto simp: uniformly_convergent_on_def) also have "(\N z. \n\N. fds_nth f n / nat_power n z) = (\N z. \nN z. \nDerivative of a Dirichlet series\ lemma fds_converges_deriv_aux: assumes conv: "fds_converges f (s0 :: 'a)" and gt: "s \ 1 > s0 \ 1" shows "fds_converges (fds_deriv f) s" proof - have "Cauchy (\n. \k\n. (-ln (real k) *\<^sub>R fds_nth f k) / nat_power k s)" proof (rule CauchyI', goal_cases) case (1 \) define \ where "\ = s \ 1 - s0 \ 1" define \' where "\' = \ / 2" from gt have \_pos: "\ > 0" by (simp add: \_def) define A where "A = sum_upto (\k. fds_nth f k / nat_power k s0)" from conv have "convergent (\n. \k\n. fds_nth f k / nat_power k s0)" by (simp add: fds_converges_def summable_iff_convergent') hence "Bseq (\n. \k\n. fds_nth f k / nat_power k s0)" by (rule convergent_imp_Bseq) then obtain C_aux where C_aux: "\n. norm (\k\n. fds_nth f k / nat_power k s0) \ C_aux" by (auto simp: Bseq_def) define C where "C = max C_aux 1" have C_pos: "C > 0" by (simp add: C_def) have C: "norm (A x) \ C" for x proof - have "A x = (\k\nat \x\. fds_nth f k / nat_power k s0)" unfolding A_def sum_upto_altdef by (intro sum.mono_neutral_left) auto also have "norm \ \ C_aux" by (rule C_aux) also have "\ \ C" by (simp add: C_def) finally show ?thesis . qed define C' where "C' = 2 * C + C * (norm (s0 - s) * (1 + 1 / \) + 1) / \" have "(\m. C' * real m powr (-\')) \ 0" unfolding \'_def using gt \_pos by (intro tendsto_mult_right_zero tendsto_neg_powr filterlim_real_sequentially) simp_all from order_tendstoD(2)[OF this \\ > 0\] obtain M1 where M1: "\m. m \ M1 \ C' * real m powr - \' < \" by (auto simp: eventually_at_top_linorder) have "((\x. ln (real x) / real x powr \') \ 0) at_top" using \_pos by (intro lim_ln_over_power) (simp_all add: \'_def) from order_tendstoD(2)[OF this zero_less_one] eventually_gt_at_top[of "1::nat"] have "eventually (\n. ln (real n) \ n powr \') at_top" by eventually_elim simp_all then obtain M2 where M2: "\n. n \ M2 \ ln (real n) \ n powr \'" by (auto simp: eventually_at_top_linorder) let ?f' = "\k. -ln (real k) *\<^sub>R fds_nth f k" show ?case proof (intro exI[of _ "max (max M1 M2) 1"] allI impI, goal_cases) case (1 m n) hence mn: "m \ M1" "m \ M2" "m > 0" "m < n" by simp_all define g :: "real \ 'a" where "g = (\t. real_power t (s0 - s) * of_real (ln t))" define g' :: "real \ 'a" where "g' = (\t. real_power t (s0 - s - 1) * ((s0 - s) * of_real (ln t) + 1))" define norm_g' :: "real \ real" where "norm_g' = (\t. t powr (-\ - 1) * (norm (s0 - s) * ln t + 1))" define norm_g :: "real \ real" where "norm_g = (\t. -(t powr -\) * (norm (s0 - s) * (\ * ln t + 1) + \) / \^2)" have g_g': "(g has_vector_derivative g' t) (at t)" if "t \ {real m..real n}" for t using mn that by (auto simp: g_def g'_def real_power_diff field_simps real_power_add intro!: derivative_eq_intros) have [continuous_intros]: "continuous_on {real m..real n} g" using mn by (auto simp: g_def intro!: continuous_intros) let ?S = "\k\real -` {real m<..real n}. fds_nth f k / nat_power k s0 * g k" have "dist (\k\m. ?f' k / nat_power k s) (\k\n. ?f' k / nat_power k s) = norm (\k\{..n} - {..m}. fds_nth f k / nat_power k s * of_real (ln (real k)))" using mn by (subst sum_diff) (simp_all add: dist_norm norm_minus_commute sum_negf scaleR_conv_of_real mult_ac) also have "{..n} - {..m} = real -` {real m<..real n}" by auto also have "(\k\\. fds_nth f k / nat_power k s * of_real (ln (real k))) = (\k\\. fds_nth f k / nat_power k s0 * g k)" using mn unfolding g_def by (intro sum.cong refl) (auto simp: real_power_nat_power field_simps nat_power_diff) also have *: "((\t. A t * g' t) has_integral (A (real n) * g n - A (real m) * g m - ?S)) {real m..real n}" (is "(?h has_integral _) _") unfolding A_def using mn by (intro partial_summation_strong[of "{}"]) (auto intro!: g_g' simp: field_simps continuous_intros) hence "?S = A (real n) * g n - A (real m) * g m - integral {real m..real n} ?h" using mn by (simp add: has_integral_iff field_simps) also have "norm \ \ norm (A (real n) * g n) + norm (A (real m) * g m) + norm (integral {real m..real n} ?h)" by (intro order.trans[OF norm_triangle_ineq4] add_right_mono order.refl) also have "norm (A (real n) * g n) \ C * norm (g n)" unfolding norm_mult using mn C_pos by (intro mult_mono C) auto also have "norm (g n) \ n powr -\ * n powr \'" using mn M2[of n] by (simp add: g_def norm_real_power norm_mult \_def inner_diff_left) also have "\ = n powr -\'" using mn by (simp add: \'_def powr_minus field_simps powr_add [symmetric]) also have "norm (A (real m) * g m) \ C * norm (g m)" unfolding norm_mult using mn C_pos by (intro mult_mono C) auto also have "norm (g m) \ m powr -\ * m powr \'" using mn M2[of m] by (simp add: g_def norm_real_power norm_mult \_def inner_diff_left) also have "\ = m powr -\'" using mn by (simp add: \'_def powr_minus field_simps powr_add [symmetric]) also have "C * real n powr - \' \ C * real m powr - \'" using \_pos mn C_pos by (intro mult_left_mono powr_mono2') (simp_all add: \'_def) also have "\ + \ = 2 * \" by simp also have "norm (integral {m..n} ?h) \ integral {m..n} (\t. C * norm_g' t)" proof (intro integral_norm_bound_integral ballI, goal_cases) case 1 with * show ?case by (simp add: has_integral_iff) next case 2 from mn show ?case by (auto intro!: integrable_continuous_real continuous_intros simp: norm_g'_def) next case (3 t) have "norm (g' t) \ norm_g' t" unfolding g'_def norm_g'_def using 3 mn unfolding norm_mult by (intro mult_mono order.trans[OF norm_triangle_ineq]) (auto simp: norm_real_power inner_diff_left dot_square_norm norm_mult \_def intro!: mult_left_mono) thus ?case unfolding norm_mult using C_pos mn by (intro mult_mono C) simp_all qed also have "\ = C * integral {m..n} norm_g'" unfolding norm_g'_def by (simp add: norm_g'_def \_def inner_diff_left) also { have "(norm_g' has_integral (norm_g n - norm_g m)) {m..n}" unfolding norm_g'_def norm_g_def power2_eq_square using mn \_pos by (intro fundamental_theorem_of_calculus) (auto simp: has_field_derivative_iff_has_vector_derivative [symmetric] field_simps powr_diff intro!: derivative_eq_intros) hence "integral {m..n} norm_g' = norm_g n - norm_g m" by (simp add: has_integral_iff) also have "norm_g n \ 0" unfolding norm_g_def using \_pos mn by (intro divide_nonpos_pos mult_nonpos_nonneg add_nonneg_nonneg mult_nonneg_nonneg) simp_all hence "norm_g n - norm_g m \ -norm_g m" by simp also have "\ = real m powr -\ * ln (real m) * (norm (s0 - s)) / \ + real m powr -\ * ((norm (s0 - s) / \ + 1) / \)" using \_pos by (simp add: field_simps norm_g_def power2_eq_square) also { have "ln (real m) \ real m powr \'" using M2[of m] mn by simp also have "real m powr -\ * \ = real m powr -\'" by (simp add: powr_add [symmetric] \'_def) finally have "real m powr -\ * ln (real m) * (norm (s0 - s)) / \ \ \ * (norm (s0 - s)) / \" using \_pos by (intro divide_right_mono mult_right_mono) (simp_all add: mult_left_mono) } also have "real m powr -\ * ((norm (s0 - s) / \ + 1) / \) \ real m powr -\' * ((norm (s0 - s) / \ + 1) / \)" using mn \_pos by (intro mult_right_mono powr_mono) (simp_all add: \'_def) also have "real m powr - \' * norm (s0 - s) / \ + \ = real m powr -\' * (norm (s0 - s) * (1 + 1 / \) + 1) / \" using \_pos by (simp add: field_simps power2_eq_square) finally have "integral {real m..real n} norm_g' \ real m powr - \' * (norm (s0 - s) * (1 + 1 / \) + 1) / \" by - simp_all } also have "2 * (C * m powr - \') + C * (m powr - \' * (norm (s0 - s) * (1 + 1 / \) + 1) / \) = C' * m powr -\'" by (simp add: algebra_simps C'_def) also have "\ < \" using M1[of m] mn by simp finally show ?case using C_pos by - simp_all qed qed from Cauchy_convergent[OF this] show ?thesis by (simp add: summable_iff_convergent' fds_converges_def fds_nth_deriv) qed theorem assumes "s \ 1 > conv_abscissa (f :: 'a fds)" shows fds_converges_deriv: "fds_converges (fds_deriv f) s" and has_field_derivative_eval_fds [derivative_intros]: "(eval_fds f has_field_derivative eval_fds (fds_deriv f) s) (at s within A)" proof - define s1 :: real where "s1 = (if conv_abscissa f = -\ then s \ 1 - 2 else (s \ 1 * 1 / 3 + real_of_ereal (conv_abscissa f) * 2 / 3))" define s2 :: real where "s2 = (if conv_abscissa f = -\ then s \ 1 - 1 else (s \ 1 * 2 / 3 + real_of_ereal (conv_abscissa f) * 1 / 3))" from assms have s: "conv_abscissa f < s1 \ s1 < s2 \ s2 < s \ 1" by (cases "conv_abscissa f") (auto simp: s1_def s2_def field_simps) from s have *: "fds_converges f (of_real s1)" by (intro fds_converges) simp_all thus conv': "fds_converges (fds_deriv f) s" by (rule fds_converges_deriv_aux) (insert s, simp_all) from * have conv: "fds_converges (fds_deriv f) (of_real s2)" by (rule fds_converges_deriv_aux) (insert s, simp_all) define \ :: real where "\ = (s \ 1 - s2) / 2" from s have \_pos: "\ > 0" by (simp add: \_def) have "uniformly_convergent_on (cball s \) (\n s. \k\n. fds_nth (fds_deriv f) k / nat_power k s)" proof (intro uniformly_convergent_eval_fds_aux'[OF conv]) fix s'' :: 'a assume s'': "s'' \ cball s \" have "dist (s \ 1) (s'' \ 1) \ dist s s''" by (intro Euclidean_dist_upper) (simp_all add: one_in_Basis) also from s'' have "\ \ \" by simp finally show "s'' \ 1 > (of_real s2 :: 'a) \ 1" using s by (auto simp: \_def dist_real_def abs_if split: if_splits) qed (insert \_pos, auto) then obtain l where "uniform_limit (cball s \) (\n s. \k\n. fds_nth (fds_deriv f) k / nat_power k s) l at_top" by (auto simp: uniformly_convergent_on_def) also have "(\n s. \k\n. fds_nth (fds_deriv f) k / nat_power k s) = (\n s. \k) (\n s. \k) (\n s. \k cball s \" "s \ interior (cball s \)" using s by (simp_all add: \_def) show "summable (\n. fds_nth f n / nat_power n s)" using assms fds_converges[of f s] by (simp add: fds_converges_def) next fix s' :: 'a and n :: nat show "((\s. fds_nth f n / nat_power n s) has_field_derivative fds_nth (fds_deriv f) n / nat_power n s') (at s' within cball s \)" by (cases "n = 0") (simp, auto intro!: derivative_eq_intros simp: fds_nth_deriv field_simps) qed (auto simp: fds_nth_deriv intro!: derivative_eq_intros) thus "(eval_fds f has_field_derivative eval_fds (fds_deriv f) s) (at s within A)" by (rule has_field_derivative_at_within) qed lemmas has_field_derivative_eval_fds' [derivative_intros] = DERIV_chain2[OF has_field_derivative_eval_fds] lemma continuous_eval_fds [continuous_intros]: assumes "s \ 1 > conv_abscissa f" shows "continuous (at s within A) (eval_fds (f :: 'a :: dirichlet_series fds))" proof - have "isCont (eval_fds f) s" by (rule has_field_derivative_eval_fds DERIV_isCont assms)+ thus ?thesis by (rule continuous_within_subset) auto qed lemma continuous_eval_fds' [continuous_intros]: fixes f :: "'a :: dirichlet_series fds" assumes "continuous (at s within A) g" "g s \ 1 > conv_abscissa f" shows "continuous (at s within A) (\x. eval_fds f (g x))" by (rule continuous_within_compose3[OF _ assms(1)] continuous_intros assms)+ lemma continuous_on_eval_fds [continuous_intros]: fixes f :: "'a :: dirichlet_series fds" assumes "A \ {s. s \ 1 > conv_abscissa f}" shows "continuous_on A (eval_fds f)" by (rule DERIV_continuous_on derivative_intros)+ (insert assms, auto) lemma continuous_on_eval_fds' [continuous_intros]: fixes f :: "'a :: dirichlet_series fds" assumes "continuous_on A g" "g ` A \ {s. s \ 1 > conv_abscissa f}" shows "continuous_on A (\x. eval_fds f (g x))" by (rule continuous_on_compose2[OF continuous_on_eval_fds assms(1)]) (insert assms, auto simp: image_iff) lemma conv_abscissa_deriv_le: fixes f :: "'a fds" shows "conv_abscissa (fds_deriv f) \ conv_abscissa f" proof (rule conv_abscissa_leI) fix c' :: real assume "ereal c' > conv_abscissa f" thus "\s. s \ 1 = c' \ fds_converges (fds_deriv f) s" by (intro exI[of _ "of_real c'"]) (auto simp: fds_converges_deriv) qed lemma abs_conv_abscissa_integral: fixes f :: "'a fds" shows "abs_conv_abscissa (fds_integral a f) = abs_conv_abscissa f" proof (rule antisym) show "abs_conv_abscissa (fds_integral a f) \ abs_conv_abscissa f" proof (rule abs_conv_abscissa_leI, goal_cases) case (1 c) have "fds_abs_converges (fds_integral a f) (of_real c)" unfolding fds_abs_converges_def proof (rule summable_comparison_test_ev) from 1 have "fds_abs_converges f (of_real c)" by (intro fds_abs_converges) auto thus "summable (\n. norm (fds_nth f n / nat_power n (of_real c)))" by (simp add: fds_abs_converges_def) next show "\\<^sub>F n in sequentially. norm (norm (fds_nth (fds_integral a f) n / nat_power n (of_real c))) \ norm (fds_nth f n / nat_power n (of_real c))" using eventually_gt_at_top[of 3] proof eventually_elim case (elim n) from elim and exp_le have "ln (exp 1) \ ln (real n)" by (subst ln_le_cancel_iff) auto hence "1 * norm (fds_nth f n) \ ln (real n) * norm (fds_nth f n)" by (intro mult_right_mono) auto with elim show ?case by (simp add: norm_divide norm_nat_power fds_integral_def field_simps) qed qed thus ?case by (intro exI[of _ "of_real c"]) auto qed next show "abs_conv_abscissa f \ abs_conv_abscissa (fds_integral a f)" (is "_ \ ?s0") proof (cases "abs_conv_abscissa (fds_integral a f) = \") case False show ?thesis proof (rule abs_conv_abscissa_leI) fix c :: real define \ where "\ = (if ?s0 = -\ then 1 else (c - real_of_ereal ?s0) / 2)" assume "ereal c > ?s0" with False have \: "\ > 0" "c - \ > ?s0" by (cases ?s0; force simp: \_def field_simps)+ have "fds_abs_converges f (of_real c)" unfolding fds_abs_converges_def proof (rule summable_comparison_test_ev) from \ have "fds_abs_converges (fds_integral a f) (of_real (c - \))" by (intro fds_abs_converges) (auto simp: algebra_simps) thus "summable (\n. norm (fds_nth (fds_integral a f) n / nat_power n (of_real (c - \))))" by (simp add: fds_abs_converges_def) next have "\\<^sub>F n in at_top. ln (real n) / real n powr \ < 1" by (rule order_tendstoD lim_ln_over_power \\ > 0\ zero_less_one)+ thus "\\<^sub>F n in sequentially. norm (norm (fds_nth f n / nat_power n (of_real c))) \ norm (fds_nth (fds_integral a f) n / nat_power n (of_real (c - \)))" using eventually_gt_at_top[of 1] proof eventually_elim case (elim n) hence "ln (real n) * norm (fds_nth f n) \ real n powr \ * norm (fds_nth f n)" by (intro mult_right_mono) auto with elim show ?case by (simp add: norm_divide norm_nat_power field_simps powr_diff inner_diff_left fds_integral_def) qed qed thus "\s. s \ 1 = c \ fds_abs_converges f s" by (intro exI[of _ "of_real c"]) auto qed qed auto qed lemma abs_conv_abscissa_ln: "abs_conv_abscissa (fds_ln l (f :: 'a :: dirichlet_series fds)) = abs_conv_abscissa (fds_deriv f / f)" by (simp add: fds_ln_def abs_conv_abscissa_integral) lemma abs_conv_abscissa_deriv: fixes f :: "'a fds" shows "abs_conv_abscissa (fds_deriv f) = abs_conv_abscissa f" proof - have "abs_conv_abscissa (fds_deriv f) = abs_conv_abscissa (fds_integral (fds_nth f 1) (fds_deriv f))" by (rule abs_conv_abscissa_integral [symmetric]) also have "fds_integral (fds_nth f 1) (fds_deriv f) = f" by (rule fds_integral_fds_deriv) finally show ?thesis . qed lemma abs_conv_abscissa_higher_deriv: "abs_conv_abscissa ((fds_deriv ^^ n) f) = abs_conv_abscissa (f :: 'a :: dirichlet_series fds)" by (induction n) (simp_all add: abs_conv_abscissa_deriv) lemma conv_abscissa_higher_deriv_le: "conv_abscissa ((fds_deriv ^^ n) f) \ conv_abscissa (f :: 'a :: dirichlet_series fds)" by (induction n) (auto intro: order.trans[OF conv_abscissa_deriv_le]) lemma abs_conv_abscissa_restrict: "abs_conv_abscissa (fds_subseries P f) \ abs_conv_abscissa f" by (rule abs_conv_abscissa_mono) auto lemma eval_fds_deriv: fixes f :: "'a fds" assumes "s \ 1 > conv_abscissa f" shows "eval_fds (fds_deriv f) s = deriv (eval_fds f) s" by (intro DERIV_imp_deriv [symmetric] derivative_intros assms) lemma eval_fds_higher_deriv: assumes "(s :: 'a :: dirichlet_series) \ 1 > conv_abscissa f" shows "eval_fds ((fds_deriv ^^ n) f) s = (deriv ^^ n) (eval_fds f) s" using assms proof (induction n arbitrary: f s) case (Suc n f s) have ev: "eventually (\s. s \ {s. s \ 1 > conv_abscissa f}) (nhds s)" using Suc.prems open_halfspace_gt[of _ "1::'a"] by (intro eventually_nhds_in_open, cases "conv_abscissa f") (auto simp: open_halfspace_gt inner_commute) have "eval_fds ((fds_deriv ^^ Suc n) f) s = eval_fds ((fds_deriv ^^ n) (fds_deriv f)) s" by (subst funpow_Suc_right) simp also have "\ = (deriv ^^ n) (eval_fds (fds_deriv f)) s" by (intro Suc.IH le_less_trans[OF conv_abscissa_deriv_le] Suc.prems) also have "\ = (deriv ^^ n) (deriv (eval_fds f)) s" by (intro higher_deriv_cong_ev refl eventually_mono[OF ev] eval_fds_deriv) auto also have "\ = (deriv ^^ Suc n) (eval_fds f) s" by (subst funpow_Suc_right) simp finally show ?case . qed auto end subsection \Multiplication of two series\ lemma fixes f g :: "nat \ 'a :: {banach, real_normed_field, second_countable_topology, nat_power}" fixes s :: 'a assumes [simp]: "f 0 = 0" "g 0 = 0" assumes summable: "summable (\n. norm (f n / nat_power n s))" "summable (\n. norm (g n / nat_power n s))" shows summable_dirichlet_prod: "summable (\n. norm (dirichlet_prod f g n / nat_power n s))" and suminf_dirichlet_prod: "(\n. dirichlet_prod f g n / nat_power n s) = (\n. f n / nat_power n s) * (\n. g n / nat_power n s)" proof - have summable': "(\n. f n / nat_power n s) abs_summable_on A" "(\n. g n / nat_power n s) abs_summable_on A" for A by ((rule abs_summable_on_subset[OF _ subset_UNIV], insert summable, simp add: abs_summable_on_nat_iff'); fail)+ have f_g: "f a / nat_power a s * (g b / nat_power b s) = f a * g b / nat_power (a * b) s" for a b by (cases "a * b = 0") (auto simp: nat_power_mult_distrib) have eq: "(\\<^sub>a(m, n)\{(m, n). m * n = x}. f m * g n / nat_power x s) = dirichlet_prod f g x / nat_power x s" for x :: nat proof (cases "x > 0") case False hence "(\\<^sub>a(m,n) | m * n = x. f m * g n / nat_power x s) = (\\<^sub>a(m,n) | m * n = x. 0)" by (intro infsetsum_cong) auto with False show ?thesis by simp next case True from finite_divisors_nat'[OF this] show ?thesis by (simp add: dirichlet_prod_altdef2 case_prod_unfold sum_divide_distrib) qed have "(\(m,n). (f m / nat_power m s) * (g n / nat_power n s)) abs_summable_on UNIV \ UNIV" using summable' by (intro abs_summable_on_product) auto also have "?this \ (\(m,n). f m * g n / nat_power (m*n) s) abs_summable_on UNIV" using f_g by (intro abs_summable_on_cong) auto also have "\ \ (\(x,(m,n)). f m * g n / nat_power (m*n) s) abs_summable_on (SIGMA x:UNIV. {(m,n). m * n = x})" unfolding case_prod_unfold by (rule abs_summable_on_reindex_bij_betw [symmetric]) (auto simp: bij_betw_def inj_on_def image_iff) also have "\ \ (\(x,(m,n)). f m * g n / nat_power x s) abs_summable_on (SIGMA x:UNIV. {(m,n). m * n = x})" by (intro abs_summable_on_cong) auto finally have summable'': \ . from abs_summable_on_Sigma_project1'[OF this] show summable''': "summable (\n. norm (dirichlet_prod f g n / nat_power n s))" by (simp add: eq abs_summable_on_nat_iff') have "(\n. f n / nat_power n s) * (\n. g n / nat_power n s) = (\\<^sub>an. f n / nat_power n s) * (\\<^sub>an. g n / nat_power n s)" using summable' by (simp add: infsetsum_nat') also have "\ = (\\<^sub>a(m,n). (f m / nat_power m s) * (g n / nat_power n s))" using summable' by (subst infsetsum_product [symmetric]) simp_all also have "\ = (\\<^sub>a(m,n). f m * g n / nat_power (m * n) s)" using f_g by (intro infsetsum_cong refl) auto also have "\ = (\\<^sub>a(x,(m,n))\(SIGMA x:UNIV. {(m,n). m * n = x}). f m * g n / nat_power (m * n) s)" unfolding case_prod_unfold by (rule infsetsum_reindex_bij_betw [symmetric]) (auto simp: bij_betw_def inj_on_def image_iff) also have "\ = (\\<^sub>a(x,(m,n))\(SIGMA x:UNIV. {(m,n). m * n = x}). f m * g n / nat_power x s)" by (intro infsetsum_cong refl) (auto simp: case_prod_unfold) also have "\ = (\\<^sub>ax. dirichlet_prod f g x / nat_power x s)" (is "_ = infsetsum ?T _") using summable'' by (subst infsetsum_Sigma) (auto simp: eq) also have "\ = (\x. dirichlet_prod f g x / nat_power x s)" using summable''' by (intro infsetsum_nat') (simp_all add: abs_summable_on_nat_iff') finally show "\ = (\n. f n / nat_power n s) * (\n. g n / nat_power n s)" .. qed lemma fixes f g :: "nat \ real" fixes s :: real assumes "f 0 = 0" "g 0 = 0" assumes summable: "summable (\n. norm (f n / real n powr s))" "summable (\n. norm (g n / real n powr s))" shows summable_dirichlet_prod_real: "summable (\n. norm (dirichlet_prod f g n / real n powr s))" and suminf_dirichlet_prod_real: "(\n. dirichlet_prod f g n / real n powr s) = (\n. f n / nat_power n s) * (\n. g n / real n powr s)" using summable_dirichlet_prod[of f g s] suminf_dirichlet_prod[of f g s] assms by simp_all lemma fds_abs_converges_mult: fixes s :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology}" assumes "fds_abs_converges f s" "fds_abs_converges g s" shows "fds_abs_converges (f * g) s" using summable_dirichlet_prod[OF _ _ assms[unfolded fds_abs_converges_def]] by (simp add: fds_abs_converges_def fds_nth_mult) lemma fds_abs_converges_power: fixes s :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology}" shows "fds_abs_converges f s \ fds_abs_converges (f ^ n) s" by (induction n) (auto intro!: fds_abs_converges_mult) lemma fds_abs_converges_prod: fixes s :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology}" shows "(\x. x \ A \ fds_abs_converges (f x) s) \ fds_abs_converges (prod f A) s" by (induction A rule: infinite_finite_induct) (auto intro!: fds_abs_converges_mult) lemma abs_conv_abscissa_mult_le: "abs_conv_abscissa (f * g :: 'a :: dirichlet_series fds) \ max (abs_conv_abscissa f) (abs_conv_abscissa g)" proof (rule abs_conv_abscissa_leI, goal_cases) case (1 c') thus ?case by (auto intro!: exI[of _ "of_real c'"] fds_abs_converges_mult intro: fds_abs_converges) qed lemma abs_conv_abscissa_mult_leI: "abs_conv_abscissa (f :: 'a :: dirichlet_series fds) \ d \ abs_conv_abscissa g \ d \ abs_conv_abscissa (f * g) \ d" using abs_conv_abscissa_mult_le[of f g] by (auto simp add: le_max_iff_disj) lemma abs_conv_abscissa_shift [simp]: "abs_conv_abscissa (fds_shift c f) = abs_conv_abscissa (f :: 'a :: dirichlet_series fds) + c \ 1" proof - have "abs_conv_abscissa (fds_shift c f) \ abs_conv_abscissa f + c \ 1" for c :: 'a and f proof (rule abs_conv_abscissa_leI) fix d assume "abs_conv_abscissa f + c \ 1 < ereal d" hence "abs_conv_abscissa f < ereal (d - c \ 1)" by (cases "abs_conv_abscissa f") auto hence "fds_abs_converges (fds_shift c f) (of_real d)" by (auto intro!: fds_abs_converges_shift fds_abs_converges simp: algebra_simps) thus "\s. s \ 1 = d \ fds_abs_converges (fds_shift c f) s" by (auto intro!: exI[of _ "of_real d"]) qed note * = this[of c f] this[of "-c" "fds_shift c f"] show ?thesis by (cases "abs_conv_abscissa (fds_shift c f)"; cases "abs_conv_abscissa f") (insert *, auto intro!: antisym) qed lemma eval_fds_mult: fixes s :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology}" assumes "fds_abs_converges f s" "fds_abs_converges g s" shows "eval_fds (f * g) s = eval_fds f s * eval_fds g s" using suminf_dirichlet_prod[OF _ _ assms[unfolded fds_abs_converges_def]] by (simp_all add: eval_fds_def fds_nth_mult) lemma eval_fds_power: fixes s :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology}" assumes "fds_abs_converges f s" shows "eval_fds (f ^ n) s = eval_fds f s ^ n" using assms by (induction n) (simp_all add: eval_fds_mult fds_abs_converges_power) lemma eval_fds_prod: fixes s :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology}" assumes "(\x. x \ A \ fds_abs_converges (f x) s)" shows "eval_fds (prod f A) s = (\x\A. eval_fds (f x) s)" using assms by (induction A rule: infinite_finite_induct) (auto simp: eval_fds_mult fds_abs_converges_prod) lemma eval_fds_inverse: fixes s :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology}" assumes "fds_abs_converges f s" "fds_abs_converges (inverse f) s" "fds_nth f 1 \ 0" shows "eval_fds (inverse f) s = inverse (eval_fds f s)" proof - have "eval_fds (inverse f * f) s = eval_fds (inverse f) s * eval_fds f s" by (intro eval_fds_mult assms) also have "inverse f * f = 1" by (intro fds_left_inverse assms) also have "eval_fds 1 s = 1" by simp finally show ?thesis by (auto simp: divide_simps) qed lemma eval_fds_integral_has_field_derivative: fixes s :: "'a :: dirichlet_series" assumes "ereal (s \ 1) > abs_conv_abscissa f" assumes "fds_nth f 1 = 0" shows "(eval_fds (fds_integral c f) has_field_derivative eval_fds f s) (at s)" proof - have "conv_abscissa (fds_integral c f) \ abs_conv_abscissa (fds_integral c f)" by (rule conv_le_abs_conv_abscissa) also from assms have "\ < ereal (s \ 1)" by (simp add: abs_conv_abscissa_integral) finally have "(eval_fds (fds_integral c f) has_field_derivative eval_fds (fds_deriv (fds_integral c f)) s) (at s)" by (intro derivative_eq_intros) auto also from assms have "fds_deriv (fds_integral c f) = f" by simp finally show ?thesis . qed lemma holomorphic_fds_eval [holomorphic_intros]: "A \ {z. Re z > conv_abscissa f} \ eval_fds f holomorphic_on A" unfolding holomorphic_on_def field_differentiable_def by (rule ballI exI derivative_intros)+ auto lemma analytic_fds_eval [holomorphic_intros]: assumes "A \ {z. Re z > conv_abscissa f}" shows "eval_fds f analytic_on A" proof - have "eval_fds f analytic_on {z. Re z > conv_abscissa f}" proof (subst analytic_on_open) show "open {z. Re z > conv_abscissa f}" by (cases "conv_abscissa f") (simp_all add: open_halfspace_Re_gt) qed (intro holomorphic_intros, simp_all) from analytic_on_subset[OF this assms] show ?thesis . qed lemma conv_abscissa_0 [simp]: "conv_abscissa (0 :: 'a :: dirichlet_series fds) = -\" by (auto simp: conv_abscissa_MInf_iff) lemma abs_conv_abscissa_0 [simp]: "abs_conv_abscissa (0 :: 'a :: dirichlet_series fds) = -\" by (auto simp: abs_conv_abscissa_MInf_iff) lemma conv_abscissa_1 [simp]: "conv_abscissa (1 :: 'a :: dirichlet_series fds) = -\" by (auto simp: conv_abscissa_MInf_iff) lemma abs_conv_abscissa_1 [simp]: "abs_conv_abscissa (1 :: 'a :: dirichlet_series fds) = -\" by (auto simp: abs_conv_abscissa_MInf_iff) lemma conv_abscissa_const [simp]: "conv_abscissa (fds_const (c :: 'a :: dirichlet_series)) = -\" by (auto simp: conv_abscissa_MInf_iff) lemma abs_conv_abscissa_const [simp]: "abs_conv_abscissa (fds_const (c :: 'a :: dirichlet_series)) = -\" by (auto simp: abs_conv_abscissa_MInf_iff) lemma conv_abscissa_numeral [simp]: "conv_abscissa (numeral n :: 'a :: dirichlet_series fds) = -\" by (auto simp: numeral_fds) lemma abs_conv_abscissa_numeral [simp]: "abs_conv_abscissa (numeral n :: 'a :: dirichlet_series fds) = -\" by (auto simp: numeral_fds) lemma abs_conv_abscissa_power_le: "abs_conv_abscissa (f ^ n :: 'a :: dirichlet_series fds) \ abs_conv_abscissa f" by (induction n) (auto intro!: order.trans[OF abs_conv_abscissa_mult_le]) lemma abs_conv_abscissa_power_leI: "abs_conv_abscissa (f :: 'a :: dirichlet_series fds) \ d \ abs_conv_abscissa (f ^ n) \ d" by (rule order.trans[OF abs_conv_abscissa_power_le]) lemma abs_conv_abscissa_prod_le: assumes "\x. x \ A \ abs_conv_abscissa (f x :: 'a :: dirichlet_series fds) \ d" shows "abs_conv_abscissa (prod f A) \ d" using assms by (induction A rule: infinite_finite_induct) (auto intro!: abs_conv_abscissa_mult_leI) lemma conv_abscissa_add_le: "conv_abscissa (f + g :: 'a :: dirichlet_series fds) \ max (conv_abscissa f) (conv_abscissa g)" by (rule conv_abscissa_leI_weak) (auto intro!: fds_converges_add intro: fds_converges) lemma conv_abscissa_add_leI: "conv_abscissa (f :: 'a :: dirichlet_series fds) \ d \ conv_abscissa g \ d \ conv_abscissa (f + g) \ d" using conv_abscissa_add_le[of f g] by (auto simp: le_max_iff_disj) lemma conv_abscissa_sum_leI: assumes "\x. x \ A \ conv_abscissa (f x :: 'a :: dirichlet_series fds) \ d" shows "conv_abscissa (sum f A) \ d" using assms by (induction A rule: infinite_finite_induct) (auto intro!: conv_abscissa_add_leI) lemma abs_conv_abscissa_add_le: "abs_conv_abscissa (f + g :: 'a :: dirichlet_series fds) \ max (abs_conv_abscissa f) (abs_conv_abscissa g)" by (rule abs_conv_abscissa_leI_weak) (auto intro!: fds_abs_converges_add intro: fds_abs_converges) lemma abs_conv_abscissa_add_leI: "abs_conv_abscissa (f :: 'a :: dirichlet_series fds) \ d \ abs_conv_abscissa g \ d \ abs_conv_abscissa (f + g) \ d" using abs_conv_abscissa_add_le[of f g] by (auto simp: le_max_iff_disj) lemma abs_conv_abscissa_sum_leI: assumes "\x. x \ A \ abs_conv_abscissa (f x :: 'a :: dirichlet_series fds) \ d" shows "abs_conv_abscissa (sum f A) \ d" using assms by (induction A rule: infinite_finite_induct) (auto intro!: abs_conv_abscissa_add_leI) lemma fds_converges_cmult_left [intro]: assumes "fds_converges f s" shows "fds_converges (fds_const c * f) s" proof - from assms have "summable (\n. c * (fds_nth f n / nat_power n s))" by (intro summable_mult) (auto simp: fds_converges_def) thus ?thesis by (simp add: fds_converges_def mult_ac) qed lemma fds_converges_cmult_right [intro]: assumes "fds_converges f s" shows "fds_converges (f * fds_const c) s" using fds_converges_cmult_left[OF assms] by (simp add: mult_ac) lemma conv_abscissa_cmult_left [simp]: fixes c :: "'a :: dirichlet_series" assumes "c \ 0" shows "conv_abscissa (fds_const c * f) = conv_abscissa f" proof - have "fds_converges (fds_const c * f) s \ fds_converges f s" for s proof assume "fds_converges (fds_const c * f) s" hence "fds_converges (fds_const (inverse c) * (fds_const c * f)) s" by (rule fds_converges_cmult_left) also have "fds_const (inverse c) * (fds_const c * f) = fds_const (inverse c * c) * f" by simp also have "inverse c * c = 1" using assms by simp finally show "fds_converges f s" by simp qed auto thus ?thesis by (simp add: conv_abscissa_def) qed lemma conv_abscissa_cmult_right [simp]: fixes c :: "'a :: dirichlet_series" assumes "c \ 0" shows "conv_abscissa (f * fds_const c) = conv_abscissa f" using assms by (subst mult.commute) auto lemma abs_conv_abscissa_cmult: fixes c :: "'a :: dirichlet_series" assumes "c \ 0" shows "abs_conv_abscissa (fds_const c * f) = abs_conv_abscissa f" proof (intro antisym) have "abs_conv_abscissa (fds_const (inverse c) * (fds_const c * f)) \ abs_conv_abscissa (fds_const c * f)" using abs_conv_abscissa_mult_le[of "fds_const (inverse c)" "fds_const c * f"] by (auto simp: max_def) also have "fds_const (inverse c) * (fds_const c * f) = fds_const (inverse c * c) * f" by (simp add: mult_ac) also have "inverse c * c = 1" using assms by simp finally show "abs_conv_abscissa f \ abs_conv_abscissa (fds_const c * f)" by simp qed (insert abs_conv_abscissa_mult_le[of "fds_const c" f], auto simp: max_def) lemma conv_abscissa_minus [simp]: fixes f :: "'a :: dirichlet_series fds" shows "conv_abscissa (-f) = conv_abscissa f" using conv_abscissa_cmult_left[of "-1" f] by simp lemma abs_conv_abscissa_minus [simp]: fixes f :: "'a :: dirichlet_series fds" shows "abs_conv_abscissa (-f) = abs_conv_abscissa f" using abs_conv_abscissa_cmult[of "-1" f] by simp lemma conv_abscissa_diff_le: "conv_abscissa (f - g :: 'a :: dirichlet_series fds) \ max (conv_abscissa f) (conv_abscissa g)" using conv_abscissa_add_le[of f "-g"] by simp lemma conv_abscissa_diff_leI: "conv_abscissa (f :: 'a :: dirichlet_series fds) \ d \ conv_abscissa g \ d \ conv_abscissa (f - g) \ d" using conv_abscissa_add_le[of f "-g"] by (auto simp: le_max_iff_disj) lemma abs_conv_abscissa_diff_le: "abs_conv_abscissa (f - g :: 'a :: dirichlet_series fds) \ max (abs_conv_abscissa f) (abs_conv_abscissa g)" using abs_conv_abscissa_add_le[of f "-g"] by simp lemma abs_conv_abscissa_diff_leI: "abs_conv_abscissa (f :: 'a :: dirichlet_series fds) \ d \ abs_conv_abscissa g \ d \ abs_conv_abscissa (f - g) \ d" using abs_conv_abscissa_add_le[of f "-g"] by (auto simp: le_max_iff_disj) lemmas eval_fds_integral_has_field_derivative' [derivative_intros] = DERIV_chain'[OF _ eval_fds_integral_has_field_derivative] lemma abs_conv_abscissa_completely_multiplicative_log_deriv: fixes f :: "'a :: dirichlet_series fds" assumes "completely_multiplicative_function (fds_nth f)" "fds_nth f 1 \ 0" shows "abs_conv_abscissa (fds_deriv f / f) \ abs_conv_abscissa f" proof - have "fds_deriv f = - fds (\n. fds_nth f n * mangoldt n) * f" using assms by (subst completely_multiplicative_fds_deriv') simp_all also have "\ / f = - fds (\n. fds_nth f n * mangoldt n) * (f * inverse f)" by (simp add: divide_fds_def) also have "f * inverse f = 1" using assms by (intro fds_right_inverse) finally have "fds_deriv f / f = - fds (\n. fds_nth f n * mangoldt n)" by simp also have "abs_conv_abscissa \ = abs_conv_abscissa (fds (\n. fds_nth f n * mangoldt n))" (is "_ = abs_conv_abscissa ?f") by (rule abs_conv_abscissa_minus) also have "\ \ abs_conv_abscissa f" proof (rule abs_conv_abscissa_leI, goal_cases) case (1 c) have "fds_abs_converges ?f (of_real c)" unfolding fds_abs_converges_def proof (rule summable_comparison_test_ev) from 1 have "fds_abs_converges (fds_deriv f) (of_real c)" by (intro fds_abs_converges) (auto simp: abs_conv_abscissa_deriv) thus "summable (\n. \ln (real n)\ * norm (fds_nth f n) / norm (nat_power n (of_real c :: 'a)))" by (simp add: fds_abs_converges_def fds_deriv_def fds_nth_fds' scaleR_conv_of_real powr_minus norm_mult norm_divide norm_nat_power) next show "\\<^sub>F n in sequentially. norm (norm (fds_nth (fds (\n. fds_nth f n * mangoldt n)) n / nat_power n (of_real c))) \ \ln (real n)\ * norm (fds_nth f n) / norm (nat_power n (of_real c) :: 'a)" using eventually_gt_at_top[of 0] proof eventually_elim case (elim n) have "norm (norm (fds_nth (fds (\n. fds_nth f n * mangoldt n)) n / nat_power n (of_real c))) = norm (fds_nth f n) * mangoldt n / real n powr c" using elim by (simp add: fds_nth_fds' norm_mult norm_divide norm_nat_power abs_mult mangoldt_nonneg) also have "\ \ norm (fds_nth f n) * ln n / real n powr c" using elim by (intro mult_left_mono divide_right_mono mangoldt_le) (simp_all add: mangoldt_def) finally show ?case using elim by (simp add: norm_nat_power algebra_simps) qed qed thus ?case by (intro exI[of _ "of_real c"]) auto qed finally show ?thesis . qed subsection \Uniqueness\ context assumes "SORT_CONSTRAINT ('a :: dirichlet_series)" begin lemma norm_dirichlet_series_cutoff_le: assumes "fds_abs_converges f (s0 :: 'a)" "N > 0" "s \ 1 \ c" "c \ s0 \ 1" shows "summable (\n. fds_nth f (n + N) / nat_power (n + N) s)" "summable (\n. norm (fds_nth f (n + N)) / nat_power (n + N) c)" and "norm (\n. fds_nth f (n + N) / nat_power (n + N) s) \ (\n. norm (fds_nth f (n + N)) / nat_power (n + N) c) / nat_power N (s \ 1 - c)" proof - from assms have "fds_abs_converges f (of_real c)" using fds_abs_converges_Re_le[of f s0 "of_real c"] by auto hence "summable (\n. norm (fds_nth f (n + N) / nat_power (n + N) (of_real c)))" unfolding fds_abs_converges_def by (rule summable_ignore_initial_segment) also have "?this \ summable (\n. norm (fds_nth f (n + N)) / nat_power (n + N) c)" by (intro summable_cong eventually_mono[OF eventually_gt_at_top[of "0::nat"]]) (auto simp: norm_divide norm_nat_power) finally show *: "summable (\n. norm (fds_nth f (n + N)) / nat_power (n + N) c)" . from assms have "fds_abs_converges f s" using fds_abs_converges_Re_le[of f s0 s] by auto hence **: "summable (\n. norm (fds_nth f (n + N) / nat_power (n + N) s))" unfolding fds_abs_converges_def by (rule summable_ignore_initial_segment) thus "summable (\n. fds_nth f (n + N) / nat_power (n + N) s)" by (rule summable_norm_cancel) have "norm (\n. fds_nth f (n + N) / nat_power (n + N) s) \ (\n. norm (fds_nth f (n + N) / nat_power (n + N) s))" by (intro summable_norm **) also have "\ \ (\n. norm (fds_nth f (n + N)) / nat_power (n + N) c / nat_power N (s \ 1 - c))" proof (intro suminf_le * ** summable_divide allI) fix n :: nat have "real N powr (s \ 1 - c) \ real (n + N) powr (s \ 1 - c)" using assms by (intro powr_mono2) simp_all also have "real (n + N) powr c * \ = real (n + N) powr (s \ 1)" by (simp add: powr_diff) finally have "norm (fds_nth f (n + N)) / real (n + N) powr (s \ 1) \ norm (fds_nth f (n + N)) / (real (n + N) powr c * real N powr (s \ 1 - c))" using \N > 0\ by (intro divide_left_mono) (simp_all add: mult_left_mono) thus "norm (fds_nth f (n + N) / nat_power (n + N) s) \ norm (fds_nth f (n + N)) / nat_power (n + N) c / nat_power N (s \ 1 - c)" using \N > 0\ by (simp add: norm_divide norm_nat_power ) qed also have "\ = (\n. norm (fds_nth f (n + N)) / nat_power (n + N) c) / nat_power N (s \ 1 - c)" using * by (rule suminf_divide) finally show "norm (\n. fds_nth f (n + N) / nat_power (n + N) s) \ \" . qed lemma eval_fds_zeroD_aux: fixes h :: "'a fds" assumes conv: "fds_abs_converges h (s0 :: 'a)" assumes freq: "frequently (\s. eval_fds h s = 0) ((\s. s \ 1) going_to at_top)" shows "h = 0" proof (rule ccontr) assume "h \ 0" hence ex: "\n>0. fds_nth h n \ 0" by (auto simp: fds_eq_iff) define N :: nat where "N = (LEAST n. n > 0 \ fds_nth h n \ 0)" have N: "N > 0" "fds_nth h N \ 0" using LeastI_ex[OF ex, folded N_def] by auto have less_N: "fds_nth h n = 0" if "n < N" for n using Least_le[of "\n. n > 0 \ fds_nth h n \ 0" n, folded N_def] that by (cases "n = 0") (auto simp: not_less) define c where "c = s0 \ 1" define remainder where "remainder = (\s. (\n. fds_nth h (n + Suc N) / nat_power (n + Suc N) s))" define A where "A = (\n. norm (fds_nth h (n + Suc N)) / nat_power (n + Suc N) c) * nat_power (Suc N) c" have eq: "fds_nth h N = nat_power N s * eval_fds h s - nat_power N s * remainder s" if "s \ 1 \ c" for s :: 'a proof - from conv and that have conv': "fds_abs_converges h s" unfolding c_def by (rule fds_abs_converges_Re_le) hence conv'': "fds_converges h s" by blast from conv'' have "(\n. fds_nth h n / nat_power n s) sums eval_fds h s" by (simp add: fds_converges_iff) hence "(\n. fds_nth h (n + Suc N) / nat_power (n + Suc N) s) sums (eval_fds h s - (\nnn = fds_nth h N / nat_power N s" by (subst sum.delta) auto finally show ?thesis unfolding remainder_def using \N > 0\ by (auto simp: sums_iff field_simps) qed have remainder_bound: "norm (remainder s) \ A / real (Suc N) powr (s \ 1)" if "s \ 1 \ c" for s :: 'a proof - note * = norm_dirichlet_series_cutoff_le[of h s0 "Suc N" c s, folded remainder_def] have "norm (remainder s) \ (\n. norm (fds_nth h (n + Suc N)) / nat_power (n + Suc N) c) / nat_power (Suc N) (s \ 1 - c)" using that assms unfolding remainder_def by (intro *) (simp_all add: c_def) also have "\ = A / real (Suc N) powr (s \ 1)" by (simp add: A_def powr_diff) finally show ?thesis . qed from freq have "\c. \s. s \ 1 \ c \ eval_fds h s = 0" unfolding frequently_def by (auto simp: eventually_going_to_at_top_linorder) hence "\k. \s. s \ 1 \ real k \ eval_fds h s = 0" by blast then obtain S where S: "\k. S k \ 1 \ real k \ eval_fds h (S k) = 0" by metis have S_limit: "filterlim (\k. S k \ 1) at_top sequentially" by (rule filterlim_at_top_mono[OF filterlim_real_sequentially]) (use S in auto) have "eventually (\k. real k \ c) sequentially" by real_asymp hence "eventually (\k. norm (fds_nth h N) \ (real N / real (Suc N)) powr (S k \ 1) * A) sequentially" proof eventually_elim case (elim k) hence "norm (fds_nth h N) = real N powr (S k \ 1) * norm (remainder (S k))" (is "_ = _ * ?X") using \N > 0\ S[of k] eq[of "S k"] by (auto simp: norm_mult norm_nat_power c_def) also have "norm (remainder (S k)) \ A / real (Suc N) powr (S k \ 1)" using elim S[of k] by (intro remainder_bound) (simp_all add: c_def) finally show ?case using N by (simp add: mult_left_mono powr_divide field_simps del: of_nat_Suc) qed moreover have "((\k. (real N / real (Suc N)) powr (S k \ 1) * A) \ 0) sequentially" by (rule filterlim_compose[OF _ S_limit]) (use \N > 0\ in real_asymp) ultimately have "((\_. fds_nth h N) \ 0) sequentially" by (rule Lim_null_comparison) hence "fds_nth h N = 0" by (simp add: tendsto_const_iff) with \fds_nth h N \ 0\ show False by contradiction qed lemma eval_fds_zeroD: fixes h :: "'a fds" assumes conv: "conv_abscissa h < \" assumes freq: "frequently (\s. eval_fds h s = 0) ((\s. s \ 1) going_to at_top)" shows "h = 0" proof - have [simp]: "2 \ (1 :: 'a) = 2" using of_real_inner_1[of 2] unfolding of_real_numeral by simp from conv obtain s where "fds_converges h s" by auto hence "fds_abs_converges h (s + 2)" by (rule fds_converges_imp_abs_converges) (auto simp: algebra_simps) from this assms(2-) show ?thesis by (rule eval_fds_zeroD_aux) qed lemma eval_fds_eqD: fixes f g :: "'a fds" assumes conv: "conv_abscissa f < \" "conv_abscissa g < \" assumes eq: "frequently (\s. eval_fds f s = eval_fds g s) ((\s. s \ 1) going_to at_top)" shows "f = g" proof - have conv': "conv_abscissa (f - g) < \" using assms by (intro le_less_trans[OF conv_abscissa_diff_le]) (auto simp: max_def) have "max (conv_abscissa f) (conv_abscissa g) < \" using conv by (auto simp: max_def) from ereal_dense2[OF this] obtain c where c: "max (conv_abscissa f) (conv_abscissa g) < ereal c" by auto (* TODO: something like "frequently_elim" would be great here *) have "frequently (\s. eval_fds f s = eval_fds g s \ s \ 1 \ c) ((\s. s \ 1) going_to at_top)" using eq by (rule frequently_eventually_frequently) auto hence *: "frequently (\s. eval_fds (f - g) s = 0) ((\s. s \ 1) going_to at_top)" proof (rule frequently_mono [rotated], safe, goal_cases) case (1 s) thus ?case using c by (subst eval_fds_diff) (auto intro!: fds_converges intro: less_le_trans) qed have "f - g = 0" by (rule eval_fds_zeroD fds_abs_converges_diff assms * conv')+ thus ?thesis by simp qed end subsection \Limit at infinity\ lemma eval_fds_at_top_tail_bound: fixes f :: "'a :: dirichlet_series fds" assumes c: "ereal c > abs_conv_abscissa f" defines "B \ (\n. norm (fds_nth f (n+2)) / real (n+2) powr c) * 2 powr c" assumes s: "s \ 1 \ c" shows "norm (eval_fds f s - fds_nth f 1) \ B / 2 powr (s \ 1)" proof - from c have "fds_abs_converges f (of_real c)" by (intro fds_abs_converges) simp_all also have "?this \ summable (\n. norm (fds_nth f n) / real n powr c)" unfolding fds_abs_converges_def by (intro summable_cong eventually_mono[OF eventually_gt_at_top[of "0::nat"]]) (auto simp: norm_divide norm_nat_power norm_powr_real_powr) finally have summable_c: \ . note c also from s have "ereal c \ ereal (s \ 1)" by simp finally have "fds_abs_converges f s" by (intro fds_abs_converges) auto hence summable: "summable (\n. norm (fds_nth f n / nat_power n s))" by (simp add: fds_abs_converges_def) from summable_norm_cancel[OF this] have "(\n. fds_nth f n / nat_power n s) sums eval_fds f s" by (simp add: eval_fds_def sums_iff) from sums_split_initial_segment[OF this, of "Suc (Suc 0)"] have "norm (eval_fds f s - fds_nth f 1) = norm (\n. fds_nth f (n+2) / nat_power (n+2) s)" by (auto simp: sums_iff) also have "\ \ (\n. norm (fds_nth f (n+2) / nat_power (n+2) s))" by (intro summable_norm summable_ignore_initial_segment summable) also have "\ \ (\n. norm (fds_nth f (n+2)) / real (n+2) powr c / 2 powr (s \ 1 - c))" proof (intro suminf_le allI) fix n :: nat have "norm (fds_nth f (n + 2) / nat_power (n + 2) s) = norm (fds_nth f (n + 2)) / real (n+2) powr c / real (n+2) powr (s \ 1 - c)" by (simp add: field_simps powr_diff norm_divide norm_nat_power) also have "\ \ norm (fds_nth f (n + 2)) / real (n+2) powr c / 2 powr (s \ 1 - c)" using s by (intro divide_left_mono divide_nonneg_pos powr_mono2 mult_pos_pos) simp_all finally show "norm (fds_nth f (n + 2) / nat_power (n + 2) s) \ \" . qed (intro summable_ignore_initial_segment summable summable_divide summable_c)+ also have "\ = (\n. norm (fds_nth f (n+2)) / real (n+2) powr c) / 2 powr (s \ 1 - c)" by (intro suminf_divide summable_ignore_initial_segment summable_c) also have "\ = B / 2 powr (s \ 1)" by (simp add: B_def powr_diff) finally show ?thesis . qed lemma tendsto_eval_fds_Re_at_top: assumes "conv_abscissa (f :: 'a :: dirichlet_series fds) \ \" assumes lim: "filterlim (\x. S x \ 1) at_top F" shows "((\x. eval_fds f (S x)) \ fds_nth f 1) F" proof - from assms(1) have "abs_conv_abscissa f < \" using abs_conv_le_conv_abscissa_plus_1[of f] by auto from ereal_dense2[OF this] obtain c where c: "abs_conv_abscissa f < ereal c" by auto define B where "B = (\n. norm (fds_nth f (n+2)) / real (n+2) powr c) * 2 powr c" have *: "norm (eval_fds f s - fds_nth f 1) \ B / 2 powr (s \ 1)" if s: "s \ 1 \ c" for s using eval_fds_at_top_tail_bound[of f c s] that c by (simp add: B_def) moreover from lim have "eventually (\x. S x \ 1 \ c) F" by (auto simp: filterlim_at_top) ultimately have "eventually (\x. norm (eval_fds f (S x) - fds_nth f 1) \ B / 2 powr (S x \ 1)) F" by (auto elim!: eventually_mono) moreover have "((\x. B / 2 powr (S x \ 1)) \ 0) F" using filterlim_tendsto_pos_mult_at_top[OF tendsto_const[of "ln 2"] _ lim] by (intro real_tendsto_divide_at_top[OF tendsto_const]) (auto simp: powr_def mult_ac intro!: filterlim_compose[OF exp_at_top]) ultimately have "((\x. eval_fds f (S x) - fds_nth f 1) \ 0) F" by (rule Lim_null_comparison) thus ?thesis by (subst (asm) Lim_null [symmetric]) qed lemma tendsto_eval_fds_Re_at_top': assumes "conv_abscissa (f :: complex fds) \ \" shows "uniform_limit UNIV (\\ t. eval_fds f (of_real \ + of_real t * \) ) (\_ .fds_nth f 1) at_top" proof - from assms(1) have "abs_conv_abscissa f < \" using abs_conv_le_conv_abscissa_plus_1[of f] by auto from ereal_dense2[OF this] obtain c where c: "abs_conv_abscissa f < ereal c" by auto define B where "B \ (\n. norm (fds_nth f (n+2)) / real (n+2) powr c) * 2 powr c" show ?thesis unfolding uniform_limit_iff proof safe fix \ :: real assume "\ > 0" hence "eventually (\\. B / 2 powr \ < \) at_top" by real_asymp thus "eventually (\\. \t\UNIV. dist (eval_fds f (of_real \ + of_real t * \)) (fds_nth f 1) < \) at_top" using eventually_ge_at_top[of c] proof eventually_elim case (elim \) show ?case proof fix t :: real have "dist (eval_fds f (of_real \ + of_real t * \)) (fds_nth f 1) \ B / 2 powr \" using eval_fds_at_top_tail_bound[of f c "of_real \ + of_real t * \"] elim c by (simp add: dist_norm B_def) also have "\ < \" by fact finally show "dist (eval_fds f (of_real \ + of_real t * \)) (fds_nth f 1) < \" . qed qed qed qed lemma tendsto_eval_fds_Re_going_to_at_top: assumes "conv_abscissa (f :: 'a :: dirichlet_series fds) \ \" shows "((\s. eval_fds f s) \ fds_nth f 1) ((\s. s \ 1) going_to at_top)" using assms by (rule tendsto_eval_fds_Re_at_top) auto lemma tendsto_eval_fds_Re_going_to_at_top': assumes "conv_abscissa (f :: complex fds) \ \" shows "((\s. eval_fds f s) \ fds_nth f 1) (Re going_to at_top)" using assms by (rule tendsto_eval_fds_Re_at_top) auto text \ Any Dirichlet series that is not identically zero and does not diverge everywhere has a half-plane in which it converges and is non-zero. \ theorem fds_nonzero_halfplane_exists: fixes f :: "'a :: dirichlet_series fds" assumes "conv_abscissa f < \" "f \ 0" shows "eventually (\s. fds_converges f s \ eval_fds f s \ 0) ((\s. s \ 1) going_to at_top)" proof - from ereal_dense2[OF assms(1)] obtain c where c: "conv_abscissa f < ereal c" by auto have "eventually (\s::'a. s \ 1 > c) ((\s. s \ 1) going_to at_top)" using eventually_gt_at_top[of c] by auto hence "eventually (\s. fds_converges f s) ((\s. s \ 1) going_to at_top)" by eventually_elim (use c in \auto intro!: fds_converges simp: less_le_trans\) moreover have "eventually (\s. eval_fds f s \ 0) ((\s. s \ 1) going_to at_top)" using eval_fds_zeroD[OF assms(1)] assms(2) by (auto simp: frequently_def) ultimately show ?thesis by (rule eventually_conj) qed subsection \Normed series\ lemma fds_converges_norm_iff [simp]: fixes s :: "'a :: {nat_power_normed_field,banach}" shows "fds_converges (fds_norm f) (s \ 1) \ fds_abs_converges f s" unfolding fds_converges_def fds_abs_converges_def by (rule summable_cong [OF eventually_mono[OF eventually_gt_at_top[of 0]]]) (simp add: fds_abs_converges_def fds_norm_def fds_nth_fds' norm_divide norm_nat_power) lemma fds_abs_converges_norm_iff [simp]: fixes s :: "'a :: {nat_power_normed_field,banach}" shows "fds_abs_converges (fds_norm f) (s \ 1) \ fds_abs_converges f s" unfolding fds_abs_converges_def by (rule summable_cong [OF eventually_mono[OF eventually_gt_at_top[of 0]]]) (simp add: fds_abs_converges_def fds_norm_def fds_nth_fds' norm_divide norm_nat_power) lemma fds_converges_norm_iff': fixes f :: "'a :: {nat_power_normed_field,banach} fds" shows "fds_converges (fds_norm f) s \ fds_abs_converges f (of_real s)" unfolding fds_converges_def fds_abs_converges_def by (rule summable_cong [OF eventually_mono[OF eventually_gt_at_top[of 0]]]) (simp add: fds_abs_converges_def fds_norm_def fds_nth_fds' norm_divide norm_nat_power) lemma fds_abs_converges_norm_iff': fixes f :: "'a :: {nat_power_normed_field,banach} fds" shows "fds_abs_converges (fds_norm f) s \ fds_abs_converges f (of_real s)" unfolding fds_abs_converges_def by (rule summable_cong [OF eventually_mono[OF eventually_gt_at_top[of 0]]]) (simp add: fds_abs_converges_def fds_norm_def fds_nth_fds' norm_divide norm_nat_power) lemma abs_conv_abscissa_norm [simp]: fixes f :: "'a :: dirichlet_series fds" shows "abs_conv_abscissa (fds_norm f) = abs_conv_abscissa f" proof (rule antisym) show "abs_conv_abscissa f \ abs_conv_abscissa (fds_norm f)" proof (rule abs_conv_abscissa_leI_weak) fix x assume "abs_conv_abscissa (fds_norm f) < ereal x" hence "fds_abs_converges (fds_norm f) (of_real x)" by (intro fds_abs_converges) auto thus "fds_abs_converges f (of_real x)" by (simp add: fds_abs_converges_norm_iff') qed qed (auto intro!: abs_conv_abscissa_leI_weak simp: fds_abs_converges_norm_iff' fds_abs_converges) lemma conv_abscissa_norm [simp]: fixes f :: "'a :: dirichlet_series fds" shows "conv_abscissa (fds_norm f) = abs_conv_abscissa f" proof (rule antisym) show "abs_conv_abscissa f \ conv_abscissa (fds_norm f)" proof (rule abs_conv_abscissa_leI_weak) fix x assume "conv_abscissa (fds_norm f) < ereal x" hence "fds_converges (fds_norm f) (of_real x)" by (intro fds_converges) auto thus "fds_abs_converges f (of_real x)" by (simp add: fds_converges_norm_iff') qed qed (auto intro!: conv_abscissa_leI_weak simp: fds_abs_converges) lemma fixes f g :: "'a :: dirichlet_series fds" assumes "fds_abs_converges (fds_norm f) s" "fds_abs_converges (fds_norm g) s" shows fds_abs_converges_norm_mult: "fds_abs_converges (fds_norm (f * g)) s" and eval_fds_norm_mult_le: "eval_fds (fds_norm (f * g)) s \ eval_fds (fds_norm f) s * eval_fds (fds_norm g) s" proof - show conv: "fds_abs_converges (fds_norm (f * g)) s" unfolding fds_abs_converges_def proof (rule summable_comparison_test_ev) have "fds_abs_converges (fds_norm f * fds_norm g) s" by (rule fds_abs_converges_mult assms)+ thus "summable (\n. norm (fds_nth (fds_norm f * fds_norm g) n) / nat_power n s)" by (simp add: fds_abs_converges_def) qed (auto intro!: always_eventually divide_right_mono order.trans[OF fds_nth_norm_mult_le] simp: norm_divide) have conv': "fds_abs_converges (fds_norm f * fds_norm g) s" by (intro fds_abs_converges_mult assms) hence "eval_fds (fds_norm (f * g)) s \ eval_fds (fds_norm f * fds_norm g) s" using conv unfolding eval_fds_def fds_abs_converges_def norm_divide by (intro suminf_le allI divide_right_mono) (simp_all add: norm_mult fds_nth_norm_mult_le) also have "\ = eval_fds (fds_norm f) s * eval_fds (fds_norm g) s" by (intro eval_fds_mult assms) finally show "eval_fds (fds_norm (f * g)) s \ eval_fds (fds_norm f) s * eval_fds (fds_norm g) s" . qed lemma eval_fds_norm_nonneg: assumes "fds_abs_converges (fds_norm f) s" shows "eval_fds (fds_norm f) s \ 0" using assms unfolding eval_fds_def fds_abs_converges_def by (intro suminf_nonneg) auto lemma fixes f :: "'a :: dirichlet_series fds" assumes "fds_abs_converges (fds_norm f) s" shows fds_abs_converges_norm_power: "fds_abs_converges (fds_norm (f ^ n)) s" and eval_fds_norm_power_le: "eval_fds (fds_norm (f ^ n)) s \ eval_fds (fds_norm f) s ^ n" proof - show *: "fds_abs_converges (fds_norm (f ^ n)) s" for n by (induction n) (auto intro!: fds_abs_converges_norm_mult assms) show "eval_fds (fds_norm (f ^ n)) s \ eval_fds (fds_norm f) s ^ n" by (induction n) (auto intro!: order.trans[OF eval_fds_norm_mult_le] assms * mult_left_mono eval_fds_norm_nonneg) qed subsection \Logarithms of Dirichlet series\ (* TODO: Move ? *) lemma eventually_gt_ereal_at_top: "c \ \ \ eventually (\x. ereal x > c) at_top" by (cases c) auto lemma eval_fds_log_deriv: fixes s :: "'a :: dirichlet_series" assumes "fds_nth f 1 \ 0" "s \ 1 > abs_conv_abscissa f" "s \ 1 > abs_conv_abscissa (fds_deriv f / f)" assumes "eval_fds f s \ 0" shows "eval_fds (fds_deriv f / f) s = eval_fds (fds_deriv f) s / eval_fds f s" proof - have "eval_fds (fds_deriv f / f * f) s = eval_fds (fds_deriv f / f) s * eval_fds f s" using assms by (intro eval_fds_mult fds_abs_converges) auto also have "fds_deriv f / f * f = fds_deriv f * (f * inverse f)" by (simp add: divide_fds_def algebra_simps) also have "f * inverse f = 1" using assms by (intro fds_right_inverse) finally show ?thesis using assms by simp qed text \ Given a sufficiently nice absolutely convergent Dirichlet series that converges to some function $f(s)$ and a holomorphic branch of $\ln f(s)$, we can construct a Dirichlet series that absolutely converges to that logarithm. \ lemma eval_fds_ln: fixes s0 :: ereal assumes nz: "\s. Re s > s0 \ eval_fds f s \ 0" "fds_nth f 1 \ 0" assumes l: "exp l = fds_nth f 1" "((g \ of_real) \ l) at_top" assumes g: "\s. Re s > s0 \ exp (g s) = eval_fds f s" assumes holo_g: "g holomorphic_on {s. Re s > s0}" assumes "ereal (Re s) > s0" assumes "s0 \ abs_conv_abscissa f" and "s0 \ abs_conv_abscissa (fds_deriv f / f)" shows "eval_fds (fds_ln l f) s = g s" proof - let ?s0 = "abs_conv_abscissa f" and ?s1 = "abs_conv_abscissa (inverse f)" let ?h = "\s. eval_fds (fds_ln l f) s - g s" let ?A = "{s. Re s > s0}" have open_A: "open ?A" by (cases s0) (auto simp: open_halfspace_Re_gt) have "conv_abscissa f \ abs_conv_abscissa f" by (rule conv_le_abs_conv_abscissa) moreover from assms have "\ \ \" by auto ultimately have "conv_abscissa f \ \" by auto have "conv_abscissa (fds_ln l f) \ abs_conv_abscissa (fds_ln l f)" by (rule conv_le_abs_conv_abscissa) also have "\ \ abs_conv_abscissa (fds_deriv f / f)" unfolding fds_ln_def by (simp add: abs_conv_abscissa_integral) finally have "conv_abscissa (fds_ln l f) \ \" using assms by (auto simp: max_def abs_conv_abscissa_deriv split: if_splits) have deriv_g [derivative_intros]: "(g has_field_derivative eval_fds (fds_deriv f) s / eval_fds f s) (at s within B)" if s: "Re s > s0" for s B proof - have "conv_abscissa f \ abs_conv_abscissa f" by (rule conv_le_abs_conv_abscissa) also have "\ \ s0" using assms by simp also have "\ < Re s" by fact finally have s': "Re s > conv_abscissa f" . have deriv_g: "(g has_field_derivative deriv g s) (at s)" using holomorphic_derivI[OF holo_g open_A, of s] s by (auto simp: at_within_open[OF _ open_A]) have "((\s. exp (g s)) has_field_derivative eval_fds f s * deriv g s) (at s)" (is ?P) by (rule derivative_eq_intros deriv_g s)+ (insert s, simp_all add: g) also from s have ev: "eventually (\t. t \ ?A) (nhds s)" by (intro eventually_nhds_in_open open_A) auto have "?P \ (eval_fds f has_field_derivative eval_fds f s * deriv g s) (at s)" by (intro DERIV_cong_ev refl eventually_mono[OF ev]) (auto simp: g) finally have "(eval_fds f has_field_derivative eval_fds f s * deriv g s) (at s)" . moreover have "(eval_fds f has_field_derivative eval_fds (fds_deriv f) s) (at s)" using s' assms by (intro derivative_intros) auto ultimately have "eval_fds f s * deriv g s = eval_fds (fds_deriv f) s" by (rule DERIV_unique) hence "deriv g s = eval_fds (fds_deriv f) s / eval_fds f s" using s nz by (simp add: field_simps) with deriv_g show ?thesis by (auto intro: has_field_derivative_at_within) qed have "\c. \z\{z. Re z > s0}. ?h z = c" - proof (rule DERIV_zero_constant, goal_cases) + proof (rule has_field_derivative_zero_constant, goal_cases) case 1 show ?case using convex_halfspace_gt[of _ "1::complex"] by (cases s0) auto next case (2 z) have "conv_abscissa (fds_ln l f) \ abs_conv_abscissa (fds_ln l f)" by (rule conv_le_abs_conv_abscissa) also have "\ \ abs_conv_abscissa (fds_deriv f / f)" by (simp add: abs_conv_abscissa_ln) also have "\ < Re z" using 2 assms by (auto simp: abs_conv_abscissa_deriv) finally have s1: "conv_abscissa (fds_ln l f) < ereal (Re z)" . have "conv_abscissa f \ abs_conv_abscissa f" by (rule conv_le_abs_conv_abscissa) also have "\ < Re z" using 2 assms by auto finally have s2: "conv_abscissa f < ereal (Re z)" . from l have "fds_nth f 1 \ 0" by auto with 2 assms have *: "eval_fds (fds_deriv f / f) z = eval_fds (fds_deriv f) z / (eval_fds f z)" by (auto simp: eval_fds_log_deriv) have "eval_fds f z \ 0" using 2 assms by auto show ?case using s1 s2 2 nz by (auto intro!: derivative_eq_intros simp: * field_simps) qed then obtain c where c: "\z. Re z > s0 \ ?h z = c" by blast have "(at_top :: real filter) \ bot" by simp moreover from assms have "s0 \ \" by auto have "eventually (\x. c = (?h \ of_real) x) at_top" using eventually_gt_ereal_at_top[OF \s0 \ \\] by eventually_elim (simp add: c) hence "((?h \ of_real) \ c) at_top" by (force intro: Lim_transform_eventually) moreover have "((?h \ of_real) \ fds_nth (fds_ln l f) 1 - l) at_top" using \conv_abscissa (fds_ln l f) \ \\ and l unfolding o_def by (intro tendsto_intros tendsto_eval_fds_Re_at_top) (auto simp: filterlim_ident) ultimately have "c = fds_nth (fds_ln l f) 1 - l" by (rule tendsto_unique) with c[OF \Re s > s0\] and l and nz show ?thesis by (simp add: exp_minus field_simps) qed text \ Less explicitly: For a sufficiently nice absolutely convergent Dirichlet series converging to a function $f(s)$, the formal logarithm absolutely converges to some logarithm of $f(s)$. \ lemma eval_fds_ln': fixes s0 :: ereal assumes "ereal (Re s) > s0" assumes "s0 \ abs_conv_abscissa f" and "s0 \ abs_conv_abscissa (fds_deriv f / f)" and nz: "\s. Re s > s0 \ eval_fds f s \ 0" "fds_nth f 1 \ 0" assumes l: "exp l = fds_nth f 1" shows "exp (eval_fds (fds_ln l f) s) = eval_fds f s" proof - let ?s0 = "abs_conv_abscissa f" and ?s1 = "abs_conv_abscissa (inverse f)" let ?h = "\s. eval_fds f s * exp (-eval_fds (fds_ln l f) s)" have "conv_abscissa f \ abs_conv_abscissa f" by (rule conv_le_abs_conv_abscissa) moreover from assms have "\ \ \" by auto ultimately have "conv_abscissa f \ \" by auto have "conv_abscissa (fds_ln l f) \ abs_conv_abscissa (fds_ln l f)" by (rule conv_le_abs_conv_abscissa) also have "\ \ abs_conv_abscissa (fds_deriv f / f)" unfolding fds_ln_def by (simp add: abs_conv_abscissa_integral) finally have "conv_abscissa (fds_ln l f) \ \" using assms by (auto simp: max_def abs_conv_abscissa_deriv split: if_splits) have "\c. \z\{z. Re z > s0}. ?h z = c" - proof (rule DERIV_zero_constant, goal_cases) + proof (rule has_field_derivative_zero_constant, goal_cases) case 1 show ?case using convex_halfspace_gt[of _ "1::complex"] by (cases s0) auto next case (2 z) have "conv_abscissa (fds_ln l f) \ abs_conv_abscissa (fds_ln l f)" by (rule conv_le_abs_conv_abscissa) also have "\ \ abs_conv_abscissa (fds_deriv f / f)" unfolding fds_ln_def by (simp add: abs_conv_abscissa_integral) also have "\ < Re z" using 2 assms by (auto simp: abs_conv_abscissa_deriv) finally have s1: "conv_abscissa (fds_ln l f) < ereal (Re z)" . have "conv_abscissa f \ abs_conv_abscissa f" by (rule conv_le_abs_conv_abscissa) also have "\ < Re z" using 2 assms by auto finally have s2: "conv_abscissa f < ereal (Re z)" . from l have "fds_nth f 1 \ 0" by auto with 2 assms have *: "eval_fds (fds_deriv f / f) z = eval_fds (fds_deriv f) z / (eval_fds f z)" by (subst eval_fds_log_deriv) auto have "eval_fds f z \ 0" using 2 assms by auto thus ?case using s1 s2 by (auto intro!: derivative_eq_intros simp: *) qed then obtain c where c: "\z. Re z > s0 \ ?h z = c" by blast have "(at_top :: real filter) \ bot" by simp moreover from assms have "s0 \ \" by auto have "eventually (\x. c = (?h \ of_real) x) at_top" using eventually_gt_ereal_at_top[OF \s0 \ \\] by eventually_elim (simp add: c) hence "((?h \ of_real) \ c) at_top" by (force intro: Lim_transform_eventually) moreover have "((?h \ of_real) \ fds_nth f 1 * exp (-fds_nth (fds_ln l f) 1)) at_top" unfolding o_def using \conv_abscissa (fds_ln l f) \ \\ and \conv_abscissa f \ \\ by (intro tendsto_intros tendsto_eval_fds_Re_at_top) (auto simp: filterlim_ident) ultimately have "c = fds_nth f 1 * exp (-fds_nth (fds_ln l f) 1)" by (rule tendsto_unique) with c[OF \Re s > s0\] and l and nz show ?thesis by (simp add: exp_minus field_simps) qed lemma fds_ln_completely_multiplicative: fixes f :: "'a :: dirichlet_series fds" assumes "completely_multiplicative_function (fds_nth f)" assumes "fds_nth f 1 \ 0" shows "fds_ln l f = fds (\n. if n = 1 then l else fds_nth f n * mangoldt n /\<^sub>R ln n)" proof - have "fds_ln l f = fds_integral l (fds_deriv f / f)" by (simp add: fds_ln_def) also have "fds_deriv f = -fds (\n. fds_nth f n * mangoldt n) * f" by (intro completely_multiplicative_fds_deriv' assms) also have "\ / f = -fds (\n. fds_nth f n * mangoldt n) * (f * inverse f)" by (simp add: divide_fds_def) also from assms have "f * inverse f = 1" by (simp add: fds_right_inverse) also have "fds_integral l (- fds (\n. fds_nth f n * mangoldt n) * 1) = fds (\n. if n = 1 then l else fds_nth f n * mangoldt n /\<^sub>R ln n)" by (simp add: fds_integral_def cong: if_cong) finally show ?thesis . qed lemma eval_fds_ln_completely_multiplicative_strong: fixes s :: "'a :: dirichlet_series" and l :: 'a and f :: "'a fds" and g :: "nat \ 'a" defines "h \ fds (\n. fds_nth (fds_ln l f) n * g n)" assumes "fds_abs_converges h s" assumes "completely_multiplicative_function (fds_nth f)" and "fds_nth f 1 \ 0" shows "(\(p,k). (fds_nth f p / nat_power p s) ^ Suc k * g (p ^ Suc k) / of_nat (Suc k)) abs_summable_on ({p. prime p} \ UNIV)" (is ?th1) and "eval_fds h s = l * g 1 + (\\<^sub>a(p, k)\{p. prime p}\UNIV. (fds_nth f p / nat_power p s) ^ Suc k * g (p ^ Suc k) / of_nat (Suc k))" (is ?th2) proof - let ?P = "{p::nat. prime p}" interpret f: completely_multiplicative_function "fds_nth f" by fact from assms have *: "(\n. fds_nth h n / nat_power n s) abs_summable_on UNIV" by (auto simp: abs_summable_on_nat_iff' fds_abs_converges_def) have eq: "h = fds (\n. if n = 1 then l * g 1 else fds_nth f n * g n * mangoldt n /\<^sub>R ln (real n))" using fds_ln_completely_multiplicative [OF assms(3), of l] by (simp add: h_def fds_eq_iff) note * also have "(\n. fds_nth h n / nat_power n s) abs_summable_on UNIV \ (\x. if x = Suc 0 then l * g 1 else fds_nth f x * g x * mangoldt x /\<^sub>R ln (real x) / nat_power x s) abs_summable_on {1} \ Collect primepow" using eq by (intro abs_summable_on_cong_neutral) (auto simp: fds_nth_fds mangoldt_def) finally have sum1: "(\x. if x = Suc 0 then l * g 1 else fds_nth f x * g x * mangoldt x /\<^sub>R ln (real x) / nat_power x s) abs_summable_on Collect primepow" by (rule abs_summable_on_subset) auto also have "?this \ (\x. fds_nth f x * g x * mangoldt x /\<^sub>R ln (real x) / nat_power x s) abs_summable_on Collect primepow" by (intro abs_summable_on_cong) (insert primepow_gt_Suc_0, auto) also have "\ \ (\(p,k). fds_nth f (p ^ Suc k) * g (p ^ Suc k) * mangoldt (p ^ Suc k) /\<^sub>R ln (real (p ^ Suc k)) / nat_power (p ^ Suc k) s) abs_summable_on (?P \ UNIV)" using bij_betw_primepows unfolding case_prod_unfold by (intro abs_summable_on_reindex_bij_betw [symmetric]) also have "\ \ ?th1" by (intro abs_summable_on_cong) (auto simp: f.mult f.power mangoldt_def aprimedivisor_prime_power ln_realpow prime_gt_0_nat nat_power_power_left divide_simps scaleR_conv_of_real simp del: power_Suc) finally show ?th1 . have "eval_fds h s = (\\<^sub>an. fds_nth h n / nat_power n s)" using * unfolding eval_fds_def by (subst infsetsum_nat') auto also have "\ = (\\<^sub>an \ {1} \ {n. primepow n}. if n = 1 then l * g 1 else fds_nth f n * g n * mangoldt n /\<^sub>R ln (real n) / nat_power n s)" by (intro infsetsum_cong_neutral) (auto simp: eq fds_nth_fds mangoldt_def) also have "\ = l * g 1 + (\\<^sub>an | primepow n. if n = 1 then l * g 1 else fds_nth f n * g n * mangoldt n /\<^sub>R ln (real n) / nat_power n s)" (is "_ = _ + ?x") using sum1 primepow_gt_Suc_0 by (subst infsetsum_Un_disjoint) auto also have "?x = (\\<^sub>an\Collect primepow. fds_nth f n * g n * mangoldt n /\<^sub>R ln (real n) / nat_power n s)" (is "_ = infsetsum ?f _") by (intro infsetsum_cong refl) (insert primepow_gt_Suc_0, auto) also have "\ = (\\<^sub>a(p,k)\(?P \ UNIV). fds_nth f (p ^ Suc k) * g (p ^ Suc k) * mangoldt (p ^ Suc k) /\<^sub>R ln (p ^ Suc k) / nat_power (p ^ Suc k) s)" using bij_betw_primepows unfolding case_prod_unfold by (intro infsetsum_reindex_bij_betw [symmetric]) also have "\ = (\\<^sub>a(p,k)\(?P \ UNIV). (fds_nth f p / nat_power p s) ^ Suc k * g (p ^ Suc k) / of_nat (Suc k))" by (intro infsetsum_cong) (auto simp: f.mult f.power mangoldt_def aprimedivisor_prime_power ln_realpow prime_gt_0_nat nat_power_power_left divide_simps scaleR_conv_of_real simp del: power_Suc) finally show ?th2 . qed lemma eval_fds_ln_completely_multiplicative: fixes s :: "'a :: dirichlet_series" and l :: 'a and f :: "'a fds" assumes "completely_multiplicative_function (fds_nth f)" and "fds_nth f 1 \ 0" assumes "s \ 1 > abs_conv_abscissa (fds_deriv f / f)" shows "(\(p,k). (fds_nth f p / nat_power p s) ^ Suc k / of_nat (Suc k)) abs_summable_on ({p. prime p} \ UNIV)" (is ?th1) and "eval_fds (fds_ln l f) s = l + (\\<^sub>a(p, k)\{p. prime p}\UNIV. (fds_nth f p / nat_power p s) ^ Suc k / of_nat (Suc k))" (is ?th2) proof - from assms have "fds_abs_converges (fds_ln l f) s" by (intro fds_abs_converges_ln) (auto intro!: fds_abs_converges_mult intro: fds_abs_converges) hence "fds_abs_converges (fds (\n. fds_nth (fds_ln l f) n * 1)) s" by simp from eval_fds_ln_completely_multiplicative_strong [OF this assms(1,2)] show ?th1 ?th2 by simp_all qed subsection \Exponential and logarithm\ lemma summable_fds_exp_aux: assumes "fds_nth f' 1 = (0 :: 'a :: real_normed_algebra_1)" shows "summable (\k. fds_nth (f' ^ k) n /\<^sub>R fact k)" proof (rule summable_finite) fix k assume "k \ {..n}" hence "n < k" by simp also have "\ < 2 ^ k" by (induction k) auto finally have "fds_nth (f' ^ k) n = 0" using assms by (intro fds_nth_power_eq_0) auto thus "fds_nth (f' ^ k) n /\<^sub>R fact k = 0" by simp qed auto lemma fixes f :: "'a :: dirichlet_series fds" assumes "fds_abs_converges f s" shows fds_abs_converges_exp: "fds_abs_converges (fds_exp f) s" and eval_fds_exp: "eval_fds (fds_exp f) s = exp (eval_fds f s)" proof - have conv: "fds_abs_converges (fds_exp f) s" and ev: "eval_fds (fds_exp f) s = exp (eval_fds f s)" if "fds_abs_converges f s" and [simp]: "fds_nth f (Suc 0) = 0" for f proof - have [simp]: "fds (\n. if n = Suc 0 then 0 else fds_nth f n) = f" by (intro fds_eqI) simp_all have "(\(k,n). fds_nth (f ^ k) n / fact k / nat_power n s) abs_summable_on (UNIV \ {1..})" proof (subst abs_summable_on_Sigma_iff, safe, goal_cases) case (3 k) from that have "fds_abs_converges (f ^ k) s" by (intro fds_abs_converges_power) hence "(\n. fds_nth (f ^ k) n / nat_power n s * inverse (fact k)) abs_summable_on {1..}" unfolding fds_abs_converges_altdef by (intro abs_summable_on_cmult_left) thus ?case by (simp add: field_simps) next case 4 show ?case unfolding abs_summable_on_nat_iff' proof (rule summable_comparison_test_ev[OF always_eventually[OF allI]]) fix k :: nat from that have *: "fds_abs_converges (fds_norm (f ^ k)) (s \ 1)" by (auto simp: fds_abs_converges_power) have "(\\<^sub>an\{1..}. norm (fds_nth (f ^ k) n / fact k / nat_power n s)) = (\\<^sub>an\{1..}. fds_nth (fds_norm (f ^ k)) n / nat_power n (s \ 1) / fact k)" (is "?S = _") by (intro infsetsum_cong) (simp_all add: norm_divide norm_mult norm_nat_power) also have "\ = (\\<^sub>an\{1..}. fds_nth (fds_norm (f ^ k)) n / nat_power n (s \ 1)) /\<^sub>R fact k" (is "_ = ?S' /\<^sub>R _") using * unfolding fds_abs_converges_altdef by (subst infsetsum_cdiv) (auto simp: abs_summable_on_nat_iff scaleR_conv_of_real divide_simps) also have "?S' = eval_fds (fds_norm (f ^ k)) (s \ 1)" using * unfolding fds_abs_converges_altdef eval_fds_def by (subst infsetsum_nat) (auto intro!: suminf_cong) finally have eq: "?S = \ /\<^sub>R fact k" . note eq also have "?S \ 0" by (intro infsetsum_nonneg) auto hence "?S = norm (norm ?S)" by simp also have "eval_fds (fds_norm (f ^ k)) (s \ 1) \ eval_fds (fds_norm f) (s \ 1) ^ k" using that by (intro eval_fds_norm_power_le) auto finally show "norm (norm (\\<^sub>an\{1..}. norm (fds_nth (f ^ k) n / fact k / nat_power n s))) \ eval_fds (fds_norm f) (s \ 1) ^ k /\<^sub>R fact k" by (simp add: divide_right_mono) next from exp_converges[of "eval_fds (fds_norm f) (s \ 1)"] show "summable (\x. eval_fds (fds_norm f) (s \ 1) ^ x /\<^sub>R fact x)" by (simp add: sums_iff) qed qed auto hence summable: "(\(n,k). fds_nth (f ^ k) n / fact k / nat_power n s) abs_summable_on {1..} \ UNIV" by (subst abs_summable_on_Times_swap) (simp add: case_prod_unfold) have summable': "(\k. fds_nth (f ^ k) n / fact k) abs_summable_on UNIV" for n using abs_summable_on_cmult_left[of "nat_power n s", OF abs_summable_on_Sigma_project2 [OF summable, of n]] by (cases "n = 0") simp_all have "(\n. \\<^sub>ak. fds_nth (f ^ k) n / fact k / nat_power n s) abs_summable_on {1..}" using summable by (rule abs_summable_on_Sigma_project1') auto also have "?this \ (\n. (\k. fds_nth (f ^ k) n / fact k) * inverse (nat_power n s)) abs_summable_on {1..}" proof (intro abs_summable_on_cong refl, goal_cases) case (1 n) hence "(\\<^sub>ak. fds_nth (f ^ k) n / fact k / nat_power n s) = (\\<^sub>ak. fds_nth (f ^ k) n / fact k) * inverse (nat_power n s)" using summable'[of n] by (subst infsetsum_cmult_left [symmetric]) (auto simp: field_simps) also have "(\\<^sub>ak. fds_nth (f ^ k) n / fact k) = (\k. fds_nth (f ^ k) n / fact k)" using summable'[of n] 1 by (intro abs_summable_on_cong refl infsetsum_nat') auto finally show ?case . qed finally show "fds_abs_converges (fds_exp f) s" by (simp add: fds_exp_def fds_nth_fds' abs_summable_on_Sigma_iff scaleR_conv_of_real fds_abs_converges_altdef field_simps) have "eval_fds (fds_exp f) s = (\n. (\k. fds_nth (f ^ k) n /\<^sub>R fact k) / nat_power n s)" by (simp add: fds_exp_def eval_fds_def fds_nth_fds') also have "\ = (\n. (\\<^sub>ak. fds_nth (f ^ k) n /\<^sub>R fact k) / nat_power n s)" proof (intro suminf_cong, goal_cases) case (1 n) show ?case proof (cases "n = 0") case False have "(\k. fds_nth (f ^ k) n /\<^sub>R fact k) = (\\<^sub>ak. fds_nth (f ^ k) n /\<^sub>R fact k)" using summable'[of n] False by (intro infsetsum_nat' [symmetric]) (auto simp: scaleR_conv_of_real field_simps) thus ?thesis by simp qed simp_all qed also have "\ = (\\<^sub>an. (\\<^sub>ak. fds_nth (f ^ k) n /\<^sub>R fact k) / nat_power n s)" proof (intro infsetsum_nat' [symmetric], goal_cases) case 1 have *: "UNIV - {Suc 0..} = {0}" by auto have "(\x. \\<^sub>ay. fds_nth (f ^ y) x / fact y / nat_power x s) abs_summable_on {1..}" by (intro abs_summable_on_Sigma_project1'[OF summable]) auto also have "?this \ (\x. (\\<^sub>ay. fds_nth (f ^ y) x / fact y) * inverse (nat_power x s)) abs_summable_on {1..}" using summable' by (intro abs_summable_on_cong refl, subst infsetsum_cmult_left [symmetric]) (auto simp: field_simps) also have "\ \ (\x. (\\<^sub>ay. fds_nth (f ^ y) x /\<^sub>R fact y) / (nat_power x s)) abs_summable_on {1..}" by (simp add: field_simps scaleR_conv_of_real) finally show ?case by (rule abs_summable_on_finite_diff) (use * in auto) qed also have "\ = (\\<^sub>an. (\\<^sub>ak. fds_nth (f ^ k) n /\<^sub>R fact k * inverse (nat_power n s)))" using summable' by (subst infsetsum_cmult_left) (auto simp: field_simps scaleR_conv_of_real) also have "\ = (\\<^sub>an\{1..}. (\\<^sub>ak. fds_nth (f ^ k) n /\<^sub>R fact k * inverse (nat_power n s)))" by (intro infsetsum_cong_neutral) (auto simp: Suc_le_eq) also have "\ = (\\<^sub>ak. \\<^sub>an\{1..}. fds_nth (f ^ k) n / nat_power n s /\<^sub>R fact k)" using summable by (subst infsetsum_swap) (auto simp: field_simps scaleR_conv_of_real case_prod_unfold) also have "\ = (\\<^sub>ak. (\\<^sub>an\{1..}. fds_nth (f ^ k) n / nat_power n s) /\<^sub>R fact k)" by (subst infsetsum_scaleR_right) simp also have "\ = (\\<^sub>ak. eval_fds f s ^ k /\<^sub>R fact k)" proof (intro infsetsum_cong refl, goal_cases) case (1 k) have *: "fds_abs_converges (f ^ k) s" by (intro fds_abs_converges_power that) have "(\\<^sub>an\{1..}. fds_nth (f ^ k) n / nat_power n s) = (\\<^sub>an. fds_nth (f ^ k) n / nat_power n s)" by (intro infsetsum_cong_neutral) (auto simp: Suc_le_eq) also have "\ = eval_fds (f ^ k) s" using * unfolding eval_fds_def by (intro infsetsum_nat') (auto simp: fds_abs_converges_def abs_summable_on_nat_iff') also from that have "\ = eval_fds f s ^ k" by (simp add: eval_fds_power) finally show ?case by simp qed also have "\ = (\k. eval_fds f s ^ k /\<^sub>R fact k)" using exp_converges[of "norm (eval_fds f s)"] by (intro infsetsum_nat') (auto simp: abs_summable_on_nat_iff' sums_iff field_simps norm_power) also have "\ = exp (eval_fds f s)" by (simp add: exp_def) finally show "eval_fds (fds_exp f) s = exp (eval_fds f s)" . qed define f' where "f' = f - fds_const (fds_nth f 1)" have *: "fds_abs_converges (fds_exp f') s" by (auto simp: f'_def intro!: fds_abs_converges_diff conv assms) have "fds_abs_converges (fds_const (exp (fds_nth f 1)) * fds_exp f') s" unfolding f'_def by (intro fds_abs_converges_mult conv fds_abs_converges_diff assms) auto thus "fds_abs_converges (fds_exp f) s" unfolding f'_def by (simp add: fds_exp_times_fds_nth_0) have "eval_fds (fds_exp f) s = eval_fds (fds_const (exp (fds_nth f 1)) * fds_exp f') s" by (simp add: f'_def fds_exp_times_fds_nth_0) also have "\ = exp (fds_nth f (Suc 0)) * eval_fds (fds_exp f') s" using * using assms by (subst eval_fds_mult) (simp_all) also have "\ = exp (eval_fds f s)" using ev[of f'] assms unfolding f'_def by (auto simp: fds_abs_converges_diff eval_fds_diff fds_abs_converges_imp_converges exp_diff) finally show "eval_fds (fds_exp f) s = exp (eval_fds f s)" . qed lemma fds_exp_add: fixes f :: "'a :: dirichlet_series fds" shows "fds_exp (f + g) = fds_exp f * fds_exp g" proof (rule fds_eqI_truncate) fix m :: nat assume m: "m > 0" let ?T = "fds_truncate m" have "?T (fds_exp (f + g)) = ?T (fds_exp (?T f + ?T g))" by (simp add: fds_truncate_exp fds_truncate_add_strong [symmetric]) also have "fds_exp (?T f + ?T g) = fds_exp (?T f) * fds_exp (?T g)" proof (rule eval_fds_eqD) have "fds_abs_converges (fds_exp (?T f + ?T g)) 0" by (intro fds_abs_converges_exp fds_abs_converges_add) auto thus "conv_abscissa (fds_exp (?T f + ?T g)) < \" using conv_abscissa_PInf_iff by blast hence "fds_abs_converges (fds_exp (fds_truncate m f) * fds_exp (fds_truncate m g)) 0" by (intro fds_abs_converges_mult fds_abs_converges_exp) auto thus "conv_abscissa (fds_exp (fds_truncate m f) * fds_exp (fds_truncate m g)) < \" using conv_abscissa_PInf_iff by blast show "frequently (\s. eval_fds (fds_exp (fds_truncate m f + fds_truncate m g)) s = eval_fds (fds_exp (fds_truncate m f) * fds_exp (fds_truncate m g)) s) ((\s. s \ 1) going_to at_top)" by (auto simp: eval_fds_add eval_fds_mult eval_fds_exp fds_abs_converges_add fds_abs_converges_exp exp_add) qed also have "?T \ = ?T (fds_exp f * fds_exp g)" by (subst fds_truncate_mult [symmetric], subst (1 2) fds_truncate_exp) (simp add: fds_truncate_mult) finally show "?T (fds_exp (f + g)) = \" . qed lemma fds_exp_minus: fixes f :: "'a :: dirichlet_series fds" shows "fds_exp (-f) = inverse (fds_exp f)" proof (rule fds_right_inverse_unique) have "fds_exp f * fds_exp (- f) = fds_exp (f + (-f))" by (subst fds_exp_add) simp_all also have "f + (-f) = 0" by simp also have "fds_exp \ = 1" by simp finally show "fds_exp f * fds_exp (-f) = 1" . qed lemma abs_conv_abscissa_exp: fixes f :: "'a :: dirichlet_series fds" shows "abs_conv_abscissa (fds_exp f) \ abs_conv_abscissa f" by (intro abs_conv_abscissa_mono fds_abs_converges_exp) lemma fds_deriv_exp [simp]: fixes f :: "'a :: dirichlet_series fds" shows "fds_deriv (fds_exp f) = fds_exp f * fds_deriv f" proof (rule fds_eqI_truncate) fix m :: nat assume m: "m > 0" let ?T = "fds_truncate m" have "abs_conv_abscissa (fds_deriv (?T f)) = -\" by (simp add: abs_conv_abscissa_deriv) have "?T (fds_deriv (fds_exp f)) = ?T (fds_deriv (fds_exp (?T f)))" by (simp add: fds_truncate_deriv fds_truncate_exp) also have "fds_deriv (fds_exp (?T f)) = fds_exp (?T f) * fds_deriv (?T f)" proof (rule eval_fds_eqD) note abscissa = conv_le_abs_conv_abscissa abs_conv_abscissa_exp note abscissa' = abscissa[THEN le_less_trans] have "fds_abs_converges (fds_deriv (fds_exp (fds_truncate m f))) 0" by (intro fds_abs_converges ) (auto simp: abs_conv_abscissa_deriv intro: le_less_trans[OF abs_conv_abscissa_exp]) thus "conv_abscissa (fds_deriv (fds_exp (fds_truncate m f))) < \" using conv_abscissa_PInf_iff by blast have "fds_abs_converges (fds_exp (fds_truncate m f) * fds_deriv (fds_truncate m f)) 0" by (intro fds_abs_converges_mult fds_abs_converges_exp) (auto intro: fds_abs_converges simp add: fds_truncate_deriv [symmetric]) thus "conv_abscissa (fds_exp (fds_truncate m f) * fds_deriv (fds_truncate m f)) < \" using conv_abscissa_PInf_iff by blast show "\\<^sub>F s in (\s. s \ 1) going_to at_top. eval_fds (fds_deriv (fds_exp (?T f))) s = eval_fds (fds_exp (?T f) * fds_deriv (?T f)) s" proof (intro always_eventually eventually_frequently allI, goal_cases) case (2 s) have "eval_fds (fds_deriv (fds_exp (?T f))) s = deriv (eval_fds (fds_exp (?T f))) s" by (auto simp: eval_fds_exp eval_fds_mult fds_abs_converges_mult fds_abs_converges_exp fds_abs_converges eval_fds_deriv abscissa') also have "eval_fds (fds_exp (?T f)) = (\s. exp (eval_fds (?T f) s))" by (intro ext eval_fds_exp) auto also have "deriv \ = (\s. exp (eval_fds (?T f) s) * deriv (eval_fds (?T f)) s)" by (auto intro!: DERIV_imp_deriv derivative_eq_intros simp: eval_fds_deriv) also have "\ = eval_fds (fds_exp (?T f) * fds_deriv (?T f))" by (auto simp: eval_fds_exp eval_fds_mult fds_abs_converges_mult fds_abs_converges_exp fds_abs_converges eval_fds_deriv abs_conv_abscissa_deriv) finally show ?case . qed auto qed also have "?T \ = ?T (fds_exp f * fds_deriv f)" by (subst fds_truncate_mult [symmetric]) (simp add: fds_truncate_exp fds_truncate_deriv [symmetric], simp add: fds_truncate_mult) finally show "?T (fds_deriv (fds_exp f)) = \" . qed lemma fds_exp_ln_strong: fixes f :: "'a :: dirichlet_series fds" assumes "fds_nth f (Suc 0) \ 0" shows "fds_exp (fds_ln l f) = fds_const (exp l / fds_nth f (Suc 0)) * f" proof - let ?c = "exp l / fds_nth f (Suc 0)" have "f * fds_const ?c = f * (fds_exp (-fds_ln l f) * fds_exp (fds_ln l f)) * fds_const ?c" (is "_ = _ * (?g * ?h) * _") by (subst fds_exp_add [symmetric]) simp also have "\ = fds_const ?c * (f * ?g) * ?h" by (simp add: mult_ac) also have "f * ?g = fds_const (inverse ?c)" proof (rule fds_deriv_eq_imp_eq) have "fds_deriv (f * fds_exp (-fds_ln l f)) = fds_exp (- fds_ln l f) * fds_deriv f * (1 - f / f)" by (simp add: divide_fds_def algebra_simps) also from assms have "f / f = 1" by (simp add: divide_fds_def fds_right_inverse) finally show "fds_deriv (f * fds_exp (-fds_ln l f)) = fds_deriv (fds_const (inverse ?c))" by simp qed (insert assms, auto simp: exp_minus field_simps) also have "fds_const ?c * fds_const (inverse ?c) = 1" using assms by (subst fds_const_mult [symmetric]) (simp add: divide_simps) finally show ?thesis by (simp add: mult_ac) qed lemma fds_exp_ln [simp]: fixes f :: "'a :: dirichlet_series fds" assumes "exp l = fds_nth f (Suc 0)" shows "fds_exp (fds_ln l f) = f" using assms by (subst fds_exp_ln_strong) auto lemma fds_ln_exp [simp]: fixes f :: "'a :: dirichlet_series fds" assumes "l = fds_nth f (Suc 0)" shows "fds_ln l (fds_exp f) = f" proof (rule fds_deriv_eq_imp_eq) have "fds_deriv (fds_ln l (fds_exp f)) = fds_deriv f * (fds_exp f / fds_exp f)" by (simp add: algebra_simps divide_fds_def) also have "fds_exp f / fds_exp f = 1" by (simp add: divide_fds_def fds_right_inverse) finally show "fds_deriv (fds_ln l (fds_exp f)) = fds_deriv f" by simp qed (insert assms, auto simp: field_simps) subsection \Euler products\ lemma fds_euler_product_LIMSEQ: fixes f :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology} fds" assumes "multiplicative_function (fds_nth f)" and "fds_abs_converges f s" shows "(\n. \p\n. if prime p then \i. fds_nth f (p ^ i) / nat_power (p ^ i) s else 1) \ eval_fds f s" unfolding eval_fds_def proof (rule euler_product_LIMSEQ) show "multiplicative_function (\n. fds_nth f n / nat_power n s)" by (rule multiplicative_function_divide_nat_power) fact+ qed (insert assms, auto simp: fds_abs_converges_def) lemma fds_euler_product_LIMSEQ': fixes f :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology} fds" assumes "completely_multiplicative_function (fds_nth f)" and "fds_abs_converges f s" shows "(\n. \p\n. if prime p then inverse (1 - fds_nth f p / nat_power p s) else 1) \ eval_fds f s" unfolding eval_fds_def proof (rule euler_product_LIMSEQ') show "completely_multiplicative_function (\n. fds_nth f n / nat_power n s)" by (rule completely_multiplicative_function_divide_nat_power) fact+ qed (insert assms, auto simp: fds_abs_converges_def) lemma fds_abs_convergent_euler_product: fixes f :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology} fds" assumes "multiplicative_function (fds_nth f)" and "fds_abs_converges f s" shows "abs_convergent_prod (\p. if prime p then \i. fds_nth f (p ^ i) / nat_power (p ^ i) s else 1)" unfolding eval_fds_def proof (rule abs_convergent_euler_product) show "multiplicative_function (\n. fds_nth f n / nat_power n s)" by (rule multiplicative_function_divide_nat_power) fact+ qed (insert assms, auto simp: fds_abs_converges_def) lemma fds_abs_convergent_euler_product': fixes f :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology} fds" assumes "completely_multiplicative_function (fds_nth f)" and "fds_abs_converges f s" shows "abs_convergent_prod (\p. if prime p then inverse (1 - fds_nth f p / nat_power p s) else 1)" unfolding eval_fds_def proof (rule abs_convergent_euler_product') show "completely_multiplicative_function (\n. fds_nth f n / nat_power n s)" by (rule completely_multiplicative_function_divide_nat_power) fact+ qed (insert assms, auto simp: fds_abs_converges_def) lemma fds_abs_convergent_zero_iff: fixes f :: "'a :: {nat_power_field, real_normed_field, banach, second_countable_topology} fds" assumes "completely_multiplicative_function (fds_nth f)" assumes "fds_abs_converges f s" shows "eval_fds f s = 0 \ (\p. prime p \ fds_nth f p = nat_power p s)" proof - let ?g = "\p. if prime p then inverse (1 - fds_nth f p / nat_power p s) else 1" have lim: "(\n. \p\n. ?g p) \ eval_fds f s" by (intro fds_euler_product_LIMSEQ' assms) have conv: "convergent_prod ?g" by (intro abs_convergent_prod_imp_convergent_prod fds_abs_convergent_euler_product' assms) { assume "eval_fds f s = 0" from convergent_prod_to_zero_iff[OF conv] and this and lim have "\p. prime p \ fds_nth f p = nat_power p s" by (auto split: if_splits) } moreover { assume "\p. prime p \ fds_nth f p = nat_power p s" then obtain p where "prime p" "fds_nth f p = nat_power p s" by blast moreover from this have "nat_power p s \ 0" by (intro nat_power_nonzero) (auto simp: prime_gt_0_nat) ultimately have "(\n. \p\n. ?g p) \ 0" using convergent_prod_to_zero_iff[OF conv] by (auto intro!: exI[of _ p] split: if_splits) from tendsto_unique[OF _ lim this] have "eval_fds f s = 0" by simp } ultimately show ?thesis by blast qed lemma fixes s :: "'a :: {nat_power_normed_field,banach,euclidean_space}" assumes "s \ 1 > 1" shows euler_product_fds_zeta: "(\n. \p\n. if prime p then inverse (1 - 1 / nat_power p s) else 1) \ eval_fds fds_zeta s" (is ?th1) and eval_fds_zeta_nonzero: "eval_fds fds_zeta s \ 0" proof - have *: "completely_multiplicative_function (fds_nth fds_zeta)" by standard auto have lim: "(\n. \p\n. if prime p then inverse (1 - fds_nth fds_zeta p / nat_power p s) else 1) \ eval_fds fds_zeta s" (is "filterlim ?g _ _") using assms by (intro fds_euler_product_LIMSEQ' * fds_abs_summable_zeta) also have "?g = (\n. \p\n. if prime p then inverse (1 - 1 / nat_power p s) else 1)" by (intro ext prod.cong refl) (auto simp: fds_zeta_def fds_nth_fds) finally show ?th1 . { fix p :: nat assume "prime p" from this have "p > 1" by (simp add: prime_gt_Suc_0_nat) hence "norm (nat_power p s) = real p powr (s \ 1)" by (simp add: norm_nat_power) also have "\ > real p powr 0" using assms and \p > 1\ by (intro powr_less_mono) auto finally have "nat_power p s \ 1" using \p > 1\ by auto } hence **: "\p. prime p \ fds_nth fds_zeta p = nat_power p s" by (auto simp: fds_zeta_def fds_nth_fds) show "eval_fds fds_zeta s \ 0" using assms * ** by (subst fds_abs_convergent_zero_iff) simp_all qed lemma fds_primepow_subseries_euler_product_cm: fixes f :: "'a :: dirichlet_series fds" assumes "completely_multiplicative_function (fds_nth f)" "prime p" assumes "s \ 1 > abs_conv_abscissa f" shows "eval_fds (fds_primepow_subseries p f) s = 1 / (1 - fds_nth f p / nat_power p s)" proof - let ?f = "(\n. \pa\n. if prime pa then inverse (1 - fds_nth (fds_primepow_subseries p f) pa / nat_power pa s) else 1)" have "sequentially \ bot" by simp moreover have "?f \ eval_fds (fds_primepow_subseries p f) s" by (intro fds_euler_product_LIMSEQ' completely_multiplicative_function_only_pows assms fds_abs_converges_subseries) (insert assms, auto intro!: fds_abs_converges) moreover have "eventually (\n. ?f n = 1 / (1 - fds_nth f p / nat_power p s)) at_top" using eventually_ge_at_top[of p] proof eventually_elim case (elim n) have "(\pa\n. if prime pa then inverse (1 - fds_nth (fds_primepow_subseries p f) pa / nat_power pa s) else 1) = (\q\n. if q = p then inverse (1 - fds_nth f p / nat_power p s) else 1)" using \prime p\ by (intro prod.cong) (auto simp: fds_nth_subseries prime_prime_factors) also have "\ = 1 / (1 - fds_nth f p / nat_power p s)" using elim by (subst prod.delta) (auto simp: divide_simps) finally show ?case . qed hence "?f \ 1 / (1 - fds_nth f p / nat_power p s)" by (rule tendsto_eventually) ultimately show ?thesis by (rule tendsto_unique) qed subsection \Non-negative Dirichlet series\ lemma nonneg_Reals_sum: "(\x. x \ A \ f x \ \\<^sub>\\<^sub>0) \ sum f A \ \\<^sub>\\<^sub>0" by (induction A rule: infinite_finite_induct) auto locale nonneg_dirichlet_series = fixes f :: "'a :: dirichlet_series fds" assumes nonneg_coeffs_aux: "n > 0 \ fds_nth f n \ \\<^sub>\\<^sub>0" begin lemma nonneg_coeffs: "fds_nth f n \ \\<^sub>\\<^sub>0" using nonneg_coeffs_aux[of n] by (cases "n = 0") auto end lemma nonneg_dirichlet_series_0 [simp,intro]: "nonneg_dirichlet_series 0" by standard (auto simp: zero_fds_def) lemma nonneg_dirichlet_series_1 [simp,intro]: "nonneg_dirichlet_series 1" by standard (auto simp: one_fds_def) lemma nonneg_dirichlet_series_const [simp,intro]: "c \ \\<^sub>\\<^sub>0 \ nonneg_dirichlet_series (fds_const c)" by standard (auto simp: fds_const_def) lemma nonneg_dirichlet_series_add [intro]: assumes "nonneg_dirichlet_series f" "nonneg_dirichlet_series g" shows "nonneg_dirichlet_series (f + g)" proof - interpret f: nonneg_dirichlet_series f by fact interpret g: nonneg_dirichlet_series g by fact show ?thesis by standard (auto intro!: nonneg_Reals_add_I f.nonneg_coeffs g.nonneg_coeffs) qed lemma nonneg_dirichlet_series_mult [intro]: assumes "nonneg_dirichlet_series f" "nonneg_dirichlet_series g" shows "nonneg_dirichlet_series (f * g)" proof - interpret f: nonneg_dirichlet_series f by fact interpret g: nonneg_dirichlet_series g by fact show ?thesis by standard (auto intro!: nonneg_Reals_sum nonneg_Reals_mult_I f.nonneg_coeffs g.nonneg_coeffs simp: fds_nth_mult dirichlet_prod_def) qed lemma nonneg_dirichlet_series_power [intro]: assumes "nonneg_dirichlet_series f" shows "nonneg_dirichlet_series (f ^ n)" using assms by (induction n) auto context nonneg_dirichlet_series begin lemma nonneg_exp [intro]: "nonneg_dirichlet_series (fds_exp f)" proof fix n :: nat assume "n > 0" define c where "c = exp (fds_nth f (Suc 0))" define f' where "f' = fds (\n. if n = Suc 0 then 0 else fds_nth f n)" from nonneg_coeffs[of 1] obtain c' where "fds_nth f (Suc 0) = of_real c'" by (auto elim!: nonneg_Reals_cases) hence "c = of_real (exp c')" by (simp add: c_def exp_of_real) hence c: "c \ \\<^sub>\\<^sub>0" by simp have less: "n < 2 ^ k" if "n < k" for k proof - have "n < k" by fact also have "\ < 2 ^ k" by (induction k) auto finally show ?thesis . qed have nonneg_power: "fds_nth (f' ^ k) n \ \\<^sub>\\<^sub>0" for k proof - have "nonneg_dirichlet_series f'" by standard (insert nonneg_coeffs, auto simp: f'_def) interpret nonneg_dirichlet_series "f' ^ k" by (intro nonneg_dirichlet_series_power) fact+ from nonneg_coeffs[of n] show ?thesis . qed hence "fds_nth (fds_exp f) n = c * (\k. fds_nth (f' ^ k) n /\<^sub>R fact k)" by (simp add: fds_exp_def fds_nth_fds' f'_def c_def) also have "(\k. fds_nth (f' ^ k) n /\<^sub>R fact k) = (\k\n. fds_nth (f' ^ k) n /\<^sub>R fact k)" by (intro suminf_finite) (auto intro!: fds_nth_power_eq_0 less simp: f'_def not_le) also have "c * \ \ \\<^sub>\\<^sub>0" unfolding scaleR_conv_of_real by (intro nonneg_Reals_mult_I nonneg_Reals_sum nonneg_power, unfold nonneg_Reals_of_real_iff ) (auto simp: c) finally show "fds_nth (fds_exp f) n \ \\<^sub>\\<^sub>0" . qed end lemma nonneg_dirichlet_series_lnD: assumes "nonneg_dirichlet_series (fds_ln l f)" "exp l = fds_nth f (Suc 0)" shows "nonneg_dirichlet_series f" proof - from assms have "nonneg_dirichlet_series (fds_exp (fds_ln l f))" by (intro nonneg_dirichlet_series.nonneg_exp) thus ?thesis using assms by simp qed context nonneg_dirichlet_series begin lemma fds_of_real_norm: "fds_of_real (fds_norm f) = f" proof (rule fds_eqI) fix n :: nat assume n: "n > 0" show "fds_nth (fds_of_real (fds_norm f)) n = fds_nth f n" using nonneg_coeffs[of n] by (auto elim!: nonneg_Reals_cases) qed end (* TODO: Simplify proof *) lemma pringsheim_landau_aux: fixes c :: real and f :: "complex fds" assumes "nonneg_dirichlet_series f" assumes abscissa: "c \ abs_conv_abscissa f" assumes g: "\s. s \ A \ Re s > c \ g s = eval_fds f s" assumes "g holomorphic_on A" "open A" "c \ A" shows "\x. x < c \ fds_abs_converges f (of_real x)" proof - interpret nonneg_dirichlet_series f by fact define a where "a = 1 + c" define g' where "g' = (\s. if s \ {s. Re s > c} then eval_fds f s else g s)" \ \We can find some $\varepsilon > 0$ such that the Dirichlet series can be continued analytically in a ball of radius $1 + \varepsilon$ around $a$.\ from \open A\ \c \ A\ obtain \ where \: "\ > 0" "ball c \ \ A" by (auto simp: open_contains_ball) define \ where "\ = sqrt (1 + \^2) - 1" from \ have \: "\ > 0" by (simp add: \_def) have ball_a_subset: "ball a (1 + \) \ {s. Re s > c} \ A" proof (intro subsetI) fix s :: complex assume s: "s \ ball a (1 + \)" define x y where "x = Re s" and "y = Im s" have [simp]: "s = x + \ * y" by (simp add: complex_eq_iff x_def y_def) show "s \ {s. Re s > c} \ A" proof (cases "Re s \ c") case True hence "(c - x)\<^sup>2 + y\<^sup>2 \ (1 + c - x)\<^sup>2 + y\<^sup>2 - 1" by (simp add: power2_eq_square algebra_simps) also from s have "(1 + c - x)\<^sup>2 + y\<^sup>2 - 1 < \\<^sup>2" by (auto simp: dist_norm cmod_def a_def \_def) finally have "sqrt ((c - x)\<^sup>2 + y\<^sup>2) < \" using \ by (intro real_less_lsqrt) auto hence "s \ ball c \" by (auto simp: dist_norm cmod_def) also have "\ \ A" by fact finally show ?thesis .. qed auto qed have holo: "g' holomorphic_on ball a (1 + \)" unfolding g'_def proof (intro holomorphic_on_subset[OF _ ball_a_subset] holomorphic_on_If_Un) have "conv_abscissa f \ abs_conv_abscissa f" by (rule conv_le_abs_conv_abscissa) also have "\ \ ereal c" by fact finally have*: "conv_abscissa f \ ereal c" . show "eval_fds f holomorphic_on {s. c < Re s}" by (intro holomorphic_intros) (auto intro: le_less_trans[OF *]) qed (insert assms, auto intro!: holomorphic_intros open_halfspace_Re_gt) define f' where "f' = fds_norm f" have f_f': "f = fds_of_real f'" by (simp add: f'_def fds_of_real_norm) have f'_nonneg: "fds_nth f' n \ 0" for n using nonneg_coeffs[of n] by (auto elim!: nonneg_Reals_cases simp: f'_def) have deriv: "(\n. (deriv ^^ n) g' a) = (\n. eval_fds ((fds_deriv ^^ n) f) a)" proof fix n :: nat have ev: "eventually (\s. s \ {s. Re s > c}) (nhds (complex_of_real a))" by (intro eventually_nhds_in_open open_halfspace_Re_gt) (auto simp: a_def) have "(deriv ^^ n) g' a = (deriv ^^ n) (eval_fds f) a" by (intro higher_deriv_cong_ev refl eventually_mono[OF ev]) (auto simp: g'_def) also have "\ = eval_fds ((fds_deriv ^^ n) f) a" proof (intro eval_fds_higher_deriv [symmetric]) have "conv_abscissa f \ abs_conv_abscissa f" by (rule conv_le_abs_conv_abscissa) also have "\ \ ereal c" by (rule assms) also have "\ < a" by (simp add: a_def) finally show "conv_abscissa f < ereal (complex_of_real a \ 1)" by simp qed finally show "(deriv ^^ n) g' a = eval_fds ((fds_deriv ^^ n) f) a" . qed have nth_deriv_conv: "fds_abs_converges ((fds_deriv ^^ n) f) (of_real a)" for n by (intro fds_abs_converges) (auto simp: abs_conv_abscissa_higher_deriv a_def intro!: le_less_trans[OF abscissa]) have nth_deriv_eq: "(fds_deriv ^^ n) f = fds (\k. (-1) ^ n * fds_nth f k * ln (real k) ^ n)" for n proof - have "fds_nth ((fds_deriv ^^ n) f) k = (-1) ^ n * fds_nth f k * ln (real k) ^ n" for k by (induction n) (simp_all add: fds_deriv_def fds_eq_iff fds_nth_fds' scaleR_conv_of_real) thus ?thesis by (intro fds_eqI) simp_all qed have deriv': "(\n. eval_fds ((fds_deriv ^^ n) f) (complex_of_real a)) = (\n. (- 1) ^ n * complex_of_real (\\<^sub>ak. fds_nth f' k * ln (real k) ^ n / real k powr a))" proof fix n have "eval_fds ((fds_deriv ^^ n) f) (of_real a) = (\\<^sub>ak. fds_nth ((fds_deriv ^^ n) f) k / of_nat k powr complex_of_real a)" using nth_deriv_conv by (subst eval_fds_altdef) auto hence "eval_fds ((fds_deriv ^^ n) f) (of_real a) = (\\<^sub>ak. (- 1) ^ n *\<^sub>R (fds_nth f k * ln (real k) ^ n / k powr a))" by (simp add: nth_deriv_eq fds_nth_fds' powr_Reals_eq scaleR_conv_of_real algebra_simps) also have "\ = (- 1) ^ n * (\\<^sub>ak. of_real (fds_nth f' k * ln (real k) ^ n / k powr a))" by (subst infsetsum_scaleR_right) (simp_all add: scaleR_conv_of_real f_f') also have "\ = (- 1) ^ n * of_real (\\<^sub>ak. fds_nth f' k * ln (real k) ^ n / k powr a)" by (subst infsetsum_of_real) (rule refl) finally show "eval_fds ((fds_deriv ^^ n) f) (complex_of_real a) = (- 1) ^ n * complex_of_real (\\<^sub>ak. fds_nth f' k * ln (real k) ^ n / real k powr a)" . qed define s :: complex where "s = c - \ / 2" have s: "Re s < c" using assms \ by (simp_all add: s_def \_def field_simps) have "s \ ball a (1 + \)" using s by (simp add: a_def dist_norm cmod_def s_def) from holomorphic_power_series[OF holo this] have sums: "(\n. (deriv ^^ n) g' a / fact n * (s - a) ^ n) sums g' s" by simp also note deriv also have "s - a = -of_real (1 + \ / 2)" by (simp add: s_def a_def) also have "(\n. \ ^ n) = (\n. of_real ((-1) ^ n * (1 + \ / 2) ^ n))" by (intro ext) (subst power_minus, auto) also have "(\n. eval_fds ((fds_deriv ^^ n) f) a / fact n * \ n) = (\n. of_real ((-1) ^ n * eval_fds ((fds_deriv ^^ n) f') a / fact n * (1+\/2) ^ n))" using nth_deriv_conv by (simp add: f_f' fds_abs_converges_imp_converges mult_ac) finally have "summable \" by (simp add: sums_iff) hence summable: "summable (\n. (-1)^n * eval_fds ((fds_deriv ^^ n) f') a / fact n * (1+\/2)^n)" by (subst (asm) summable_of_real_iff) have "(\(n,k). (-1)^n * fds_nth f k * ln (real k) ^ n / (real k powr a) * ((s-a) ^ n / fact n)) abs_summable_on (UNIV \ UNIV)" proof (subst abs_summable_on_Sigma_iff, safe, goal_cases) case (3 n) from nth_deriv_conv[of n] show ?case unfolding fds_abs_converges_altdef' by (intro abs_summable_on_cmult_left) (simp add: nth_deriv_eq fds_nth_fds' powr_Reals_eq) next case 4 have nth_deriv_f_f': "(fds_deriv ^^ n) f = fds_of_real ((fds_deriv ^^ n) f')" for n by (induction n) (auto simp: f'_def fds_of_real_norm) have norm_nth_deriv_f: "norm (fds_nth ((fds_deriv ^^ n) f) k) = (-1) ^ n * of_real (fds_nth ((fds_deriv ^^ n) f') k)" for n k proof (induction n) case (Suc n) thus ?case by (cases k) (auto simp: f_f' fds_nth_deriv scaleR_conv_of_real norm_mult) qed (auto simp: f'_nonneg f_f') note summable also have "(\n. (-1)^n * eval_fds ((fds_deriv ^^ n) f') a / fact n * (1+\/2)^n) = (\n. \\<^sub>ak. norm ((- 1) ^ n * fds_nth f k * ln (real k) ^ n / (real k powr a) * ((s - a) ^ n / fact n)))" (is "_ = ?h") proof (rule ext, goal_cases) case (1 n) have "(\\<^sub>ak. norm ((- 1) ^ n * fds_nth f k * ln (real k) ^ n / (real k powr a) * ((s - a) ^ n / fact n))) = (norm ((s - a) ^ n / fact n) * (-1) ^ n) *\<^sub>R (\\<^sub>ak. (-1) ^ n * norm (fds_nth ((fds_deriv ^^ n) f) k / real k powr a))" (is "_ = _ *\<^sub>R ?S") by (subst infsetsum_scaleR_right [symmetric]) (auto simp: norm_mult norm_divide norm_power mult_ac nth_deriv_eq fds_nth_fds') also have "?S = (\\<^sub>ak. fds_nth ((fds_deriv ^^ n) f') k / real k powr a)" by (intro infsetsum_cong) (auto simp: norm_mult norm_divide norm_power norm_nth_deriv_f) also have "\ = eval_fds ((fds_deriv ^^ n) f') a" using nth_deriv_conv[of n] by (subst eval_fds_altdef) (auto simp: f'_def nth_deriv_f_f') also have "(norm ((s - a) ^ n / fact n) * (- 1) ^ n) *\<^sub>R eval_fds ((fds_deriv ^^ n) f') a = (-1) ^ n * eval_fds ((fds_deriv ^^ n) f') a / fact n * norm (s - a) ^ n" by (simp add: norm_divide norm_power) also have s_a: "s - a = -of_real (1 + \ / 2)" by (simp add: s_def a_def) have "norm (s - a) = 1 + \ / 2" unfolding s_a norm_minus_cancel norm_of_real using \ by simp finally show ?case .. qed also have "?h n \ 0" for n by (intro infsetsum_nonneg) auto hence "?h = (\n. norm (?h n))" by simp finally show ?case unfolding abs_summable_on_nat_iff' . qed auto hence "(\(k,n). (-1)^n * fds_nth f k * ln (real k) ^ n / (real k powr a) * ((s-a) ^ n / fact n)) abs_summable_on (UNIV \ UNIV)" by (subst (asm) abs_summable_on_Times_swap) (simp add: case_prod_unfold) hence "(\k. \\<^sub>an. (- 1) ^ n * fds_nth f k * ln (real k) ^ n / (k powr a) * ((s - a) ^ n / fact n)) abs_summable_on UNIV" (is "?h abs_summable_on _") by (rule abs_summable_on_Sigma_project1') auto also have "?this \ (\k. fds_nth f k / nat_power k s) abs_summable_on UNIV" proof (intro abs_summable_on_cong refl, goal_cases) case (1 k) have "?h k = (fds_nth f' k / k powr a) *\<^sub>R (\\<^sub>an. (-ln (real k) * (s - a)) ^ n / fact n)" by (subst infsetsum_scaleR_right [symmetric], rule infsetsum_cong) (simp_all add: scaleR_conv_of_real f_f' power_minus' power_mult_distrib divide_simps) also have "(\\<^sub>an. (-ln (real k) * (s - a)) ^ n / fact n) = exp (-ln (real k) * (s - a))" using exp_converges[of "-ln k * (s - a)"] exp_converges[of "norm (-ln k * (s - a))"] by (subst infsetsum_nat') (auto simp: abs_summable_on_nat_iff' sums_iff scaleR_conv_of_real divide_simps norm_divide norm_mult norm_power) also have "(fds_nth f' k / k powr a) *\<^sub>R \ = fds_nth f k / nat_power k s" by (auto simp: scaleR_conv_of_real f_f' powr_def exp_minus field_simps exp_of_real [symmetric] exp_diff) finally show ?case . qed finally have "fds_abs_converges f s" by (simp add: fds_abs_converges_def abs_summable_on_nat_iff') thus ?thesis by (intro exI[of _ "(c - \ / 2)"]) (auto simp: s_def a_def \) qed theorem pringsheim_landau: fixes c :: real and f :: "complex fds" assumes "nonneg_dirichlet_series f" assumes abscissa: "abs_conv_abscissa f = c" assumes g: "\s. s \ A \ Re s > c \ g s = eval_fds f s" assumes "g holomorphic_on A" "open A" "c \ A" shows False proof - have "\x complex_of_real x \ 1" unfolding abs_conv_abscissa_def by (intro Inf_lower) (auto simp: image_iff intro!: exI[of _ "of_real x"]) also have "\ < abs_conv_abscissa f" using assms x by simp finally show False by simp qed corollary entire_continuation_imp_abs_conv_abscissa_MInfty: assumes "nonneg_dirichlet_series f" assumes c: "c \ abs_conv_abscissa f" assumes g: "\s. Re s > c \ g s = eval_fds f s" assumes holo: "g holomorphic_on UNIV" shows "abs_conv_abscissa f = -\" proof (rule ccontr) assume "abs_conv_abscissa f \ -\" with c obtain a where abscissa [simp]: "abs_conv_abscissa f = ereal a" by (cases "abs_conv_abscissa f") auto show False proof (rule pringsheim_landau[OF assms(1) abscissa _ holo]) fix s assume s: "Re s > a" show "g s = eval_fds f s" proof (rule sym, rule analytic_continuation_open[of _ _ _ g]) show "g holomorphic_on {s. Re s > a}" by (rule holomorphic_on_subset[OF holo]) auto from assms show "{s. Re s > c} \ {s. Re s > a}" by auto next have "conv_abscissa f \ abs_conv_abscissa f" by (rule conv_le_abs_conv_abscissa) also have "\ = ereal a" by simp finally show "eval_fds f holomorphic_on {s. Re s > a}" by (intro holomorphic_intros) (auto intro: le_less_trans) qed (insert assms s, auto intro!: exI[of _ "of_real (c + 1)"] open_halfspace_Re_gt convex_connected convex_halfspace_Re_gt) qed auto qed subsection \Convergence of the $\zeta$ and M\"{o}bius $\mu$ series\ lemma fds_abs_summable_zeta_real_iff [simp]: "fds_abs_converges fds_zeta s \ s > (1 :: real)" proof - have "fds_abs_converges fds_zeta s \ summable (\n. real n powr -s)" unfolding fds_abs_converges_def by (intro summable_cong always_eventually) (auto simp: fds_nth_zeta powr_minus divide_simps) also have "\ \ s > 1" by (simp add: summable_real_powr_iff) finally show ?thesis . qed lemma fds_abs_summable_zeta_real: "s > (1 :: real) \ fds_abs_converges fds_zeta s" by simp lemma fds_abs_converges_moebius_mu_real: assumes "s > (1 :: real)" shows "fds_abs_converges (fds moebius_mu) s" unfolding fds_abs_converges_def proof (rule summable_comparison_test, intro exI allI impI) fix n :: nat show "norm (norm (fds_nth (fds moebius_mu) n / nat_power n s)) \ n powr (-s)" by (simp add: powr_minus divide_simps abs_moebius_mu_le) next from assms show "summable (\n. real n powr -s)" by (simp add: summable_real_powr_iff) qed subsection \Application to the M\"{o}bius $\mu$ function\ lemma inverse_squares_sums': "(\n. 1 / real n ^ 2) sums (pi ^ 2 / 6)" using inverse_squares_sums sums_Suc_iff[of "\n. 1 / real n ^ 2" "pi^2 / 6"] by simp lemma norm_summable_moebius_over_square: "summable (\n. norm (moebius_mu n / real n ^ 2))" proof (subst summable_Suc_iff [symmetric], rule summable_comparison_test) show "summable (\n. 1 / real (Suc n) ^ 2)" using inverse_squares_sums by (simp add: sums_iff) qed (auto simp del: of_nat_Suc simp: field_simps abs_moebius_mu_le) lemma summable_moebius_over_square: "summable (\n. moebius_mu n / real n ^ 2)" using norm_summable_moebius_over_square by (rule summable_norm_cancel) lemma moebius_over_square_sums: "(\n. moebius_mu n / n\<^sup>2) sums (6 / pi\<^sup>2)" proof - have "1 = eval_fds (1 :: real fds) 2" by simp also have "(1 :: real fds) = fds_zeta * fds moebius_mu" by (rule fds_zeta_times_moebius_mu [symmetric]) also have "eval_fds \ 2 = eval_fds fds_zeta 2 * eval_fds (fds moebius_mu) 2" by (intro eval_fds_mult fds_abs_converges_moebius_mu_real) simp_all also have "\ = pi ^ 2 / 6 * (\n. moebius_mu n / (real n)\<^sup>2)" using inverse_squares_sums' by (simp add: eval_fds_at_numeral suminf_fds_zeta_aux sums_iff) finally have "(\n. moebius_mu n / (real n)\<^sup>2) = 6 / pi ^ 2" by (simp add: field_simps) with summable_moebius_over_square show ?thesis by (simp add: sums_iff) qed end diff --git a/thys/Error_Function/Error_Function.thy b/thys/Error_Function/Error_Function.thy --- a/thys/Error_Function/Error_Function.thy +++ b/thys/Error_Function/Error_Function.thy @@ -1,655 +1,655 @@ (* File: Error_Function.thy Author: Manuel Eberl, TU München The complex and real error function (most results are on the real error function though) *) section \The complex and real error function\ theory Error_Function imports "HOL-Analysis.Analysis" "HOL-Library.Landau_Symbols" begin subsection \Auxiliary Facts\ lemma tendsto_sandwich_mono: assumes "(\n. f (real n)) \ (c::real)" assumes "eventually (\x. \y z. x \ y \ y \ z \ f y \ f z) at_top" shows "(f \ c) at_top" proof (rule tendsto_sandwich) from assms(2) obtain C where C: "\x y. C \ x \ x \ y \ f x \ f y" by (auto simp: eventually_at_top_linorder) show "eventually (\x. f (real (nat \x\)) \ f x) at_top" using eventually_gt_at_top[of "0::real"] eventually_gt_at_top[of "C+1::real"] by eventually_elim (rule C, linarith+) show "eventually (\x. f (real (Suc (nat \x\))) \ f x) at_top" using eventually_gt_at_top[of "0::real"] eventually_gt_at_top[of "C+1::real"] by eventually_elim (rule C, linarith+) qed (auto intro!: filterlim_compose[OF assms(1)] filterlim_compose[OF filterlim_nat_sequentially] filterlim_compose[OF filterlim_Suc] filterlim_floor_sequentially simp del: of_nat_Suc) lemma tendsto_sandwich_antimono: assumes "(\n. f (real n)) \ (c::real)" assumes "eventually (\x. \y z. x \ y \ y \ z \ f y \ f z) at_top" shows "(f \ c) at_top" proof (rule tendsto_sandwich) from assms(2) obtain C where C: "\x y. C \ x \ x \ y \ f x \ f y" by (auto simp: eventually_at_top_linorder) show "eventually (\x. f (real (nat \x\)) \ f x) at_top" using eventually_gt_at_top[of "0::real"] eventually_gt_at_top[of "C+1::real"] by eventually_elim (rule C, linarith+) show "eventually (\x. f (real (Suc (nat \x\))) \ f x) at_top" using eventually_gt_at_top[of "0::real"] eventually_gt_at_top[of "C+1::real"] by eventually_elim (rule C, linarith+) qed (auto intro!: filterlim_compose[OF assms(1)] filterlim_compose[OF filterlim_nat_sequentially] filterlim_compose[OF filterlim_Suc] filterlim_floor_sequentially simp del: of_nat_Suc) lemma has_bochner_integral_completion [intro]: fixes f :: "'a \ 'b::{banach, second_countable_topology}" shows "has_bochner_integral M f I \ has_bochner_integral (completion M) f I" by (auto simp: has_bochner_integral_iff integrable_completion integral_completion borel_measurable_integrable) lemma has_bochner_integral_imp_has_integral: "has_bochner_integral lebesgue (\x. indicator S x *\<^sub>R f x) I \ (f has_integral (I :: 'b :: euclidean_space)) S" using has_integral_set_lebesgue[of S f] by (simp add: has_bochner_integral_iff set_integrable_def set_lebesgue_integral_def) lemma has_bochner_integral_imp_has_integral': "has_bochner_integral lborel (\x. indicator S x *\<^sub>R f x) I \ (f has_integral (I :: 'b :: euclidean_space)) S" by (intro has_bochner_integral_imp_has_integral has_bochner_integral_completion) lemma has_bochner_integral_erf_aux: "has_bochner_integral lborel (\x. indicator {0..} x *\<^sub>R exp (- x\<^sup>2)) (sqrt pi / 2)" proof - let ?pI = "\f. (\\<^sup>+s. f (s::real) * indicator {0..} s \lborel)" let ?gauss = "\x. exp (- x\<^sup>2)" let ?I = "indicator {0<..} :: real \ real" let ?ff= "\x s. x * exp (- x\<^sup>2 * (1 + s\<^sup>2)) :: real" have *: "?pI ?gauss = (\\<^sup>+x. ?gauss x * ?I x \lborel)" by (intro nn_integral_cong_AE AE_I[where N="{0}"]) (auto split: split_indicator) have "?pI ?gauss * ?pI ?gauss = (\\<^sup>+x. \\<^sup>+s. ?gauss x * ?gauss s * ?I s * ?I x \lborel \lborel)" by (auto simp: nn_integral_cmult[symmetric] nn_integral_multc[symmetric] * ennreal_mult[symmetric] intro!: nn_integral_cong split: split_indicator) also have "\ = (\\<^sup>+x. \\<^sup>+s. ?ff x s * ?I s * ?I x \lborel \lborel)" proof (rule nn_integral_cong, cases) fix x :: real assume "x \ 0" then show "(\\<^sup>+s. ?gauss x * ?gauss s * ?I s * ?I x \lborel) = (\\<^sup>+s. ?ff x s * ?I s * ?I x \lborel)" by (subst nn_integral_real_affine[where t="0" and c="x"]) (auto simp: mult_exp_exp nn_integral_cmult[symmetric] field_simps zero_less_mult_iff ennreal_mult[symmetric] intro!: nn_integral_cong split: split_indicator) qed simp also have "... = \\<^sup>+s. \\<^sup>+x. ?ff x s * ?I s * ?I x \lborel \lborel" by (rule lborel_pair.Fubini'[symmetric]) auto also have "... = ?pI (\s. ?pI (\x. ?ff x s))" by (rule nn_integral_cong_AE) (auto intro!: nn_integral_cong_AE AE_I[where N="{0}"] split: split_indicator_asm) also have "\ = ?pI (\s. ennreal (1 / (2 * (1 + s\<^sup>2))))" proof (intro nn_integral_cong ennreal_mult_right_cong) fix s :: real show "?pI (\x. ?ff x s) = ennreal (1 / (2 * (1 + s\<^sup>2)))" proof (subst nn_integral_FTC_atLeast) have "((\a. - (exp (- ((1 + s\<^sup>2) * a\<^sup>2)) / (2 + 2 * s\<^sup>2))) \ (- (0 / (2 + 2 * s\<^sup>2)))) at_top" by (intro tendsto_intros filterlim_compose[OF exp_at_bot] filterlim_compose[OF filterlim_uminus_at_bot_at_top] filterlim_tendsto_pos_mult_at_top) (auto intro!: filterlim_at_top_mult_at_top[OF filterlim_ident filterlim_ident] simp: add_pos_nonneg power2_eq_square add_nonneg_eq_0_iff) then show "((\a. - (exp (- a\<^sup>2 - s\<^sup>2 * a\<^sup>2) / (2 + 2 * s\<^sup>2))) \ 0) at_top" by (simp add: field_simps) qed (auto intro!: derivative_eq_intros simp: field_simps add_nonneg_eq_0_iff) qed also have "... = ennreal (pi / 4)" proof (subst nn_integral_FTC_atLeast) show "((\a. arctan a / 2) \ (pi / 2) / 2 ) at_top" by (intro tendsto_intros) (simp_all add: tendsto_arctan_at_top) qed (auto intro!: derivative_eq_intros simp: add_nonneg_eq_0_iff field_simps power2_eq_square) finally have "?pI ?gauss^2 = pi / 4" by (simp add: power2_eq_square) then have "?pI ?gauss = sqrt (pi / 4)" using power_eq_iff_eq_base[of 2 "enn2real (?pI ?gauss)" "sqrt (pi / 4)"] by (cases "?pI ?gauss") (auto simp: power2_eq_square ennreal_mult[symmetric] ennreal_top_mult) also have "?pI ?gauss = (\\<^sup>+x. indicator {0..} x *\<^sub>R exp (- x\<^sup>2) \lborel)" by (intro nn_integral_cong) (simp split: split_indicator) also have "sqrt (pi / 4) = sqrt pi / 2" by (simp add: real_sqrt_divide) finally show ?thesis by (rule has_bochner_integral_nn_integral[rotated 3]) auto qed lemma has_integral_erf_aux: "((\t::real. exp (-t\<^sup>2)) has_integral (sqrt pi / 2)) {0..}" by (intro has_bochner_integral_imp_has_integral' has_bochner_integral_erf_aux) lemma contour_integrable_on_linepath_neg_exp_squared [simp, intro]: "(\t. exp (-(t^2))) contour_integrable_on linepath 0 z" by (auto intro!: contour_integrable_continuous_linepath continuous_intros) lemma holomorphic_on_chain: "g holomorphic_on t \ f holomorphic_on s \ f ` s \ t \ (\x. g (f x)) holomorphic_on s" using holomorphic_on_compose_gen[of f s g t] by (simp add: o_def) lemma holomorphic_on_chain_UNIV: "g holomorphic_on UNIV \ f holomorphic_on s\ (\x. g (f x)) holomorphic_on s" using holomorphic_on_compose_gen[of f s g UNIV] by (simp add: o_def) lemmas holomorphic_on_exp' [holomorphic_intros] = holomorphic_on_exp [THEN holomorphic_on_chain_UNIV] lemma leibniz_rule_field_derivative_real: fixes f::"'a::{real_normed_field, banach} \ real \ 'a" assumes fx: "\x t. x \ U \ t \ {a..b} \ ((\x. f x t) has_field_derivative fx x t) (at x within U)" assumes integrable_f2: "\x. x \ U \ (f x) integrable_on {a..b}" assumes cont_fx: "continuous_on (U \ {a..b}) (\(x, t). fx x t)" assumes U: "x0 \ U" "convex U" shows "((\x. integral {a..b} (f x)) has_field_derivative integral {a..b} (fx x0)) (at x0 within U)" using leibniz_rule_field_derivative[of U a b f fx x0] assms by simp lemma has_vector_derivative_linepath_within [derivative_intros]: assumes [derivative_intros]: "(f has_vector_derivative f') (at x within S)" "(g has_vector_derivative g') (at x within S)" "(h has_real_derivative h') (at x within S)" shows "((\x. linepath (f x) (g x) (h x)) has_vector_derivative (1 - h x) *\<^sub>R f' + h x *\<^sub>R g' - h' *\<^sub>R (f x - g x)) (at x within S)" unfolding linepath_def [abs_def] by (auto intro!: derivative_eq_intros simp: field_simps scaleR_diff_right) lemma has_field_derivative_linepath_within [derivative_intros]: assumes [derivative_intros]: "(f has_field_derivative f') (at x within S)" "(g has_field_derivative g') (at x within S)" "(h has_real_derivative h') (at x within S)" shows "((\x. linepath (f x) (g x) (h x)) has_field_derivative (1 - h x) *\<^sub>R f' + h x *\<^sub>R g' - h' *\<^sub>R (f x - g x)) (at x within S)" unfolding linepath_def [abs_def] by (auto intro!: derivative_eq_intros simp: field_simps scaleR_diff_right) lemma continuous_on_linepath' [continuous_intros]: assumes [continuous_intros]: "continuous_on A f" "continuous_on A g" "continuous_on A h" shows "continuous_on A (\x. linepath (f x) (g x) (h x))" using assms unfolding linepath_def by (auto intro!: continuous_intros) lemma contour_integral_has_field_derivative: assumes A: "open A" "convex A" "a \ A" "z \ A" assumes integrable: "\z. z \ A \ f contour_integrable_on linepath a z" assumes holo: "f holomorphic_on A" shows "((\z. contour_integral (linepath a z) f) has_field_derivative f z) (at z within B)" proof - have "(f has_field_derivative deriv f z) (at z)" if "z \ A" for z using that assms by (auto intro!: holomorphic_derivI) note [derivative_intros] = DERIV_chain2[OF this] note [continuous_intros] = continuous_on_compose2[OF holomorphic_on_imp_continuous_on [OF holo]] continuous_on_compose2[OF holomorphic_on_imp_continuous_on [OF holomorphic_deriv[OF holo]]] have [derivative_intros]: "((\x. linepath a x t) has_field_derivative of_real t) (at x within A)" for t x by (auto simp: linepath_def scaleR_conv_of_real intro!: derivative_eq_intros) have *: "linepath a b t \ A" if "a \ A" "b \ A" "t \ {0..1}" for a b t using that linepath_in_convex_hull[of a A b t] \convex A\ by (simp add: hull_same) have "((\z. integral {0..1} (\x. f (linepath a z x)) * (z - a)) has_field_derivative integral {0..1} (\t. deriv f (linepath a z t) * of_real t) * (z - a) + integral {0..1} (\x. f (linepath a z x))) (at z within A)" (is "(_ has_field_derivative ?I) _") by (rule derivative_eq_intros leibniz_rule_field_derivative_real)+ (insert assms, auto intro!: derivative_eq_intros leibniz_rule_field_derivative_real integrable_continuous_real continuous_intros simp: split_beta scaleR_conv_of_real *) also have "(\z. integral {0..1} (\x. f (linepath a z x)) * (z - a)) = (\z. contour_integral (linepath a z) f)" by (simp add: contour_integral_integral) also have "?I = integral {0..1} (\x. deriv f (linepath a z x) * of_real x * (z - a) + f (linepath a z x))" (is "_ = integral _ ?g") by (subst integral_mult_left [symmetric], subst integral_add [symmetric]) (insert assms, auto intro!: integrable_continuous_real continuous_intros simp: *) also have "(?g has_integral of_real 1 * f (linepath a z 1) - of_real 0 * f (linepath a z 0)) {0..1}" using * A by (intro fundamental_theorem_of_calculus) - (auto intro!: derivative_eq_intros has_vector_derivative_real_complex + (auto intro!: derivative_eq_intros has_vector_derivative_real_field simp: linepath_def scaleR_conv_of_real) hence "integral {0..1} ?g = f (linepath a z 1)" by (simp add: has_integral_iff) also have "linepath a z 1 = z" by (simp add: linepath_def) also from \z \ A\ and \open A\ have "at z within A = at z" by (rule at_within_open) finally show ?thesis by (rule DERIV_subset) simp_all qed subsection \Definition of the error function\ definition erf_coeffs :: "nat \ real" where "erf_coeffs n = (if odd n then 2 / sqrt pi * (-1) ^ (n div 2) / (of_nat n * fact (n div 2)) else 0)" lemma summable_erf: fixes z :: "'a :: {real_normed_div_algebra, banach}" shows "summable (\n. of_real (erf_coeffs n) * z ^ n)" proof - define b where "b = (\n. 2 / sqrt pi * (if odd n then inverse (fact (n div 2)) else 0))" show ?thesis proof (rule summable_comparison_test[OF exI[of _ 1]], clarify) fix n :: nat assume n: "n \ 1" hence "norm (of_real (erf_coeffs n) * z ^ n) \ b n * norm z ^ n" unfolding norm_mult norm_power erf_coeffs_def b_def by (intro mult_right_mono) (auto simp: field_simps norm_divide abs_mult) thus "norm (of_real (erf_coeffs n) * z ^ n) \ b n * norm z ^ n" by (simp add: mult_ac) next have "summable (\n. (norm z * 2 / sqrt pi) * (inverse (fact n) * norm z ^ (2*n)))" (is "summable ?c") unfolding power_mult by (intro summable_mult summable_exp) also have "?c = (\n. b (2*n+1) * norm z ^ (2*n+1))" unfolding b_def by (auto simp: fun_eq_iff b_def) also have "summable \ \ summable (\n. b n * norm z ^ n)" using summable_mono_reindex [of "\n. 2*n+1"] by (intro summable_mono_reindex [of "\n. 2*n+1"]) (auto elim!: oddE simp: strict_mono_def b_def) finally show \ . qed qed definition erf :: "('a :: {real_normed_field, banach}) \ 'a" where "erf z = (\n. of_real (erf_coeffs n) * z ^ n)" lemma erf_converges: "(\n. of_real (erf_coeffs n) * z ^ n) sums erf z" using summable_erf by (simp add: sums_iff erf_def) lemma erf_0 [simp]: "erf 0 = 0" unfolding erf_def powser_zero by (simp add: erf_coeffs_def) lemma erf_minus [simp]: "erf (-z) = - erf z" unfolding erf_def by (subst suminf_minus [OF summable_erf, symmetric], rule suminf_cong) (simp_all add: erf_coeffs_def) lemma erf_of_real [simp]: "erf (of_real x) = of_real (erf x)" unfolding erf_def using summable_erf[of x] by (subst suminf_of_real) (simp_all add: summable_erf) lemma of_real_erf_numeral [simp]: "of_real (erf (numeral n)) = erf (numeral n)" by (simp only: erf_of_real [symmetric] of_real_numeral) lemma of_real_erf_1 [simp]: "of_real (erf 1) = erf 1" by (simp only: erf_of_real [symmetric] of_real_1) lemma erf_has_field_derivative: "(erf has_field_derivative of_real (2 / sqrt pi) * exp (-(z^2))) (at z within A)" proof - define a' where "a' = (\n. 2 / sqrt pi * (if even n then (- 1) ^ (n div 2) / fact (n div 2) else 0))" have "(erf has_field_derivative (\n. diffs (\n. of_real (erf_coeffs n)) n * z ^ n)) (at z)" using summable_erf unfolding erf_def by (rule termdiffs_strong_converges_everywhere) also have "diffs (\n. of_real (erf_coeffs n)) = (\n. of_real (a' n) :: 'a)" by (simp add: erf_coeffs_def a'_def diffs_def fun_eq_iff del: of_nat_Suc) hence "(\n. diffs (\n. of_real (erf_coeffs n)) n * z ^ n) = (\n. of_real (a' n) * z ^ n)" by simp also have "\ = (\n. of_real (a' (2*n)) * z ^ (2*n))" by (intro suminf_mono_reindex [symmetric]) (auto simp: strict_mono_def a'_def elim!: evenE) also have "(\n. of_real (a' (2*n)) * z ^ (2*n)) = (\n. of_real (2 / sqrt pi) * (inverse (fact n) * (-(z^2))^n))" by (simp add: fun_eq_iff power_mult [symmetric] a'_def field_simps power_minus') also have "suminf \ = of_real (2 / sqrt pi) * exp (-(z^2))" by (subst suminf_mult, intro summable_exp) (auto simp: field_simps scaleR_conv_of_real exp_def) finally show ?thesis by (rule DERIV_subset) simp_all qed lemmas erf_has_field_derivative' [derivative_intros] = erf_has_field_derivative [THEN DERIV_chain2] lemma erf_continuous_on: "continuous_on A erf" by (rule DERIV_continuous_on erf_has_field_derivative)+ lemma continuous_on_compose2_UNIV: "continuous_on UNIV g \ continuous_on s f \ continuous_on s (\x. g (f x))" by (rule continuous_on_compose2[of UNIV g s f]) simp_all lemmas erf_continuous_on' [continuous_intros] = erf_continuous_on [THEN continuous_on_compose2_UNIV] lemma erf_continuous [continuous_intros]: "continuous (at x within A) erf" by (rule continuous_within_subset[OF _ subset_UNIV]) (insert erf_continuous_on[of UNIV], auto simp: continuous_on_eq_continuous_at) lemmas erf_continuous' [continuous_intros] = continuous_within_compose2[OF _ erf_continuous] lemmas tendsto_erf [tendsto_intros] = isCont_tendsto_compose[OF erf_continuous] lemma erf_cnj [simp]: "erf (cnj z) = cnj (erf z)" proof - interpret bounded_linear cnj by (rule bounded_linear_cnj) from suminf[OF summable_erf] show ?thesis by (simp add: erf_def erf_coeffs_def) qed lemma integral_exp_minus_squared_real: assumes "a \ b" shows "((\t. exp (-(t^2))) has_integral (sqrt pi / 2 * (erf b - erf a))) {a..b}" proof - have "((\t. exp (-(t^2))) has_integral (sqrt pi / 2 * erf b - sqrt pi / 2 * erf a)) {a..b}" using assms by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros simp: has_field_derivative_iff_has_vector_derivative [symmetric]) thus ?thesis by (simp add: field_simps) qed lemma erf_real_altdef_nonneg: "x \ 0 \ erf (x::real) = 2 / sqrt pi * integral {0..x} (\t. exp (-(t^2)))" using integral_exp_minus_squared_real[of 0 x] by (simp add: has_integral_iff field_simps) lemma erf_real_altdef_nonpos: "x \ 0 \ erf (x::real) = -2 / sqrt pi * integral {0..-x} (\t. exp (-(t^2)))" using erf_real_altdef_nonneg[of "-x"] by simp lemma less_imp_erf_real_less: assumes "a < (b::real)" shows "erf a < erf b" proof - from assms have "\z. z > a \ z < b \ erf b - erf a = (b - a) * (2 / sqrt pi * exp (- z\<^sup>2))" by (intro MVT2) (auto intro!: derivative_eq_intros simp: field_simps) then guess z by (elim exE conjE) note z = this note z(3) also from assms have "(b - a) * (2 / sqrt pi * exp (- z\<^sup>2)) > 0" by (intro mult_pos_pos divide_pos_pos) simp_all finally show ?thesis by simp qed lemma le_imp_erf_real_le: "a \ (b::real) \ erf a \ erf b" by (cases "a < b") (auto dest: less_imp_erf_real_less) lemma erf_real_less_cancel [simp]: "(erf (a :: real) < erf b) \ a < b" using less_imp_erf_real_less[of a b] less_imp_erf_real_less[of b a] by (cases a b rule: linorder_cases) simp_all lemma erf_real_eq_iff [simp]: "erf (a::real) = erf b \ a = b" by (cases a b rule: linorder_cases) (auto dest: less_imp_erf_real_less) lemma erf_real_le_cancel [simp]: "(erf (a :: real) \ erf b) \ a \ b" by (cases a b rule: linorder_cases) (auto simp: less_eq_real_def) lemma inj_on_erf_real [intro]: "inj_on (erf :: real \ real) A" by (auto simp: inj_on_def) lemma strict_mono_erf_real [intro]: "strict_mono (erf :: real \ real)" by (auto simp: strict_mono_def) lemma mono_erf_real [intro]: "mono (erf :: real \ real)" by (auto simp: mono_def) lemma erf_real_ge_0_iff [simp]: "erf (x::real) \ 0 \ x \ 0" using erf_real_le_cancel[of 0 x] unfolding erf_0 . lemma erf_real_le_0_iff [simp]: "erf (x::real) \ 0 \ x \ 0" using erf_real_le_cancel[of x 0] unfolding erf_0 . lemma erf_real_gt_0_iff [simp]: "erf (x::real) > 0 \ x > 0" using erf_real_less_cancel[of 0 x] unfolding erf_0 . lemma erf_real_less_0_iff [simp]: "erf (x::real) < 0 \ x < 0" using erf_real_less_cancel[of x 0] unfolding erf_0 . lemma erf_at_top [tendsto_intros]: "((erf :: real \ real) \ 1) at_top" proof - have *: "(\n. {0..real n}) = {0..}" by (auto intro!: real_nat_ceiling_ge) let ?f = "\t::real. exp (-t\<^sup>2)" have "(\n. set_lebesgue_integral lborel {0..real n} ?f) \ set_lebesgue_integral lborel (\n. {0..real n}) ?f" using has_bochner_integral_erf_aux by (intro set_integral_cont_up ) (insert *, auto simp: incseq_def has_bochner_integral_iff set_integrable_def) also note * also have "(\n. set_lebesgue_integral lborel {0..real n} ?f) = (\n. integral {0..real n} ?f)" proof - have "\n. set_integrable lborel {0..real n} (\x. exp (- x\<^sup>2))" unfolding set_integrable_def by (intro borel_integrable_compact) (auto intro!: continuous_intros) then show ?thesis by (intro set_borel_integral_eq_integral ext) qed also have "\ = (\n. sqrt pi / 2 * erf (real n))" by (simp add: erf_real_altdef_nonneg) also have "set_lebesgue_integral lborel {0..} ?f = sqrt pi / 2" using has_bochner_integral_erf_aux by (simp add: has_bochner_integral_iff set_lebesgue_integral_def) finally have "(\n. 2 / sqrt pi * (sqrt pi / 2 * erf (real n))) \ (2 / sqrt pi) * (sqrt pi / 2)" by (intro tendsto_intros) hence "(\n. erf (real n)) \ 1" by simp thus ?thesis by (rule tendsto_sandwich_mono) auto qed lemma erf_at_bot [tendsto_intros]: "((erf :: real \ real) \ -1) at_bot" by (simp add: filterlim_at_bot_mirror tendsto_minus_cancel_left erf_at_top) lemmas tendsto_erf_at_top [tendsto_intros] = filterlim_compose[OF erf_at_top] lemmas tendsto_erf_at_bot [tendsto_intros] = filterlim_compose[OF erf_at_bot] subsection \The complimentary error function\ definition erfc where "erfc z = 1 - erf z" lemma erf_conv_erfc: "erf z = 1 - erfc z" by (simp add: erfc_def) lemma erfc_0 [simp]: "erfc 0 = 1" by (simp add: erfc_def) lemma erfc_minus: "erfc (-z) = 2 - erfc z" by (simp add: erfc_def) lemma erfc_of_real [simp]: "erfc (of_real x) = of_real (erfc x)" by (simp add: erfc_def) lemma of_real_erfc_numeral [simp]: "of_real (erfc (numeral n)) = erfc (numeral n)" by (simp add: erfc_def) lemma of_real_erfc_1 [simp]: "of_real (erfc 1) = erfc 1" by (simp add: erfc_def) lemma less_imp_erfc_real_less: "a < (b::real) \ erfc a > erfc b" by (simp add: erfc_def) lemma le_imp_erfc_real_le: "a \ (b::real) \ erfc a \ erfc b" by (simp add: erfc_def) lemma erfc_real_less_cancel [simp]: "(erfc (a :: real) < erfc b) \ a > b" by (simp add: erfc_def) lemma erfc_real_eq_iff [simp]: "erfc (a::real) = erfc b \ a = b" by (simp add: erfc_def) lemma erfc_real_le_cancel [simp]: "(erfc (a :: real) \ erfc b) \ a \ b" by (simp add: erfc_def) lemma inj_on_erfc_real [intro]: "inj_on (erfc :: real \ real) A" by (auto simp: inj_on_def) lemma antimono_erfc_real [intro]: "antimono (erfc :: real \ real)" by (auto simp: antimono_def) lemma erfc_real_ge_0_iff [simp]: "erfc (x::real) \ 1 \ x \ 0" by (simp add: erfc_def) lemma erfc_real_le_0_iff [simp]: "erfc (x::real) \ 1 \ x \ 0" by (simp add: erfc_def) lemma erfc_real_gt_0_iff [simp]: "erfc (x::real) > 1 \ x < 0" by (simp add: erfc_def) lemma erfc_real_less_0_iff [simp]: "erfc (x::real) < 1 \ x > 0" by (simp add: erfc_def) lemma erfc_has_field_derivative: "(erfc has_field_derivative -of_real (2 / sqrt pi) * exp (-(z^2))) (at z within A)" unfolding erfc_def [abs_def] by (auto intro!: derivative_eq_intros) lemmas erfc_has_field_derivative' [derivative_intros] = erfc_has_field_derivative [THEN DERIV_chain2] lemma erfc_continuous_on: "continuous_on A erfc" by (rule DERIV_continuous_on erfc_has_field_derivative)+ lemmas erfc_continuous_on' [continuous_intros] = erfc_continuous_on [THEN continuous_on_compose2_UNIV] lemma erfc_continuous [continuous_intros]: "continuous (at x within A) erfc" by (rule continuous_within_subset[OF _ subset_UNIV]) (insert erfc_continuous_on[of UNIV], auto simp: continuous_on_eq_continuous_at) lemmas erfc_continuous' [continuous_intros] = continuous_within_compose2[OF _ erfc_continuous] lemmas tendsto_erfc [tendsto_intros] = isCont_tendsto_compose[OF erfc_continuous] lemma erfc_at_top [tendsto_intros]: "((erfc :: real \ real) \ 0) at_top" unfolding erfc_def [abs_def] by (auto intro!: tendsto_eq_intros) lemma erfc_at_bot [tendsto_intros]: "((erfc :: real \ real) \ 2) at_bot" unfolding erfc_def [abs_def] by (auto intro!: tendsto_eq_intros) lemmas tendsto_erfc_at_top [tendsto_intros] = filterlim_compose[OF erfc_at_top] lemmas tendsto_erfc_at_bot [tendsto_intros] = filterlim_compose[OF erfc_at_bot] lemma integrable_exp_minus_squared: assumes "A \ {0..}" "A \ sets lborel" shows "set_integrable lborel A (\t::real. exp (-t\<^sup>2))" (is ?thesis1) and "(\t::real. exp (-t\<^sup>2)) integrable_on A" (is ?thesis2) proof - show ?thesis1 by (rule set_integrable_subset[of _ "{0..}"]) (insert assms has_bochner_integral_erf_aux, auto simp: has_bochner_integral_iff set_integrable_def) thus ?thesis2 by (rule set_borel_integral_eq_integral) qed lemma assumes "x \ 0" shows erfc_real_altdef_nonneg: "erfc x = 2 / sqrt pi * integral {x..} (\t. exp (-t\<^sup>2))" and has_integral_erfc: "((\t. exp (-t\<^sup>2)) has_integral (sqrt pi / 2 * erfc x)) {x..}" proof - let ?f = "\t::real. exp (-t\<^sup>2)" have int: "set_integrable lborel {0..} ?f" using has_bochner_integral_erf_aux by (simp add: has_bochner_integral_iff set_integrable_def) from assms have *: "{(0::real)..} = {0..x} \ {x..}" by auto have "set_lebesgue_integral lborel ({0..x} \ {x..}) ?f = set_lebesgue_integral lborel {0..x} ?f + set_lebesgue_integral lborel {x..} ?f" by (subst set_integral_Un_AE; (rule set_integrable_subset[OF int])?) (insert assms AE_lborel_singleton[of x], auto elim!: eventually_mono) also note * [symmetric] also have "set_lebesgue_integral lborel {0..} ?f = sqrt pi / 2" using has_bochner_integral_erf_aux by (simp add: has_bochner_integral_iff set_lebesgue_integral_def) also have "set_lebesgue_integral lborel {0..x} ?f = sqrt pi / 2 * erf x" by (subst set_borel_integral_eq_integral(2)[OF set_integrable_subset[OF int]]) (insert assms, auto simp: erf_real_altdef_nonneg) also have "set_lebesgue_integral lborel {x..} ?f = integral {x..} ?f" by (subst set_borel_integral_eq_integral(2)[OF set_integrable_subset[OF int]]) (insert assms, auto) finally show "erfc x = 2 / sqrt pi * integral {x..} ?f" by (simp add: field_simps erfc_def) with integrable_exp_minus_squared(2)[of "{x..}"] assms show "(?f has_integral (sqrt pi / 2 * erfc x)) {x..}" by (simp add: has_integral_iff) qed lemma erfc_real_gt_0 [simp, intro]: "erfc (x::real) > 0" proof (cases "x \ 0") case True have "0 < integral {x..x+1} (\t. exp (-(x+1)\<^sup>2))" by simp also from True have "\ \ integral {x..x+1} (\t. exp (-t\<^sup>2))" by (intro integral_le) (auto intro!: integrable_continuous_real continuous_intros power_mono) also have "\ \ sqrt pi / 2 * erfc x" by (rule has_integral_subset_le[OF _ integrable_integral has_integral_erfc]) (auto intro!: integrable_continuous_real continuous_intros True) finally have "sqrt pi / 2 * erfc x > 0" . hence "\ * (2 / sqrt pi) > 0" by (rule mult_pos_pos) simp_all thus "erfc x > 0" by simp next case False have "0 \ (1::real)" by simp also from False have "\ < erfc x" by simp finally show ?thesis . qed lemma erfc_real_less_2 [intro]: "erfc (x::real) < 2" using erfc_real_gt_0[of "-x"] unfolding erfc_minus by simp lemma erf_real_gt_neg1 [intro]: "erf (x::real) > -1" using erfc_real_less_2[of x] unfolding erfc_def by simp lemma erf_real_less_1 [intro]: "erf (x::real) < 1" using erfc_real_gt_0[of x] unfolding erfc_def by simp lemma erfc_cnj [simp]: "erfc (cnj z) = cnj (erfc z)" by (simp add: erfc_def) subsection \Specific facts about the complex case\ lemma erf_complex_altdef: "erf z = of_real (2 / sqrt pi) * contour_integral (linepath 0 z) (\t. exp (-(t^2)))" proof - define A where "A = (\z. contour_integral (linepath 0 z) (\t. exp (-(t^2))))" have [derivative_intros]: "(A has_field_derivative exp (-(z^2))) (at z)" for z :: complex unfolding A_def by (rule contour_integral_has_field_derivative[where A = UNIV]) (auto intro!: holomorphic_intros) have "erf z - 2 / sqrt pi * A z = erf 0 - 2 / sqrt pi * A 0" by (intro DERIV_zero_UNIV_unique[of "\z. erf z - 2 / sqrt pi * A z"]) (auto intro!: derivative_eq_intros) also have "A 0 = 0" by (simp only: A_def contour_integral_trivial) finally show ?thesis unfolding A_def by (simp add: algebra_simps) qed lemma erf_holomorphic_on: "erf holomorphic_on A" by (auto simp: holomorphic_on_def field_differentiable_def intro!: erf_has_field_derivative) lemmas erf_holomorphic_on' [holomorphic_intros] = erf_holomorphic_on [THEN holomorphic_on_chain_UNIV] lemma erf_analytic_on: "erf analytic_on A" by (auto simp: analytic_on_def) (auto intro!: exI[of _ 1] holomorphic_intros) lemma erf_analytic_on' [analytic_intros]: assumes "f analytic_on A" shows "(\x. erf (f x)) analytic_on A" proof - from assms and erf_analytic_on have "erf \ f analytic_on A" by (rule analytic_on_compose_gen) auto thus ?thesis by (simp add: o_def) qed lemma erfc_holomorphic_on: "erfc holomorphic_on A" by (auto simp: holomorphic_on_def field_differentiable_def intro!: erfc_has_field_derivative) lemmas erfc_holomorphic_on' [holomorphic_intros] = erfc_holomorphic_on [THEN holomorphic_on_chain_UNIV] lemma erfc_analytic_on: "erfc analytic_on A" by (auto simp: analytic_on_def) (auto intro!: exI[of _ 1] holomorphic_intros) lemma erfc_analytic_on' [analytic_intros]: assumes "f analytic_on A" shows "(\x. erfc (f x)) analytic_on A" proof - from assms and erfc_analytic_on have "erfc \ f analytic_on A" by (rule analytic_on_compose_gen) auto thus ?thesis by (simp add: o_def) qed end diff --git a/thys/Stirling_Formula/Ln_Gamma_Asymptotics.thy b/thys/Stirling_Formula/Ln_Gamma_Asymptotics.thy --- a/thys/Stirling_Formula/Ln_Gamma_Asymptotics.thy +++ b/thys/Stirling_Formula/Ln_Gamma_Asymptotics.thy @@ -1,1328 +1,1328 @@ (* File: Ln_Gamma_Asymptotics.thy Author: Manuel Eberl The complete asymptotics of the logarithmic Gamma function and the Polygamma functions. *) section \Complete asymptotics of the logarithmic Gamma function\ theory Ln_Gamma_Asymptotics imports "HOL-Analysis.Analysis" Bernoulli.Bernoulli_FPS Bernoulli.Periodic_Bernpoly Stirling_Formula begin subsection \Auxiliary Facts\ (* TODO Move *) lemma filterlim_at_infinity_conv_norm_at_top: "filterlim f at_infinity G \ filterlim (\x. norm (f x)) at_top G" by (auto simp: filterlim_at_infinity[OF order.refl] filterlim_at_top_gt[of _ _ 0]) corollary Ln_times_of_nat: "\r > 0; z \ 0\ \ Ln(of_nat r * z :: complex) = ln (of_nat r) + Ln(z)" using Ln_times_of_real[of "of_nat r" z] by simp lemma tendsto_of_real_0_I: "(f \ 0) G \ ((\x. (of_real (f x))) \ (0 ::'a::real_normed_div_algebra)) G" by (subst (asm) tendsto_of_real_iff [symmetric]) simp lemma negligible_atLeastAtMostI: "b \ a \ negligible {a..(b::real)}" by (cases "b < a") auto lemma integrable_on_negligible: "negligible A \ (f :: 'n :: euclidean_space \ 'a :: banach) integrable_on A" by (subst integrable_spike_set_eq[of _ "{}"]) (simp_all add: integrable_on_empty) lemma vector_derivative_cong_eq: assumes "eventually (\x. x \ A \ f x = g x) (nhds x)" "x = y" "A = B" "x \ A" shows "vector_derivative f (at x within A) = vector_derivative g (at y within B)" proof - from eventually_nhds_x_imp_x[OF assms(1)] assms(4) have "f x = g x" by blast hence "(\D. (f has_vector_derivative D) (at x within A)) = (\D. (g has_vector_derivative D) (at x within A))" using assms by (intro ext has_vector_derivative_cong_ev refl assms) simp_all thus ?thesis by (simp add: vector_derivative_def assms) qed lemma differentiable_of_real [simp]: "of_real differentiable at x within A" proof - have "(of_real has_vector_derivative 1) (at x within A)" by (auto intro!: derivative_eq_intros) thus ?thesis by (rule differentiableI_vector) qed lemma higher_deriv_cong_ev: assumes "eventually (\x. f x = g x) (nhds x)" "x = y" shows "(deriv ^^ n) f x = (deriv ^^ n) g y" proof - from assms(1) have "eventually (\x. (deriv ^^ n) f x = (deriv ^^ n) g x) (nhds x)" proof (induction n arbitrary: f g) case (Suc n) from Suc.prems have "eventually (\y. eventually (\z. f z = g z) (nhds y)) (nhds x)" by (simp add: eventually_eventually) hence "eventually (\x. deriv f x = deriv g x) (nhds x)" by eventually_elim (rule deriv_cong_ev, simp_all) thus ?case by (auto intro!: deriv_cong_ev Suc simp: funpow_Suc_right simp del: funpow.simps) qed auto from eventually_nhds_x_imp_x[OF this] assms(2) show ?thesis by simp qed lemma deriv_of_real [simp]: "at x within A \ bot \ vector_derivative of_real (at x within A) = 1" by (auto intro!: vector_derivative_within derivative_eq_intros) lemma deriv_Re [simp]: "deriv Re = (\_. 1)" by (auto intro!: DERIV_imp_deriv simp: fun_eq_iff) lemma vector_derivative_of_real_left: assumes "f differentiable at x" shows "vector_derivative (\x. of_real (f x)) (at x) = of_real (deriv f x)" proof - have "vector_derivative (of_real \ f) (at x) = (of_real (deriv f x))" by (subst vector_derivative_chain_at) (simp_all add: scaleR_conv_of_real field_derivative_eq_vector_derivative assms) thus ?thesis by (simp add: o_def) qed lemma vector_derivative_of_real_right: assumes "f field_differentiable at (of_real x)" shows "vector_derivative (\x. f (of_real x)) (at x) = deriv f (of_real x)" proof - have "vector_derivative (f \ of_real) (at x) = deriv f (of_real x)" using assms by (subst vector_derivative_chain_at_general) simp_all thus ?thesis by (simp add: o_def) qed lemma Ln_holomorphic [holomorphic_intros]: assumes "A \ \\<^sub>\\<^sub>0 = {}" shows "Ln holomorphic_on (A :: complex set)" proof (intro holomorphic_onI) fix z assume "z \ A" with assms have "(Ln has_field_derivative inverse z) (at z within A)" by (auto intro!: derivative_eq_intros) thus "Ln field_differentiable at z within A" by (auto simp: field_differentiable_def) qed lemma ln_Gamma_holomorphic [holomorphic_intros]: assumes "A \ \\<^sub>\\<^sub>0 = {}" shows "ln_Gamma holomorphic_on (A :: complex set)" proof (intro holomorphic_onI) fix z assume "z \ A" with assms have "(ln_Gamma has_field_derivative Digamma z) (at z within A)" by (auto intro!: derivative_eq_intros) thus "ln_Gamma field_differentiable at z within A" by (auto simp: field_differentiable_def) qed lemma higher_deriv_Polygamma: assumes "z \ \\<^sub>\\<^sub>0" shows "(deriv ^^ n) (Polygamma m) z = Polygamma (m + n) (z :: 'a :: {real_normed_field,euclidean_space})" proof - have "eventually (\u. (deriv ^^ n) (Polygamma m) u = Polygamma (m + n) u) (nhds z)" proof (induction n) case (Suc n) from Suc.IH have "eventually (\z. eventually (\u. (deriv ^^ n) (Polygamma m) u = Polygamma (m + n) u) (nhds z)) (nhds z)" by (simp add: eventually_eventually) hence "eventually (\z. deriv ((deriv ^^ n) (Polygamma m)) z = deriv (Polygamma (m + n)) z) (nhds z)" by eventually_elim (intro deriv_cong_ev refl) moreover have "eventually (\z. z \ UNIV - \\<^sub>\\<^sub>0) (nhds z)" using assms by (intro eventually_nhds_in_open open_Diff open_UNIV) auto ultimately show ?case by eventually_elim (simp_all add: deriv_Polygamma) qed simp_all thus ?thesis by (rule eventually_nhds_x_imp_x) qed lemma higher_deriv_cmult: assumes "f holomorphic_on A" "x \ A" "open A" shows "(deriv ^^ j) (\x. c * f x) x = c * (deriv ^^ j) f x" using assms proof (induction j arbitrary: f x) case (Suc j f x) have "deriv ((deriv ^^ j) (\x. c * f x)) x = deriv (\x. c * (deriv ^^ j) f x) x" using eventually_nhds_in_open[of A x] assms(2,3) Suc.prems by (intro deriv_cong_ev refl) (auto elim!: eventually_mono simp: Suc.IH) also have "\ = c * deriv ((deriv ^^ j) f) x" using Suc.prems assms(2,3) by (intro deriv_cmult holomorphic_on_imp_differentiable_at holomorphic_higher_deriv) auto finally show ?case by simp qed simp_all lemma higher_deriv_ln_Gamma_complex: assumes "(x::complex) \ \\<^sub>\\<^sub>0" shows "(deriv ^^ j) ln_Gamma x = (if j = 0 then ln_Gamma x else Polygamma (j - 1) x)" proof (cases j) case (Suc j') have "(deriv ^^ j') (deriv ln_Gamma) x = (deriv ^^ j') Digamma x" using eventually_nhds_in_open[of "UNIV - \\<^sub>\\<^sub>0" x] assms by (intro higher_deriv_cong_ev refl) (auto elim!: eventually_mono simp: open_Diff deriv_ln_Gamma_complex) also have "\ = Polygamma j' x" using assms by (subst higher_deriv_Polygamma) (auto elim!: nonpos_Ints_cases simp: complex_nonpos_Reals_iff) finally show ?thesis using Suc by (simp del: funpow.simps add: funpow_Suc_right) qed simp_all lemma higher_deriv_ln_Gamma_real: assumes "(x::real) > 0" shows "(deriv ^^ j) ln_Gamma x = (if j = 0 then ln_Gamma x else Polygamma (j - 1) x)" proof (cases j) case (Suc j') have "(deriv ^^ j') (deriv ln_Gamma) x = (deriv ^^ j') Digamma x" using eventually_nhds_in_open[of "{0<..}" x] assms by (intro higher_deriv_cong_ev refl) (auto elim!: eventually_mono simp: open_Diff deriv_ln_Gamma_real) also have "\ = Polygamma j' x" using assms by (subst higher_deriv_Polygamma) (auto elim!: nonpos_Ints_cases simp: complex_nonpos_Reals_iff) finally show ?thesis using Suc by (simp del: funpow.simps add: funpow_Suc_right) qed simp_all lemma higher_deriv_ln_Gamma_complex_of_real: assumes "(x :: real) > 0" shows "(deriv ^^ j) ln_Gamma (complex_of_real x) = of_real ((deriv ^^ j) ln_Gamma x)" using assms by (auto simp: higher_deriv_ln_Gamma_real higher_deriv_ln_Gamma_complex ln_Gamma_complex_of_real Polygamma_of_real) (* END TODO *) lemma stirling_limit_aux1: "((\y. Ln (1 + z * of_real y) / of_real y) \ z) (at_right 0)" for z :: complex proof (cases "z = 0") case True then show ?thesis by simp next case False have "((\y. ln (1 + z * of_real y)) has_vector_derivative 1 * z) (at 0)" - by (rule has_vector_derivative_real_complex) (auto intro!: derivative_eq_intros) + by (rule has_vector_derivative_real_field) (auto intro!: derivative_eq_intros) then have "(\y. (Ln (1 + z * of_real y) - of_real y * z) / of_real \y\) \0\ 0" by (auto simp add: has_vector_derivative_def has_derivative_def netlimit_at scaleR_conv_of_real field_simps) then have "((\y. (Ln (1 + z * of_real y) - of_real y * z) / of_real \y\) \ 0) (at_right 0)" by (rule filterlim_mono[OF _ _ at_le]) simp_all also have "?this \ ((\y. Ln (1 + z * of_real y) / (of_real y) - z) \ 0) (at_right 0)" using eventually_at_right_less[of "0::real"] by (intro filterlim_cong refl) (auto elim!: eventually_mono simp: field_simps) finally show ?thesis by (simp only: LIM_zero_iff) qed lemma stirling_limit_aux2: "((\y. y * Ln (1 + z / of_real y)) \ z) at_top" for z :: complex using stirling_limit_aux1[of z] by (subst filterlim_at_top_to_right) (simp add: field_simps) lemma Union_atLeastAtMost: assumes "N > 0" shows "(\n\{0.. {0..real N}" thus "x \ (\n\{0.. 0" "x < real N" by simp_all hence "x \ real (nat \x\)" "x \ real (nat \x\ + 1)" by linarith+ moreover from x have "nat \x\ < N" by linarith ultimately have "\n\{0.. {real n..real (n + 1)}" by (intro bexI[of _ "nat \x\"]) simp_all thus ?thesis by blast qed qed auto subsection \Asymptotics of @{term ln_Gamma}\ text \ This is the error term that occurs in the expansion of @{term ln_Gamma}. It can be shown to be of order $O(s^{-n})$. \ definition stirling_integral :: "nat \ 'a :: {real_normed_div_algebra, banach} \ 'a" where "stirling_integral n s = lim (\N. integral {0..N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n))" text \ \ context fixes s :: complex assumes s: "Re s > 0" fixes approx :: "nat \ complex" defines "approx \ (\N. (\n = 1.. \\\ ln_Gamma s\\ (ln_Gamma (of_nat N) - ln (2 * pi / of_nat N) / 2 - of_nat N * ln (of_nat N) + of_nat N) - \ \\\ 0\\ s * (harm (N - 1) - ln (of_nat (N - 1)) - euler_mascheroni) + \ \\\ 0\\ s * (ln (of_nat N + s) - ln (of_nat (N - 1))) - \ \\\ 0\\ (1/2) * (ln (of_nat N + s) - ln (of_nat N)) + \ \\\ 0\\ of_nat N * (ln (of_nat N + s) - ln (of_nat N)) - \ \\\ s\\ (s - 1/2) * ln s - ln (2 * pi) / 2)" begin qualified lemma assumes N: "N > 0" shows integrable_pbernpoly_1: "(\x. of_real (-pbernpoly 1 x) / (of_real x + s)) integrable_on {0..real N}" and integral_pbernpoly_1_aux: "integral {0..real N} (\x. -of_real (pbernpoly 1 x) / (of_real x + s)) = approx N" and has_integral_pbernpoly_1: "((\x. pbernpoly 1 x /(x + s)) has_integral (\mx. -pbernpoly 1 x / (x + s)) has_integral (of_nat n + 1/2 + s) * (ln (of_nat (n + 1) + s) - ln (of_nat n + s)) - 1) {of_nat n..of_nat (n + 1)}" for n proof (rule has_integral_spike) have "((\x. (of_nat n + 1/2 + s) * (1 / (x + s)) - 1) has_integral (of_nat n + 1/2 + s) * (ln (of_real (real (n + 1)) + s) - ln (of_real (real n) + s)) - 1) {of_nat n..of_nat (n + 1)}" using s has_integral_const_real[of 1 "of_nat n" "of_nat (n + 1)"] by (intro has_integral_diff has_integral_mult_right fundamental_theorem_of_calculus) - (auto intro!: derivative_eq_intros has_vector_derivative_real_complex + (auto intro!: derivative_eq_intros has_vector_derivative_real_field simp: has_field_derivative_iff_has_vector_derivative [symmetric] field_simps complex_nonpos_Reals_iff) thus "((\x. (of_nat n + 1/2 + s) * (1 / (x + s)) - 1) has_integral (of_nat n + 1/2 + s) * (ln (of_nat (n + 1) + s) - ln (of_nat n + s)) - 1) {of_nat n..of_nat (n + 1)}" by simp show "-pbernpoly 1 x / (x + s) = (of_nat n + 1/2 + s) * (1 / (x + s)) - 1" if "x \ {of_nat n..of_nat (n + 1)} - {of_nat (n + 1)}" for x proof - have x: "x \ real n" "x < real (n + 1)" using that by simp_all hence "floor x = int n" by linarith moreover from s x have "complex_of_real x \ -s" by (auto simp add: complex_eq_iff simp del: of_nat_Suc) ultimately show "-pbernpoly 1 x / (x + s) = (of_nat n + 1/2 + s) * (1 / (x + s)) - 1" by (auto simp: pbernpoly_def bernpoly_def frac_def divide_simps add_eq_0_iff2) qed qed simp_all hence *: "\I. I\?A \ ((\x. -pbernpoly 1 x / (x + s)) has_integral (Inf I + 1/2 + s) * (ln (Inf I + 1 + s) - ln (Inf I + s)) - 1) I" by (auto simp: add_ac) have "((\x. - pbernpoly 1 x / (x + s)) has_integral (\I\?A. (Inf I + 1 / 2 + s) * (ln (Inf I + 1 + s) - ln (Inf I + s)) - 1)) (\n\{0..x. - pbernpoly 1 x / (x + s)) has_integral ?i) {0..real N}" by (subst has_integral_spike_set_eq) (use Union_atLeastAtMost assms in \auto simp: intro!: empty_imp_negligible\) hence "(\x. - pbernpoly 1 x / (x + s)) integrable_on {0..real N}" and integral: "integral {0..real N} (\x. - pbernpoly 1 x / (x + s)) = ?i" by (simp_all add: has_integral_iff) show "(\x. - pbernpoly 1 x / (x + s)) integrable_on {0..real N}" by fact note has_integral_neg[OF has_integral] also have "-?i = (\xx. of_real (pbernpoly 1 x) / (of_real x + s)) has_integral \) {0..real N}" by simp note integral also have "?i = (\nnnn=1.. = (\n=1..n=1..n=1..n=1.. - (\n = 1..n=1.. 0" for x by (auto simp: complex_eq_iff) hence "(\n=1..n=1.. = ln (fact (N - 1)) + (\n=1..n=1..n=1..n=1..n = 1..n = 1..x. -of_real (pbernpoly 1 x) / (of_real x + s)) = \" by simp qed lemma integrable_ln_Gamma_aux: shows "(\x. of_real (pbernpoly n x) / (of_real x + s) ^ n) integrable_on {0..real N}" proof (cases "n = 1") case True with s show ?thesis using integrable_neg[OF integrable_pbernpoly_1[of N]] by (cases "N = 0") (simp_all add: integrable_on_negligible) next case False from s have "of_real x + s \ 0" if "x \ 0" for x using that by (auto simp: complex_eq_iff add_eq_0_iff2) with False s show ?thesis by (auto intro!: integrable_continuous_real continuous_intros) qed text \ This following proof is based on ``Rudiments of the theory of the gamma function'' by Bruce Berndt~\cite{berndt}. \ qualified lemma integral_pbernpoly_1: "(\N. integral {0..real N} (\x. pbernpoly 1 x / (x + s))) \ -ln_Gamma s - s + (s - 1 / 2) * ln s + ln (2 * pi) / 2" proof - have neq: "s + of_real x \ 0" if "x \ 0" for x :: real using that s by (auto simp: complex_eq_iff) have "(approx \ ln_Gamma s - 0 - 0 + 0 - 0 + s - (s - 1/2) * ln s - ln (2 * pi) / 2) at_top" unfolding approx_def proof (intro tendsto_add tendsto_diff) from s have s': "s \ \\<^sub>\\<^sub>0" by (auto elim!: nonpos_Ints_cases) have "(\n. \i=1.. ln_Gamma s + euler_mascheroni * s + ln s" (is "?f \ _") using ln_Gamma_series'_aux[OF s'] unfolding sums_def by (subst LIMSEQ_Suc_iff [symmetric], subst (asm) sum.atLeast1_atMost_eq [symmetric]) (simp add: atLeastLessThanSuc_atLeastAtMost) thus "((\n. ?f n - (euler_mascheroni * s + ln s)) \ ln_Gamma s) at_top" by (auto intro: tendsto_eq_intros) next show "(\x. complex_of_real (ln_Gamma (real x) - ln (2 * pi / real x) / 2 - real x * ln (real x) + real x)) \ 0" proof (intro tendsto_of_real_0_I filterlim_compose[OF tendsto_sandwich filterlim_real_sequentially]) show "eventually (\x::real. ln_Gamma x - ln (2 * pi / x) / 2 - x * ln x + x \ 0) at_top" using eventually_ge_at_top[of "1::real"] by eventually_elim (insert ln_Gamma_bounds(1), simp add: algebra_simps) show "eventually (\x::real. ln_Gamma x - ln (2 * pi / x) / 2 - x * ln x + x \ 1 / 12 * inverse x) at_top" using eventually_ge_at_top[of "1::real"] by eventually_elim (insert ln_Gamma_bounds(2), simp add: field_simps) show "((\x::real. 1 / 12 * inverse x) \ 0) at_top" by (intro tendsto_mult_right_zero tendsto_inverse_0_at_top filterlim_ident) qed simp_all next have "(\x. s * of_real (harm (x - 1) - ln (real (x - 1)) - euler_mascheroni)) \ s * of_real (euler_mascheroni - euler_mascheroni)" by (subst LIMSEQ_Suc_iff [symmetric], intro tendsto_intros) (insert euler_mascheroni_LIMSEQ, simp_all) also have "?this \ (\x. s * (harm (x - 1) - ln (of_nat (x - 1)) - euler_mascheroni)) \ 0" by (intro filterlim_cong refl eventually_mono[OF eventually_gt_at_top[of "1::nat"]]) (auto simp: Ln_of_nat of_real_harm) finally show "(\x. s * (harm (x - 1) - ln (of_nat (x - 1)) - euler_mascheroni)) \ 0" . next have "((\x. ln (1 + (s + 1) / of_real x)) \ ln (1 + 0)) at_top" (is ?P) by (intro tendsto_intros tendsto_divide_0[OF tendsto_const]) (simp_all add: filterlim_ident filterlim_at_infinity_conv_norm_at_top filterlim_abs_real) also have "ln (of_real (x + 1) + s) - ln (complex_of_real x) = ln (1 + (s + 1) / of_real x)" if "x > 1" for x using that s using Ln_divide_of_real[of x "of_real (x + 1) + s", symmetric] neq[of "x+1"] by (simp add: field_simps Ln_of_real) hence "?P \ ((\x. ln (of_real (x + 1) + s) - ln (of_real x)) \ 0) at_top" by (intro filterlim_cong refl) (auto intro: eventually_mono[OF eventually_gt_at_top[of "1::real"]]) finally have "((\n. ln (of_real (real n + 1) + s) - ln (of_real (real n))) \ 0) at_top" by (rule filterlim_compose[OF _ filterlim_real_sequentially]) hence "((\n. ln (of_nat n + s) - ln (of_nat (n - 1))) \ 0) at_top" by (subst LIMSEQ_Suc_iff [symmetric]) (simp add: add_ac) thus "(\x. s * (ln (of_nat x + s) - ln (of_nat (x - 1)))) \ 0" by (rule tendsto_mult_right_zero) next have "((\x. ln (1 + s / of_real x)) \ ln (1 + 0)) at_top" (is ?P) by (intro tendsto_intros tendsto_divide_0[OF tendsto_const]) (simp_all add: filterlim_ident filterlim_at_infinity_conv_norm_at_top filterlim_abs_real) also have "ln (of_real x + s) - ln (of_real x) = ln (1 + s / of_real x)" if "x > 0" for x using Ln_divide_of_real[of x "of_real x + s"] neq[of x] that by (auto simp: field_simps Ln_of_real) hence "?P \ ((\x. ln (of_real x + s) - ln (of_real x)) \ 0) at_top" using s by (intro filterlim_cong refl) (auto intro: eventually_mono [OF eventually_gt_at_top[of "1::real"]]) finally have "(\x. (1/2) * (ln (of_real (real x) + s) - ln (of_real (real x)))) \ 0" by (rule tendsto_mult_right_zero[OF filterlim_compose[OF _ filterlim_real_sequentially]]) thus "(\x. (1/2) * (ln (of_nat x + s) - ln (of_nat x))) \ 0" by simp next have "((\x. x * (ln (1 + s / of_real x))) \ s) at_top" (is ?P) by (rule stirling_limit_aux2) also have "ln (1 + s / of_real x) = ln (of_real x + s) - ln (of_real x)" if "x > 1" for x using that s Ln_divide_of_real [of x "of_real x + s", symmetric] neq[of x] by (auto simp: Ln_of_real field_simps) hence "?P \ ((\x. of_real x * (ln (of_real x + s) - ln (of_real x))) \ s) at_top" by (intro filterlim_cong refl) (auto intro: eventually_mono[OF eventually_gt_at_top[of "1::real"]]) finally have "(\n. of_real (real n) * (ln (of_real (real n) + s) - ln (of_real (real n)))) \ s" by (rule filterlim_compose[OF _ filterlim_real_sequentially]) thus "(\n. of_nat n * (ln (of_nat n + s) - ln (of_nat n))) \ s" by simp qed simp_all also have "?this \ ((\N. integral {0..real N} (\x. -pbernpoly 1 x / (x + s))) \ ln_Gamma s + s - (s - 1/2) * ln s - ln (2 * pi) / 2) at_top" using integral_pbernpoly_1_aux by (intro filterlim_cong refl) (auto intro: eventually_mono[OF eventually_gt_at_top[of "0::nat"]]) also have "(\N. integral {0..real N} (\x. -pbernpoly 1 x / (x + s))) = (\N. -integral {0..real N} (\x. pbernpoly 1 x / (x + s)))" by (simp add: fun_eq_iff) finally show ?thesis by (simp add: tendsto_minus_cancel_left [symmetric] algebra_simps) qed qualified lemma pbernpoly_integral_conv_pbernpoly_integral_Suc: assumes "n \ 1" shows "integral {0..real N} (\x. pbernpoly n x / (x + s) ^ n) = of_real (pbernpoly (Suc n) (real N)) / (of_nat (Suc n) * (s + of_nat N) ^ n) - of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n) + of_nat n / of_nat (Suc n) * integral {0..real N} (\x. of_real (pbernpoly (Suc n) x) / (of_real x + s) ^ Suc n)" proof - note [derivative_intros] = has_field_derivative_pbernpoly_Suc' define I where "I = -of_real (pbernpoly (Suc n) (of_nat N)) / (of_nat (Suc n) * (of_nat N + s) ^ n) + of_real (bernoulli (Suc n) / real (Suc n)) / s ^ n + integral {0..real N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n)" have "((\x. (-of_nat n * inverse (of_real x + s) ^ Suc n) * (of_real (pbernpoly (Suc n) x) / (of_nat (Suc n)))) has_integral -I) {0..real N}" proof (rule integration_by_parts_interior_strong[OF bounded_bilinear_mult]) fix x :: real assume x: "x \ {0<.. \" proof assume "x \ \" then obtain n where "x = of_int n" by (auto elim!: Ints_cases) with x have x': "x = of_nat (nat n)" by simp from x show False by (auto simp: x') qed hence "((\x. of_real (pbernpoly (Suc n) x / of_nat (Suc n))) has_vector_derivative complex_of_real (pbernpoly n x)) (at x)" by (intro has_vector_derivative_of_real) (auto intro!: derivative_eq_intros) thus "((\x. of_real (pbernpoly (Suc n) x) / of_nat (Suc n)) has_vector_derivative complex_of_real (pbernpoly n x)) (at x)" by simp from x s have "complex_of_real x + s \ 0" by (auto simp: complex_eq_iff) thus "((\x. inverse (of_real x + s) ^ n) has_vector_derivative - of_nat n * inverse (of_real x + s) ^ Suc n) (at x)" using x s assms - by (auto intro!: derivative_eq_intros has_vector_derivative_real_complex simp: divide_simps power_add [symmetric] + by (auto intro!: derivative_eq_intros has_vector_derivative_real_field simp: divide_simps power_add [symmetric] simp del: power_Suc) next have "complex_of_real x + s \ 0" if "x \ 0" for x using that s by (auto simp: complex_eq_iff) thus "continuous_on {0..real N} (\x. inverse (of_real x + s) ^ n)" "continuous_on {0..real N} (\x. complex_of_real (pbernpoly (Suc n) x) / of_nat (Suc n))" using assms s by (auto intro!: continuous_intros simp del: of_nat_Suc) next have "((\x. inverse (of_real x + s) ^ n * of_real (pbernpoly n x)) has_integral pbernpoly (Suc n) (of_nat N) / (of_nat (Suc n) * (of_nat N + s) ^ n) - of_real (bernoulli (Suc n) / real (Suc n)) / s ^ n - -I) {0..real N}" using integrable_ln_Gamma_aux[of n N] assms by (auto simp: I_def has_integral_integral divide_simps) thus "((\x. inverse (of_real x + s) ^ n * of_real (pbernpoly n x)) has_integral inverse (of_real (real N) + s) ^ n * (of_real (pbernpoly (Suc n) (real N)) / of_nat (Suc n)) - inverse (of_real 0 + s) ^ n * (of_real (pbernpoly (Suc n) 0) / of_nat (Suc n)) - - I) {0..real N}" by (simp_all add: field_simps) qed simp_all also have "(\x. - of_nat n * inverse (of_real x + s) ^ Suc n * (of_real (pbernpoly (Suc n) x) / of_nat (Suc n))) = (\x. - (of_nat n / of_nat (Suc n) * of_real (pbernpoly (Suc n) x) / (of_real x + s) ^ Suc n))" by (simp add: divide_simps fun_eq_iff) finally have "((\x. - (of_nat n / of_nat (Suc n) * of_real (pbernpoly (Suc n) x) / (of_real x + s) ^ Suc n)) has_integral - I) {0..real N}" . from has_integral_neg[OF this] show ?thesis by (auto simp add: I_def has_integral_iff algebra_simps integral_mult_right [symmetric] simp del: power_Suc of_nat_Suc ) qed lemma pbernpoly_over_power_tendsto_0: assumes "n > 0" shows "(\x. of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \ 0" proof - from s have neq: "s + of_nat n \ 0" for n by (auto simp: complex_eq_iff) from bounded_pbernpoly[of "Suc n"] guess c . note c = this have "eventually (\x. norm (of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \ (c / real (Suc n)) / real x ^ n) at_top" using eventually_gt_at_top[of "0::nat"] proof eventually_elim case (elim x) have "norm (of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \ (c / real (Suc n)) / norm (s + of_nat x) ^ n" (is "_ \ ?rhs") using c[of x] by (auto simp: norm_divide norm_mult norm_power neq field_simps simp del: of_nat_Suc) also have "real x \ cmod (s + of_nat x)" using complex_Re_le_cmod[of "s + of_nat x"] s by simp hence "?rhs \ (c / real (Suc n)) / real x ^ n" using s elim c[of 0] neq[of x] by (intro divide_left_mono power_mono mult_pos_pos divide_nonneg_pos zero_less_power) auto finally show ?case . qed moreover have "(\x. (c / real (Suc n)) / real x ^ n) \ 0" by (intro real_tendsto_divide_at_top[OF tendsto_const] filterlim_pow_at_top assms filterlim_real_sequentially) ultimately show ?thesis by (rule Lim_null_comparison) qed lemma convergent_stirling_integral: assumes "n > 0" shows "convergent (\N. integral {0..real N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n))" (is "convergent (?f n)") proof - have "convergent (?f (Suc n))" for n proof (induction n) case 0 thus ?case using integral_pbernpoly_1 by (auto intro!: convergentI) next case (Suc n) have "convergent (\N. ?f (Suc n) N - of_real (pbernpoly (Suc (Suc n)) (real N)) / (of_nat (Suc (Suc n)) * (s + of_nat N) ^ Suc n) + of_real (bernoulli (Suc (Suc n)) / (real (Suc (Suc n)))) / s ^ Suc n)" (is "convergent ?g") by (intro convergent_add convergent_diff Suc convergent_const convergentI[OF pbernpoly_over_power_tendsto_0]) simp_all also have "?g = (\N. of_nat (Suc n) / of_nat (Suc (Suc n)) * ?f (Suc (Suc n)) N)" using s by (subst pbernpoly_integral_conv_pbernpoly_integral_Suc) (auto simp: fun_eq_iff field_simps simp del: of_nat_Suc power_Suc) also have "convergent \ \ convergent (?f (Suc (Suc n)))" by (intro convergent_mult_const_iff) (simp_all del: of_nat_Suc) finally show ?case . qed from this[of "n - 1"] assms show ?thesis by simp qed lemma stirling_integral_conv_stirling_integral_Suc: assumes "n > 0" shows "stirling_integral n s = of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s - of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)" proof - have "(\N. of_real (pbernpoly (Suc n) (real N)) / (of_nat (Suc n) * (s + of_nat N) ^ n) - of_real (bernoulli (Suc n)) / (real (Suc n) * s ^ n) + integral {0..real N} (\x. of_nat n / of_nat (Suc n) * (of_real (pbernpoly (Suc n) x) / (of_real x + s) ^ Suc n))) \ 0 - of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n) + of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s" (is "?f \ _") unfolding stirling_integral_def integral_mult_right using convergent_stirling_integral[of "Suc n"] assms s by (intro tendsto_intros pbernpoly_over_power_tendsto_0) (auto simp: convergent_LIMSEQ_iff simp del: of_nat_Suc) also have "?this \ (\N. integral {0..real N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n)) \ of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s - of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)" using eventually_gt_at_top[of "0::nat"] pbernpoly_integral_conv_pbernpoly_integral_Suc[of n] assms unfolding integral_mult_right by (intro filterlim_cong refl) (auto elim!: eventually_mono simp del: power_Suc) finally show ?thesis unfolding stirling_integral_def[of n] by (rule limI) qed lemma stirling_integral_1_unfold: assumes "m > 0" shows "stirling_integral 1 s = stirling_integral m s / of_nat m - (\k=1..k=1..k = 1.. 0" shows "ln_Gamma s = (s - 1 / 2) * ln s - s + ln (2 * pi) / 2 + (\k=1..k = 1.. 0 \ (\x. integral {0..real x} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n)) \ stirling_integral n s" unfolding stirling_integral_def using convergent_stirling_integral[of n] by (simp only: convergent_LIMSEQ_iff) end lemmas has_integral_of_real = has_integral_linear[OF _ bounded_linear_of_real, unfolded o_def] lemmas integral_of_real = integral_linear[OF _ bounded_linear_of_real, unfolded o_def] lemma integrable_ln_Gamma_aux_real: assumes "0 < s" shows "(\x. pbernpoly n x / (x + s) ^ n) integrable_on {0..real N}" proof - have "(\x. complex_of_real (pbernpoly n x / (x + s) ^ n)) integrable_on {0..real N}" using integrable_ln_Gamma_aux[of "of_real s" n N] assms by simp from integrable_linear[OF this bounded_linear_Re] show ?thesis by (simp only: o_def Re_complex_of_real) qed lemma assumes "x > 0" "n > 0" shows stirling_integral_complex_of_real: "stirling_integral n (complex_of_real x) = of_real (stirling_integral n x)" and LIMSEQ_stirling_integral_real: "(\N. integral {0..real N} (\t. pbernpoly n t / (t + x) ^ n)) \ stirling_integral n x" and stirling_integral_real_convergent: "convergent (\N. integral {0..real N} (\t. pbernpoly n t / (t + x) ^ n))" proof - have "(\N. integral {0..real N} (\t. of_real (pbernpoly n t / (t + x) ^ n))) \ stirling_integral n (complex_of_real x)" using LIMSEQ_stirling_integral[of "complex_of_real x" n] assms by simp hence "(\N. of_real (integral {0..real N} (\t. pbernpoly n t / (t + x) ^ n))) \ stirling_integral n (complex_of_real x)" using integrable_ln_Gamma_aux_real[OF assms(1), of n] by (subst (asm) integral_of_real) simp from tendsto_Re[OF this] have "(\N. integral {0..real N} (\t. pbernpoly n t / (t + x) ^ n)) \ Re (stirling_integral n (complex_of_real x))" by simp thus "convergent (\N. integral {0..real N} (\t. pbernpoly n t / (t + x) ^ n))" by (rule convergentI) thus "(\N. integral {0..real N} (\t. pbernpoly n t / (t + x) ^ n)) \ stirling_integral n x" unfolding stirling_integral_def by (simp add: convergent_LIMSEQ_iff) from tendsto_of_real[OF this, where 'a = complex] integrable_ln_Gamma_aux_real[OF assms(1), of n] have "(\xa. integral {0..real xa} (\xa. complex_of_real (pbernpoly n xa) / (complex_of_real xa + x) ^ n)) \ complex_of_real (stirling_integral n x)" by (subst (asm) integral_of_real [symmetric]) simp_all from LIMSEQ_unique[OF this LIMSEQ_stirling_integral[of "complex_of_real x" n]] assms show "stirling_integral n (complex_of_real x) = of_real (stirling_integral n x)" by simp qed lemma ln_Gamma_stirling_real: assumes "x > (0 :: real)" "m > (0::nat)" shows "ln_Gamma x = (x - 1 / 2) * ln x - x + ln (2 * pi) / 2 + (\k = 1..k = 1.. (1::nat)" obtains c where "\s. Re s > 0 \ norm (stirling_integral n s) \ c / Re s ^ (n - 1)" proof - obtain c where c: "norm (pbernpoly n x) \ c" for x by (rule bounded_pbernpoly[of n]) blast have c': "pbernpoly n x \ c" for x using c[of x] by (simp add: abs_real_def split: if_splits) from c[of 0] have c_nonneg: "c \ 0" by simp have "norm (stirling_integral n s) \ c / (real n - 1) / Re s ^ (n - 1)" if s: "Re s > 0" for s proof (rule Lim_norm_ubound[OF _ LIMSEQ_stirling_integral]) have pos: "x + norm s > 0" if "x \ 0" for x using s that by (intro add_nonneg_pos) auto have nz: "of_real x + s \ 0" if "x \ 0" for x using s that by (auto simp: complex_eq_iff) let ?bound = "\N. c / (Re s ^ (n - 1) * (real n - 1)) - c / ((real N + Re s) ^ (n - 1) * (real n - 1))" show "eventually (\N. norm (integral {0..real N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n)) \ c / (real n - 1) / Re s ^ (n - 1)) at_top" using eventually_gt_at_top[of "0::nat"] proof eventually_elim case (elim N) let ?F = "\x. -c / ((x + Re s) ^ (n - 1) * (real n - 1))" from n s have "((\x. c / (x + Re s) ^ n) has_integral (?F (real N) - ?F 0)) {0..real N}" by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros simp: divide_simps power_diff add_eq_0_iff2 has_field_derivative_iff_has_vector_derivative [symmetric]) also have "?F (real N) - ?F 0 = ?bound N" by simp finally have *: "((\x. c / (x + Re s) ^ n) has_integral ?bound N) {0..real N}" . have "norm (integral {0..real N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n)) \ integral {0..real N} (\x. c / (x + Re s) ^ n)" proof (intro integral_norm_bound_integral integrable_ln_Gamma_aux s ballI) fix x assume x: "x \ {0..real N}" have "norm (of_real (pbernpoly n x) / (of_real x + s) ^ n) \ c / norm (of_real x + s) ^ n" unfolding norm_divide norm_power using c by (intro divide_right_mono) simp_all also have "\ \ c / (x + Re s) ^ n" using x c c_nonneg s nz[of x] complex_Re_le_cmod[of "of_real x + s"] by (intro divide_left_mono power_mono mult_pos_pos zero_less_power add_nonneg_pos) auto finally show "norm (of_real (pbernpoly n x) / (of_real x + s) ^ n) \ \" . qed (insert n s * pos nz c, auto) also have "\ = ?bound N" using * by (simp add: has_integral_iff) also have "\ \ c / (Re s ^ (n - 1) * (real n - 1))" using c_nonneg elim s n by simp also have "\ = c / (real n - 1) / (Re s ^ (n - 1))" by simp finally show "norm (integral {0..real N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n)) \ c / (real n - 1) / Re s ^ (n - 1)" . qed qed (insert s n, simp_all) thus ?thesis by (rule that) qed lemma stirling_integral_bound: assumes "n > 0" obtains c where "\s. Re s > 0 \ norm (stirling_integral n s) \ c / Re s ^ n" proof - let ?f = "\s. of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s - of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)" from stirling_integral_bound_aux[of "Suc n"] assms obtain c where c: "\s. Re s > 0 \ norm (stirling_integral (Suc n) s) \ c / Re s ^ n" by auto define c1 where "c1 = real n / real (Suc n) * c" define c2 where "c2 = \bernoulli (Suc n)\ / real (Suc n)" have c2_nonneg: "c2 \ 0" by (simp add: c2_def) show ?thesis proof (rule that) fix s :: complex assume s: "Re s > 0" have "stirling_integral n s = ?f s" using s assms by (rule stirling_integral_conv_stirling_integral_Suc) also have "norm \ \ norm (of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s) + norm (of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n))" by (rule norm_triangle_ineq4) also have "\ = real n / real (Suc n) * norm (stirling_integral (Suc n) s) + c2 / norm s ^ n" (is "_ = ?A + ?B") by (simp add: norm_divide norm_mult norm_power c2_def field_simps del: of_nat_Suc) also have "?A \ real n / real (Suc n) * (c / Re s ^ n)" by (intro mult_left_mono c s) simp_all also have "\ = c1 / Re s ^ n" by (simp add: c1_def) also have "c2 / norm s ^ n \ c2 / Re s ^ n" using s c2_nonneg by (intro divide_left_mono power_mono complex_Re_le_cmod mult_pos_pos zero_less_power) auto also have "c1 / Re s ^ n + c2 / Re s ^ n = (c1 + c2) / Re s ^ n" using s by (simp add: field_simps) finally show "norm (stirling_integral n s) \ (c1 + c2) / Re s ^ n" by - simp_all qed qed end lemma stirling_integral_holomorphic [holomorphic_intros]: assumes m: "m > 0" and "\s\A. Re s > 0" shows "stirling_integral m holomorphic_on A" proof - let ?f = "\s::complex. of_nat m * ((s - 1 / 2) * Ln s - s + of_real (ln (2 * pi) / 2) + (\k=1.. stirling_integral m holomorphic_on A" using assms by (intro holomorphic_cong refl) (simp_all add: field_simps ln_Gamma_stirling_complex) finally show "stirling_integral m holomorphic_on A" . qed lemma stirling_integral_continuous_on [continuous_intros]: assumes m: "m > 0" and "\s\A. Re s > 0" shows "continuous_on A (stirling_integral m)" by (intro holomorphic_on_imp_continuous_on stirling_integral_holomorphic assms) lemma has_field_derivative_stirling_integral: assumes "Re x > 0" "n > 0" shows "(stirling_integral n has_field_derivative deriv (stirling_integral n) x) (at x)" using assms by (intro holomorphic_derivI[OF stirling_integral_holomorphic, of n "{s. Re s > 0}"] open_halfspace_Re_gt) auto lemma assumes n: "n > 0" and "x > 0" shows deriv_stirling_integral_complex_of_real: "(deriv ^^ j) (stirling_integral n) (complex_of_real x) = complex_of_real ((deriv ^^ j) (stirling_integral n) x)" (is "?lhs x = ?rhs x") and differentiable_stirling_integral_real: "(deriv ^^ j) (stirling_integral n) field_differentiable at x" (is ?thesis2) proof - let ?A = "{s. Re s > 0}" let ?f = "\j x. (deriv ^^ j) (stirling_integral n) (complex_of_real x)" let ?f' = "\j x. complex_of_real ((deriv ^^ j) (stirling_integral n) x)" have [simp]: "open ?A" by (simp add: open_halfspace_Re_gt) have "?lhs x = ?rhs x \ (deriv ^^ j) (stirling_integral n) field_differentiable at x" if "x > 0" for x using that proof (induction j arbitrary: x) case 0 have "((\x. Re (stirling_integral n (of_real x))) has_field_derivative Re (deriv (\x. stirling_integral n x) (of_real x))) (at x)" using 0 n - by (auto intro!: derivative_intros has_vector_derivative_real_complex + by (auto intro!: derivative_intros has_vector_derivative_real_field field_differentiable_derivI holomorphic_on_imp_differentiable_at[of _ ?A] stirling_integral_holomorphic) also have "?this \ (stirling_integral n has_field_derivative Re (deriv (\x. stirling_integral n x) (of_real x))) (at x)" using eventually_nhds_in_open[of "{0<..}" x] 0 n by (intro has_field_derivative_cong_ev refl) (auto elim!: eventually_mono simp: stirling_integral_complex_of_real) finally have "stirling_integral n field_differentiable at x" by (auto simp: field_differentiable_def) with 0 n show ?case by (auto simp: stirling_integral_complex_of_real) next case (Suc j x) note IH = conjunct1[OF Suc.IH] conjunct2[OF Suc.IH] have *: "(deriv ^^ Suc j) (stirling_integral n) (complex_of_real x) = of_real ((deriv ^^ Suc j) (stirling_integral n) x)" if x: "x > 0" for x proof - have "deriv ((deriv ^^ j) (stirling_integral n)) (complex_of_real x) = vector_derivative (\x. (deriv ^^ j) (stirling_integral n) (of_real x)) (at x)" using n x by (intro vector_derivative_of_real_right [symmetric] holomorphic_on_imp_differentiable_at[of _ ?A] holomorphic_higher_deriv stirling_integral_holomorphic) auto also have "\ = vector_derivative (\x. of_real ((deriv ^^ j) (stirling_integral n) x)) (at x)" using eventually_nhds_in_open[of "{0<..}" x] x by (intro vector_derivative_cong_eq) (auto elim!: eventually_mono simp: IH(1)) also have "\ = of_real (deriv ((deriv ^^ j) (stirling_integral n)) x)" by (intro vector_derivative_of_real_left holomorphic_on_imp_differentiable_at[of _ ?A] field_differentiable_imp_differentiable IH(2) x) finally show ?thesis by simp qed have "((\x. Re ((deriv ^^ Suc j) (stirling_integral n) (of_real x))) has_field_derivative Re (deriv ((deriv ^^ Suc j) (stirling_integral n)) (of_real x))) (at x)" using Suc.prems n - by (intro derivative_intros has_vector_derivative_real_complex field_differentiable_derivI + by (intro derivative_intros has_vector_derivative_real_field field_differentiable_derivI holomorphic_on_imp_differentiable_at[of _ ?A] stirling_integral_holomorphic holomorphic_higher_deriv) auto also have "?this \ ((deriv ^^ Suc j) (stirling_integral n) has_field_derivative Re (deriv ((deriv ^^ Suc j) (stirling_integral n)) (of_real x))) (at x)" using eventually_nhds_in_open[of "{0<..}" x] Suc.prems * by (intro has_field_derivative_cong_ev refl) (auto elim!: eventually_mono) finally have "(deriv ^^ Suc j) (stirling_integral n) field_differentiable at x" by (auto simp: field_differentiable_def) with *[OF Suc.prems] show ?case by blast qed from this[OF assms(2)] show "?lhs x = ?rhs x" ?thesis2 by blast+ qed text \ Unfortunately, asymptotic power series cannot, in general, be differentiated. However, since @{term ln_Gamma} is holomorphic on the entire positive real half-space, we can differentiate its asymptotic expansion after all. To do this, we use an ad-hoc version of the more general approach outlined in Erdelyi's ``Asymptotic Expansions'' for holomorphic functions: We bound the value of the $j$-th derivative of the remainder term at some value $x$ by applying Cauchy's integral formula along a circle centred at $x$ with radius $\frac{1}{2} x$. \ lemma deriv_stirling_integral_real_bound: assumes m: "m > 0" shows "(deriv ^^ j) (stirling_integral m) \ O(\x::real. 1 / x ^ (m + j))" proof - from stirling_integral_bound[OF m] guess c . note c = this have "0 \ cmod (stirling_integral m 1)" by simp also have "\ \ c" using c[of 1] by simp finally have c_nonneg: "c \ 0" . define B where "B = c * 2 ^ (m + Suc j)" define B' where "B' = B * fact j / 2" have "eventually (\x::real. norm ((deriv ^^ j) (stirling_integral m) x) \ B' * norm (1 / x ^ (m+ j))) at_top" using eventually_gt_at_top[of "0::real"] proof eventually_elim case (elim x) have "Re s > 0" if "s \ cball (of_real x) (x/2)" for s :: complex proof - have "x - Re s \ norm (of_real x - s)" using complex_Re_le_cmod[of "of_real x - s"] by simp also from that have "\ \ x/2" by (simp add: dist_complex_def) finally show ?thesis using elim by simp qed hence "((\u. stirling_integral m u / (u - of_real x) ^ Suc j) has_contour_integral complex_of_real (2 * pi) * \ / fact j * (deriv ^^ j) (stirling_integral m) (of_real x)) (circlepath (of_real x) (x/2))" using m elim by (intro Cauchy_has_contour_integral_higher_derivative_circlepath stirling_integral_continuous_on stirling_integral_holomorphic) auto hence "norm (of_real (2 * pi) * \ / fact j * (deriv ^^ j) (stirling_integral m) (of_real x)) \ B / x ^ (m + Suc j) * (2 * pi * (x / 2))" proof (rule has_contour_integral_bound_circlepath) fix u :: complex assume dist: "norm (u - of_real x) = x / 2" have "Re (of_real x - u) \ norm (of_real x - u)" by (rule complex_Re_le_cmod) also have "\ = x / 2" using dist by (simp add: norm_minus_commute) finally have Re_u: "Re u \ x/2" using elim by simp have "norm (stirling_integral m u / (u - of_real x) ^ Suc j) \ c / Re u ^ m / (x / 2) ^ Suc j" using Re_u elim unfolding norm_divide norm_power dist by (intro divide_right_mono zero_le_power c) simp_all also have "\ \ c / (x/2) ^ m / (x / 2) ^ Suc j" using c_nonneg elim Re_u by (intro divide_right_mono divide_left_mono power_mono) simp_all also have "\ = B / x ^ (m + Suc j)" using elim by (simp add: B_def field_simps power_add) finally show "norm (stirling_integral m u / (u - of_real x) ^ Suc j) \ B / x ^ (m + Suc j)" . qed (insert elim c_nonneg, auto simp: B_def simp del: power_Suc) hence "cmod ((deriv ^^ j) (stirling_integral m) (of_real x)) \ B' / x ^ (j + m)" using elim by (simp add: field_simps norm_divide norm_mult norm_power B'_def) with elim m show ?case by (simp_all add: add_ac deriv_stirling_integral_complex_of_real) qed thus ?thesis by (rule bigoI) qed definition stirling_sum where "stirling_sum j m x = (-1) ^ j * (\k = 1..k\m. (of_real (bernoulli' k) * pochhammer (of_nat (Suc k)) (j - 1) * inverse x ^ (k + j)))" lemma stirling_sum_complex_of_real: "stirling_sum j m (complex_of_real x) = complex_of_real (stirling_sum j m x)" by (simp add: stirling_sum_def pochhammer_of_real [symmetric] del: of_nat_Suc) lemma stirling_sum'_complex_of_real: "stirling_sum' j m (complex_of_real x) = complex_of_real (stirling_sum' j m x)" by (simp add: stirling_sum'_def pochhammer_of_real [symmetric] del: of_nat_Suc) lemma has_field_derivative_stirling_sum_complex [derivative_intros]: "Re x > 0 \ (stirling_sum j m has_field_derivative stirling_sum (Suc j) m x) (at x)" unfolding stirling_sum_def [abs_def] sum_distrib_left by (rule DERIV_sum) (auto intro!: derivative_eq_intros simp del: of_nat_Suc simp: pochhammer_Suc power_diff) lemma has_field_derivative_stirling_sum_real [derivative_intros]: "x > (0::real) \ (stirling_sum j m has_field_derivative stirling_sum (Suc j) m x) (at x)" unfolding stirling_sum_def [abs_def] sum_distrib_left by (rule DERIV_sum) (auto intro!: derivative_eq_intros simp del: of_nat_Suc simp: pochhammer_Suc power_diff) lemma has_field_derivative_stirling_sum'_complex [derivative_intros]: assumes "j > 0" "Re x > 0" shows "(stirling_sum' j m has_field_derivative stirling_sum' (Suc j) m x) (at x)" proof (cases j) case (Suc j') from assms have [simp]: "x \ 0" by auto define c where "c = (\n. (-1) ^ Suc j * complex_of_real (bernoulli' n) * pochhammer (of_nat (Suc n)) j')" define T where "T = (\n x. c n * inverse x ^ (j + n))" define T' where "T' = (\n x. - (of_nat (j + n)) * c n * inverse x ^ (Suc (j + n)))" have "((\x. \k\m. T k x) has_field_derivative (\k\m. T' k x)) (at x)" using assms Suc by (intro DERIV_sum) (auto simp: T_def T'_def intro!: derivative_eq_intros simp: field_simps power_add [symmetric] simp del: of_nat_Suc power_Suc of_nat_add) also have "(\x. (\k\m. T k x)) = stirling_sum' j m" by (simp add: Suc T_def c_def stirling_sum'_def fun_eq_iff add_ac mult.assoc sum_distrib_left) also have "(\k\m. T' k x) = stirling_sum' (Suc j) m x" by (simp add: T'_def c_def Suc stirling_sum'_def sum_distrib_left sum_distrib_right algebra_simps pochhammer_Suc) finally show ?thesis . qed (insert assms, simp_all) lemma has_field_derivative_stirling_sum'_real [derivative_intros]: assumes "j > 0" "x > (0::real)" shows "(stirling_sum' j m has_field_derivative stirling_sum' (Suc j) m x) (at x)" proof (cases j) case (Suc j') from assms have [simp]: "x \ 0" by auto define c where "c = (\n. (-1) ^ Suc j * (bernoulli' n) * pochhammer (of_nat (Suc n)) j')" define T where "T = (\n x. c n * inverse x ^ (j + n))" define T' where "T' = (\n x. - (of_nat (j + n)) * c n * inverse x ^ (Suc (j + n)))" have "((\x. \k\m. T k x) has_field_derivative (\k\m. T' k x)) (at x)" using assms Suc by (intro DERIV_sum) (auto simp: T_def T'_def intro!: derivative_eq_intros simp: field_simps power_add [symmetric] simp del: of_nat_Suc power_Suc of_nat_add) also have "(\x. (\k\m. T k x)) = stirling_sum' j m" by (simp add: Suc T_def c_def stirling_sum'_def fun_eq_iff add_ac mult.assoc sum_distrib_left) also have "(\k\m. T' k x) = stirling_sum' (Suc j) m x" by (simp add: T'_def c_def Suc stirling_sum'_def sum_distrib_left sum_distrib_right algebra_simps pochhammer_Suc) finally show ?thesis . qed (insert assms, simp_all) lemma higher_deriv_stirling_sum_complex: "Re x > 0 \ (deriv ^^ i) (stirling_sum j m) x = stirling_sum (i + j) m x" proof (induction i arbitrary: x) case (Suc i) have "deriv ((deriv ^^ i) (stirling_sum j m)) x = deriv (stirling_sum (i + j) m) x" using eventually_nhds_in_open[of "{x. Re x > 0}" x] Suc.prems by (intro deriv_cong_ev refl) (auto elim!: eventually_mono simp: open_halfspace_Re_gt Suc.IH) also from Suc.prems have "\ = stirling_sum (Suc (i + j)) m x" by (intro DERIV_imp_deriv has_field_derivative_stirling_sum_complex) finally show ?case by simp qed simp_all definition Polygamma_approx :: "nat \ nat \ 'a \ 'a :: {real_normed_field, ln}" where "Polygamma_approx j m = (deriv ^^ j) (\x. (x - 1 / 2) * ln x - x + of_real (ln (2 * pi)) / 2 + stirling_sum 0 m x)" lemma Polygamma_approx_Suc: "Polygamma_approx (Suc j) m = deriv (Polygamma_approx j m)" by (simp add: Polygamma_approx_def) lemma Polygamma_approx_0: "Polygamma_approx 0 m x = (x - 1/2) * ln x - x + of_real (ln (2*pi)) / 2 + stirling_sum 0 m x" by (simp add: Polygamma_approx_def) lemma Polygamma_approx_1_complex: "Re x > 0 \ Polygamma_approx (Suc 0) m x = ln x - 1 / (2*x) + stirling_sum (Suc 0) m x" unfolding Polygamma_approx_Suc Polygamma_approx_0 by (intro DERIV_imp_deriv) (auto intro!: derivative_eq_intros elim!: nonpos_Reals_cases simp: field_simps) lemma Polygamma_approx_1_real: "x > (0 :: real) \ Polygamma_approx (Suc 0) m x = ln x - 1 / (2*x) + stirling_sum (Suc 0) m x" unfolding Polygamma_approx_Suc Polygamma_approx_0 by (intro DERIV_imp_deriv) (auto intro!: derivative_eq_intros elim!: nonpos_Reals_cases simp: field_simps) lemma stirling_sum_2_conv_stirling_sum'_1: fixes x :: "'a :: {real_div_algebra, field_char_0}" assumes "m > 0" "x \ 0" shows "stirling_sum' 1 m x = 1 / x + 1 / (2 * x^2) + stirling_sum 2 m x" proof - have pochhammer_2: "pochhammer (of_nat k) 2 = of_nat k * of_nat (Suc k)" for k by (simp add: pochhammer_Suc eval_nat_numeral add_ac) have "stirling_sum 2 m x = (\k = Suc 0.. = (\k=0.. = (\k=0.. = (\k\m. of_real (bernoulli' k) * inverse x ^ Suc k)" by (intro sum.cong) auto also have "\ = stirling_sum' 1 m x" by (simp add: stirling_sum'_def) finally show ?thesis by (simp add: add_ac) qed lemma Polygamma_approx_2_real: assumes "x > (0::real)" "m > 0" shows "Polygamma_approx (Suc (Suc 0)) m x = stirling_sum' 1 m x" proof - have "Polygamma_approx (Suc (Suc 0)) m x = deriv (Polygamma_approx (Suc 0) m) x" by (simp add: Polygamma_approx_Suc) also have "\ = deriv (\x. ln x - 1 / (2*x) + stirling_sum (Suc 0) m x) x" using eventually_nhds_in_open[of "{0<..}" x] assms by (intro deriv_cong_ev) (auto elim!: eventually_mono simp: Polygamma_approx_1_real) also have "\ = 1 / x + 1 / (2*x^2) + stirling_sum (Suc (Suc 0)) m x" using assms by (intro DERIV_imp_deriv) (auto intro!: derivative_eq_intros elim!: nonpos_Reals_cases simp: field_simps power2_eq_square) also have "\ = stirling_sum' 1 m x" using stirling_sum_2_conv_stirling_sum'_1[of m x] assms by (simp add: eval_nat_numeral) finally show ?thesis . qed lemma Polygamma_approx_2_complex: assumes "Re x > 0" "m > 0" shows "Polygamma_approx (Suc (Suc 0)) m x = stirling_sum' 1 m x" proof - have "Polygamma_approx (Suc (Suc 0)) m x = deriv (Polygamma_approx (Suc 0) m) x" by (simp add: Polygamma_approx_Suc) also have "\ = deriv (\x. ln x - 1 / (2*x) + stirling_sum (Suc 0) m x) x" using eventually_nhds_in_open[of "{s. Re s > 0}" x] assms by (intro deriv_cong_ev) (auto simp: open_halfspace_Re_gt elim!: eventually_mono simp: Polygamma_approx_1_complex) also have "\ = 1 / x + 1 / (2*x^2) + stirling_sum (Suc (Suc 0)) m x" using assms by (intro DERIV_imp_deriv) (auto intro!: derivative_eq_intros elim!: nonpos_Reals_cases simp: field_simps power2_eq_square) also have "\ = stirling_sum' 1 m x" using stirling_sum_2_conv_stirling_sum'_1[of m x] assms by (subst stirling_sum_2_conv_stirling_sum'_1) (auto simp: eval_nat_numeral) finally show ?thesis . qed lemma Polygamma_approx_ge_2_real: assumes "x > (0::real)" "m > 0" shows "Polygamma_approx (Suc (Suc j)) m x = stirling_sum' (Suc j) m x" using assms(1) proof (induction j arbitrary: x) case (0 x) with assms show ?case by (simp add: Polygamma_approx_2_real) next case (Suc j x) have "Polygamma_approx (Suc (Suc (Suc j))) m x = deriv (Polygamma_approx (Suc (Suc j)) m) x" by (simp add: Polygamma_approx_Suc) also have "\ = deriv (stirling_sum' (Suc j) m) x" using eventually_nhds_in_open[of "{0<..}" x] Suc.prems by (intro deriv_cong_ev refl) (auto elim!: eventually_mono simp: Suc.IH) also have "\ = stirling_sum' (Suc (Suc j)) m x" using Suc.prems by (intro DERIV_imp_deriv derivative_intros) simp_all finally show ?case . qed lemma Polygamma_approx_ge_2_complex: assumes "Re x > 0" "m > 0" shows "Polygamma_approx (Suc (Suc j)) m x = stirling_sum' (Suc j) m x" using assms(1) proof (induction j arbitrary: x) case (0 x) with assms show ?case by (simp add: Polygamma_approx_2_complex) next case (Suc j x) have "Polygamma_approx (Suc (Suc (Suc j))) m x = deriv (Polygamma_approx (Suc (Suc j)) m) x" by (simp add: Polygamma_approx_Suc) also have "\ = deriv (stirling_sum' (Suc j) m) x" using eventually_nhds_in_open[of "{x. Re x > 0}" x] Suc.prems by (intro deriv_cong_ev refl) (auto elim!: eventually_mono simp: Suc.IH open_halfspace_Re_gt) also have "\ = stirling_sum' (Suc (Suc j)) m x" using Suc.prems by (intro DERIV_imp_deriv derivative_intros) simp_all finally show ?case . qed lemma Polygamma_approx_complex_of_real: assumes "x > 0" "m > 0" shows "Polygamma_approx j m (complex_of_real x) = of_real (Polygamma_approx j m x)" proof (cases j) case 0 with assms show ?thesis by (simp add: Polygamma_approx_0 Ln_of_real stirling_sum_complex_of_real) next case [simp]: (Suc j') thus ?thesis proof (cases j') case 0 with assms show ?thesis by (simp add: Polygamma_approx_1_complex Polygamma_approx_1_real stirling_sum_complex_of_real Ln_of_real) next case (Suc j'') with assms show ?thesis by (simp add: Polygamma_approx_ge_2_complex Polygamma_approx_ge_2_real stirling_sum'_complex_of_real) qed qed lemma higher_deriv_Polygamma_approx [simp]: "(deriv ^^ j) (Polygamma_approx i m) = Polygamma_approx (j + i) m" by (simp add: Polygamma_approx_def funpow_add) lemma stirling_sum_holomorphic [holomorphic_intros]: "0 \ A \ stirling_sum j m holomorphic_on A" unfolding stirling_sum_def by (intro holomorphic_intros) auto lemma Polygamma_approx_holomorphic [holomorphic_intros]: "Polygamma_approx j m holomorphic_on {s. Re s > 0}" unfolding Polygamma_approx_def by (intro holomorphic_intros) (auto simp: open_halfspace_Re_gt elim!: nonpos_Reals_cases) lemma higher_deriv_lnGamma_stirling: assumes m: "m > 0" shows "(\x::real. (deriv ^^ j) ln_Gamma x - Polygamma_approx j m x) \ O(\x. 1 / x ^ (m + j))" proof - have "eventually (\x. \(deriv ^^ j) ln_Gamma x - Polygamma_approx j m x\ = inverse (real m) * \(deriv ^^ j) (stirling_integral m) x\) at_top" using eventually_gt_at_top[of "0::real"] proof eventually_elim case (elim x) note x = this have "(deriv ^^ j) (\x. ln_Gamma x - Polygamma_approx 0 m x) (complex_of_real x) = (deriv ^^ j) (\x. (-inverse (of_nat m)) * stirling_integral m x) (complex_of_real x)" using eventually_nhds_in_open[of "{s. Re s > 0}" x] x m by (intro higher_deriv_cong_ev refl) (auto elim!: eventually_mono simp: ln_Gamma_stirling_complex Polygamma_approx_def field_simps open_halfspace_Re_gt stirling_sum_def) also have "\ = - inverse (of_nat m) * (deriv ^^ j) (stirling_integral m) (of_real x)" using x m by (intro higher_deriv_cmult[of _ "{s. Re s > 0}"] stirling_integral_holomorphic) (auto simp: open_halfspace_Re_gt) also have "(deriv ^^ j) (\x. ln_Gamma x - Polygamma_approx 0 m x) (complex_of_real x) = (deriv ^^ j) ln_Gamma (of_real x) - (deriv ^^ j) (Polygamma_approx 0 m) (of_real x)" using x by (intro higher_deriv_diff[of _ "{s. Re s > 0}"]) (auto intro!: holomorphic_intros elim!: nonpos_Reals_cases simp: open_halfspace_Re_gt) also have "(deriv ^^ j) (Polygamma_approx 0 m) (complex_of_real x) = of_real (Polygamma_approx j m x)" using x m by (simp add: Polygamma_approx_complex_of_real) also have "norm (- inverse (of_nat m) * (deriv ^^ j) (stirling_integral m) (complex_of_real x)) = inverse (real m) * \(deriv ^^ j) (stirling_integral m) x\" using x m by (simp add: norm_mult norm_inverse deriv_stirling_integral_complex_of_real) also have "(deriv ^^ j) ln_Gamma (complex_of_real x) = of_real ((deriv ^^ j) ln_Gamma x)" using x by (simp add: higher_deriv_ln_Gamma_complex_of_real) also have "norm (\ - of_real (Polygamma_approx j m x)) = \(deriv ^^ j) ln_Gamma x - Polygamma_approx j m x\" by (simp only: of_real_diff [symmetric] norm_of_real) finally show ?case . qed from bigthetaI_cong[OF this] m have "(\x::real. (deriv ^^ j) ln_Gamma x - Polygamma_approx j m x) \ \(\x. (deriv ^^ j) (stirling_integral m) x)" by simp also have "(\x::real. (deriv ^^ j) (stirling_integral m) x) \ O(\x. 1 / x ^ (m + j))" using m by (rule deriv_stirling_integral_real_bound) finally show ?thesis . qed lemma Polygamma_approx_1_real': assumes x: "(x::real) > 0" and m: "m > 0" shows "Polygamma_approx 1 m x = ln x - (\k = Suc 0..m. bernoulli' k * inverse x ^ k / real k)" proof - have "Polygamma_approx 1 m x = ln x - (1 / (2 * x) + (\k=Suc 0..k=Suc 0.. = (\k=0.. = (\k = Suc 0..m. bernoulli' k * inverse x ^ k / real k)" using assms by (subst sum.shift_bounds_Suc_ivl [symmetric]) (simp add: atLeastLessThanSuc_atLeastAtMost) finally show ?thesis . qed theorem assumes m: "m > 0" shows ln_Gamma_real_asymptotics: "(\x. ln_Gamma x - ((x - 1 / 2) * ln x - x + ln (2 * pi) / 2 + (\k = 1.. O(\x. 1 / x ^ m)" (is ?th1) and Digamma_real_asymptotics: "(\x. Digamma x - (ln x - (\k=1..m. bernoulli' k / real k / x ^ k))) \ O(\x. 1 / (x ^ Suc m))" (is ?th2) and Polygamma_real_asymptotics: "j > 0 \ (\x. Polygamma j x - (- 1) ^ Suc j * (\k\m. bernoulli' k * pochhammer (real (Suc k)) (j - 1) / x ^ (k + j))) \ O(\x. 1 / x ^ (m+j+1))" (is "_ \ ?th3") proof - define G :: "nat \ real \ real" where "G = (\m. if m = 0 then ln_Gamma else Polygamma (m - 1))" have *: "(\x. G j x - h x) \ O(\x. 1 / x ^ (m + j))" if "\x::real. x > 0 \ Polygamma_approx j m x = h x" for j h proof - have "(\x. G j x - h x) \ \(\x. (deriv ^^ j) ln_Gamma x - Polygamma_approx j m x)" (is "_ \ \(?f)") using that by (intro bigthetaI_cong) (auto intro: eventually_mono[OF eventually_gt_at_top[of "0::real"]] simp del: funpow.simps simp: higher_deriv_ln_Gamma_real G_def) also have "?f \ O(\x::real. 1 / x ^ (m + j))" using m by (rule higher_deriv_lnGamma_stirling) finally show ?thesis . qed note [[simproc del: simplify_landau_sum]] from *[OF Polygamma_approx_0] assms show ?th1 by (simp add: G_def Polygamma_approx_0 stirling_sum_def field_simps) from *[OF Polygamma_approx_1_real'] assms show ?th2 by (simp add: G_def field_simps) assume j: "j > 0" from *[OF Polygamma_approx_ge_2_real, of "j - 1"] assms j show ?th3 by (simp add: G_def stirling_sum'_def power_add power_diff field_simps) qed end