(* Title: HOL/Analysis/Gamma_Function.thy Author: Manuel Eberl, TU München
*)
section \<open>The Gamma Function\<close>
theory Gamma_Function imports
Equivalence_Lebesgue_Henstock_Integration
Summation_Tests
Harmonic_Numbers "HOL-Library.Nonpos_Ints" "HOL-Library.Periodic_Fun" begin
text\<open>
Several equivalent definitions of the Gamma functionand its
most important properties. Alsocontains the definitionand some properties
of the log-Gamma functionand the Digamma functionand the other Polygamma functions.
Based on the Gamma function, we also prove the Weierstra{\ss} product form of the
sin functionand, based on this, the solution of the Basel problem (the
sum over all \<^term>\<open>1 / (n::nat)^2\<close>. \<close>
lemma pochhammer_eq_0_imp_nonpos_Int: "pochhammer (x::'a::field_char_0) n = 0 \ x \ \\<^sub>\\<^sub>0" by (auto simp: pochhammer_eq_0_iff)
lemma closed_nonpos_Ints [simp]: "closed (\\<^sub>\\<^sub>0 :: 'a :: real_normed_algebra_1 set)" proof - have"\\<^sub>\\<^sub>0 = (of_int ` {n. n \ 0} :: 'a set)" by (auto elim!: nonpos_Ints_cases intro!: nonpos_Ints_of_int) alsohave"closed \" by (rule closed_of_int_image) finallyshow ?thesis . qed
lemma sin_series: "(\n. ((-1)^n / fact (2*n+1)) *\<^sub>R z^(2*n+1)) sums sin z" proof - from sin_converges[of z] have"(\n. sin_coeff n *\<^sub>R z^n) sums sin z" . alsohave"(\n. sin_coeff n *\<^sub>R z^n) sums sin z \
(\<lambda>n. ((-1)^n / fact (2*n+1)) *\<^sub>R z^(2*n+1)) sums sin z" by (subst sums_mono_reindex[of "\n. 2*n+1", symmetric])
(auto simp: sin_coeff_def strict_mono_def ac_simps elim!: oddE) finallyshow ?thesis . qed
lemma cos_series: "(\n. ((-1)^n / fact (2*n)) *\<^sub>R z^(2*n)) sums cos z" proof - from cos_converges[of z] have"(\n. cos_coeff n *\<^sub>R z^n) sums cos z" . alsohave"(\n. cos_coeff n *\<^sub>R z^n) sums cos z \
(\<lambda>n. ((-1)^n / fact (2*n)) *\<^sub>R z^(2*n)) sums cos z" by (subst sums_mono_reindex[of "\n. 2*n", symmetric])
(auto simp: cos_coeff_def strict_mono_def ac_simps elim!: evenE) finallyshow ?thesis . qed
lemma sin_z_over_z_series: fixes z :: "'a :: {real_normed_field,banach}" assumes"z \ 0" shows"(\n. (-1)^n / fact (2*n+1) * z^(2*n)) sums (sin z / z)" proof - from sin_series[of z] have"(\n. z * ((-1)^n / fact (2*n+1)) * z^(2*n)) sums sin z" by (simp add: field_simps scaleR_conv_of_real) from sums_mult[OF this, of "inverse z"] and assms show ?thesis by (simp add: field_simps) qed
lemma sin_z_over_z_series': fixes z :: "'a :: {real_normed_field,banach}" assumes"z \ 0" shows"(\n. sin_coeff (n+1) *\<^sub>R z^n) sums (sin z / z)" proof - from sums_split_initial_segment[OF sin_converges[of z], of 1] have"(\n. z * (sin_coeff (n+1) *\<^sub>R z ^ n)) sums sin z" by simp from sums_mult[OF this, of "inverse z"] assms show ?thesis by (simp add: field_simps) qed
lemma has_field_derivative_sin_z_over_z: fixes A :: "'a :: {real_normed_field,banach} set" shows"((\z. if z = 0 then 1 else sin z / z) has_field_derivative 0) (at 0 within A)"
(is"(?f has_field_derivative ?f') _") proof (rule has_field_derivative_at_within) have"((\z::'a. \n. of_real (sin_coeff (n+1)) * z^n)
has_field_derivative (\<Sum>n. diffs (\<lambda>n. of_real (sin_coeff (n+1))) n * 0^n)) (at 0)" proof (rule termdiffs_strong) from summable_ignore_initial_segment[OF sums_summable[OF sin_converges[of "1::'a"]], of 1] show"summable (\n. of_real (sin_coeff (n+1)) * (1::'a)^n)" by (simp add: of_real_def) qed simp alsohave"(\z::'a. \n. of_real (sin_coeff (n+1)) * z^n) = ?f" proof fix z show"(\n. of_real (sin_coeff (n+1)) * z^n) = ?f z" by (cases "z = 0") (insert sin_z_over_z_series'[of z],
simp_all add: scaleR_conv_of_real sums_iff sin_coeff_def) qed alsohave"(\n. diffs (\n. of_real (sin_coeff (n + 1))) n * (0::'a) ^ n) =
diffs (\<lambda>n. of_real (sin_coeff (Suc n))) 0" by simp alsohave"\ = 0" by (simp add: sin_coeff_def diffs_def) finallyshow"((\z::'a. if z = 0 then 1 else sin z / z) has_field_derivative 0) (at 0)" . qed
lemma round_Re_minimises_norm: "norm ((z::complex) - of_int m) \ norm (z - of_int (round (Re z)))" proof - let ?n = "round (Re z)" have"norm (z - of_int ?n) = sqrt ((Re z - of_int ?n)\<^sup>2 + (Im z)\<^sup>2)" by (simp add: cmod_def) alsohave"\Re z - of_int ?n\ \ \Re z - of_int m\" by (rule round_diff_minimal) hence"sqrt ((Re z - of_int ?n)\<^sup>2 + (Im z)\<^sup>2) \ sqrt ((Re z - of_int m)\<^sup>2 + (Im z)\<^sup>2)" by (intro real_sqrt_le_mono add_mono) (simp_all add: abs_le_square_iff) alsohave"\ = norm (z - of_int m)" by (simp add: cmod_def) finallyshow ?thesis . qed
lemma Re_pos_in_ball: assumes"Re z > 0""t \ ball z (Re z/2)" shows"Re t > 0" proof - have"Re (z - t) \ norm (z - t)" by (rule complex_Re_le_cmod) alsofrom assms have"\ < Re z / 2" by (simp add: dist_complex_def) finallyshow"Re t > 0"using assms by simp qed
lemma no_nonpos_Int_in_ball_complex: assumes"Re z > 0""t \ ball z (Re z/2)" shows"t \ \\<^sub>\\<^sub>0" using Re_pos_in_ball[OF assms] by (force elim!: nonpos_Ints_cases)
lemma no_nonpos_Int_in_ball: assumes"t \ ball z (dist z (round (Re z)))" shows"t \ \\<^sub>\\<^sub>0" proof assume"t \ \\<^sub>\\<^sub>0" thenobtain n where"t = of_int n"by (auto elim!: nonpos_Ints_cases) have"dist z (of_int n) \ dist z t + dist t (of_int n)" by (rule dist_triangle) alsofrom assms have"dist z t < dist z (round (Re z))"by simp alsohave"\ \ dist z (of_int n)" using round_Re_minimises_norm[of z] by (simp add: dist_complex_def) finallyhave"dist t (of_int n) > 0"by simp with\<open>t = of_int n\<close> show False by simp qed
lemma no_nonpos_Int_in_ball': assumes"(z :: 'a :: {euclidean_space,real_normed_algebra_1}) \ \\<^sub>\\<^sub>0" obtains d where"d > 0""\t. t \ ball z d \ t \ \\<^sub>\\<^sub>0" proof (rule that) from assms show"setdist {z} \\<^sub>\\<^sub>0 > 0" by (subst setdist_gt_0_compact_closed) auto next fix t assume"t \ ball z (setdist {z} \\<^sub>\\<^sub>0)" thus"t \ \\<^sub>\\<^sub>0" using setdist_le_dist[of z "{z}" t "\\<^sub>\\<^sub>0"] by force qed
lemma no_nonpos_Real_in_ball: assumes z: "z \ \\<^sub>\\<^sub>0" and t: "t \ ball z (if Im z = 0 then Re z / 2 else abs (Im z) / 2)" shows"t \ \\<^sub>\\<^sub>0" using z proof (cases "Im z = 0") assume A: "Im z = 0" with z have"Re z > 0"by (force simp add: complex_nonpos_Reals_iff) with t A Re_pos_in_ball[of z t] show ?thesis by (force simp add: complex_nonpos_Reals_iff) next assume A: "Im z \ 0" have"abs (Im z) - abs (Im t) \ abs (Im z - Im t)" by linarith alsohave"\ = abs (Im (z - t))" by simp alsohave"\ \ norm (z - t)" by (rule abs_Im_le_cmod) alsofrom A t have"\ \ abs (Im z) / 2" by (simp add: dist_complex_def) finallyhave"abs (Im t) > 0"using A by simp thus ?thesis by (force simp add: complex_nonpos_Reals_iff) qed
subsection \<open>The Euler form and the logarithmic Gamma function\<close>
text\<open>
We define the Gamma functionby first defining its multiplicative inverse \<open>rGamma\<close>.
This is more convenient because \<open>rGamma\<close> is entire, which makes proofs of its
properties more convenient because one does not haveto watch out for discontinuities.
(e.g. \<open>rGamma\<close> fulfils \<open>rGamma z = z * rGamma (z + 1)\<close> everywhere, whereas the \<open>\<Gamma>\<close> function
does not fulfil the analogous equation on the non-positive integers)
We define the \<open>\<Gamma>\<close> function (resp.\ its reciprocale) in the Euler form. This form has the advantage
that it is a relatively simple limit that converges everywhere. The limit at the poles is 0
(due to division by 0). The functional equation \<open>Gamma (z + 1) = z * Gamma z\<close> follows
immediately from the definition. \<close>
definition\<^marker>\<open>tag important\<close> Gamma_series :: "('a :: {banach,real_normed_field}) \<Rightarrow> nat \<Rightarrow> 'a" where "Gamma_series z n = fact n * exp (z * of_real (ln (of_nat n))) / pochhammer z (n+1)"
definition Gamma_series' :: "('a :: {banach,real_normed_field}) \<Rightarrow> nat \<Rightarrow> 'a" where "Gamma_series' z n = fact (n - 1) * exp (z * of_real (ln (of_nat n))) / pochhammer z n"
definition rGamma_series :: "('a :: {banach,real_normed_field}) \ nat \ 'a" where "rGamma_series z n = pochhammer z (n+1) / (fact n * exp (z * of_real (ln (of_nat n))))"
lemma Gamma_series_altdef: "Gamma_series z n = inverse (rGamma_series z n)" and rGamma_series_altdef: "rGamma_series z n = inverse (Gamma_series z n)" unfolding Gamma_series_def rGamma_series_def by simp_all
lemma rGamma_series_minus_of_nat: "eventually (\n. rGamma_series (- of_nat k) n = 0) sequentially" using eventually_ge_at_top[of k] by eventually_elim (auto simp: rGamma_series_def pochhammer_of_nat_eq_0_iff)
lemma Gamma_series_minus_of_nat: "eventually (\n. Gamma_series (- of_nat k) n = 0) sequentially" using eventually_ge_at_top[of k] by eventually_elim (auto simp: Gamma_series_def pochhammer_of_nat_eq_0_iff)
lemma Gamma_series'_minus_of_nat: "eventually (\n. Gamma_series' (- of_nat k) n = 0) sequentially" using eventually_gt_at_top[of k] by eventually_elim (auto simp: Gamma_series'_def pochhammer_of_nat_eq_0_iff)
lemma rGamma_series_nonpos_Ints_LIMSEQ: "z \ \\<^sub>\\<^sub>0 \ rGamma_series z \ 0" by (elim nonpos_Ints_cases', hypsubst, subst tendsto_cong, rule rGamma_series_minus_of_nat, simp)
lemma Gamma_series_nonpos_Ints_LIMSEQ: "z \ \\<^sub>\\<^sub>0 \ Gamma_series z \ 0" by (elim nonpos_Ints_cases', hypsubst, subst tendsto_cong, rule Gamma_series_minus_of_nat, simp)
lemma Gamma_series'_nonpos_Ints_LIMSEQ: "z \ \\<^sub>\\<^sub>0 \ Gamma_series' z \ 0" by (elim nonpos_Ints_cases', hypsubst, subst tendsto_cong, rule Gamma_series'_minus_of_nat, simp)
lemma Gamma_series_Gamma_series': assumes z: "z \ \\<^sub>\\<^sub>0" shows"(\n. Gamma_series' z n / Gamma_series z n) \ 1" proof (rule Lim_transform_eventually) from eventually_gt_at_top[of "0::nat"] show"eventually (\n. z / of_nat n + 1 = Gamma_series' z n / Gamma_series z n) sequentially" proof eventually_elim fix n :: nat assume n: "n > 0" from n z have"Gamma_series' z n / Gamma_series z n = (z + of_nat n) / of_nat n" by (cases n, simp)
(auto simp add: Gamma_series_def Gamma_series'_def pochhammer_rec'
dest: pochhammer_eq_0_imp_nonpos_Int plus_of_nat_eq_0_imp) alsofrom n have"\ = z / of_nat n + 1" by (simp add: field_split_simps) finallyshow"z / of_nat n + 1 = Gamma_series' z n / Gamma_series z n" .. qed have"(\x. z / of_nat x) \ 0" by (rule tendsto_norm_zero_cancel)
(insert tendsto_mult[OF tendsto_const[of "norm z"] lim_inverse_n],
simp add: norm_divide inverse_eq_divide) from tendsto_add[OF this tendsto_const[of 1]] show"(\n. z / of_nat n + 1) \ 1" by simp qed
text\<open>
We now show that the series that defines the \<open>\<Gamma>\<close> function in the Euler form converges and that the function defined by it is continuous on the complex halfspace with positive
real part.
We do this by showing that the logarithm of the Euler series is continuous and converges
locally uniformly, which means that the log-Gamma function defined by its limit isalso
continuous.
This will later allow us to lift holomorphicity and continuity from the log-Gamma functionto the inverse of the Gamma function, andfrom that to the Gamma function itself. \<close>
definition\<^marker>\<open>tag important\<close> ln_Gamma_series :: "('a :: {banach,real_normed_field,ln}) \<Rightarrow> nat \<Rightarrow> 'a" where "ln_Gamma_series z n = z * ln (of_nat n) - ln z - (\k=1..n. ln (z / of_nat k + 1))"
definition\<^marker>\<open>tag unimportant\<close> ln_Gamma_series' :: "('a :: {banach,real_normed_field,ln}) \<Rightarrow> nat \<Rightarrow> 'a" where "ln_Gamma_series' z n =
- euler_mascheroni*z - ln z + (\<Sum>k=1..n. z / of_nat n - ln (z / of_nat k + 1))"
definition ln_Gamma :: "('a :: {banach,real_normed_field,ln}) \ 'a" where "ln_Gamma z = lim (ln_Gamma_series z)"
text\<open>
We now show that the log-Gamma series converges locally uniformly for all complex numbers except
the non-positive integers. We do this by proving that the series is locally Cauchy. \<close>
context begin
private lemma ln_Gamma_series_complex_converges_aux: fixes z :: complex and k :: nat assumes z: "z \ 0" and k: "of_nat k \ 2*norm z" "k \ 2" shows"norm (z * ln (1 - 1/of_nat k) + ln (z/of_nat k + 1)) \ 2*(norm z + norm z^2) / of_nat k^2" proof - let ?k = "of_nat k :: complex"and ?z = "norm z" have"z *ln (1 - 1/?k) + ln (z/?k+1) = z*(ln (1 - 1/?k :: complex) + 1/?k) + (ln (1+z/?k) - z/?k)" by (simp add: algebra_simps) alsohave"norm ... \ ?z * norm (ln (1-1/?k) + 1/?k :: complex) + norm (ln (1+z/?k) - z/?k)" by (subst norm_mult [symmetric], rule norm_triangle_ineq) alsohave"norm (Ln (1 + -1/?k) - (-1/?k)) \ (norm (-1/?k))\<^sup>2 / (1 - norm(-1/?k))" using k by (intro Ln_approx_linear) (simp add: norm_divide) hence"?z * norm (ln (1-1/?k) + 1/?k) \ ?z * ((norm (1/?k))^2 / (1 - norm (1/?k)))" by (intro mult_left_mono) simp_all alsohave"... \ (?z * (of_nat k / (of_nat k - 1))) / of_nat k^2" using k by (simp add: field_simps power2_eq_square norm_divide) alsohave"... \ (?z * 2) / of_nat k^2" using k by (intro divide_right_mono mult_left_mono) (simp_all add: field_simps) alsohave"norm (ln (1+z/?k) - z/?k) \ norm (z/?k)^2 / (1 - norm (z/?k))" using k by (intro Ln_approx_linear) (simp add: norm_divide) hence"norm (ln (1+z/?k) - z/?k) \ ?z^2 / of_nat k^2 / (1 - ?z / of_nat k)" by (simp add: field_simps norm_divide) alsohave"... \ (?z^2 * (of_nat k / (of_nat k - ?z))) / of_nat k^2" using k by (simp add: field_simps power2_eq_square) alsohave"... \ (?z^2 * 2) / of_nat k^2" using k by (intro divide_right_mono mult_left_mono) (simp_all add: field_simps) alsonote add_divide_distrib [symmetric] finallyshow ?thesis by (simp only: distrib_left mult.commute) qed
lemma ln_Gamma_series_complex_converges: assumes z: "z \ \\<^sub>\\<^sub>0" assumes d: "d > 0""\n. n \ \\<^sub>\\<^sub>0 \ norm (z - of_int n) > d" shows"uniformly_convergent_on (ball z d) (\n z. ln_Gamma_series z n :: complex)" proof (intro Cauchy_uniformly_convergent uniformly_Cauchy_onI') fix e :: real assume e: "e > 0"
define e''where"e'' = (SUP t\ball z d. norm t + norm t^2)"
define e' where "e' = e / (2*e'')" have"bounded ((\t. norm t + norm t^2) ` cball z d)" by (intro compact_imp_bounded compact_continuous_image) (auto intro!: continuous_intros) hence"bounded ((\t. norm t + norm t^2) ` ball z d)" by (rule bounded_subset) auto hence bdd: "bdd_above ((\t. norm t + norm t^2) ` ball z d)" by (rule bounded_imp_bdd_above)
with z d(1) d(2)[of "-1"] have e''_pos: "e'' > 0"unfolding e''_def by (subst less_cSUP_iff) (auto intro!: add_pos_nonneg bexI[of _ z]) have e'': "norm t + norm t^2 \ e''" if "t \ ball z d" for t unfolding e''_def using that by (rule cSUP_upper[OF _ bdd]) from e z e''_pos have e': "e' > 0" unfolding e'_def by (intro divide_pos_pos mult_pos_pos add_pos_pos) (simp_all add: field_simps)
have"summable (\k. inverse ((real_of_nat k)^2))" by (rule inverse_power_summable) simp from summable_partial_sum_bound[OF this e'] obtain M where M: "\m n. M \ m \ norm (\k = m..n. inverse ((real k)\<^sup>2)) < e'" by auto
define N where"N = max 2 (max (nat \2 * (norm z + d)\) M)"
{ from d have"\2 * (cmod z + d)\ \ \0::real\" by (intro ceiling_mono mult_nonneg_nonneg add_nonneg_nonneg) simp_all hence"2 * (norm z + d) \ of_nat (nat \2 * (norm z + d)\)" unfolding N_def by (simp_all) alsohave"... \ of_nat N" unfolding N_def by (subst of_nat_le_iff) (rule max.coboundedI2, rule max.cobounded1) finallyhave"of_nat N \ 2 * (norm z + d)" . moreoverhave"N \ 2" "N \ M" unfolding N_def by simp_all moreoverhave"(\k=m..n. 1/(of_nat k)\<^sup>2) < e'" if "m \ N" for m n using M[OF order.trans[OF \<open>N \<ge> M\<close> that]] unfolding real_norm_def by (subst (asm) abs_of_nonneg) (auto intro: sum_nonneg simp: field_split_simps) moreovernote calculation
} note N = this
show"\M. \t\ball z d. \m\M. \n>m. dist (ln_Gamma_series t m) (ln_Gamma_series t n) < e" unfolding dist_complex_def proof (intro exI[of _ N] ballI allI impI) fix t m n assume t: "t \ ball z d" and mn: "m \ N" "n > m" from d(2)[of 0] t have"0 < dist z 0 - dist z t"by (simp add: field_simps dist_complex_def) alsohave"dist z 0 - dist z t \ dist 0 t" using dist_triangle[of 0 z t] by (simp add: dist_commute) finallyhave t_nz: "t \ 0" by auto
have"norm t \ norm z + norm (t - z)" by (rule norm_triangle_sub) alsofrom t have"norm (t - z) < d"by (simp add: dist_complex_def norm_minus_commute) alsohave"2 * (norm z + d) \ of_nat N" by (rule N) alsohave"N \ m" by (rule mn) finallyhave norm_t: "2 * norm t < of_nat m"by simp
have"ln_Gamma_series t m - ln_Gamma_series t n =
(-(t * Ln (of_nat n)) - (-(t * Ln (of_nat m)))) +
((\<Sum>k=1..n. Ln (t / of_nat k + 1)) - (\<Sum>k=1..m. Ln (t / of_nat k + 1)))" by (simp add: ln_Gamma_series_def algebra_simps) alsohave"(\k=1..n. Ln (t / of_nat k + 1)) - (\k=1..m. Ln (t / of_nat k + 1)) =
(\<Sum>k\<in>{1..n}-{1..m}. Ln (t / of_nat k + 1))" using mn by (simp add: sum_diff) alsofrom mn have"{1..n}-{1..m} = {Suc m..n}"by fastforce alsohave"-(t * Ln (of_nat n)) - (-(t * Ln (of_nat m))) =
(\<Sum>k = Suc m..n. t * Ln (of_nat (k - 1)) - t * Ln (of_nat k))" using mn by (subst sum_telescope'' [symmetric]) simp_all alsohave"... = (\k = Suc m..n. t * Ln (of_nat (k - 1) / of_nat k))" using mn N by (intro sum_cong_Suc)
(simp_all del: of_nat_Suc add: field_simps Ln_of_nat Ln_of_nat_over_of_nat) alsohave"of_nat (k - 1) / of_nat k = 1 - 1 / (of_nat k :: complex)"if"k \ {Suc m..n}" for k using that of_nat_eq_0_iff[of "Suc i"for i] by (cases k) (simp_all add: field_split_simps) hence"(\k = Suc m..n. t * Ln (of_nat (k - 1) / of_nat k)) =
(\<Sum>k = Suc m..n. t * Ln (1 - 1 / of_nat k))" using mn N by (intro sum.cong) simp_all alsonote sum.distrib [symmetric] alsohave"norm (\k=Suc m..n. t * Ln (1 - 1/of_nat k) + Ln (t/of_nat k + 1)) \
(\<Sum>k=Suc m..n. 2 * (norm t + (norm t)\<^sup>2) / (real_of_nat k)\<^sup>2)" using t_nz N(2) mn norm_t by (intro order.trans[OF norm_sum sum_mono[OF ln_Gamma_series_complex_converges_aux]]) simp_all alsohave"... \ 2 * (norm t + norm t^2) * (\k=Suc m..n. 1 / (of_nat k)\<^sup>2)" by (simp add: sum_distrib_left) alsohave"... < 2 * (norm t + norm t^2) * e'"using mn z t_nz by (intro mult_strict_left_mono N mult_pos_pos add_pos_pos) simp_all alsofrom e''_pos have"... = e * ((cmod t + (cmod t)\<^sup>2) / e'')" by (simp add: e'_def field_simps power2_eq_square) alsofrom e''[OF t] e''_pos e have"\ \ e * 1" by (intro mult_left_mono) (simp_all add: field_simps) finallyshow"norm (ln_Gamma_series t m - ln_Gamma_series t n) < e"by simp qed qed
end
lemma ln_Gamma_series_complex_converges': assumes z: "(z :: complex) \ \\<^sub>\\<^sub>0" shows"\d>0. uniformly_convergent_on (ball z d) (\n z. ln_Gamma_series z n)" proof -
define d' where "d' = Re z"
define d where"d = (if d' > 0 then d' / 2 else norm (z - of_int (round d')) / 2)" have"of_int (round d') \ \\<^sub>\\<^sub>0" if "d' \ 0" using that by (intro nonpos_Ints_of_int) (simp_all add: round_def) with assms have d_pos: "d > 0"unfolding d_def by (force simp: not_less)
have"d < cmod (z - of_int n)"if"n \ \\<^sub>\\<^sub>0" for n proof (cases "Re z > 0") case True from nonpos_Ints_nonpos[OF that] have n: "n \ 0" by simp from True have"d = Re z/2"by (simp add: d_def d'_def) alsofrom n True have"\ < Re (z - of_int n)" by simp alsohave"\ \ norm (z - of_int n)" by (rule complex_Re_le_cmod) finallyshow ?thesis . next case False with assms nonpos_Ints_of_int[of "round (Re z)"] have"z \ of_int (round d')" by (auto simp: not_less) with False have"d < norm (z - of_int (round d'))"by (simp add: d_def d'_def) alsohave"\ \ norm (z - of_int n)" unfolding d'_def by (rule round_Re_minimises_norm) finallyshow ?thesis . qed hence conv: "uniformly_convergent_on (ball z d) (\n z. ln_Gamma_series z n)" by (intro ln_Gamma_series_complex_converges d_pos z) simp_all from d_pos conv show ?thesis by blast qed
theorem ln_Gamma_complex_LIMSEQ: "(z :: complex) \ \\<^sub>\\<^sub>0 \ ln_Gamma_series z \ ln_Gamma z" using ln_Gamma_series_complex_converges''by (simp add: convergent_LIMSEQ_iff ln_Gamma_def)
lemma exp_ln_Gamma_series_complex: assumes"n > 0""z \ \\<^sub>\\<^sub>0" shows"exp (ln_Gamma_series z n :: complex) = Gamma_series z n" proof - from assms obtain m where m: "n = Suc m"by (cases n) blast from assms have"z \ 0" by (intro notI) auto with assms have"exp (ln_Gamma_series z n) =
(of_nat n) powr z / (z * (\<Prod>k=1..n. exp (Ln (z / of_nat k + 1))))" unfolding ln_Gamma_series_def powr_def by (simp add: exp_diff exp_sum) alsofrom assms have"(\k=1..n. exp (Ln (z / of_nat k + 1))) = (\k=1..n. z / of_nat k + 1)" by (intro prod.cong[OF refl], subst exp_Ln) (auto simp: field_simps plus_of_nat_eq_0_imp) alsohave"... = (\k=1..n. z + k) / fact n" by (simp add: fact_prod)
(subst prod_dividef [symmetric], simp_all add: field_simps) alsofrom m have"z * ... = (\k=0..n. z + k) / fact n" by (simp add: prod.atLeast0_atMost_Suc_shift prod.atLeast_Suc_atMost_Suc_shift del: prod.cl_ivl_Suc) alsohave"(\k=0..n. z + k) = pochhammer z (Suc n)" unfolding pochhammer_prod by (simp add: prod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost) alsohave"of_nat n powr z / (pochhammer z (Suc n) / fact n) = Gamma_series z n" unfolding Gamma_series_def using assms by (simp add: field_split_simps powr_def) finallyshow ?thesis . qed
lemma ln_Gamma_series'_aux: assumes"(z::complex) \ \\<^sub>\\<^sub>0" shows"(\k. z / of_nat (Suc k) - ln (1 + z / of_nat (Suc k))) sums
(ln_Gamma z + euler_mascheroni * z + ln z)" (is "?f sums ?s") unfolding sums_def proof (rule Lim_transform) show"(\n. ln_Gamma_series z n + of_real (harm n - ln (of_nat n)) * z + ln z) \ ?s"
(is"?g \ _") by (intro tendsto_intros ln_Gamma_complex_LIMSEQ euler_mascheroni_LIMSEQ_of_real assms)
have A: "eventually (\n. (\k using eventually_gt_at_top[of "0::nat"] proof eventually_elim fix n :: nat assume n: "n > 0" have"(\kk=1..n. z / of_nat k - ln (1 + z / of_nat k))" by (subst atLeast0LessThan [symmetric], subst sum.shift_bounds_Suc_ivl [symmetric],
subst atLeastLessThanSuc_atLeastAtMost) simp_all alsohave"\ = z * of_real (harm n) - (\k=1..n. ln (1 + z / of_nat k))" by (simp add: harm_def sum_subtractf sum_distrib_left divide_inverse) alsofrom n have"\ - ?g n = 0" by (simp add: ln_Gamma_series_def sum_subtractf algebra_simps) finallyshow"(\k qed show"(\n. (\k 0" by (subst tendsto_cong[OF A]) simp_all qed
lemma uniformly_summable_deriv_ln_Gamma: assumes z: "(z :: 'a :: {real_normed_field,banach}) \ 0" and d: "d > 0" "d \ norm z/2" shows"uniformly_convergent_on (ball z d)
(\<lambda>k z. \<Sum>i<k. inverse (of_nat (Suc i)) - inverse (z + of_nat (Suc i)))"
(is"uniformly_convergent_on _ (\k z. \i proof (rule Weierstrass_m_test'_ev)
{ fix t assume t: "t \ ball z d" have"norm z = norm (t + (z - t))"by simp have"norm (t + (z - t)) \ norm t + norm (z - t)" by (rule norm_triangle_ineq) alsofrom t d have"norm (z - t) < norm z / 2"by (simp add: dist_norm) finallyhave A: "norm t > norm z / 2"using z by (simp add: field_simps)
have"norm t = norm (z + (t - z))"by simp alsohave"\ \ norm z + norm (t - z)" by (rule norm_triangle_ineq) alsofrom t d have"norm (t - z) \ norm z / 2" by (simp add: dist_norm norm_minus_commute) alsofrom z have"\ < norm z" by simp finallyhave B: "norm t < 2 * norm z"by simp note A B
} note ball = this
show"eventually (\n. \t\ball z d. norm (?f n t) \ 4 * norm z * inverse (of_nat (Suc n)^2)) sequentially" using eventually_gt_at_top apply eventually_elim proof safe fix t :: 'a assume t: "t \ ball z d" from z ball[OF t] have t_nz: "t \ 0" by auto fix n :: nat assume n: "n > nat \4 * norm z\" from ball[OF t] t_nz have"4 * norm z > 2 * norm t"by simp alsofrom n have"\ < of_nat n" by linarith finallyhave n: "of_nat n > 2 * norm t" . hence"of_nat n > norm t"by simp hence t': "t \ -of_nat (Suc n)" by (intro notI) (simp del: of_nat_Suc)
with t_nz have"?f n t = 1 / (of_nat (Suc n) * (1 + of_nat (Suc n)/t))" by (simp add: field_split_simps eq_neg_iff_add_eq_0 del: of_nat_Suc) alsohave"norm \ = inverse (of_nat (Suc n)) * inverse (norm (of_nat (Suc n)/t + 1))" by (simp add: norm_divide norm_mult field_split_simps del: of_nat_Suc) also { from z t_nz ball[OF t] have"of_nat (Suc n) / (4 * norm z) \ of_nat (Suc n) / (2 * norm t)" by (intro divide_left_mono mult_pos_pos) simp_all alsohave"\ < norm (of_nat (Suc n) / t) - norm (1 :: 'a)" using t_nz n by (simp add: field_simps norm_divide del: of_nat_Suc) alsohave"\ \ norm (of_nat (Suc n)/t + 1)" by (rule norm_diff_ineq) finallyhave"inverse (norm (of_nat (Suc n)/t + 1)) \ 4 * norm z / of_nat (Suc n)" using z by (simp add: field_split_simps norm_divide mult_ac del: of_nat_Suc)
} alsohave"inverse (real_of_nat (Suc n)) * (4 * norm z / real_of_nat (Suc n)) =
4 * norm z * inverse (of_nat (Suc n)^2)" by (simp add: field_split_simps power2_eq_square del: of_nat_Suc) finallyshow"norm (?f n t) \ 4 * norm z * inverse (of_nat (Suc n)^2)" by (simp del: of_nat_Suc) qed next show"summable (\n. 4 * norm z * inverse ((of_nat (Suc n))^2))" by (subst summable_Suc_iff) (simp add: summable_mult inverse_power_summable) qed
subsection \<open>The Polygamma functions\<close>
lemma summable_deriv_ln_Gamma: "z \ (0 :: 'a :: {real_normed_field,banach}) \
summable (\<lambda>n. inverse (of_nat (Suc n)) - inverse (z + of_nat (Suc n)))" unfolding summable_iff_convergent by (rule uniformly_convergent_imp_convergent,
rule uniformly_summable_deriv_ln_Gamma[of z "norm z/2"]) simp_all
definition\<^marker>\<open>tag important\<close> Polygamma :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a" where "Polygamma n z = (if n = 0 then
(\<Sum>k. inverse (of_nat (Suc k)) - inverse (z + of_nat k)) - euler_mascheroni else
(-1)^Suc n * fact n * (\<Sum>k. inverse ((z + of_nat k)^Suc n)))"
lemma Digamma_def: "Digamma z = (\k. inverse (of_nat (Suc k)) - inverse (z + of_nat k)) - euler_mascheroni" by (simp add: Polygamma_def)
lemma summable_Digamma: assumes"(z :: 'a :: {real_normed_field,banach}) \ 0" shows"summable (\n. inverse (of_nat (Suc n)) - inverse (z + of_nat n))" proof - have sums: "(\n. inverse (z + of_nat (Suc n)) - inverse (z + of_nat n)) sums
(0 - inverse (z + of_nat 0))" by (intro telescope_sums filterlim_compose[OF tendsto_inverse_0]
tendsto_add_filterlim_at_infinity[OF tendsto_const] tendsto_of_nat) from summable_add[OF summable_deriv_ln_Gamma[OF assms] sums_summable[OF sums]] show"summable (\n. inverse (of_nat (Suc n)) - inverse (z + of_nat n))" by simp qed
lemma summable_offset: assumes"summable (\n. f (n + k) :: 'a :: real_normed_vector)" shows"summable f" proof - from assms have"convergent (\m. \n using summable_iff_convergent by blast hence"convergent (\m. (\nn by (intro convergent_add convergent_const) alsohave"(\m. (\nnm. \n proof fix m :: nat have"{.. {k.. alsohave"(\n\\. f n) = (\nn=k.. by (rule sum.union_disjoint) auto alsohave"(\n=k..n=0.. using sum.shift_bounds_nat_ivl [of f 0 k m] by simp finallyshow"(\nnn qed finallyhave"(\a. sum f {.. lim (\m. sum f {.. by (auto simp: convergent_LIMSEQ_iff dest: LIMSEQ_offset) thus ?thesis by (auto simp: summable_iff_convergent convergent_def) qed
lemma Polygamma_converges: fixes z :: "'a :: {real_normed_field,banach}" assumes z: "z \ 0" and n: "n \ 2" shows"uniformly_convergent_on (ball z d) (\k z. \i proof (rule Weierstrass_m_test'_ev)
define e where"e = (1 + d / norm z)"
define m where"m = nat \norm z * e\"
{ fix t assume t: "t \ ball z d" have"norm t = norm (z + (t - z))"by simp alsohave"\ \ norm z + norm (t - z)" by (rule norm_triangle_ineq) alsofrom t have"norm (t - z) < d"by (simp add: dist_norm norm_minus_commute) finallyhave"norm t < norm z * e"using z by (simp add: divide_simps e_def)
} note ball = this
show"eventually (\k. \t\ball z d. norm (inverse ((t + of_nat k)^n)) \
inverse (of_nat (k - m)^n)) sequentially" using eventually_gt_at_top[of m] apply eventually_elim proof (intro ballI) fix k :: nat and t :: 'a assume k: "k > m" and t: "t \ ball z d" from k have"real_of_nat (k - m) = of_nat k - of_nat m"by (simp add: of_nat_diff) alsohave"\ \ norm (of_nat k :: 'a) - norm z * e" unfolding m_def by (subst norm_of_nat) linarith alsofrom ball[OF t] have"\ \ norm (of_nat k :: 'a) - norm t" by simp alsohave"\ \ norm (of_nat k + t)" by (rule norm_diff_ineq) finallyhave"inverse ((norm (t + of_nat k))^n) \ inverse (real_of_nat (k - m)^n)" using k n by (intro le_imp_inverse_le power_mono) (simp_all add: add_ac del: of_nat_Suc) thus"norm (inverse ((t + of_nat k)^n)) \ inverse (of_nat (k - m)^n)" by (simp add: norm_inverse norm_power power_inverse) qed
have"summable (\k. inverse ((real_of_nat k)^n))" using inverse_power_summable[of n] n by simp hence"summable (\k. inverse ((real_of_nat (k + m - m))^n))" by simp thus"summable (\k. inverse ((real_of_nat (k - m))^n))" by (rule summable_offset) qed
lemma Polygamma_converges': fixes z :: "'a :: {real_normed_field,banach}" assumes z: "z \ 0" and n: "n \ 2" shows"summable (\k. inverse ((z + of_nat k)^n))" using uniformly_convergent_imp_convergent[OF Polygamma_converges[OF assms, of 1], of z] by (simp add: summable_iff_convergent)
theorem Digamma_LIMSEQ: fixes z :: "'a :: {banach,real_normed_field}" assumes z: "z \ 0" shows"(\m. of_real (ln (real m)) - (\n Digamma z" proof - have"(\n. of_real (ln (real n / (real (Suc n))))) \ (of_real (ln 1) :: 'a)" by (intro tendsto_intros LIMSEQ_n_over_Suc_n) simp_all hence"(\n. of_real (ln (real n / (real n + 1)))) \ (0 :: 'a)" by (simp add: add_ac) hence lim: "(\n. of_real (ln (real n)) - of_real (ln (real n + 1))) \ (0::'a)" proof (rule Lim_transform_eventually) show"eventually (\n. of_real (ln (real n / (real n + 1))) =
of_real (ln (real n)) - (of_real (ln (real n + 1)) :: 'a)) at_top" using eventually_gt_at_top[of "0::nat"] by eventually_elim (simp add: ln_div) qed
from summable_Digamma[OF z] have"(\n. inverse (of_nat (n+1)) - inverse (z + of_nat n))
sums (Digamma z + euler_mascheroni)" by (simp add: Digamma_def summable_sums) from sums_diff[OF this euler_mascheroni_sum] have"(\n. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1)) - inverse (z + of_nat n))
sums Digamma z" by (simp add: add_ac) hence"(\m. (\n
(\<Sum>n<m. inverse (z + of_nat n))) \<longlonglongrightarrow> Digamma z" by (simp add: sums_def sum_subtractf) alsohave"(\m. (\n
(\<lambda>m. of_real (ln (m + 1)) :: 'a)" by (subst sum_lessThan_telescope) simp_all finallyshow ?thesis by (rule Lim_transform) (insert lim, simp) qed
theorem Polygamma_LIMSEQ: fixes z :: "'a :: {banach,real_normed_field}" assumes"z \ 0" and "n > 0" shows"(\k. inverse ((z + of_nat k)^Suc n)) sums ((-1) ^ Suc n * Polygamma n z / fact n)" using Polygamma_converges'[OF assms(1), of "Suc n"] assms(2) by (simp add: sums_iff Polygamma_def)
theorem has_field_derivative_ln_Gamma_complex [derivative_intros]: fixes z :: complex assumes z: "z \ \\<^sub>\\<^sub>0" shows"(ln_Gamma has_field_derivative Digamma z) (at z)" proof - have not_nonpos_Int [simp]: "t \ \\<^sub>\\<^sub>0" if "Re t > 0" for t using that by (auto elim!: nonpos_Ints_cases') from z have z': "z \ \\<^sub>\\<^sub>0" and z'': "z \ 0" using nonpos_Ints_subset_nonpos_Reals nonpos_Reals_zero_I by blast+ let ?f' = "\z k. inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))" let ?f = "\z k. z / of_nat (Suc k) - ln (1 + z / of_nat (Suc k))" and ?F' = "\z. \n. ?f' z n"
define d where"d = min (norm z/2) (if Im z = 0 then Re z / 2 else abs (Im z) / 2)" from z have d: "d > 0""norm z/2 \ d" by (auto simp add: complex_nonpos_Reals_iff d_def) have ball: "Im t = 0 \ Re t > 0" if "dist z t < d" for t using no_nonpos_Real_in_ball[OF z, of t] that unfolding d_def by (force simp add: complex_nonpos_Reals_iff) have sums: "(\n. inverse (z + of_nat (Suc n)) - inverse (z + of_nat n)) sums
(0 - inverse (z + of_nat 0))" by (intro telescope_sums filterlim_compose[OF tendsto_inverse_0]
tendsto_add_filterlim_at_infinity[OF tendsto_const] tendsto_of_nat)
have"((\z. \n. ?f z n) has_field_derivative ?F' z) (at z)" using d z ln_Gamma_series'_aux[OF z'] apply (intro has_field_derivative_series'(2)[of "ball z d" _ _ z] uniformly_summable_deriv_ln_Gamma) apply (auto intro!: derivative_eq_intros add_pos_pos mult_pos_pos dest!: ball
simp: field_simps sums_iff nonpos_Reals_divide_of_nat_iff
simp del: of_nat_Suc) apply (auto simp add: complex_nonpos_Reals_iff) done with z have"((\z. (\k. ?f z k) - euler_mascheroni * z - Ln z) has_field_derivative
?F' z - euler_mascheroni - inverse z) (at z)" by (force intro!: derivative_eq_intros simp: Digamma_def) alsohave"?F' z - euler_mascheroni - inverse z = (?F' z + -inverse z) - euler_mascheroni"by simp alsofrom sums have"-inverse z = (\n. inverse (z + of_nat (Suc n)) - inverse (z + of_nat n))" by (simp add: sums_iff) alsofrom sums summable_deriv_ln_Gamma[OF z''] have"?F' z + \ = (\n. inverse (of_nat (Suc n)) - inverse (z + of_nat n))" by (subst suminf_add) (simp_all add: add_ac sums_iff) alsohave"\ - euler_mascheroni = Digamma z" by (simp add: Digamma_def) finallyhave"((\z. (\k. ?f z k) - euler_mascheroni * z - Ln z)
has_field_derivative Digamma z) (at z)" . moreoverfrom eventually_nhds_ball[OF d(1), of z] have"eventually (\z. ln_Gamma z = (\k. ?f z k) - euler_mascheroni * z - Ln z) (nhds z)" proof eventually_elim fix t assume"t \ ball z d" hence"t \ \\<^sub>\\<^sub>0" by (auto dest!: ball elim!: nonpos_Ints_cases) from ln_Gamma_series'_aux[OF this] show"ln_Gamma t = (\k. ?f t k) - euler_mascheroni * t - Ln t" by (simp add: sums_iff) qed ultimatelyshow ?thesis by (subst DERIV_cong_ev[OF refl _ refl]) qed
theorem has_field_derivative_Polygamma [derivative_intros]: fixes z :: "'a :: {real_normed_field,euclidean_space}" assumes z: "z \ \\<^sub>\\<^sub>0" shows"(Polygamma n has_field_derivative Polygamma (Suc n) z) (at z within A)" proof (rule has_field_derivative_at_within, cases "n = 0") assume n: "n = 0" let ?f = "\k z. inverse (of_nat (Suc k)) - inverse (z + of_nat k)" let ?F = "\z. \k. ?f k z" and ?f' = "\k z. inverse ((z + of_nat k)\<^sup>2)" from no_nonpos_Int_in_ball'[OF z] obtain d where d: "0 < d" "\t. t \ ball z d \ t \ \\<^sub>\\<^sub>0" by auto from z have summable: "summable (\k. inverse (of_nat (Suc k)) - inverse (z + of_nat k))" by (intro summable_Digamma) force from z have conv: "uniformly_convergent_on (ball z d) (\k z. \i2))" by (intro Polygamma_converges) auto with d have"summable (\k. inverse ((z + of_nat k)\<^sup>2))" unfolding summable_iff_convergent by (auto dest!: uniformly_convergent_imp_convergent simp: summable_iff_convergent )
have"(?F has_field_derivative (\k. ?f' k z)) (at z)" proof (rule has_field_derivative_series'[of "ball z d" _ _ z]) fix k :: nat and t :: 'a assume t: "t \ ball z d" from t d(2)[of t] show"((\z. ?f k z) has_field_derivative ?f' k t) (at t within ball z d)" by (auto intro!: derivative_eq_intros simp: power2_eq_square simp del: of_nat_Suc
dest!: plus_of_nat_eq_0_imp elim!: nonpos_Ints_cases) qed (insert d(1) summable conv, (assumption|simp)+) with z show"(Polygamma n has_field_derivative Polygamma (Suc n) z) (at z)" unfolding Digamma_def [abs_def] Polygamma_def [abs_def] using n by (force simp: power2_eq_square intro!: derivative_eq_intros) next assume n: "n \ 0" from z have z': "z \ 0" by auto from no_nonpos_Int_in_ball'[OF z] obtain d where d: "0 < d" "\t. t \ ball z d \ t \ \\<^sub>\\<^sub>0" by auto
define n' where "n' = Suc n" from n have n': "n'\<ge> 2" by (simp add: n'_def) have"((\z. \k. inverse ((z + of_nat k) ^ n')) has_field_derivative
(\<Sum>k. - of_nat n' * inverse ((z + of_nat k) ^ (n'+1)))) (at z)" proof (rule has_field_derivative_series'[of "ball z d" _ _ z]) fix k :: nat and t :: 'a assume t: "t \ ball z d" with d have t': "t \ \\<^sub>\\<^sub>0" "t \ 0" by auto show"((\a. inverse ((a + of_nat k) ^ n')) has_field_derivative
- of_nat n' * inverse ((t + of_nat k) ^ (n'+1))) (at t within ball z d)" using t' by (fastforce intro!: derivative_eq_intros simp: divide_simps power_diff dest: plus_of_nat_eq_0_imp) next have"uniformly_convergent_on (ball z d)
(\<lambda>k z. (- of_nat n' :: 'a) * (\<Sum>i<k. inverse ((z + of_nat i) ^ (n'+1))))" using z' n by (intro uniformly_convergent_mult Polygamma_converges) (simp_all add: n'_def) thus"uniformly_convergent_on (ball z d)
(\<lambda>k z. \<Sum>i<k. - of_nat n' * inverse ((z + of_nat i :: 'a) ^ (n'+1)))" by (subst (asm) sum_distrib_left) simp qed (insert Polygamma_converges'[OF z' n'] d, simp_all) alsohave"(\k. - of_nat n' * inverse ((z + of_nat k) ^ (n' + 1))) =
(- of_nat n') * (\k. inverse ((z + of_nat k) ^ (n' + 1)))" using Polygamma_converges'[OF z', of "n'+1"] n' by (subst suminf_mult) simp_all finallyhave"((\z. \k. inverse ((z + of_nat k) ^ n')) has_field_derivative
- of_nat n' * (\k. inverse ((z + of_nat k) ^ (n' + 1)))) (at z)" . from DERIV_cmult[OF this, of "(-1)^Suc n * fact n :: 'a"] show"(Polygamma n has_field_derivative Polygamma (Suc n) z) (at z)" unfolding n'_def Polygamma_def[abs_def] using n by (simp add: algebra_simps) qed
lemma isCont_Polygamma [continuous_intros]: fixes f :: "_ \ 'a :: {real_normed_field,euclidean_space}" shows"isCont f z \ f z \ \\<^sub>\\<^sub>0 \ isCont (\x. Polygamma n (f x)) z" by (rule isCont_o2[OF _ DERIV_isCont[OF has_field_derivative_Polygamma]])
lemma continuous_on_Polygamma: "A \ \\<^sub>\\<^sub>0 = {} \ continuous_on A (Polygamma n :: _ \ 'a :: {real_normed_field,euclidean_space})" by (intro continuous_at_imp_continuous_on isCont_Polygamma[OF continuous_ident] ballI) blast
lemma isCont_ln_Gamma_complex [continuous_intros]: fixes f :: "'a::t2_space \ complex" shows"isCont f z \ f z \ \\<^sub>\\<^sub>0 \ isCont (\z. ln_Gamma (f z)) z" by (rule isCont_o2[OF _ DERIV_isCont[OF has_field_derivative_ln_Gamma_complex]])
lemma continuous_on_ln_Gamma_complex [continuous_intros]: fixes A :: "complex set" shows"A \ \\<^sub>\\<^sub>0 = {} \ continuous_on A ln_Gamma" by (intro continuous_at_imp_continuous_on ballI isCont_ln_Gamma_complex[OF continuous_ident])
fastforce
lemma deriv_Polygamma: assumes"z \ \\<^sub>\\<^sub>0" shows"deriv (Polygamma m) z =
Polygamma (Suc m) (z :: 'a :: {real_normed_field,euclidean_space})" by (intro DERIV_imp_deriv has_field_derivative_Polygamma assms) thm has_field_derivative_Polygamma
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) moreoverhave"eventually (\z. z \ UNIV - \\<^sub>\\<^sub>0) (nhds z)" using assms by (intro eventually_nhds_in_open open_Diff open_UNIV) auto ultimatelyshow ?caseby eventually_elim (simp_all add: deriv_Polygamma) qed simp_all thus ?thesis by (rule eventually_nhds_x_imp_x) qed
lemma deriv_ln_Gamma_complex: assumes"z \ \\<^sub>\\<^sub>0" shows"deriv ln_Gamma z = Digamma (z :: complex)" by (intro DERIV_imp_deriv has_field_derivative_ln_Gamma_complex assms)
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) alsohave"\ = Polygamma j' x" using assms by (subst higher_deriv_Polygamma)
(auto elim!: nonpos_Ints_cases simp: complex_nonpos_Reals_iff) finallyshow ?thesis using Suc by (simp del: funpow.simps add: funpow_Suc_right) qed simp_all
text\<open>
We define a type class that captures all the fundamental properties of the inverse of the Gamma function anddefines the Gamma function upon that. This allows us to instantiate the type class both for
the reals andfor the complex numbers with a minimal amount of proof duplication. \<close>
class\<^marker>\<open>tag unimportant\<close> Gamma = real_normed_field + complete_space + fixes rGamma :: "'a \ 'a" assumes rGamma_eq_zero_iff_aux: "rGamma z = 0 \ (\n. z = - of_nat n)" assumes differentiable_rGamma_aux1: "(\n. z \ - of_nat n) \ let d = (THE d. (\<lambda>n. \<Sum>k<n. inverse (of_nat (Suc k)) - inverse (z + of_nat k)) \<longlonglongrightarrow> d) - scaleR euler_mascheroni 1 in filterlim (\<lambda>y. (rGamma y - rGamma z + rGamma z * d * (y - z)) /\<^sub>R
norm (y - z)) (nhds 0) (at z)" assumes differentiable_rGamma_aux2: "let z = - of_nat n in filterlim (\<lambda>y. (rGamma y - rGamma z - (-1)^n * (prod of_nat {1..n}) * (y - z)) /\<^sub>R
norm (y - z)) (nhds 0) (at z)" assumes rGamma_series_aux: "(\n. z \ - of_nat n) \ let fact' = (\n. prod of_nat {1..n});
exp = (\<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x^k /\<^sub>R fact k) \<longlonglongrightarrow> e);
pochhammer' = (\a n. (\n = 0..n. a + of_nat n)) in filterlim (\<lambda>n. pochhammer' z n / (fact' n * exp (z * (ln (of_nat n) *\<^sub>R 1))))
(nhds (rGamma z)) sequentially" begin subclass banach .. end
definition"Gamma z = inverse (rGamma z)"
subsection \<open>Basic properties\<close>
lemma Gamma_nonpos_Int: "z \ \\<^sub>\\<^sub>0 \ Gamma z = 0" and rGamma_nonpos_Int: "z \ \\<^sub>\\<^sub>0 \ rGamma z = 0" using rGamma_eq_zero_iff_aux[of z] unfolding Gamma_def by (auto elim!: nonpos_Ints_cases')
lemma Gamma_nonzero: "z \ \\<^sub>\\<^sub>0 \ Gamma z \ 0" and rGamma_nonzero: "z \ \\<^sub>\\<^sub>0 \ rGamma z \ 0" using rGamma_eq_zero_iff_aux[of z] unfolding Gamma_def by (auto elim!: nonpos_Ints_cases')
lemma Gamma_eq_zero_iff: "Gamma z = 0 \ z \ \\<^sub>\\<^sub>0" and rGamma_eq_zero_iff: "rGamma z = 0 \ z \ \\<^sub>\\<^sub>0" using rGamma_eq_zero_iff_aux[of z] unfolding Gamma_def by (auto elim!: nonpos_Ints_cases')
lemma rGamma_inverse_Gamma: "rGamma z = inverse (Gamma z)" unfolding Gamma_def by simp
lemma rGamma_series_LIMSEQ [tendsto_intros]: "rGamma_series z \ rGamma z" proof (cases "z \ \\<^sub>\\<^sub>0") case False hence"z \ - of_nat n" for n by auto from rGamma_series_aux[OF this] show ?thesis by (simp add: rGamma_series_def[abs_def] fact_prod pochhammer_Suc_prod
exp_def of_real_def[symmetric] suminf_def sums_def[abs_def] atLeast0AtMost) qed (insert rGamma_eq_zero_iff[of z], simp_all add: rGamma_series_nonpos_Ints_LIMSEQ)
theorem Gamma_series_LIMSEQ [tendsto_intros]: "Gamma_series z \ Gamma z" proof (cases "z \ \\<^sub>\\<^sub>0") case False hence"(\n. inverse (rGamma_series z n)) \ inverse (rGamma z)" by (intro tendsto_intros) (simp_all add: rGamma_eq_zero_iff) alsohave"(\n. inverse (rGamma_series z n)) = Gamma_series z" by (simp add: rGamma_series_def Gamma_series_def[abs_def]) finallyshow ?thesis by (simp add: Gamma_def) qed (insert Gamma_eq_zero_iff[of z], simp_all add: Gamma_series_nonpos_Ints_LIMSEQ)
lemma Gamma_altdef: "Gamma z = lim (Gamma_series z)" using Gamma_series_LIMSEQ[of z] by (simp add: limI)
lemma rGamma_1 [simp]: "rGamma 1 = 1" proof - have A: "eventually (\n. rGamma_series 1 n = of_nat (Suc n) / of_nat n) sequentially" using eventually_gt_at_top[of "0::nat"] by (force elim!: eventually_mono simp: rGamma_series_def exp_of_real pochhammer_fact
field_split_simps pochhammer_rec' dest!: pochhammer_eq_0_imp_nonpos_Int) have"rGamma_series 1 \ 1" by (subst tendsto_cong[OF A]) (rule LIMSEQ_Suc_n_over_n) moreoverhave"rGamma_series 1 \ rGamma 1" by (rule tendsto_intros) ultimatelyshow ?thesis by (intro LIMSEQ_unique) qed
lemma rGamma_plus1: "z * rGamma (z + 1) = rGamma z" proof - let ?f = "\n. (z + 1) * inverse (of_nat n) + 1" have"eventually (\n. ?f n * rGamma_series z n = z * rGamma_series (z + 1) n) sequentially" using eventually_gt_at_top[of "0::nat"] proof eventually_elim fix n :: nat assume n: "n > 0" hence"z * rGamma_series (z + 1) n = inverse (of_nat n) *
pochhammer z (Suc (Suc n)) / (fact n * exp (z * of_real (ln (of_nat n))))" by (subst pochhammer_rec) (simp add: rGamma_series_def field_simps exp_add exp_of_real) alsofrom n have"\ = ?f n * rGamma_series z n" by (subst pochhammer_rec') (simp_all add: field_split_simps rGamma_series_def) finallyshow"?f n * rGamma_series z n = z * rGamma_series (z + 1) n" .. qed moreoverhave"(\n. ?f n * rGamma_series z n) \ ((z+1) * 0 + 1) * rGamma z" by (intro tendsto_intros lim_inverse_n) hence"(\n. ?f n * rGamma_series z n) \ rGamma z" by simp ultimatelyhave"(\n. z * rGamma_series (z + 1) n) \ rGamma z" by (blast intro: Lim_transform_eventually) moreoverhave"(\n. z * rGamma_series (z + 1) n) \ z * rGamma (z + 1)" by (intro tendsto_intros) ultimatelyshow"z * rGamma (z + 1) = rGamma z"using LIMSEQ_unique by blast qed
lemma pochhammer_rGamma: "rGamma z = pochhammer z n * rGamma (z + of_nat n)" proof (induction n arbitrary: z) case (Suc n z) have"rGamma z = pochhammer z n * rGamma (z + of_nat n)"by (rule Suc.IH) alsonote rGamma_plus1 [symmetric] finallyshow ?caseby (simp add: add_ac pochhammer_rec') qed simp_all
theorem Gamma_plus1: "z \ \\<^sub>\\<^sub>0 \ Gamma (z + 1) = z * Gamma z" using rGamma_plus1[of z] by (simp add: rGamma_inverse_Gamma field_simps Gamma_eq_zero_iff)
theorem pochhammer_Gamma: "z \ \\<^sub>\\<^sub>0 \ pochhammer z n = Gamma (z + of_nat n) / Gamma z" using pochhammer_rGamma[of z] by (simp add: rGamma_inverse_Gamma Gamma_eq_zero_iff field_simps)
lemma Gamma_0 [simp]: "Gamma 0 = 0" and rGamma_0 [simp]: "rGamma 0 = 0" and Gamma_neg_1 [simp]: "Gamma (- 1) = 0" and rGamma_neg_1 [simp]: "rGamma (- 1) = 0" and Gamma_neg_numeral [simp]: "Gamma (- numeral n) = 0" and rGamma_neg_numeral [simp]: "rGamma (- numeral n) = 0" and Gamma_neg_of_nat [simp]: "Gamma (- of_nat m) = 0" and rGamma_neg_of_nat [simp]: "rGamma (- of_nat m) = 0" by (simp_all add: rGamma_eq_zero_iff Gamma_eq_zero_iff)
lemma Gamma_1 [simp]: "Gamma 1 = 1"unfolding Gamma_def by simp
lemma Gamma_of_int: "Gamma (of_int n) = (if n > 0 then fact (nat (n - 1)) else 0)" proof (cases "n > 0") case True hence"Gamma (of_int n) = Gamma (of_nat (Suc (nat (n - 1))))"by (subst of_nat_Suc) simp_all with True show ?thesis by (subst (asm) of_nat_Suc, subst (asm) Gamma_fact) simp qed (simp_all add: Gamma_eq_zero_iff nonpos_Ints_of_int)
lemma rGamma_of_int: "rGamma (of_int n) = (if n > 0 then inverse (fact (nat (n - 1))) else 0)" by (simp add: Gamma_of_int rGamma_inverse_Gamma)
lemma Gamma_seriesI: assumes"(\n. g n / Gamma_series z n) \ 1" shows"g \ Gamma z" proof (rule Lim_transform_eventually) have"1/2 > (0::real)"by simp from tendstoD[OF assms, OF this] show"eventually (\n. g n / Gamma_series z n * Gamma_series z n = g n) sequentially" by (force elim!: eventually_mono simp: dist_real_def) from assms have"(\n. g n / Gamma_series z n * Gamma_series z n) \ 1 * Gamma z" by (intro tendsto_intros) thus"(\n. g n / Gamma_series z n * Gamma_series z n) \ Gamma z" by simp qed
lemma Gamma_seriesI': assumes"f \ rGamma z" assumes"(\n. g n * f n) \ 1" assumes"z \ \\<^sub>\\<^sub>0" shows"g \ Gamma z" proof (rule Lim_transform_eventually) have"1/2 > (0::real)"by simp from tendstoD[OF assms(2), OF this] show"eventually (\n. g n * f n / f n = g n) sequentially" by (force elim!: eventually_mono simp: dist_real_def) from assms have"(\n. g n * f n / f n) \ 1 / rGamma z" by (intro tendsto_divide assms) (simp_all add: rGamma_eq_zero_iff) thus"(\n. g n * f n / f n) \ Gamma z" by (simp add: Gamma_def divide_inverse) qed
lemma Gamma_series'_LIMSEQ: "Gamma_series' z \<longlonglongrightarrow> Gamma z" by (cases "z \ \\<^sub>\\<^sub>0") (simp_all add: Gamma_nonpos_Int Gamma_seriesI[OF Gamma_series_Gamma_series']
Gamma_series'_nonpos_Ints_LIMSEQ[of z])
subsection \<open>Differentiability\<close>
lemma has_field_derivative_rGamma_no_nonpos_int: assumes"z \ \\<^sub>\\<^sub>0" shows"(rGamma has_field_derivative -rGamma z * Digamma z) (at z within A)" proof (rule has_field_derivative_at_within) from assms have"z \ - of_nat n" for n by auto from differentiable_rGamma_aux1[OF this] show"(rGamma has_field_derivative -rGamma z * Digamma z) (at z)" unfolding Digamma_def suminf_def sums_def[abs_def]
has_field_derivative_def has_derivative_def netlimit_at by (simp add: Let_def bounded_linear_mult_right mult_ac of_real_def [symmetric]) qed
lemma continuous_on_rGamma [continuous_intros]: "continuous_on A rGamma" by (rule DERIV_continuous_on has_field_derivative_rGamma)+
lemma continuous_on_Gamma [continuous_intros]: "A \ \\<^sub>\\<^sub>0 = {} \ continuous_on A Gamma" by (rule DERIV_continuous_on has_field_derivative_Gamma)+ blast
lemma isCont_rGamma [continuous_intros]: "isCont f z \ isCont (\x. rGamma (f x)) z" by (rule isCont_o2[OF _ DERIV_isCont[OF has_field_derivative_rGamma]])
lemma isCont_Gamma [continuous_intros]: "isCont f z \ f z \ \\<^sub>\\<^sub>0 \ isCont (\x. Gamma (f x)) z" by (rule isCont_o2[OF _ DERIV_isCont[OF has_field_derivative_Gamma]])
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
