|
1 (* Title: HOL/Analysis/Gamma.thy |
|
2 Author: Manuel Eberl, TU München |
|
3 *) |
|
4 |
|
5 section \<open>The Gamma Function\<close> |
|
6 |
|
7 theory Gamma_Function |
|
8 imports |
|
9 Complex_Transcendental |
|
10 Summation_Tests |
|
11 Harmonic_Numbers |
|
12 "~~/src/HOL/Library/Nonpos_Ints" |
|
13 "~~/src/HOL/Library/Periodic_Fun" |
|
14 begin |
|
15 |
|
16 text \<open> |
|
17 Several equivalent definitions of the Gamma function and its |
|
18 most important properties. Also contains the definition and some properties |
|
19 of the log-Gamma function and the Digamma function and the other Polygamma functions. |
|
20 |
|
21 Based on the Gamma function, we also prove the Weierstraß product form of the |
|
22 sin function and, based on this, the solution of the Basel problem (the |
|
23 sum over all @{term "1 / (n::nat)^2"}. |
|
24 \<close> |
|
25 |
|
26 lemma pochhammer_eq_0_imp_nonpos_Int: |
|
27 "pochhammer (x::'a::field_char_0) n = 0 \<Longrightarrow> x \<in> \<int>\<^sub>\<le>\<^sub>0" |
|
28 by (auto simp: pochhammer_eq_0_iff) |
|
29 |
|
30 lemma closed_nonpos_Ints [simp]: "closed (\<int>\<^sub>\<le>\<^sub>0 :: 'a :: real_normed_algebra_1 set)" |
|
31 proof - |
|
32 have "\<int>\<^sub>\<le>\<^sub>0 = (of_int ` {n. n \<le> 0} :: 'a set)" |
|
33 by (auto elim!: nonpos_Ints_cases intro!: nonpos_Ints_of_int) |
|
34 also have "closed \<dots>" by (rule closed_of_int_image) |
|
35 finally show ?thesis . |
|
36 qed |
|
37 |
|
38 lemma plus_one_in_nonpos_Ints_imp: "z + 1 \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> z \<in> \<int>\<^sub>\<le>\<^sub>0" |
|
39 using nonpos_Ints_diff_Nats[of "z+1" "1"] by simp_all |
|
40 |
|
41 lemma of_int_in_nonpos_Ints_iff: |
|
42 "(of_int n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n \<le> 0" |
|
43 by (auto simp: nonpos_Ints_def) |
|
44 |
|
45 lemma one_plus_of_int_in_nonpos_Ints_iff: |
|
46 "(1 + of_int n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n \<le> -1" |
|
47 proof - |
|
48 have "1 + of_int n = (of_int (n + 1) :: 'a)" by simp |
|
49 also have "\<dots> \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n + 1 \<le> 0" by (subst of_int_in_nonpos_Ints_iff) simp_all |
|
50 also have "\<dots> \<longleftrightarrow> n \<le> -1" by presburger |
|
51 finally show ?thesis . |
|
52 qed |
|
53 |
|
54 lemma one_minus_of_nat_in_nonpos_Ints_iff: |
|
55 "(1 - of_nat n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n > 0" |
|
56 proof - |
|
57 have "(1 - of_nat n :: 'a) = of_int (1 - int n)" by simp |
|
58 also have "\<dots> \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n > 0" by (subst of_int_in_nonpos_Ints_iff) presburger |
|
59 finally show ?thesis . |
|
60 qed |
|
61 |
|
62 lemma fraction_not_in_ints: |
|
63 assumes "\<not>(n dvd m)" "n \<noteq> 0" |
|
64 shows "of_int m / of_int n \<notin> (\<int> :: 'a :: {division_ring,ring_char_0} set)" |
|
65 proof |
|
66 assume "of_int m / (of_int n :: 'a) \<in> \<int>" |
|
67 then obtain k where "of_int m / of_int n = (of_int k :: 'a)" by (elim Ints_cases) |
|
68 with assms have "of_int m = (of_int (k * n) :: 'a)" by (auto simp add: divide_simps) |
|
69 hence "m = k * n" by (subst (asm) of_int_eq_iff) |
|
70 hence "n dvd m" by simp |
|
71 with assms(1) show False by contradiction |
|
72 qed |
|
73 |
|
74 lemma fraction_not_in_nats: |
|
75 assumes "\<not>n dvd m" "n \<noteq> 0" |
|
76 shows "of_int m / of_int n \<notin> (\<nat> :: 'a :: {division_ring,ring_char_0} set)" |
|
77 proof |
|
78 assume "of_int m / of_int n \<in> (\<nat> :: 'a set)" |
|
79 also note Nats_subset_Ints |
|
80 finally have "of_int m / of_int n \<in> (\<int> :: 'a set)" . |
|
81 moreover have "of_int m / of_int n \<notin> (\<int> :: 'a set)" |
|
82 using assms by (intro fraction_not_in_ints) |
|
83 ultimately show False by contradiction |
|
84 qed |
|
85 |
|
86 lemma not_in_Ints_imp_not_in_nonpos_Ints: "z \<notin> \<int> \<Longrightarrow> z \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
87 by (auto simp: Ints_def nonpos_Ints_def) |
|
88 |
|
89 lemma double_in_nonpos_Ints_imp: |
|
90 assumes "2 * (z :: 'a :: field_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0" |
|
91 shows "z \<in> \<int>\<^sub>\<le>\<^sub>0 \<or> z + 1/2 \<in> \<int>\<^sub>\<le>\<^sub>0" |
|
92 proof- |
|
93 from assms obtain k where k: "2 * z = - of_nat k" by (elim nonpos_Ints_cases') |
|
94 thus ?thesis by (cases "even k") (auto elim!: evenE oddE simp: field_simps) |
|
95 qed |
|
96 |
|
97 |
|
98 lemma sin_series: "(\<lambda>n. ((-1)^n / fact (2*n+1)) *\<^sub>R z^(2*n+1)) sums sin z" |
|
99 proof - |
|
100 from sin_converges[of z] have "(\<lambda>n. sin_coeff n *\<^sub>R z^n) sums sin z" . |
|
101 also have "(\<lambda>n. sin_coeff n *\<^sub>R z^n) sums sin z \<longleftrightarrow> |
|
102 (\<lambda>n. ((-1)^n / fact (2*n+1)) *\<^sub>R z^(2*n+1)) sums sin z" |
|
103 by (subst sums_mono_reindex[of "\<lambda>n. 2*n+1", symmetric]) |
|
104 (auto simp: sin_coeff_def subseq_def ac_simps elim!: oddE) |
|
105 finally show ?thesis . |
|
106 qed |
|
107 |
|
108 lemma cos_series: "(\<lambda>n. ((-1)^n / fact (2*n)) *\<^sub>R z^(2*n)) sums cos z" |
|
109 proof - |
|
110 from cos_converges[of z] have "(\<lambda>n. cos_coeff n *\<^sub>R z^n) sums cos z" . |
|
111 also have "(\<lambda>n. cos_coeff n *\<^sub>R z^n) sums cos z \<longleftrightarrow> |
|
112 (\<lambda>n. ((-1)^n / fact (2*n)) *\<^sub>R z^(2*n)) sums cos z" |
|
113 by (subst sums_mono_reindex[of "\<lambda>n. 2*n", symmetric]) |
|
114 (auto simp: cos_coeff_def subseq_def ac_simps elim!: evenE) |
|
115 finally show ?thesis . |
|
116 qed |
|
117 |
|
118 lemma sin_z_over_z_series: |
|
119 fixes z :: "'a :: {real_normed_field,banach}" |
|
120 assumes "z \<noteq> 0" |
|
121 shows "(\<lambda>n. (-1)^n / fact (2*n+1) * z^(2*n)) sums (sin z / z)" |
|
122 proof - |
|
123 from sin_series[of z] have "(\<lambda>n. z * ((-1)^n / fact (2*n+1)) * z^(2*n)) sums sin z" |
|
124 by (simp add: field_simps scaleR_conv_of_real) |
|
125 from sums_mult[OF this, of "inverse z"] and assms show ?thesis |
|
126 by (simp add: field_simps) |
|
127 qed |
|
128 |
|
129 lemma sin_z_over_z_series': |
|
130 fixes z :: "'a :: {real_normed_field,banach}" |
|
131 assumes "z \<noteq> 0" |
|
132 shows "(\<lambda>n. sin_coeff (n+1) *\<^sub>R z^n) sums (sin z / z)" |
|
133 proof - |
|
134 from sums_split_initial_segment[OF sin_converges[of z], of 1] |
|
135 have "(\<lambda>n. z * (sin_coeff (n+1) *\<^sub>R z ^ n)) sums sin z" by simp |
|
136 from sums_mult[OF this, of "inverse z"] assms show ?thesis by (simp add: field_simps) |
|
137 qed |
|
138 |
|
139 lemma has_field_derivative_sin_z_over_z: |
|
140 fixes A :: "'a :: {real_normed_field,banach} set" |
|
141 shows "((\<lambda>z. if z = 0 then 1 else sin z / z) has_field_derivative 0) (at 0 within A)" |
|
142 (is "(?f has_field_derivative ?f') _") |
|
143 proof (rule has_field_derivative_at_within) |
|
144 have "((\<lambda>z::'a. \<Sum>n. of_real (sin_coeff (n+1)) * z^n) |
|
145 has_field_derivative (\<Sum>n. diffs (\<lambda>n. of_real (sin_coeff (n+1))) n * 0^n)) (at 0)" |
|
146 proof (rule termdiffs_strong) |
|
147 from summable_ignore_initial_segment[OF sums_summable[OF sin_converges[of "1::'a"]], of 1] |
|
148 show "summable (\<lambda>n. of_real (sin_coeff (n+1)) * (1::'a)^n)" by (simp add: of_real_def) |
|
149 qed simp |
|
150 also have "(\<lambda>z::'a. \<Sum>n. of_real (sin_coeff (n+1)) * z^n) = ?f" |
|
151 proof |
|
152 fix z |
|
153 show "(\<Sum>n. of_real (sin_coeff (n+1)) * z^n) = ?f z" |
|
154 by (cases "z = 0") (insert sin_z_over_z_series'[of z], |
|
155 simp_all add: scaleR_conv_of_real sums_iff powser_zero sin_coeff_def) |
|
156 qed |
|
157 also have "(\<Sum>n. diffs (\<lambda>n. of_real (sin_coeff (n + 1))) n * (0::'a) ^ n) = |
|
158 diffs (\<lambda>n. of_real (sin_coeff (Suc n))) 0" by (simp add: powser_zero) |
|
159 also have "\<dots> = 0" by (simp add: sin_coeff_def diffs_def) |
|
160 finally show "((\<lambda>z::'a. if z = 0 then 1 else sin z / z) has_field_derivative 0) (at 0)" . |
|
161 qed |
|
162 |
|
163 lemma round_Re_minimises_norm: |
|
164 "norm ((z::complex) - of_int m) \<ge> norm (z - of_int (round (Re z)))" |
|
165 proof - |
|
166 let ?n = "round (Re z)" |
|
167 have "norm (z - of_int ?n) = sqrt ((Re z - of_int ?n)\<^sup>2 + (Im z)\<^sup>2)" |
|
168 by (simp add: cmod_def) |
|
169 also have "\<bar>Re z - of_int ?n\<bar> \<le> \<bar>Re z - of_int m\<bar>" by (rule round_diff_minimal) |
|
170 hence "sqrt ((Re z - of_int ?n)\<^sup>2 + (Im z)\<^sup>2) \<le> sqrt ((Re z - of_int m)\<^sup>2 + (Im z)\<^sup>2)" |
|
171 by (intro real_sqrt_le_mono add_mono) (simp_all add: abs_le_square_iff) |
|
172 also have "\<dots> = norm (z - of_int m)" by (simp add: cmod_def) |
|
173 finally show ?thesis . |
|
174 qed |
|
175 |
|
176 lemma Re_pos_in_ball: |
|
177 assumes "Re z > 0" "t \<in> ball z (Re z/2)" |
|
178 shows "Re t > 0" |
|
179 proof - |
|
180 have "Re (z - t) \<le> norm (z - t)" by (rule complex_Re_le_cmod) |
|
181 also from assms have "\<dots> < Re z / 2" by (simp add: dist_complex_def) |
|
182 finally show "Re t > 0" using assms by simp |
|
183 qed |
|
184 |
|
185 lemma no_nonpos_Int_in_ball_complex: |
|
186 assumes "Re z > 0" "t \<in> ball z (Re z/2)" |
|
187 shows "t \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
188 using Re_pos_in_ball[OF assms] by (force elim!: nonpos_Ints_cases) |
|
189 |
|
190 lemma no_nonpos_Int_in_ball: |
|
191 assumes "t \<in> ball z (dist z (round (Re z)))" |
|
192 shows "t \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
193 proof |
|
194 assume "t \<in> \<int>\<^sub>\<le>\<^sub>0" |
|
195 then obtain n where "t = of_int n" by (auto elim!: nonpos_Ints_cases) |
|
196 have "dist z (of_int n) \<le> dist z t + dist t (of_int n)" by (rule dist_triangle) |
|
197 also from assms have "dist z t < dist z (round (Re z))" by simp |
|
198 also have "\<dots> \<le> dist z (of_int n)" |
|
199 using round_Re_minimises_norm[of z] by (simp add: dist_complex_def) |
|
200 finally have "dist t (of_int n) > 0" by simp |
|
201 with \<open>t = of_int n\<close> show False by simp |
|
202 qed |
|
203 |
|
204 lemma no_nonpos_Int_in_ball': |
|
205 assumes "(z :: 'a :: {euclidean_space,real_normed_algebra_1}) \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
206 obtains d where "d > 0" "\<And>t. t \<in> ball z d \<Longrightarrow> t \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
207 proof (rule that) |
|
208 from assms show "setdist {z} \<int>\<^sub>\<le>\<^sub>0 > 0" by (subst setdist_gt_0_compact_closed) auto |
|
209 next |
|
210 fix t assume "t \<in> ball z (setdist {z} \<int>\<^sub>\<le>\<^sub>0)" |
|
211 thus "t \<notin> \<int>\<^sub>\<le>\<^sub>0" using setdist_le_dist[of z "{z}" t "\<int>\<^sub>\<le>\<^sub>0"] by force |
|
212 qed |
|
213 |
|
214 lemma no_nonpos_Real_in_ball: |
|
215 assumes z: "z \<notin> \<real>\<^sub>\<le>\<^sub>0" and t: "t \<in> ball z (if Im z = 0 then Re z / 2 else abs (Im z) / 2)" |
|
216 shows "t \<notin> \<real>\<^sub>\<le>\<^sub>0" |
|
217 using z |
|
218 proof (cases "Im z = 0") |
|
219 assume A: "Im z = 0" |
|
220 with z have "Re z > 0" by (force simp add: complex_nonpos_Reals_iff) |
|
221 with t A Re_pos_in_ball[of z t] show ?thesis by (force simp add: complex_nonpos_Reals_iff) |
|
222 next |
|
223 assume A: "Im z \<noteq> 0" |
|
224 have "abs (Im z) - abs (Im t) \<le> abs (Im z - Im t)" by linarith |
|
225 also have "\<dots> = abs (Im (z - t))" by simp |
|
226 also have "\<dots> \<le> norm (z - t)" by (rule abs_Im_le_cmod) |
|
227 also from A t have "\<dots> \<le> abs (Im z) / 2" by (simp add: dist_complex_def) |
|
228 finally have "abs (Im t) > 0" using A by simp |
|
229 thus ?thesis by (force simp add: complex_nonpos_Reals_iff) |
|
230 qed |
|
231 |
|
232 |
|
233 subsection \<open>Definitions\<close> |
|
234 |
|
235 text \<open> |
|
236 We define the Gamma function by first defining its multiplicative inverse @{term "Gamma_inv"}. |
|
237 This is more convenient because @{term "Gamma_inv"} is entire, which makes proofs of its |
|
238 properties more convenient because one does not have to watch out for discontinuities. |
|
239 (e.g. @{term "Gamma_inv"} fulfils @{term "rGamma z = z * rGamma (z + 1)"} everywhere, |
|
240 whereas @{term "Gamma"} does not fulfil the analogous equation on the non-positive integers) |
|
241 |
|
242 We define the Gamma function (resp. its inverse) in the Euler form. This form has the advantage |
|
243 that it is a relatively simple limit that converges everywhere. The limit at the poles is 0 |
|
244 (due to division by 0). The functional equation @{term "Gamma (z + 1) = z * Gamma z"} follows |
|
245 immediately from the definition. |
|
246 \<close> |
|
247 |
|
248 definition Gamma_series :: "('a :: {banach,real_normed_field}) \<Rightarrow> nat \<Rightarrow> 'a" where |
|
249 "Gamma_series z n = fact n * exp (z * of_real (ln (of_nat n))) / pochhammer z (n+1)" |
|
250 |
|
251 definition Gamma_series' :: "('a :: {banach,real_normed_field}) \<Rightarrow> nat \<Rightarrow> 'a" where |
|
252 "Gamma_series' z n = fact (n - 1) * exp (z * of_real (ln (of_nat n))) / pochhammer z n" |
|
253 |
|
254 definition rGamma_series :: "('a :: {banach,real_normed_field}) \<Rightarrow> nat \<Rightarrow> 'a" where |
|
255 "rGamma_series z n = pochhammer z (n+1) / (fact n * exp (z * of_real (ln (of_nat n))))" |
|
256 |
|
257 lemma Gamma_series_altdef: "Gamma_series z n = inverse (rGamma_series z n)" |
|
258 and rGamma_series_altdef: "rGamma_series z n = inverse (Gamma_series z n)" |
|
259 unfolding Gamma_series_def rGamma_series_def by simp_all |
|
260 |
|
261 lemma rGamma_series_minus_of_nat: |
|
262 "eventually (\<lambda>n. rGamma_series (- of_nat k) n = 0) sequentially" |
|
263 using eventually_ge_at_top[of k] |
|
264 by eventually_elim (auto simp: rGamma_series_def pochhammer_of_nat_eq_0_iff) |
|
265 |
|
266 lemma Gamma_series_minus_of_nat: |
|
267 "eventually (\<lambda>n. Gamma_series (- of_nat k) n = 0) sequentially" |
|
268 using eventually_ge_at_top[of k] |
|
269 by eventually_elim (auto simp: Gamma_series_def pochhammer_of_nat_eq_0_iff) |
|
270 |
|
271 lemma Gamma_series'_minus_of_nat: |
|
272 "eventually (\<lambda>n. Gamma_series' (- of_nat k) n = 0) sequentially" |
|
273 using eventually_gt_at_top[of k] |
|
274 by eventually_elim (auto simp: Gamma_series'_def pochhammer_of_nat_eq_0_iff) |
|
275 |
|
276 lemma rGamma_series_nonpos_Ints_LIMSEQ: "z \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma_series z \<longlonglongrightarrow> 0" |
|
277 by (elim nonpos_Ints_cases', hypsubst, subst tendsto_cong, rule rGamma_series_minus_of_nat, simp) |
|
278 |
|
279 lemma Gamma_series_nonpos_Ints_LIMSEQ: "z \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Gamma_series z \<longlonglongrightarrow> 0" |
|
280 by (elim nonpos_Ints_cases', hypsubst, subst tendsto_cong, rule Gamma_series_minus_of_nat, simp) |
|
281 |
|
282 lemma Gamma_series'_nonpos_Ints_LIMSEQ: "z \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Gamma_series' z \<longlonglongrightarrow> 0" |
|
283 by (elim nonpos_Ints_cases', hypsubst, subst tendsto_cong, rule Gamma_series'_minus_of_nat, simp) |
|
284 |
|
285 lemma Gamma_series_Gamma_series': |
|
286 assumes z: "z \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
287 shows "(\<lambda>n. Gamma_series' z n / Gamma_series z n) \<longlonglongrightarrow> 1" |
|
288 proof (rule Lim_transform_eventually) |
|
289 from eventually_gt_at_top[of "0::nat"] |
|
290 show "eventually (\<lambda>n. z / of_nat n + 1 = Gamma_series' z n / Gamma_series z n) sequentially" |
|
291 proof eventually_elim |
|
292 fix n :: nat assume n: "n > 0" |
|
293 from n z have "Gamma_series' z n / Gamma_series z n = (z + of_nat n) / of_nat n" |
|
294 by (cases n, simp) |
|
295 (auto simp add: Gamma_series_def Gamma_series'_def pochhammer_rec' |
|
296 dest: pochhammer_eq_0_imp_nonpos_Int plus_of_nat_eq_0_imp) |
|
297 also from n have "\<dots> = z / of_nat n + 1" by (simp add: divide_simps) |
|
298 finally show "z / of_nat n + 1 = Gamma_series' z n / Gamma_series z n" .. |
|
299 qed |
|
300 have "(\<lambda>x. z / of_nat x) \<longlonglongrightarrow> 0" |
|
301 by (rule tendsto_norm_zero_cancel) |
|
302 (insert tendsto_mult[OF tendsto_const[of "norm z"] lim_inverse_n], |
|
303 simp add: norm_divide inverse_eq_divide) |
|
304 from tendsto_add[OF this tendsto_const[of 1]] show "(\<lambda>n. z / of_nat n + 1) \<longlonglongrightarrow> 1" by simp |
|
305 qed |
|
306 |
|
307 |
|
308 subsection \<open>Convergence of the Euler series form\<close> |
|
309 |
|
310 text \<open> |
|
311 We now show that the series that defines the Gamma function in the Euler form converges |
|
312 and that the function defined by it is continuous on the complex halfspace with positive |
|
313 real part. |
|
314 |
|
315 We do this by showing that the logarithm of the Euler series is continuous and converges |
|
316 locally uniformly, which means that the log-Gamma function defined by its limit is also |
|
317 continuous. |
|
318 |
|
319 This will later allow us to lift holomorphicity and continuity from the log-Gamma |
|
320 function to the inverse of the Gamma function, and from that to the Gamma function itself. |
|
321 \<close> |
|
322 |
|
323 definition ln_Gamma_series :: "('a :: {banach,real_normed_field,ln}) \<Rightarrow> nat \<Rightarrow> 'a" where |
|
324 "ln_Gamma_series z n = z * ln (of_nat n) - ln z - (\<Sum>k=1..n. ln (z / of_nat k + 1))" |
|
325 |
|
326 definition ln_Gamma_series' :: "('a :: {banach,real_normed_field,ln}) \<Rightarrow> nat \<Rightarrow> 'a" where |
|
327 "ln_Gamma_series' z n = |
|
328 - euler_mascheroni*z - ln z + (\<Sum>k=1..n. z / of_nat n - ln (z / of_nat k + 1))" |
|
329 |
|
330 definition ln_Gamma :: "('a :: {banach,real_normed_field,ln}) \<Rightarrow> 'a" where |
|
331 "ln_Gamma z = lim (ln_Gamma_series z)" |
|
332 |
|
333 |
|
334 text \<open> |
|
335 We now show that the log-Gamma series converges locally uniformly for all complex numbers except |
|
336 the non-positive integers. We do this by proving that the series is locally Cauchy, adapting this |
|
337 proof: |
|
338 http://math.stackexchange.com/questions/887158/convergence-of-gammaz-lim-n-to-infty-fracnzn-prod-m-0nzm |
|
339 \<close> |
|
340 |
|
341 context |
|
342 begin |
|
343 |
|
344 private lemma ln_Gamma_series_complex_converges_aux: |
|
345 fixes z :: complex and k :: nat |
|
346 assumes z: "z \<noteq> 0" and k: "of_nat k \<ge> 2*norm z" "k \<ge> 2" |
|
347 shows "norm (z * ln (1 - 1/of_nat k) + ln (z/of_nat k + 1)) \<le> 2*(norm z + norm z^2) / of_nat k^2" |
|
348 proof - |
|
349 let ?k = "of_nat k :: complex" and ?z = "norm z" |
|
350 have "z *ln (1 - 1/?k) + ln (z/?k+1) = z*(ln (1 - 1/?k :: complex) + 1/?k) + (ln (1+z/?k) - z/?k)" |
|
351 by (simp add: algebra_simps) |
|
352 also have "norm ... \<le> ?z * norm (ln (1-1/?k) + 1/?k :: complex) + norm (ln (1+z/?k) - z/?k)" |
|
353 by (subst norm_mult [symmetric], rule norm_triangle_ineq) |
|
354 also have "norm (Ln (1 + -1/?k) - (-1/?k)) \<le> (norm (-1/?k))\<^sup>2 / (1 - norm(-1/?k))" |
|
355 using k by (intro Ln_approx_linear) (simp add: norm_divide) |
|
356 hence "?z * norm (ln (1-1/?k) + 1/?k) \<le> ?z * ((norm (1/?k))^2 / (1 - norm (1/?k)))" |
|
357 by (intro mult_left_mono) simp_all |
|
358 also have "... \<le> (?z * (of_nat k / (of_nat k - 1))) / of_nat k^2" using k |
|
359 by (simp add: field_simps power2_eq_square norm_divide) |
|
360 also have "... \<le> (?z * 2) / of_nat k^2" using k |
|
361 by (intro divide_right_mono mult_left_mono) (simp_all add: field_simps) |
|
362 also have "norm (ln (1+z/?k) - z/?k) \<le> norm (z/?k)^2 / (1 - norm (z/?k))" using k |
|
363 by (intro Ln_approx_linear) (simp add: norm_divide) |
|
364 hence "norm (ln (1+z/?k) - z/?k) \<le> ?z^2 / of_nat k^2 / (1 - ?z / of_nat k)" |
|
365 by (simp add: field_simps norm_divide) |
|
366 also have "... \<le> (?z^2 * (of_nat k / (of_nat k - ?z))) / of_nat k^2" using k |
|
367 by (simp add: field_simps power2_eq_square) |
|
368 also have "... \<le> (?z^2 * 2) / of_nat k^2" using k |
|
369 by (intro divide_right_mono mult_left_mono) (simp_all add: field_simps) |
|
370 also note add_divide_distrib [symmetric] |
|
371 finally show ?thesis by (simp only: distrib_left mult.commute) |
|
372 qed |
|
373 |
|
374 lemma ln_Gamma_series_complex_converges: |
|
375 assumes z: "z \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
376 assumes d: "d > 0" "\<And>n. n \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> norm (z - of_int n) > d" |
|
377 shows "uniformly_convergent_on (ball z d) (\<lambda>n z. ln_Gamma_series z n :: complex)" |
|
378 proof (intro Cauchy_uniformly_convergent uniformly_Cauchy_onI') |
|
379 fix e :: real assume e: "e > 0" |
|
380 define e'' where "e'' = (SUP t:ball z d. norm t + norm t^2)" |
|
381 define e' where "e' = e / (2*e'')" |
|
382 have "bounded ((\<lambda>t. norm t + norm t^2) ` cball z d)" |
|
383 by (intro compact_imp_bounded compact_continuous_image) (auto intro!: continuous_intros) |
|
384 hence "bounded ((\<lambda>t. norm t + norm t^2) ` ball z d)" by (rule bounded_subset) auto |
|
385 hence bdd: "bdd_above ((\<lambda>t. norm t + norm t^2) ` ball z d)" by (rule bounded_imp_bdd_above) |
|
386 |
|
387 with z d(1) d(2)[of "-1"] have e''_pos: "e'' > 0" unfolding e''_def |
|
388 by (subst less_cSUP_iff) (auto intro!: add_pos_nonneg bexI[of _ z]) |
|
389 have e'': "norm t + norm t^2 \<le> e''" if "t \<in> ball z d" for t unfolding e''_def using that |
|
390 by (rule cSUP_upper[OF _ bdd]) |
|
391 from e z e''_pos have e': "e' > 0" unfolding e'_def |
|
392 by (intro divide_pos_pos mult_pos_pos add_pos_pos) (simp_all add: field_simps) |
|
393 |
|
394 have "summable (\<lambda>k. inverse ((real_of_nat k)^2))" |
|
395 by (rule inverse_power_summable) simp |
|
396 from summable_partial_sum_bound[OF this e'] guess M . note M = this |
|
397 |
|
398 define N where "N = max 2 (max (nat \<lceil>2 * (norm z + d)\<rceil>) M)" |
|
399 { |
|
400 from d have "\<lceil>2 * (cmod z + d)\<rceil> \<ge> \<lceil>0::real\<rceil>" |
|
401 by (intro ceiling_mono mult_nonneg_nonneg add_nonneg_nonneg) simp_all |
|
402 hence "2 * (norm z + d) \<le> of_nat (nat \<lceil>2 * (norm z + d)\<rceil>)" unfolding N_def |
|
403 by (simp_all add: le_of_int_ceiling) |
|
404 also have "... \<le> of_nat N" unfolding N_def |
|
405 by (subst of_nat_le_iff) (rule max.coboundedI2, rule max.cobounded1) |
|
406 finally have "of_nat N \<ge> 2 * (norm z + d)" . |
|
407 moreover have "N \<ge> 2" "N \<ge> M" unfolding N_def by simp_all |
|
408 moreover have "(\<Sum>k=m..n. 1/(of_nat k)\<^sup>2) < e'" if "m \<ge> N" for m n |
|
409 using M[OF order.trans[OF \<open>N \<ge> M\<close> that]] unfolding real_norm_def |
|
410 by (subst (asm) abs_of_nonneg) (auto intro: setsum_nonneg simp: divide_simps) |
|
411 moreover note calculation |
|
412 } note N = this |
|
413 |
|
414 show "\<exists>M. \<forall>t\<in>ball z d. \<forall>m\<ge>M. \<forall>n>m. dist (ln_Gamma_series t m) (ln_Gamma_series t n) < e" |
|
415 unfolding dist_complex_def |
|
416 proof (intro exI[of _ N] ballI allI impI) |
|
417 fix t m n assume t: "t \<in> ball z d" and mn: "m \<ge> N" "n > m" |
|
418 from d(2)[of 0] t have "0 < dist z 0 - dist z t" by (simp add: field_simps dist_complex_def) |
|
419 also have "dist z 0 - dist z t \<le> dist 0 t" using dist_triangle[of 0 z t] |
|
420 by (simp add: dist_commute) |
|
421 finally have t_nz: "t \<noteq> 0" by auto |
|
422 |
|
423 have "norm t \<le> norm z + norm (t - z)" by (rule norm_triangle_sub) |
|
424 also from t have "norm (t - z) < d" by (simp add: dist_complex_def norm_minus_commute) |
|
425 also have "2 * (norm z + d) \<le> of_nat N" by (rule N) |
|
426 also have "N \<le> m" by (rule mn) |
|
427 finally have norm_t: "2 * norm t < of_nat m" by simp |
|
428 |
|
429 have "ln_Gamma_series t m - ln_Gamma_series t n = |
|
430 (-(t * Ln (of_nat n)) - (-(t * Ln (of_nat m)))) + |
|
431 ((\<Sum>k=1..n. Ln (t / of_nat k + 1)) - (\<Sum>k=1..m. Ln (t / of_nat k + 1)))" |
|
432 by (simp add: ln_Gamma_series_def algebra_simps) |
|
433 also have "(\<Sum>k=1..n. Ln (t / of_nat k + 1)) - (\<Sum>k=1..m. Ln (t / of_nat k + 1)) = |
|
434 (\<Sum>k\<in>{1..n}-{1..m}. Ln (t / of_nat k + 1))" using mn |
|
435 by (simp add: setsum_diff) |
|
436 also from mn have "{1..n}-{1..m} = {Suc m..n}" by fastforce |
|
437 also have "-(t * Ln (of_nat n)) - (-(t * Ln (of_nat m))) = |
|
438 (\<Sum>k = Suc m..n. t * Ln (of_nat (k - 1)) - t * Ln (of_nat k))" using mn |
|
439 by (subst setsum_telescope'' [symmetric]) simp_all |
|
440 also have "... = (\<Sum>k = Suc m..n. t * Ln (of_nat (k - 1) / of_nat k))" using mn N |
|
441 by (intro setsum_cong_Suc) |
|
442 (simp_all del: of_nat_Suc add: field_simps Ln_of_nat Ln_of_nat_over_of_nat) |
|
443 also have "of_nat (k - 1) / of_nat k = 1 - 1 / (of_nat k :: complex)" if "k \<in> {Suc m..n}" for k |
|
444 using that of_nat_eq_0_iff[of "Suc i" for i] by (cases k) (simp_all add: divide_simps) |
|
445 hence "(\<Sum>k = Suc m..n. t * Ln (of_nat (k - 1) / of_nat k)) = |
|
446 (\<Sum>k = Suc m..n. t * Ln (1 - 1 / of_nat k))" using mn N |
|
447 by (intro setsum.cong) simp_all |
|
448 also note setsum.distrib [symmetric] |
|
449 also have "norm (\<Sum>k=Suc m..n. t * Ln (1 - 1/of_nat k) + Ln (t/of_nat k + 1)) \<le> |
|
450 (\<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 |
|
451 by (intro order.trans[OF norm_setsum setsum_mono[OF ln_Gamma_series_complex_converges_aux]]) simp_all |
|
452 also have "... \<le> 2 * (norm t + norm t^2) * (\<Sum>k=Suc m..n. 1 / (of_nat k)\<^sup>2)" |
|
453 by (simp add: setsum_right_distrib) |
|
454 also have "... < 2 * (norm t + norm t^2) * e'" using mn z t_nz |
|
455 by (intro mult_strict_left_mono N mult_pos_pos add_pos_pos) simp_all |
|
456 also from e''_pos have "... = e * ((cmod t + (cmod t)\<^sup>2) / e'')" |
|
457 by (simp add: e'_def field_simps power2_eq_square) |
|
458 also from e''[OF t] e''_pos e |
|
459 have "\<dots> \<le> e * 1" by (intro mult_left_mono) (simp_all add: field_simps) |
|
460 finally show "norm (ln_Gamma_series t m - ln_Gamma_series t n) < e" by simp |
|
461 qed |
|
462 qed |
|
463 |
|
464 end |
|
465 |
|
466 lemma ln_Gamma_series_complex_converges': |
|
467 assumes z: "(z :: complex) \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
468 shows "\<exists>d>0. uniformly_convergent_on (ball z d) (\<lambda>n z. ln_Gamma_series z n)" |
|
469 proof - |
|
470 define d' where "d' = Re z" |
|
471 define d where "d = (if d' > 0 then d' / 2 else norm (z - of_int (round d')) / 2)" |
|
472 have "of_int (round d') \<in> \<int>\<^sub>\<le>\<^sub>0" if "d' \<le> 0" using that |
|
473 by (intro nonpos_Ints_of_int) (simp_all add: round_def) |
|
474 with assms have d_pos: "d > 0" unfolding d_def by (force simp: not_less) |
|
475 |
|
476 have "d < cmod (z - of_int n)" if "n \<in> \<int>\<^sub>\<le>\<^sub>0" for n |
|
477 proof (cases "Re z > 0") |
|
478 case True |
|
479 from nonpos_Ints_nonpos[OF that] have n: "n \<le> 0" by simp |
|
480 from True have "d = Re z/2" by (simp add: d_def d'_def) |
|
481 also from n True have "\<dots> < Re (z - of_int n)" by simp |
|
482 also have "\<dots> \<le> norm (z - of_int n)" by (rule complex_Re_le_cmod) |
|
483 finally show ?thesis . |
|
484 next |
|
485 case False |
|
486 with assms nonpos_Ints_of_int[of "round (Re z)"] |
|
487 have "z \<noteq> of_int (round d')" by (auto simp: not_less) |
|
488 with False have "d < norm (z - of_int (round d'))" by (simp add: d_def d'_def) |
|
489 also have "\<dots> \<le> norm (z - of_int n)" unfolding d'_def by (rule round_Re_minimises_norm) |
|
490 finally show ?thesis . |
|
491 qed |
|
492 hence conv: "uniformly_convergent_on (ball z d) (\<lambda>n z. ln_Gamma_series z n)" |
|
493 by (intro ln_Gamma_series_complex_converges d_pos z) simp_all |
|
494 from d_pos conv show ?thesis by blast |
|
495 qed |
|
496 |
|
497 lemma ln_Gamma_series_complex_converges'': "(z :: complex) \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> convergent (ln_Gamma_series z)" |
|
498 by (drule ln_Gamma_series_complex_converges') (auto intro: uniformly_convergent_imp_convergent) |
|
499 |
|
500 lemma ln_Gamma_complex_LIMSEQ: "(z :: complex) \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln_Gamma_series z \<longlonglongrightarrow> ln_Gamma z" |
|
501 using ln_Gamma_series_complex_converges'' by (simp add: convergent_LIMSEQ_iff ln_Gamma_def) |
|
502 |
|
503 lemma exp_ln_Gamma_series_complex: |
|
504 assumes "n > 0" "z \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
505 shows "exp (ln_Gamma_series z n :: complex) = Gamma_series z n" |
|
506 proof - |
|
507 from assms obtain m where m: "n = Suc m" by (cases n) blast |
|
508 from assms have "z \<noteq> 0" by (intro notI) auto |
|
509 with assms have "exp (ln_Gamma_series z n) = |
|
510 (of_nat n) powr z / (z * (\<Prod>k=1..n. exp (Ln (z / of_nat k + 1))))" |
|
511 unfolding ln_Gamma_series_def powr_def by (simp add: exp_diff exp_setsum) |
|
512 also from assms have "(\<Prod>k=1..n. exp (Ln (z / of_nat k + 1))) = (\<Prod>k=1..n. z / of_nat k + 1)" |
|
513 by (intro setprod.cong[OF refl], subst exp_Ln) (auto simp: field_simps plus_of_nat_eq_0_imp) |
|
514 also have "... = (\<Prod>k=1..n. z + k) / fact n" |
|
515 by (simp add: fact_setprod) |
|
516 (subst setprod_dividef [symmetric], simp_all add: field_simps) |
|
517 also from m have "z * ... = (\<Prod>k=0..n. z + k) / fact n" |
|
518 by (simp add: setprod.atLeast0_atMost_Suc_shift setprod.atLeast_Suc_atMost_Suc_shift) |
|
519 also have "(\<Prod>k=0..n. z + k) = pochhammer z (Suc n)" |
|
520 unfolding pochhammer_setprod |
|
521 by (simp add: setprod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost) |
|
522 also have "of_nat n powr z / (pochhammer z (Suc n) / fact n) = Gamma_series z n" |
|
523 unfolding Gamma_series_def using assms by (simp add: divide_simps powr_def Ln_of_nat) |
|
524 finally show ?thesis . |
|
525 qed |
|
526 |
|
527 |
|
528 lemma ln_Gamma_series'_aux: |
|
529 assumes "(z::complex) \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
530 shows "(\<lambda>k. z / of_nat (Suc k) - ln (1 + z / of_nat (Suc k))) sums |
|
531 (ln_Gamma z + euler_mascheroni * z + ln z)" (is "?f sums ?s") |
|
532 unfolding sums_def |
|
533 proof (rule Lim_transform) |
|
534 show "(\<lambda>n. ln_Gamma_series z n + of_real (harm n - ln (of_nat n)) * z + ln z) \<longlonglongrightarrow> ?s" |
|
535 (is "?g \<longlonglongrightarrow> _") |
|
536 by (intro tendsto_intros ln_Gamma_complex_LIMSEQ euler_mascheroni_LIMSEQ_of_real assms) |
|
537 |
|
538 have A: "eventually (\<lambda>n. (\<Sum>k<n. ?f k) - ?g n = 0) sequentially" |
|
539 using eventually_gt_at_top[of "0::nat"] |
|
540 proof eventually_elim |
|
541 fix n :: nat assume n: "n > 0" |
|
542 have "(\<Sum>k<n. ?f k) = (\<Sum>k=1..n. z / of_nat k - ln (1 + z / of_nat k))" |
|
543 by (subst atLeast0LessThan [symmetric], subst setsum_shift_bounds_Suc_ivl [symmetric], |
|
544 subst atLeastLessThanSuc_atLeastAtMost) simp_all |
|
545 also have "\<dots> = z * of_real (harm n) - (\<Sum>k=1..n. ln (1 + z / of_nat k))" |
|
546 by (simp add: harm_def setsum_subtractf setsum_right_distrib divide_inverse) |
|
547 also from n have "\<dots> - ?g n = 0" |
|
548 by (simp add: ln_Gamma_series_def setsum_subtractf algebra_simps Ln_of_nat) |
|
549 finally show "(\<Sum>k<n. ?f k) - ?g n = 0" . |
|
550 qed |
|
551 show "(\<lambda>n. (\<Sum>k<n. ?f k) - ?g n) \<longlonglongrightarrow> 0" by (subst tendsto_cong[OF A]) simp_all |
|
552 qed |
|
553 |
|
554 |
|
555 lemma uniformly_summable_deriv_ln_Gamma: |
|
556 assumes z: "(z :: 'a :: {real_normed_field,banach}) \<noteq> 0" and d: "d > 0" "d \<le> norm z/2" |
|
557 shows "uniformly_convergent_on (ball z d) |
|
558 (\<lambda>k z. \<Sum>i<k. inverse (of_nat (Suc i)) - inverse (z + of_nat (Suc i)))" |
|
559 (is "uniformly_convergent_on _ (\<lambda>k z. \<Sum>i<k. ?f i z)") |
|
560 proof (rule weierstrass_m_test'_ev) |
|
561 { |
|
562 fix t assume t: "t \<in> ball z d" |
|
563 have "norm z = norm (t + (z - t))" by simp |
|
564 have "norm (t + (z - t)) \<le> norm t + norm (z - t)" by (rule norm_triangle_ineq) |
|
565 also from t d have "norm (z - t) < norm z / 2" by (simp add: dist_norm) |
|
566 finally have A: "norm t > norm z / 2" using z by (simp add: field_simps) |
|
567 |
|
568 have "norm t = norm (z + (t - z))" by simp |
|
569 also have "\<dots> \<le> norm z + norm (t - z)" by (rule norm_triangle_ineq) |
|
570 also from t d have "norm (t - z) \<le> norm z / 2" by (simp add: dist_norm norm_minus_commute) |
|
571 also from z have "\<dots> < norm z" by simp |
|
572 finally have B: "norm t < 2 * norm z" by simp |
|
573 note A B |
|
574 } note ball = this |
|
575 |
|
576 show "eventually (\<lambda>n. \<forall>t\<in>ball z d. norm (?f n t) \<le> 4 * norm z * inverse (of_nat (Suc n)^2)) sequentially" |
|
577 using eventually_gt_at_top apply eventually_elim |
|
578 proof safe |
|
579 fix t :: 'a assume t: "t \<in> ball z d" |
|
580 from z ball[OF t] have t_nz: "t \<noteq> 0" by auto |
|
581 fix n :: nat assume n: "n > nat \<lceil>4 * norm z\<rceil>" |
|
582 from ball[OF t] t_nz have "4 * norm z > 2 * norm t" by simp |
|
583 also from n have "\<dots> < of_nat n" by linarith |
|
584 finally have n: "of_nat n > 2 * norm t" . |
|
585 hence "of_nat n > norm t" by simp |
|
586 hence t': "t \<noteq> -of_nat (Suc n)" by (intro notI) (simp del: of_nat_Suc) |
|
587 |
|
588 with t_nz have "?f n t = 1 / (of_nat (Suc n) * (1 + of_nat (Suc n)/t))" |
|
589 by (simp add: divide_simps eq_neg_iff_add_eq_0 del: of_nat_Suc) |
|
590 also have "norm \<dots> = inverse (of_nat (Suc n)) * inverse (norm (of_nat (Suc n)/t + 1))" |
|
591 by (simp add: norm_divide norm_mult divide_simps add_ac del: of_nat_Suc) |
|
592 also { |
|
593 from z t_nz ball[OF t] have "of_nat (Suc n) / (4 * norm z) \<le> of_nat (Suc n) / (2 * norm t)" |
|
594 by (intro divide_left_mono mult_pos_pos) simp_all |
|
595 also have "\<dots> < norm (of_nat (Suc n) / t) - norm (1 :: 'a)" |
|
596 using t_nz n by (simp add: field_simps norm_divide del: of_nat_Suc) |
|
597 also have "\<dots> \<le> norm (of_nat (Suc n)/t + 1)" by (rule norm_diff_ineq) |
|
598 finally have "inverse (norm (of_nat (Suc n)/t + 1)) \<le> 4 * norm z / of_nat (Suc n)" |
|
599 using z by (simp add: divide_simps norm_divide mult_ac del: of_nat_Suc) |
|
600 } |
|
601 also have "inverse (real_of_nat (Suc n)) * (4 * norm z / real_of_nat (Suc n)) = |
|
602 4 * norm z * inverse (of_nat (Suc n)^2)" |
|
603 by (simp add: divide_simps power2_eq_square del: of_nat_Suc) |
|
604 finally show "norm (?f n t) \<le> 4 * norm z * inverse (of_nat (Suc n)^2)" |
|
605 by (simp del: of_nat_Suc) |
|
606 qed |
|
607 next |
|
608 show "summable (\<lambda>n. 4 * norm z * inverse ((of_nat (Suc n))^2))" |
|
609 by (subst summable_Suc_iff) (simp add: summable_mult inverse_power_summable) |
|
610 qed |
|
611 |
|
612 lemma summable_deriv_ln_Gamma: |
|
613 "z \<noteq> (0 :: 'a :: {real_normed_field,banach}) \<Longrightarrow> |
|
614 summable (\<lambda>n. inverse (of_nat (Suc n)) - inverse (z + of_nat (Suc n)))" |
|
615 unfolding summable_iff_convergent |
|
616 by (rule uniformly_convergent_imp_convergent, |
|
617 rule uniformly_summable_deriv_ln_Gamma[of z "norm z/2"]) simp_all |
|
618 |
|
619 |
|
620 definition Polygamma :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a" where |
|
621 "Polygamma n z = (if n = 0 then |
|
622 (\<Sum>k. inverse (of_nat (Suc k)) - inverse (z + of_nat k)) - euler_mascheroni else |
|
623 (-1)^Suc n * fact n * (\<Sum>k. inverse ((z + of_nat k)^Suc n)))" |
|
624 |
|
625 abbreviation Digamma :: "('a :: {real_normed_field,banach}) \<Rightarrow> 'a" where |
|
626 "Digamma \<equiv> Polygamma 0" |
|
627 |
|
628 lemma Digamma_def: |
|
629 "Digamma z = (\<Sum>k. inverse (of_nat (Suc k)) - inverse (z + of_nat k)) - euler_mascheroni" |
|
630 by (simp add: Polygamma_def) |
|
631 |
|
632 |
|
633 lemma summable_Digamma: |
|
634 assumes "(z :: 'a :: {real_normed_field,banach}) \<noteq> 0" |
|
635 shows "summable (\<lambda>n. inverse (of_nat (Suc n)) - inverse (z + of_nat n))" |
|
636 proof - |
|
637 have sums: "(\<lambda>n. inverse (z + of_nat (Suc n)) - inverse (z + of_nat n)) sums |
|
638 (0 - inverse (z + of_nat 0))" |
|
639 by (intro telescope_sums filterlim_compose[OF tendsto_inverse_0] |
|
640 tendsto_add_filterlim_at_infinity[OF tendsto_const] tendsto_of_nat) |
|
641 from summable_add[OF summable_deriv_ln_Gamma[OF assms] sums_summable[OF sums]] |
|
642 show "summable (\<lambda>n. inverse (of_nat (Suc n)) - inverse (z + of_nat n))" by simp |
|
643 qed |
|
644 |
|
645 lemma summable_offset: |
|
646 assumes "summable (\<lambda>n. f (n + k) :: 'a :: real_normed_vector)" |
|
647 shows "summable f" |
|
648 proof - |
|
649 from assms have "convergent (\<lambda>m. \<Sum>n<m. f (n + k))" by (simp add: summable_iff_convergent) |
|
650 hence "convergent (\<lambda>m. (\<Sum>n<k. f n) + (\<Sum>n<m. f (n + k)))" |
|
651 by (intro convergent_add convergent_const) |
|
652 also have "(\<lambda>m. (\<Sum>n<k. f n) + (\<Sum>n<m. f (n + k))) = (\<lambda>m. \<Sum>n<m+k. f n)" |
|
653 proof |
|
654 fix m :: nat |
|
655 have "{..<m+k} = {..<k} \<union> {k..<m+k}" by auto |
|
656 also have "(\<Sum>n\<in>\<dots>. f n) = (\<Sum>n<k. f n) + (\<Sum>n=k..<m+k. f n)" |
|
657 by (rule setsum.union_disjoint) auto |
|
658 also have "(\<Sum>n=k..<m+k. f n) = (\<Sum>n=0..<m+k-k. f (n + k))" |
|
659 by (intro setsum.reindex_cong[of "\<lambda>n. n + k"]) |
|
660 (simp, subst image_add_atLeastLessThan, auto) |
|
661 finally show "(\<Sum>n<k. f n) + (\<Sum>n<m. f (n + k)) = (\<Sum>n<m+k. f n)" by (simp add: atLeast0LessThan) |
|
662 qed |
|
663 finally have "(\<lambda>a. setsum f {..<a}) \<longlonglongrightarrow> lim (\<lambda>m. setsum f {..<m + k})" |
|
664 by (auto simp: convergent_LIMSEQ_iff dest: LIMSEQ_offset) |
|
665 thus ?thesis by (auto simp: summable_iff_convergent convergent_def) |
|
666 qed |
|
667 |
|
668 lemma Polygamma_converges: |
|
669 fixes z :: "'a :: {real_normed_field,banach}" |
|
670 assumes z: "z \<noteq> 0" and n: "n \<ge> 2" |
|
671 shows "uniformly_convergent_on (ball z d) (\<lambda>k z. \<Sum>i<k. inverse ((z + of_nat i)^n))" |
|
672 proof (rule weierstrass_m_test'_ev) |
|
673 define e where "e = (1 + d / norm z)" |
|
674 define m where "m = nat \<lceil>norm z * e\<rceil>" |
|
675 { |
|
676 fix t assume t: "t \<in> ball z d" |
|
677 have "norm t = norm (z + (t - z))" by simp |
|
678 also have "\<dots> \<le> norm z + norm (t - z)" by (rule norm_triangle_ineq) |
|
679 also from t have "norm (t - z) < d" by (simp add: dist_norm norm_minus_commute) |
|
680 finally have "norm t < norm z * e" using z by (simp add: divide_simps e_def) |
|
681 } note ball = this |
|
682 |
|
683 show "eventually (\<lambda>k. \<forall>t\<in>ball z d. norm (inverse ((t + of_nat k)^n)) \<le> |
|
684 inverse (of_nat (k - m)^n)) sequentially" |
|
685 using eventually_gt_at_top[of m] apply eventually_elim |
|
686 proof (intro ballI) |
|
687 fix k :: nat and t :: 'a assume k: "k > m" and t: "t \<in> ball z d" |
|
688 from k have "real_of_nat (k - m) = of_nat k - of_nat m" by (simp add: of_nat_diff) |
|
689 also have "\<dots> \<le> norm (of_nat k :: 'a) - norm z * e" |
|
690 unfolding m_def by (subst norm_of_nat) linarith |
|
691 also from ball[OF t] have "\<dots> \<le> norm (of_nat k :: 'a) - norm t" by simp |
|
692 also have "\<dots> \<le> norm (of_nat k + t)" by (rule norm_diff_ineq) |
|
693 finally have "inverse ((norm (t + of_nat k))^n) \<le> inverse (real_of_nat (k - m)^n)" using k n |
|
694 by (intro le_imp_inverse_le power_mono) (simp_all add: add_ac del: of_nat_Suc) |
|
695 thus "norm (inverse ((t + of_nat k)^n)) \<le> inverse (of_nat (k - m)^n)" |
|
696 by (simp add: norm_inverse norm_power power_inverse) |
|
697 qed |
|
698 |
|
699 have "summable (\<lambda>k. inverse ((real_of_nat k)^n))" |
|
700 using inverse_power_summable[of n] n by simp |
|
701 hence "summable (\<lambda>k. inverse ((real_of_nat (k + m - m))^n))" by simp |
|
702 thus "summable (\<lambda>k. inverse ((real_of_nat (k - m))^n))" by (rule summable_offset) |
|
703 qed |
|
704 |
|
705 lemma Polygamma_converges': |
|
706 fixes z :: "'a :: {real_normed_field,banach}" |
|
707 assumes z: "z \<noteq> 0" and n: "n \<ge> 2" |
|
708 shows "summable (\<lambda>k. inverse ((z + of_nat k)^n))" |
|
709 using uniformly_convergent_imp_convergent[OF Polygamma_converges[OF assms, of 1], of z] |
|
710 by (simp add: summable_iff_convergent) |
|
711 |
|
712 lemma has_field_derivative_ln_Gamma_complex [derivative_intros]: |
|
713 fixes z :: complex |
|
714 assumes z: "z \<notin> \<real>\<^sub>\<le>\<^sub>0" |
|
715 shows "(ln_Gamma has_field_derivative Digamma z) (at z)" |
|
716 proof - |
|
717 have not_nonpos_Int [simp]: "t \<notin> \<int>\<^sub>\<le>\<^sub>0" if "Re t > 0" for t |
|
718 using that by (auto elim!: nonpos_Ints_cases') |
|
719 from z have z': "z \<notin> \<int>\<^sub>\<le>\<^sub>0" and z'': "z \<noteq> 0" using nonpos_Ints_subset_nonpos_Reals nonpos_Reals_zero_I |
|
720 by blast+ |
|
721 let ?f' = "\<lambda>z k. inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))" |
|
722 let ?f = "\<lambda>z k. z / of_nat (Suc k) - ln (1 + z / of_nat (Suc k))" and ?F' = "\<lambda>z. \<Sum>n. ?f' z n" |
|
723 define d where "d = min (norm z/2) (if Im z = 0 then Re z / 2 else abs (Im z) / 2)" |
|
724 from z have d: "d > 0" "norm z/2 \<ge> d" by (auto simp add: complex_nonpos_Reals_iff d_def) |
|
725 have ball: "Im t = 0 \<longrightarrow> Re t > 0" if "dist z t < d" for t |
|
726 using no_nonpos_Real_in_ball[OF z, of t] that unfolding d_def by (force simp add: complex_nonpos_Reals_iff) |
|
727 have sums: "(\<lambda>n. inverse (z + of_nat (Suc n)) - inverse (z + of_nat n)) sums |
|
728 (0 - inverse (z + of_nat 0))" |
|
729 by (intro telescope_sums filterlim_compose[OF tendsto_inverse_0] |
|
730 tendsto_add_filterlim_at_infinity[OF tendsto_const] tendsto_of_nat) |
|
731 |
|
732 have "((\<lambda>z. \<Sum>n. ?f z n) has_field_derivative ?F' z) (at z)" |
|
733 using d z ln_Gamma_series'_aux[OF z'] |
|
734 apply (intro has_field_derivative_series'(2)[of "ball z d" _ _ z] uniformly_summable_deriv_ln_Gamma) |
|
735 apply (auto intro!: derivative_eq_intros add_pos_pos mult_pos_pos dest!: ball |
|
736 simp: field_simps sums_iff nonpos_Reals_divide_of_nat_iff |
|
737 simp del: of_nat_Suc) |
|
738 apply (auto simp add: complex_nonpos_Reals_iff) |
|
739 done |
|
740 with z have "((\<lambda>z. (\<Sum>k. ?f z k) - euler_mascheroni * z - Ln z) has_field_derivative |
|
741 ?F' z - euler_mascheroni - inverse z) (at z)" |
|
742 by (force intro!: derivative_eq_intros simp: Digamma_def) |
|
743 also have "?F' z - euler_mascheroni - inverse z = (?F' z + -inverse z) - euler_mascheroni" by simp |
|
744 also from sums have "-inverse z = (\<Sum>n. inverse (z + of_nat (Suc n)) - inverse (z + of_nat n))" |
|
745 by (simp add: sums_iff) |
|
746 also from sums summable_deriv_ln_Gamma[OF z''] |
|
747 have "?F' z + \<dots> = (\<Sum>n. inverse (of_nat (Suc n)) - inverse (z + of_nat n))" |
|
748 by (subst suminf_add) (simp_all add: add_ac sums_iff) |
|
749 also have "\<dots> - euler_mascheroni = Digamma z" by (simp add: Digamma_def) |
|
750 finally have "((\<lambda>z. (\<Sum>k. ?f z k) - euler_mascheroni * z - Ln z) |
|
751 has_field_derivative Digamma z) (at z)" . |
|
752 moreover from eventually_nhds_ball[OF d(1), of z] |
|
753 have "eventually (\<lambda>z. ln_Gamma z = (\<Sum>k. ?f z k) - euler_mascheroni * z - Ln z) (nhds z)" |
|
754 proof eventually_elim |
|
755 fix t assume "t \<in> ball z d" |
|
756 hence "t \<notin> \<int>\<^sub>\<le>\<^sub>0" by (auto dest!: ball elim!: nonpos_Ints_cases) |
|
757 from ln_Gamma_series'_aux[OF this] |
|
758 show "ln_Gamma t = (\<Sum>k. ?f t k) - euler_mascheroni * t - Ln t" by (simp add: sums_iff) |
|
759 qed |
|
760 ultimately show ?thesis by (subst DERIV_cong_ev[OF refl _ refl]) |
|
761 qed |
|
762 |
|
763 declare has_field_derivative_ln_Gamma_complex[THEN DERIV_chain2, derivative_intros] |
|
764 |
|
765 |
|
766 lemma Digamma_1 [simp]: "Digamma (1 :: 'a :: {real_normed_field,banach}) = - euler_mascheroni" |
|
767 by (simp add: Digamma_def) |
|
768 |
|
769 lemma Digamma_plus1: |
|
770 assumes "z \<noteq> 0" |
|
771 shows "Digamma (z+1) = Digamma z + 1/z" |
|
772 proof - |
|
773 have sums: "(\<lambda>k. inverse (z + of_nat k) - inverse (z + of_nat (Suc k))) |
|
774 sums (inverse (z + of_nat 0) - 0)" |
|
775 by (intro telescope_sums'[OF filterlim_compose[OF tendsto_inverse_0]] |
|
776 tendsto_add_filterlim_at_infinity[OF tendsto_const] tendsto_of_nat) |
|
777 have "Digamma (z+1) = (\<Sum>k. inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) - |
|
778 euler_mascheroni" (is "_ = suminf ?f - _") by (simp add: Digamma_def add_ac) |
|
779 also have "suminf ?f = (\<Sum>k. inverse (of_nat (Suc k)) - inverse (z + of_nat k)) + |
|
780 (\<Sum>k. inverse (z + of_nat k) - inverse (z + of_nat (Suc k)))" |
|
781 using summable_Digamma[OF assms] sums by (subst suminf_add) (simp_all add: add_ac sums_iff) |
|
782 also have "(\<Sum>k. inverse (z + of_nat k) - inverse (z + of_nat (Suc k))) = 1/z" |
|
783 using sums by (simp add: sums_iff inverse_eq_divide) |
|
784 finally show ?thesis by (simp add: Digamma_def[of z]) |
|
785 qed |
|
786 |
|
787 lemma Polygamma_plus1: |
|
788 assumes "z \<noteq> 0" |
|
789 shows "Polygamma n (z + 1) = Polygamma n z + (-1)^n * fact n / (z ^ Suc n)" |
|
790 proof (cases "n = 0") |
|
791 assume n: "n \<noteq> 0" |
|
792 let ?f = "\<lambda>k. inverse ((z + of_nat k) ^ Suc n)" |
|
793 have "Polygamma n (z + 1) = (-1) ^ Suc n * fact n * (\<Sum>k. ?f (k+1))" |
|
794 using n by (simp add: Polygamma_def add_ac) |
|
795 also have "(\<Sum>k. ?f (k+1)) + (\<Sum>k<1. ?f k) = (\<Sum>k. ?f k)" |
|
796 using Polygamma_converges'[OF assms, of "Suc n"] n |
|
797 by (subst suminf_split_initial_segment [symmetric]) simp_all |
|
798 hence "(\<Sum>k. ?f (k+1)) = (\<Sum>k. ?f k) - inverse (z ^ Suc n)" by (simp add: algebra_simps) |
|
799 also have "(-1) ^ Suc n * fact n * ((\<Sum>k. ?f k) - inverse (z ^ Suc n)) = |
|
800 Polygamma n z + (-1)^n * fact n / (z ^ Suc n)" using n |
|
801 by (simp add: inverse_eq_divide algebra_simps Polygamma_def) |
|
802 finally show ?thesis . |
|
803 qed (insert assms, simp add: Digamma_plus1 inverse_eq_divide) |
|
804 |
|
805 lemma Digamma_of_nat: |
|
806 "Digamma (of_nat (Suc n) :: 'a :: {real_normed_field,banach}) = harm n - euler_mascheroni" |
|
807 proof (induction n) |
|
808 case (Suc n) |
|
809 have "Digamma (of_nat (Suc (Suc n)) :: 'a) = Digamma (of_nat (Suc n) + 1)" by simp |
|
810 also have "\<dots> = Digamma (of_nat (Suc n)) + inverse (of_nat (Suc n))" |
|
811 by (subst Digamma_plus1) (simp_all add: inverse_eq_divide del: of_nat_Suc) |
|
812 also have "Digamma (of_nat (Suc n) :: 'a) = harm n - euler_mascheroni " by (rule Suc) |
|
813 also have "\<dots> + inverse (of_nat (Suc n)) = harm (Suc n) - euler_mascheroni" |
|
814 by (simp add: harm_Suc) |
|
815 finally show ?case . |
|
816 qed (simp add: harm_def) |
|
817 |
|
818 lemma Digamma_numeral: "Digamma (numeral n) = harm (pred_numeral n) - euler_mascheroni" |
|
819 by (subst of_nat_numeral[symmetric], subst numeral_eq_Suc, subst Digamma_of_nat) (rule refl) |
|
820 |
|
821 lemma Polygamma_of_real: "x \<noteq> 0 \<Longrightarrow> Polygamma n (of_real x) = of_real (Polygamma n x)" |
|
822 unfolding Polygamma_def using summable_Digamma[of x] Polygamma_converges'[of x "Suc n"] |
|
823 by (simp_all add: suminf_of_real) |
|
824 |
|
825 lemma Polygamma_Real: "z \<in> \<real> \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> Polygamma n z \<in> \<real>" |
|
826 by (elim Reals_cases, hypsubst, subst Polygamma_of_real) simp_all |
|
827 |
|
828 lemma Digamma_half_integer: |
|
829 "Digamma (of_nat n + 1/2 :: 'a :: {real_normed_field,banach}) = |
|
830 (\<Sum>k<n. 2 / (of_nat (2*k+1))) - euler_mascheroni - of_real (2 * ln 2)" |
|
831 proof (induction n) |
|
832 case 0 |
|
833 have "Digamma (1/2 :: 'a) = of_real (Digamma (1/2))" by (simp add: Polygamma_of_real [symmetric]) |
|
834 also have "Digamma (1/2::real) = |
|
835 (\<Sum>k. inverse (of_nat (Suc k)) - inverse (of_nat k + 1/2)) - euler_mascheroni" |
|
836 by (simp add: Digamma_def add_ac) |
|
837 also have "(\<Sum>k. inverse (of_nat (Suc k) :: real) - inverse (of_nat k + 1/2)) = |
|
838 (\<Sum>k. inverse (1/2) * (inverse (2 * of_nat (Suc k)) - inverse (2 * of_nat k + 1)))" |
|
839 by (simp_all add: add_ac inverse_mult_distrib[symmetric] ring_distribs del: inverse_divide) |
|
840 also have "\<dots> = - 2 * ln 2" using sums_minus[OF alternating_harmonic_series_sums'] |
|
841 by (subst suminf_mult) (simp_all add: algebra_simps sums_iff) |
|
842 finally show ?case by simp |
|
843 next |
|
844 case (Suc n) |
|
845 have nz: "2 * of_nat n + (1:: 'a) \<noteq> 0" |
|
846 using of_nat_neq_0[of "2*n"] by (simp only: of_nat_Suc) (simp add: add_ac) |
|
847 hence nz': "of_nat n + (1/2::'a) \<noteq> 0" by (simp add: field_simps) |
|
848 have "Digamma (of_nat (Suc n) + 1/2 :: 'a) = Digamma (of_nat n + 1/2 + 1)" by simp |
|
849 also from nz' have "\<dots> = Digamma (of_nat n + 1 / 2) + 1 / (of_nat n + 1 / 2)" |
|
850 by (rule Digamma_plus1) |
|
851 also from nz nz' have "1 / (of_nat n + 1 / 2 :: 'a) = 2 / (2 * of_nat n + 1)" |
|
852 by (subst divide_eq_eq) simp_all |
|
853 also note Suc |
|
854 finally show ?case by (simp add: add_ac) |
|
855 qed |
|
856 |
|
857 lemma Digamma_one_half: "Digamma (1/2) = - euler_mascheroni - of_real (2 * ln 2)" |
|
858 using Digamma_half_integer[of 0] by simp |
|
859 |
|
860 lemma Digamma_real_three_halves_pos: "Digamma (3/2 :: real) > 0" |
|
861 proof - |
|
862 have "-Digamma (3/2 :: real) = -Digamma (of_nat 1 + 1/2)" by simp |
|
863 also have "\<dots> = 2 * ln 2 + euler_mascheroni - 2" by (subst Digamma_half_integer) simp |
|
864 also note euler_mascheroni_less_13_over_22 |
|
865 also note ln2_le_25_over_36 |
|
866 finally show ?thesis by simp |
|
867 qed |
|
868 |
|
869 |
|
870 lemma has_field_derivative_Polygamma [derivative_intros]: |
|
871 fixes z :: "'a :: {real_normed_field,euclidean_space}" |
|
872 assumes z: "z \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
873 shows "(Polygamma n has_field_derivative Polygamma (Suc n) z) (at z within A)" |
|
874 proof (rule has_field_derivative_at_within, cases "n = 0") |
|
875 assume n: "n = 0" |
|
876 let ?f = "\<lambda>k z. inverse (of_nat (Suc k)) - inverse (z + of_nat k)" |
|
877 let ?F = "\<lambda>z. \<Sum>k. ?f k z" and ?f' = "\<lambda>k z. inverse ((z + of_nat k)\<^sup>2)" |
|
878 from no_nonpos_Int_in_ball'[OF z] guess d . note d = this |
|
879 from z have summable: "summable (\<lambda>k. inverse (of_nat (Suc k)) - inverse (z + of_nat k))" |
|
880 by (intro summable_Digamma) force |
|
881 from z have conv: "uniformly_convergent_on (ball z d) (\<lambda>k z. \<Sum>i<k. inverse ((z + of_nat i)\<^sup>2))" |
|
882 by (intro Polygamma_converges) auto |
|
883 with d have "summable (\<lambda>k. inverse ((z + of_nat k)\<^sup>2))" unfolding summable_iff_convergent |
|
884 by (auto dest!: uniformly_convergent_imp_convergent simp: summable_iff_convergent ) |
|
885 |
|
886 have "(?F has_field_derivative (\<Sum>k. ?f' k z)) (at z)" |
|
887 proof (rule has_field_derivative_series'[of "ball z d" _ _ z]) |
|
888 fix k :: nat and t :: 'a assume t: "t \<in> ball z d" |
|
889 from t d(2)[of t] show "((\<lambda>z. ?f k z) has_field_derivative ?f' k t) (at t within ball z d)" |
|
890 by (auto intro!: derivative_eq_intros simp: power2_eq_square simp del: of_nat_Suc |
|
891 dest!: plus_of_nat_eq_0_imp elim!: nonpos_Ints_cases) |
|
892 qed (insert d(1) summable conv, (assumption|simp)+) |
|
893 with z show "(Polygamma n has_field_derivative Polygamma (Suc n) z) (at z)" |
|
894 unfolding Digamma_def [abs_def] Polygamma_def [abs_def] using n |
|
895 by (force simp: power2_eq_square intro!: derivative_eq_intros) |
|
896 next |
|
897 assume n: "n \<noteq> 0" |
|
898 from z have z': "z \<noteq> 0" by auto |
|
899 from no_nonpos_Int_in_ball'[OF z] guess d . note d = this |
|
900 define n' where "n' = Suc n" |
|
901 from n have n': "n' \<ge> 2" by (simp add: n'_def) |
|
902 have "((\<lambda>z. \<Sum>k. inverse ((z + of_nat k) ^ n')) has_field_derivative |
|
903 (\<Sum>k. - of_nat n' * inverse ((z + of_nat k) ^ (n'+1)))) (at z)" |
|
904 proof (rule has_field_derivative_series'[of "ball z d" _ _ z]) |
|
905 fix k :: nat and t :: 'a assume t: "t \<in> ball z d" |
|
906 with d have t': "t \<notin> \<int>\<^sub>\<le>\<^sub>0" "t \<noteq> 0" by auto |
|
907 show "((\<lambda>a. inverse ((a + of_nat k) ^ n')) has_field_derivative |
|
908 - of_nat n' * inverse ((t + of_nat k) ^ (n'+1))) (at t within ball z d)" using t' |
|
909 by (fastforce intro!: derivative_eq_intros simp: divide_simps power_diff dest: plus_of_nat_eq_0_imp) |
|
910 next |
|
911 have "uniformly_convergent_on (ball z d) |
|
912 (\<lambda>k z. (- of_nat n' :: 'a) * (\<Sum>i<k. inverse ((z + of_nat i) ^ (n'+1))))" |
|
913 using z' n by (intro uniformly_convergent_mult Polygamma_converges) (simp_all add: n'_def) |
|
914 thus "uniformly_convergent_on (ball z d) |
|
915 (\<lambda>k z. \<Sum>i<k. - of_nat n' * inverse ((z + of_nat i :: 'a) ^ (n'+1)))" |
|
916 by (subst (asm) setsum_right_distrib) simp |
|
917 qed (insert Polygamma_converges'[OF z' n'] d, simp_all) |
|
918 also have "(\<Sum>k. - of_nat n' * inverse ((z + of_nat k) ^ (n' + 1))) = |
|
919 (- of_nat n') * (\<Sum>k. inverse ((z + of_nat k) ^ (n' + 1)))" |
|
920 using Polygamma_converges'[OF z', of "n'+1"] n' by (subst suminf_mult) simp_all |
|
921 finally have "((\<lambda>z. \<Sum>k. inverse ((z + of_nat k) ^ n')) has_field_derivative |
|
922 - of_nat n' * (\<Sum>k. inverse ((z + of_nat k) ^ (n' + 1)))) (at z)" . |
|
923 from DERIV_cmult[OF this, of "(-1)^Suc n * fact n :: 'a"] |
|
924 show "(Polygamma n has_field_derivative Polygamma (Suc n) z) (at z)" |
|
925 unfolding n'_def Polygamma_def[abs_def] using n by (simp add: algebra_simps) |
|
926 qed |
|
927 |
|
928 declare has_field_derivative_Polygamma[THEN DERIV_chain2, derivative_intros] |
|
929 |
|
930 lemma isCont_Polygamma [continuous_intros]: |
|
931 fixes f :: "_ \<Rightarrow> 'a :: {real_normed_field,euclidean_space}" |
|
932 shows "isCont f z \<Longrightarrow> f z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> isCont (\<lambda>x. Polygamma n (f x)) z" |
|
933 by (rule isCont_o2[OF _ DERIV_isCont[OF has_field_derivative_Polygamma]]) |
|
934 |
|
935 lemma continuous_on_Polygamma: |
|
936 "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> continuous_on A (Polygamma n :: _ \<Rightarrow> 'a :: {real_normed_field,euclidean_space})" |
|
937 by (intro continuous_at_imp_continuous_on isCont_Polygamma[OF continuous_ident] ballI) blast |
|
938 |
|
939 lemma isCont_ln_Gamma_complex [continuous_intros]: |
|
940 fixes f :: "'a::t2_space \<Rightarrow> complex" |
|
941 shows "isCont f z \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> isCont (\<lambda>z. ln_Gamma (f z)) z" |
|
942 by (rule isCont_o2[OF _ DERIV_isCont[OF has_field_derivative_ln_Gamma_complex]]) |
|
943 |
|
944 lemma continuous_on_ln_Gamma_complex [continuous_intros]: |
|
945 fixes A :: "complex set" |
|
946 shows "A \<inter> \<real>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> continuous_on A ln_Gamma" |
|
947 by (intro continuous_at_imp_continuous_on ballI isCont_ln_Gamma_complex[OF continuous_ident]) |
|
948 fastforce |
|
949 |
|
950 text \<open> |
|
951 We define a type class that captures all the fundamental properties of the inverse of the Gamma function |
|
952 and defines the Gamma function upon that. This allows us to instantiate the type class both for |
|
953 the reals and for the complex numbers with a minimal amount of proof duplication. |
|
954 \<close> |
|
955 |
|
956 class Gamma = real_normed_field + complete_space + |
|
957 fixes rGamma :: "'a \<Rightarrow> 'a" |
|
958 assumes rGamma_eq_zero_iff_aux: "rGamma z = 0 \<longleftrightarrow> (\<exists>n. z = - of_nat n)" |
|
959 assumes differentiable_rGamma_aux1: |
|
960 "(\<And>n. z \<noteq> - of_nat n) \<Longrightarrow> |
|
961 let d = (THE d. (\<lambda>n. \<Sum>k<n. inverse (of_nat (Suc k)) - inverse (z + of_nat k)) |
|
962 \<longlonglongrightarrow> d) - scaleR euler_mascheroni 1 |
|
963 in filterlim (\<lambda>y. (rGamma y - rGamma z + rGamma z * d * (y - z)) /\<^sub>R |
|
964 norm (y - z)) (nhds 0) (at z)" |
|
965 assumes differentiable_rGamma_aux2: |
|
966 "let z = - of_nat n |
|
967 in filterlim (\<lambda>y. (rGamma y - rGamma z - (-1)^n * (setprod of_nat {1..n}) * (y - z)) /\<^sub>R |
|
968 norm (y - z)) (nhds 0) (at z)" |
|
969 assumes rGamma_series_aux: "(\<And>n. z \<noteq> - of_nat n) \<Longrightarrow> |
|
970 let fact' = (\<lambda>n. setprod of_nat {1..n}); |
|
971 exp = (\<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x^k /\<^sub>R fact k) \<longlonglongrightarrow> e); |
|
972 pochhammer' = (\<lambda>a n. (\<Prod>n = 0..n. a + of_nat n)) |
|
973 in filterlim (\<lambda>n. pochhammer' z n / (fact' n * exp (z * (ln (of_nat n) *\<^sub>R 1)))) |
|
974 (nhds (rGamma z)) sequentially" |
|
975 begin |
|
976 subclass banach .. |
|
977 end |
|
978 |
|
979 definition "Gamma z = inverse (rGamma z)" |
|
980 |
|
981 |
|
982 subsection \<open>Basic properties\<close> |
|
983 |
|
984 lemma Gamma_nonpos_Int: "z \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Gamma z = 0" |
|
985 and rGamma_nonpos_Int: "z \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma z = 0" |
|
986 using rGamma_eq_zero_iff_aux[of z] unfolding Gamma_def by (auto elim!: nonpos_Ints_cases') |
|
987 |
|
988 lemma Gamma_nonzero: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Gamma z \<noteq> 0" |
|
989 and rGamma_nonzero: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma z \<noteq> 0" |
|
990 using rGamma_eq_zero_iff_aux[of z] unfolding Gamma_def by (auto elim!: nonpos_Ints_cases') |
|
991 |
|
992 lemma Gamma_eq_zero_iff: "Gamma z = 0 \<longleftrightarrow> z \<in> \<int>\<^sub>\<le>\<^sub>0" |
|
993 and rGamma_eq_zero_iff: "rGamma z = 0 \<longleftrightarrow> z \<in> \<int>\<^sub>\<le>\<^sub>0" |
|
994 using rGamma_eq_zero_iff_aux[of z] unfolding Gamma_def by (auto elim!: nonpos_Ints_cases') |
|
995 |
|
996 lemma rGamma_inverse_Gamma: "rGamma z = inverse (Gamma z)" |
|
997 unfolding Gamma_def by simp |
|
998 |
|
999 lemma rGamma_series_LIMSEQ [tendsto_intros]: |
|
1000 "rGamma_series z \<longlonglongrightarrow> rGamma z" |
|
1001 proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0") |
|
1002 case False |
|
1003 hence "z \<noteq> - of_nat n" for n by auto |
|
1004 from rGamma_series_aux[OF this] show ?thesis |
|
1005 by (simp add: rGamma_series_def[abs_def] fact_setprod pochhammer_Suc_setprod |
|
1006 exp_def of_real_def[symmetric] suminf_def sums_def[abs_def] atLeast0AtMost) |
|
1007 qed (insert rGamma_eq_zero_iff[of z], simp_all add: rGamma_series_nonpos_Ints_LIMSEQ) |
|
1008 |
|
1009 lemma Gamma_series_LIMSEQ [tendsto_intros]: |
|
1010 "Gamma_series z \<longlonglongrightarrow> Gamma z" |
|
1011 proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0") |
|
1012 case False |
|
1013 hence "(\<lambda>n. inverse (rGamma_series z n)) \<longlonglongrightarrow> inverse (rGamma z)" |
|
1014 by (intro tendsto_intros) (simp_all add: rGamma_eq_zero_iff) |
|
1015 also have "(\<lambda>n. inverse (rGamma_series z n)) = Gamma_series z" |
|
1016 by (simp add: rGamma_series_def Gamma_series_def[abs_def]) |
|
1017 finally show ?thesis by (simp add: Gamma_def) |
|
1018 qed (insert Gamma_eq_zero_iff[of z], simp_all add: Gamma_series_nonpos_Ints_LIMSEQ) |
|
1019 |
|
1020 lemma Gamma_altdef: "Gamma z = lim (Gamma_series z)" |
|
1021 using Gamma_series_LIMSEQ[of z] by (simp add: limI) |
|
1022 |
|
1023 lemma rGamma_1 [simp]: "rGamma 1 = 1" |
|
1024 proof - |
|
1025 have A: "eventually (\<lambda>n. rGamma_series 1 n = of_nat (Suc n) / of_nat n) sequentially" |
|
1026 using eventually_gt_at_top[of "0::nat"] |
|
1027 by (force elim!: eventually_mono simp: rGamma_series_def exp_of_real pochhammer_fact |
|
1028 divide_simps pochhammer_rec' dest!: pochhammer_eq_0_imp_nonpos_Int) |
|
1029 have "rGamma_series 1 \<longlonglongrightarrow> 1" by (subst tendsto_cong[OF A]) (rule LIMSEQ_Suc_n_over_n) |
|
1030 moreover have "rGamma_series 1 \<longlonglongrightarrow> rGamma 1" by (rule tendsto_intros) |
|
1031 ultimately show ?thesis by (intro LIMSEQ_unique) |
|
1032 qed |
|
1033 |
|
1034 lemma rGamma_plus1: "z * rGamma (z + 1) = rGamma z" |
|
1035 proof - |
|
1036 let ?f = "\<lambda>n. (z + 1) * inverse (of_nat n) + 1" |
|
1037 have "eventually (\<lambda>n. ?f n * rGamma_series z n = z * rGamma_series (z + 1) n) sequentially" |
|
1038 using eventually_gt_at_top[of "0::nat"] |
|
1039 proof eventually_elim |
|
1040 fix n :: nat assume n: "n > 0" |
|
1041 hence "z * rGamma_series (z + 1) n = inverse (of_nat n) * |
|
1042 pochhammer z (Suc (Suc n)) / (fact n * exp (z * of_real (ln (of_nat n))))" |
|
1043 by (subst pochhammer_rec) (simp add: rGamma_series_def field_simps exp_add exp_of_real) |
|
1044 also from n have "\<dots> = ?f n * rGamma_series z n" |
|
1045 by (subst pochhammer_rec') (simp_all add: divide_simps rGamma_series_def add_ac) |
|
1046 finally show "?f n * rGamma_series z n = z * rGamma_series (z + 1) n" .. |
|
1047 qed |
|
1048 moreover have "(\<lambda>n. ?f n * rGamma_series z n) \<longlonglongrightarrow> ((z+1) * 0 + 1) * rGamma z" |
|
1049 by (intro tendsto_intros lim_inverse_n) |
|
1050 hence "(\<lambda>n. ?f n * rGamma_series z n) \<longlonglongrightarrow> rGamma z" by simp |
|
1051 ultimately have "(\<lambda>n. z * rGamma_series (z + 1) n) \<longlonglongrightarrow> rGamma z" |
|
1052 by (rule Lim_transform_eventually) |
|
1053 moreover have "(\<lambda>n. z * rGamma_series (z + 1) n) \<longlonglongrightarrow> z * rGamma (z + 1)" |
|
1054 by (intro tendsto_intros) |
|
1055 ultimately show "z * rGamma (z + 1) = rGamma z" using LIMSEQ_unique by blast |
|
1056 qed |
|
1057 |
|
1058 |
|
1059 lemma pochhammer_rGamma: "rGamma z = pochhammer z n * rGamma (z + of_nat n)" |
|
1060 proof (induction n arbitrary: z) |
|
1061 case (Suc n z) |
|
1062 have "rGamma z = pochhammer z n * rGamma (z + of_nat n)" by (rule Suc.IH) |
|
1063 also note rGamma_plus1 [symmetric] |
|
1064 finally show ?case by (simp add: add_ac pochhammer_rec') |
|
1065 qed simp_all |
|
1066 |
|
1067 lemma Gamma_plus1: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Gamma (z + 1) = z * Gamma z" |
|
1068 using rGamma_plus1[of z] by (simp add: rGamma_inverse_Gamma field_simps Gamma_eq_zero_iff) |
|
1069 |
|
1070 lemma pochhammer_Gamma: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> pochhammer z n = Gamma (z + of_nat n) / Gamma z" |
|
1071 using pochhammer_rGamma[of z] |
|
1072 by (simp add: rGamma_inverse_Gamma Gamma_eq_zero_iff field_simps) |
|
1073 |
|
1074 lemma Gamma_0 [simp]: "Gamma 0 = 0" |
|
1075 and rGamma_0 [simp]: "rGamma 0 = 0" |
|
1076 and Gamma_neg_1 [simp]: "Gamma (- 1) = 0" |
|
1077 and rGamma_neg_1 [simp]: "rGamma (- 1) = 0" |
|
1078 and Gamma_neg_numeral [simp]: "Gamma (- numeral n) = 0" |
|
1079 and rGamma_neg_numeral [simp]: "rGamma (- numeral n) = 0" |
|
1080 and Gamma_neg_of_nat [simp]: "Gamma (- of_nat m) = 0" |
|
1081 and rGamma_neg_of_nat [simp]: "rGamma (- of_nat m) = 0" |
|
1082 by (simp_all add: rGamma_eq_zero_iff Gamma_eq_zero_iff) |
|
1083 |
|
1084 lemma Gamma_1 [simp]: "Gamma 1 = 1" unfolding Gamma_def by simp |
|
1085 |
|
1086 lemma Gamma_fact: "Gamma (1 + of_nat n) = fact n" |
|
1087 by (simp add: pochhammer_fact pochhammer_Gamma of_nat_in_nonpos_Ints_iff |
|
1088 of_nat_Suc [symmetric] del: of_nat_Suc) |
|
1089 |
|
1090 lemma Gamma_numeral: "Gamma (numeral n) = fact (pred_numeral n)" |
|
1091 by (subst of_nat_numeral[symmetric], subst numeral_eq_Suc, |
|
1092 subst of_nat_Suc, subst Gamma_fact) (rule refl) |
|
1093 |
|
1094 lemma Gamma_of_int: "Gamma (of_int n) = (if n > 0 then fact (nat (n - 1)) else 0)" |
|
1095 proof (cases "n > 0") |
|
1096 case True |
|
1097 hence "Gamma (of_int n) = Gamma (of_nat (Suc (nat (n - 1))))" by (subst of_nat_Suc) simp_all |
|
1098 with True show ?thesis by (subst (asm) of_nat_Suc, subst (asm) Gamma_fact) simp |
|
1099 qed (simp_all add: Gamma_eq_zero_iff nonpos_Ints_of_int) |
|
1100 |
|
1101 lemma rGamma_of_int: "rGamma (of_int n) = (if n > 0 then inverse (fact (nat (n - 1))) else 0)" |
|
1102 by (simp add: Gamma_of_int rGamma_inverse_Gamma) |
|
1103 |
|
1104 lemma Gamma_seriesI: |
|
1105 assumes "(\<lambda>n. g n / Gamma_series z n) \<longlonglongrightarrow> 1" |
|
1106 shows "g \<longlonglongrightarrow> Gamma z" |
|
1107 proof (rule Lim_transform_eventually) |
|
1108 have "1/2 > (0::real)" by simp |
|
1109 from tendstoD[OF assms, OF this] |
|
1110 show "eventually (\<lambda>n. g n / Gamma_series z n * Gamma_series z n = g n) sequentially" |
|
1111 by (force elim!: eventually_mono simp: dist_real_def dist_0_norm) |
|
1112 from assms have "(\<lambda>n. g n / Gamma_series z n * Gamma_series z n) \<longlonglongrightarrow> 1 * Gamma z" |
|
1113 by (intro tendsto_intros) |
|
1114 thus "(\<lambda>n. g n / Gamma_series z n * Gamma_series z n) \<longlonglongrightarrow> Gamma z" by simp |
|
1115 qed |
|
1116 |
|
1117 lemma Gamma_seriesI': |
|
1118 assumes "f \<longlonglongrightarrow> rGamma z" |
|
1119 assumes "(\<lambda>n. g n * f n) \<longlonglongrightarrow> 1" |
|
1120 assumes "z \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
1121 shows "g \<longlonglongrightarrow> Gamma z" |
|
1122 proof (rule Lim_transform_eventually) |
|
1123 have "1/2 > (0::real)" by simp |
|
1124 from tendstoD[OF assms(2), OF this] show "eventually (\<lambda>n. g n * f n / f n = g n) sequentially" |
|
1125 by (force elim!: eventually_mono simp: dist_real_def dist_0_norm) |
|
1126 from assms have "(\<lambda>n. g n * f n / f n) \<longlonglongrightarrow> 1 / rGamma z" |
|
1127 by (intro tendsto_divide assms) (simp_all add: rGamma_eq_zero_iff) |
|
1128 thus "(\<lambda>n. g n * f n / f n) \<longlonglongrightarrow> Gamma z" by (simp add: Gamma_def divide_inverse) |
|
1129 qed |
|
1130 |
|
1131 lemma Gamma_series'_LIMSEQ: "Gamma_series' z \<longlonglongrightarrow> Gamma z" |
|
1132 by (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0") (simp_all add: Gamma_nonpos_Int Gamma_seriesI[OF Gamma_series_Gamma_series'] |
|
1133 Gamma_series'_nonpos_Ints_LIMSEQ[of z]) |
|
1134 |
|
1135 |
|
1136 subsection \<open>Differentiability\<close> |
|
1137 |
|
1138 lemma has_field_derivative_rGamma_no_nonpos_int: |
|
1139 assumes "z \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
1140 shows "(rGamma has_field_derivative -rGamma z * Digamma z) (at z within A)" |
|
1141 proof (rule has_field_derivative_at_within) |
|
1142 from assms have "z \<noteq> - of_nat n" for n by auto |
|
1143 from differentiable_rGamma_aux1[OF this] |
|
1144 show "(rGamma has_field_derivative -rGamma z * Digamma z) (at z)" |
|
1145 unfolding Digamma_def suminf_def sums_def[abs_def] |
|
1146 has_field_derivative_def has_derivative_def netlimit_at |
|
1147 by (simp add: Let_def bounded_linear_mult_right mult_ac of_real_def [symmetric]) |
|
1148 qed |
|
1149 |
|
1150 lemma has_field_derivative_rGamma_nonpos_int: |
|
1151 "(rGamma has_field_derivative (-1)^n * fact n) (at (- of_nat n) within A)" |
|
1152 apply (rule has_field_derivative_at_within) |
|
1153 using differentiable_rGamma_aux2[of n] |
|
1154 unfolding Let_def has_field_derivative_def has_derivative_def netlimit_at |
|
1155 by (simp only: bounded_linear_mult_right mult_ac of_real_def [symmetric] fact_setprod) simp |
|
1156 |
|
1157 lemma has_field_derivative_rGamma [derivative_intros]: |
|
1158 "(rGamma has_field_derivative (if z \<in> \<int>\<^sub>\<le>\<^sub>0 then (-1)^(nat \<lfloor>norm z\<rfloor>) * fact (nat \<lfloor>norm z\<rfloor>) |
|
1159 else -rGamma z * Digamma z)) (at z within A)" |
|
1160 using has_field_derivative_rGamma_no_nonpos_int[of z A] |
|
1161 has_field_derivative_rGamma_nonpos_int[of "nat \<lfloor>norm z\<rfloor>" A] |
|
1162 by (auto elim!: nonpos_Ints_cases') |
|
1163 |
|
1164 declare has_field_derivative_rGamma_no_nonpos_int [THEN DERIV_chain2, derivative_intros] |
|
1165 declare has_field_derivative_rGamma [THEN DERIV_chain2, derivative_intros] |
|
1166 declare has_field_derivative_rGamma_nonpos_int [derivative_intros] |
|
1167 declare has_field_derivative_rGamma_no_nonpos_int [derivative_intros] |
|
1168 declare has_field_derivative_rGamma [derivative_intros] |
|
1169 |
|
1170 |
|
1171 lemma has_field_derivative_Gamma [derivative_intros]: |
|
1172 "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> (Gamma has_field_derivative Gamma z * Digamma z) (at z within A)" |
|
1173 unfolding Gamma_def [abs_def] |
|
1174 by (fastforce intro!: derivative_eq_intros simp: rGamma_eq_zero_iff) |
|
1175 |
|
1176 declare has_field_derivative_Gamma[THEN DERIV_chain2, derivative_intros] |
|
1177 |
|
1178 (* TODO: Hide ugly facts properly *) |
|
1179 hide_fact rGamma_eq_zero_iff_aux differentiable_rGamma_aux1 differentiable_rGamma_aux2 |
|
1180 differentiable_rGamma_aux2 rGamma_series_aux Gamma_class.rGamma_eq_zero_iff_aux |
|
1181 |
|
1182 |
|
1183 |
|
1184 (* TODO: differentiable etc. *) |
|
1185 |
|
1186 |
|
1187 subsection \<open>Continuity\<close> |
|
1188 |
|
1189 lemma continuous_on_rGamma [continuous_intros]: "continuous_on A rGamma" |
|
1190 by (rule DERIV_continuous_on has_field_derivative_rGamma)+ |
|
1191 |
|
1192 lemma continuous_on_Gamma [continuous_intros]: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> continuous_on A Gamma" |
|
1193 by (rule DERIV_continuous_on has_field_derivative_Gamma)+ blast |
|
1194 |
|
1195 lemma isCont_rGamma [continuous_intros]: |
|
1196 "isCont f z \<Longrightarrow> isCont (\<lambda>x. rGamma (f x)) z" |
|
1197 by (rule isCont_o2[OF _ DERIV_isCont[OF has_field_derivative_rGamma]]) |
|
1198 |
|
1199 lemma isCont_Gamma [continuous_intros]: |
|
1200 "isCont f z \<Longrightarrow> f z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> isCont (\<lambda>x. Gamma (f x)) z" |
|
1201 by (rule isCont_o2[OF _ DERIV_isCont[OF has_field_derivative_Gamma]]) |
|
1202 |
|
1203 |
|
1204 |
|
1205 text \<open>The complex Gamma function\<close> |
|
1206 |
|
1207 instantiation complex :: Gamma |
|
1208 begin |
|
1209 |
|
1210 definition rGamma_complex :: "complex \<Rightarrow> complex" where |
|
1211 "rGamma_complex z = lim (rGamma_series z)" |
|
1212 |
|
1213 lemma rGamma_series_complex_converges: |
|
1214 "convergent (rGamma_series (z :: complex))" (is "?thesis1") |
|
1215 and rGamma_complex_altdef: |
|
1216 "rGamma z = (if z \<in> \<int>\<^sub>\<le>\<^sub>0 then 0 else exp (-ln_Gamma z))" (is "?thesis2") |
|
1217 proof - |
|
1218 have "?thesis1 \<and> ?thesis2" |
|
1219 proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0") |
|
1220 case False |
|
1221 have "rGamma_series z \<longlonglongrightarrow> exp (- ln_Gamma z)" |
|
1222 proof (rule Lim_transform_eventually) |
|
1223 from ln_Gamma_series_complex_converges'[OF False] guess d by (elim exE conjE) |
|
1224 from this(1) uniformly_convergent_imp_convergent[OF this(2), of z] |
|
1225 have "ln_Gamma_series z \<longlonglongrightarrow> lim (ln_Gamma_series z)" by (simp add: convergent_LIMSEQ_iff) |
|
1226 thus "(\<lambda>n. exp (-ln_Gamma_series z n)) \<longlonglongrightarrow> exp (- ln_Gamma z)" |
|
1227 unfolding convergent_def ln_Gamma_def by (intro tendsto_exp tendsto_minus) |
|
1228 from eventually_gt_at_top[of "0::nat"] exp_ln_Gamma_series_complex False |
|
1229 show "eventually (\<lambda>n. exp (-ln_Gamma_series z n) = rGamma_series z n) sequentially" |
|
1230 by (force elim!: eventually_mono simp: exp_minus Gamma_series_def rGamma_series_def) |
|
1231 qed |
|
1232 with False show ?thesis |
|
1233 by (auto simp: convergent_def rGamma_complex_def intro!: limI) |
|
1234 next |
|
1235 case True |
|
1236 then obtain k where "z = - of_nat k" by (erule nonpos_Ints_cases') |
|
1237 also have "rGamma_series \<dots> \<longlonglongrightarrow> 0" |
|
1238 by (subst tendsto_cong[OF rGamma_series_minus_of_nat]) (simp_all add: convergent_const) |
|
1239 finally show ?thesis using True |
|
1240 by (auto simp: rGamma_complex_def convergent_def intro!: limI) |
|
1241 qed |
|
1242 thus "?thesis1" "?thesis2" by blast+ |
|
1243 qed |
|
1244 |
|
1245 context |
|
1246 begin |
|
1247 |
|
1248 (* TODO: duplication *) |
|
1249 private lemma rGamma_complex_plus1: "z * rGamma (z + 1) = rGamma (z :: complex)" |
|
1250 proof - |
|
1251 let ?f = "\<lambda>n. (z + 1) * inverse (of_nat n) + 1" |
|
1252 have "eventually (\<lambda>n. ?f n * rGamma_series z n = z * rGamma_series (z + 1) n) sequentially" |
|
1253 using eventually_gt_at_top[of "0::nat"] |
|
1254 proof eventually_elim |
|
1255 fix n :: nat assume n: "n > 0" |
|
1256 hence "z * rGamma_series (z + 1) n = inverse (of_nat n) * |
|
1257 pochhammer z (Suc (Suc n)) / (fact n * exp (z * of_real (ln (of_nat n))))" |
|
1258 by (subst pochhammer_rec) (simp add: rGamma_series_def field_simps exp_add exp_of_real) |
|
1259 also from n have "\<dots> = ?f n * rGamma_series z n" |
|
1260 by (subst pochhammer_rec') (simp_all add: divide_simps rGamma_series_def add_ac) |
|
1261 finally show "?f n * rGamma_series z n = z * rGamma_series (z + 1) n" .. |
|
1262 qed |
|
1263 moreover have "(\<lambda>n. ?f n * rGamma_series z n) \<longlonglongrightarrow> ((z+1) * 0 + 1) * rGamma z" |
|
1264 using rGamma_series_complex_converges |
|
1265 by (intro tendsto_intros lim_inverse_n) |
|
1266 (simp_all add: convergent_LIMSEQ_iff rGamma_complex_def) |
|
1267 hence "(\<lambda>n. ?f n * rGamma_series z n) \<longlonglongrightarrow> rGamma z" by simp |
|
1268 ultimately have "(\<lambda>n. z * rGamma_series (z + 1) n) \<longlonglongrightarrow> rGamma z" |
|
1269 by (rule Lim_transform_eventually) |
|
1270 moreover have "(\<lambda>n. z * rGamma_series (z + 1) n) \<longlonglongrightarrow> z * rGamma (z + 1)" |
|
1271 using rGamma_series_complex_converges |
|
1272 by (auto intro!: tendsto_mult simp: rGamma_complex_def convergent_LIMSEQ_iff) |
|
1273 ultimately show "z * rGamma (z + 1) = rGamma z" using LIMSEQ_unique by blast |
|
1274 qed |
|
1275 |
|
1276 private lemma has_field_derivative_rGamma_complex_no_nonpos_Int: |
|
1277 assumes "(z :: complex) \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
1278 shows "(rGamma has_field_derivative - rGamma z * Digamma z) (at z)" |
|
1279 proof - |
|
1280 have diff: "(rGamma has_field_derivative - rGamma z * Digamma z) (at z)" if "Re z > 0" for z |
|
1281 proof (subst DERIV_cong_ev[OF refl _ refl]) |
|
1282 from that have "eventually (\<lambda>t. t \<in> ball z (Re z/2)) (nhds z)" |
|
1283 by (intro eventually_nhds_in_nhd) simp_all |
|
1284 thus "eventually (\<lambda>t. rGamma t = exp (- ln_Gamma t)) (nhds z)" |
|
1285 using no_nonpos_Int_in_ball_complex[OF that] |
|
1286 by (auto elim!: eventually_mono simp: rGamma_complex_altdef) |
|
1287 next |
|
1288 have "z \<notin> \<real>\<^sub>\<le>\<^sub>0" using that by (simp add: complex_nonpos_Reals_iff) |
|
1289 with that show "((\<lambda>t. exp (- ln_Gamma t)) has_field_derivative (-rGamma z * Digamma z)) (at z)" |
|
1290 by (force elim!: nonpos_Ints_cases intro!: derivative_eq_intros simp: rGamma_complex_altdef) |
|
1291 qed |
|
1292 |
|
1293 from assms show "(rGamma has_field_derivative - rGamma z * Digamma z) (at z)" |
|
1294 proof (induction "nat \<lfloor>1 - Re z\<rfloor>" arbitrary: z) |
|
1295 case (Suc n z) |
|
1296 from Suc.prems have z: "z \<noteq> 0" by auto |
|
1297 from Suc.hyps have "n = nat \<lfloor>- Re z\<rfloor>" by linarith |
|
1298 hence A: "n = nat \<lfloor>1 - Re (z + 1)\<rfloor>" by simp |
|
1299 from Suc.prems have B: "z + 1 \<notin> \<int>\<^sub>\<le>\<^sub>0" by (force dest: plus_one_in_nonpos_Ints_imp) |
|
1300 |
|
1301 have "((\<lambda>z. z * (rGamma \<circ> (\<lambda>z. z + 1)) z) has_field_derivative |
|
1302 -rGamma (z + 1) * (Digamma (z + 1) * z - 1)) (at z)" |
|
1303 by (rule derivative_eq_intros DERIV_chain Suc refl A B)+ (simp add: algebra_simps) |
|
1304 also have "(\<lambda>z. z * (rGamma \<circ> (\<lambda>z. z + 1 :: complex)) z) = rGamma" |
|
1305 by (simp add: rGamma_complex_plus1) |
|
1306 also from z have "Digamma (z + 1) * z - 1 = z * Digamma z" |
|
1307 by (subst Digamma_plus1) (simp_all add: field_simps) |
|
1308 also have "-rGamma (z + 1) * (z * Digamma z) = -rGamma z * Digamma z" |
|
1309 by (simp add: rGamma_complex_plus1[of z, symmetric]) |
|
1310 finally show ?case . |
|
1311 qed (intro diff, simp) |
|
1312 qed |
|
1313 |
|
1314 private lemma rGamma_complex_1: "rGamma (1 :: complex) = 1" |
|
1315 proof - |
|
1316 have A: "eventually (\<lambda>n. rGamma_series 1 n = of_nat (Suc n) / of_nat n) sequentially" |
|
1317 using eventually_gt_at_top[of "0::nat"] |
|
1318 by (force elim!: eventually_mono simp: rGamma_series_def exp_of_real pochhammer_fact |
|
1319 divide_simps pochhammer_rec' dest!: pochhammer_eq_0_imp_nonpos_Int) |
|
1320 have "rGamma_series 1 \<longlonglongrightarrow> 1" by (subst tendsto_cong[OF A]) (rule LIMSEQ_Suc_n_over_n) |
|
1321 thus "rGamma 1 = (1 :: complex)" unfolding rGamma_complex_def by (rule limI) |
|
1322 qed |
|
1323 |
|
1324 private lemma has_field_derivative_rGamma_complex_nonpos_Int: |
|
1325 "(rGamma has_field_derivative (-1)^n * fact n) (at (- of_nat n :: complex))" |
|
1326 proof (induction n) |
|
1327 case 0 |
|
1328 have A: "(0::complex) + 1 \<notin> \<int>\<^sub>\<le>\<^sub>0" by simp |
|
1329 have "((\<lambda>z. z * (rGamma \<circ> (\<lambda>z. z + 1 :: complex)) z) has_field_derivative 1) (at 0)" |
|
1330 by (rule derivative_eq_intros DERIV_chain refl |
|
1331 has_field_derivative_rGamma_complex_no_nonpos_Int A)+ (simp add: rGamma_complex_1) |
|
1332 thus ?case by (simp add: rGamma_complex_plus1) |
|
1333 next |
|
1334 case (Suc n) |
|
1335 hence A: "(rGamma has_field_derivative (-1)^n * fact n) |
|
1336 (at (- of_nat (Suc n) + 1 :: complex))" by simp |
|
1337 have "((\<lambda>z. z * (rGamma \<circ> (\<lambda>z. z + 1 :: complex)) z) has_field_derivative |
|
1338 (- 1) ^ Suc n * fact (Suc n)) (at (- of_nat (Suc n)))" |
|
1339 by (rule derivative_eq_intros refl A DERIV_chain)+ |
|
1340 (simp add: algebra_simps rGamma_complex_altdef) |
|
1341 thus ?case by (simp add: rGamma_complex_plus1) |
|
1342 qed |
|
1343 |
|
1344 instance proof |
|
1345 fix z :: complex show "(rGamma z = 0) \<longleftrightarrow> (\<exists>n. z = - of_nat n)" |
|
1346 by (auto simp: rGamma_complex_altdef elim!: nonpos_Ints_cases') |
|
1347 next |
|
1348 fix z :: complex assume "\<And>n. z \<noteq> - of_nat n" |
|
1349 hence "z \<notin> \<int>\<^sub>\<le>\<^sub>0" by (auto elim!: nonpos_Ints_cases') |
|
1350 from has_field_derivative_rGamma_complex_no_nonpos_Int[OF this] |
|
1351 show "let d = (THE d. (\<lambda>n. \<Sum>k<n. inverse (of_nat (Suc k)) - inverse (z + of_nat k)) |
|
1352 \<longlonglongrightarrow> d) - euler_mascheroni *\<^sub>R 1 in (\<lambda>y. (rGamma y - rGamma z + |
|
1353 rGamma z * d * (y - z)) /\<^sub>R cmod (y - z)) \<midarrow>z\<rightarrow> 0" |
|
1354 by (simp add: has_field_derivative_def has_derivative_def Digamma_def sums_def [abs_def] |
|
1355 netlimit_at of_real_def[symmetric] suminf_def) |
|
1356 next |
|
1357 fix n :: nat |
|
1358 from has_field_derivative_rGamma_complex_nonpos_Int[of n] |
|
1359 show "let z = - of_nat n in (\<lambda>y. (rGamma y - rGamma z - (- 1) ^ n * setprod of_nat {1..n} * |
|
1360 (y - z)) /\<^sub>R cmod (y - z)) \<midarrow>z\<rightarrow> 0" |
|
1361 by (simp add: has_field_derivative_def has_derivative_def fact_setprod netlimit_at Let_def) |
|
1362 next |
|
1363 fix z :: complex |
|
1364 from rGamma_series_complex_converges[of z] have "rGamma_series z \<longlonglongrightarrow> rGamma z" |
|
1365 by (simp add: convergent_LIMSEQ_iff rGamma_complex_def) |
|
1366 thus "let fact' = \<lambda>n. setprod of_nat {1..n}; |
|
1367 exp = \<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x ^ k /\<^sub>R fact k) \<longlonglongrightarrow> e; |
|
1368 pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n |
|
1369 in (\<lambda>n. pochhammer' z n / (fact' n * exp (z * ln (real_of_nat n) *\<^sub>R 1))) \<longlonglongrightarrow> rGamma z" |
|
1370 by (simp add: fact_setprod pochhammer_Suc_setprod rGamma_series_def [abs_def] exp_def |
|
1371 of_real_def [symmetric] suminf_def sums_def [abs_def] atLeast0AtMost) |
|
1372 qed |
|
1373 |
|
1374 end |
|
1375 end |
|
1376 |
|
1377 |
|
1378 lemma Gamma_complex_altdef: |
|
1379 "Gamma z = (if z \<in> \<int>\<^sub>\<le>\<^sub>0 then 0 else exp (ln_Gamma (z :: complex)))" |
|
1380 unfolding Gamma_def rGamma_complex_altdef by (simp add: exp_minus) |
|
1381 |
|
1382 lemma cnj_rGamma: "cnj (rGamma z) = rGamma (cnj z)" |
|
1383 proof - |
|
1384 have "rGamma_series (cnj z) = (\<lambda>n. cnj (rGamma_series z n))" |
|
1385 by (intro ext) (simp_all add: rGamma_series_def exp_cnj) |
|
1386 also have "... \<longlonglongrightarrow> cnj (rGamma z)" by (intro tendsto_cnj tendsto_intros) |
|
1387 finally show ?thesis unfolding rGamma_complex_def by (intro sym[OF limI]) |
|
1388 qed |
|
1389 |
|
1390 lemma cnj_Gamma: "cnj (Gamma z) = Gamma (cnj z)" |
|
1391 unfolding Gamma_def by (simp add: cnj_rGamma) |
|
1392 |
|
1393 lemma Gamma_complex_real: |
|
1394 "z \<in> \<real> \<Longrightarrow> Gamma z \<in> (\<real> :: complex set)" and rGamma_complex_real: "z \<in> \<real> \<Longrightarrow> rGamma z \<in> \<real>" |
|
1395 by (simp_all add: Reals_cnj_iff cnj_Gamma cnj_rGamma) |
|
1396 |
|
1397 lemma field_differentiable_rGamma: "rGamma field_differentiable (at z within A)" |
|
1398 using has_field_derivative_rGamma[of z] unfolding field_differentiable_def by blast |
|
1399 |
|
1400 lemma holomorphic_on_rGamma: "rGamma holomorphic_on A" |
|
1401 unfolding holomorphic_on_def by (auto intro!: field_differentiable_rGamma) |
|
1402 |
|
1403 lemma analytic_on_rGamma: "rGamma analytic_on A" |
|
1404 unfolding analytic_on_def by (auto intro!: exI[of _ 1] holomorphic_on_rGamma) |
|
1405 |
|
1406 |
|
1407 lemma field_differentiable_Gamma: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Gamma field_differentiable (at z within A)" |
|
1408 using has_field_derivative_Gamma[of z] unfolding field_differentiable_def by auto |
|
1409 |
|
1410 lemma holomorphic_on_Gamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma holomorphic_on A" |
|
1411 unfolding holomorphic_on_def by (auto intro!: field_differentiable_Gamma) |
|
1412 |
|
1413 lemma analytic_on_Gamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma analytic_on A" |
|
1414 by (rule analytic_on_subset[of _ "UNIV - \<int>\<^sub>\<le>\<^sub>0"], subst analytic_on_open) |
|
1415 (auto intro!: holomorphic_on_Gamma) |
|
1416 |
|
1417 lemma has_field_derivative_rGamma_complex' [derivative_intros]: |
|
1418 "(rGamma has_field_derivative (if z \<in> \<int>\<^sub>\<le>\<^sub>0 then (-1)^(nat \<lfloor>-Re z\<rfloor>) * fact (nat \<lfloor>-Re z\<rfloor>) else |
|
1419 -rGamma z * Digamma z)) (at z within A)" |
|
1420 using has_field_derivative_rGamma[of z] by (auto elim!: nonpos_Ints_cases') |
|
1421 |
|
1422 declare has_field_derivative_rGamma_complex'[THEN DERIV_chain2, derivative_intros] |
|
1423 |
|
1424 |
|
1425 lemma field_differentiable_Polygamma: |
|
1426 fixes z::complex |
|
1427 shows |
|
1428 "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Polygamma n field_differentiable (at z within A)" |
|
1429 using has_field_derivative_Polygamma[of z n] unfolding field_differentiable_def by auto |
|
1430 |
|
1431 lemma holomorphic_on_Polygamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Polygamma n holomorphic_on A" |
|
1432 unfolding holomorphic_on_def by (auto intro!: field_differentiable_Polygamma) |
|
1433 |
|
1434 lemma analytic_on_Polygamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Polygamma n analytic_on A" |
|
1435 by (rule analytic_on_subset[of _ "UNIV - \<int>\<^sub>\<le>\<^sub>0"], subst analytic_on_open) |
|
1436 (auto intro!: holomorphic_on_Polygamma) |
|
1437 |
|
1438 |
|
1439 |
|
1440 text \<open>The real Gamma function\<close> |
|
1441 |
|
1442 lemma rGamma_series_real: |
|
1443 "eventually (\<lambda>n. rGamma_series x n = Re (rGamma_series (of_real x) n)) sequentially" |
|
1444 using eventually_gt_at_top[of "0 :: nat"] |
|
1445 proof eventually_elim |
|
1446 fix n :: nat assume n: "n > 0" |
|
1447 have "Re (rGamma_series (of_real x) n) = |
|
1448 Re (of_real (pochhammer x (Suc n)) / (fact n * exp (of_real (x * ln (real_of_nat n)))))" |
|
1449 using n by (simp add: rGamma_series_def powr_def Ln_of_nat pochhammer_of_real) |
|
1450 also from n have "\<dots> = Re (of_real ((pochhammer x (Suc n)) / |
|
1451 (fact n * (exp (x * ln (real_of_nat n))))))" |
|
1452 by (subst exp_of_real) simp |
|
1453 also from n have "\<dots> = rGamma_series x n" |
|
1454 by (subst Re_complex_of_real) (simp add: rGamma_series_def powr_def) |
|
1455 finally show "rGamma_series x n = Re (rGamma_series (of_real x) n)" .. |
|
1456 qed |
|
1457 |
|
1458 instantiation real :: Gamma |
|
1459 begin |
|
1460 |
|
1461 definition "rGamma_real x = Re (rGamma (of_real x :: complex))" |
|
1462 |
|
1463 instance proof |
|
1464 fix x :: real |
|
1465 have "rGamma x = Re (rGamma (of_real x))" by (simp add: rGamma_real_def) |
|
1466 also have "of_real \<dots> = rGamma (of_real x :: complex)" |
|
1467 by (intro of_real_Re rGamma_complex_real) simp_all |
|
1468 also have "\<dots> = 0 \<longleftrightarrow> x \<in> \<int>\<^sub>\<le>\<^sub>0" by (simp add: rGamma_eq_zero_iff of_real_in_nonpos_Ints_iff) |
|
1469 also have "\<dots> \<longleftrightarrow> (\<exists>n. x = - of_nat n)" by (auto elim!: nonpos_Ints_cases') |
|
1470 finally show "(rGamma x) = 0 \<longleftrightarrow> (\<exists>n. x = - real_of_nat n)" by simp |
|
1471 next |
|
1472 fix x :: real assume "\<And>n. x \<noteq> - of_nat n" |
|
1473 hence x: "complex_of_real x \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
1474 by (subst of_real_in_nonpos_Ints_iff) (auto elim!: nonpos_Ints_cases') |
|
1475 then have "x \<noteq> 0" by auto |
|
1476 with x have "(rGamma has_field_derivative - rGamma x * Digamma x) (at x)" |
|
1477 by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_complex |
|
1478 simp: Polygamma_of_real rGamma_real_def [abs_def]) |
|
1479 thus "let d = (THE d. (\<lambda>n. \<Sum>k<n. inverse (of_nat (Suc k)) - inverse (x + of_nat k)) |
|
1480 \<longlonglongrightarrow> d) - euler_mascheroni *\<^sub>R 1 in (\<lambda>y. (rGamma y - rGamma x + |
|
1481 rGamma x * d * (y - x)) /\<^sub>R norm (y - x)) \<midarrow>x\<rightarrow> 0" |
|
1482 by (simp add: has_field_derivative_def has_derivative_def Digamma_def sums_def [abs_def] |
|
1483 netlimit_at of_real_def[symmetric] suminf_def) |
|
1484 next |
|
1485 fix n :: nat |
|
1486 have "(rGamma has_field_derivative (-1)^n * fact n) (at (- of_nat n :: real))" |
|
1487 by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_complex |
|
1488 simp: Polygamma_of_real rGamma_real_def [abs_def]) |
|
1489 thus "let x = - of_nat n in (\<lambda>y. (rGamma y - rGamma x - (- 1) ^ n * setprod of_nat {1..n} * |
|
1490 (y - x)) /\<^sub>R norm (y - x)) \<midarrow>x::real\<rightarrow> 0" |
|
1491 by (simp add: has_field_derivative_def has_derivative_def fact_setprod netlimit_at Let_def) |
|
1492 next |
|
1493 fix x :: real |
|
1494 have "rGamma_series x \<longlonglongrightarrow> rGamma x" |
|
1495 proof (rule Lim_transform_eventually) |
|
1496 show "(\<lambda>n. Re (rGamma_series (of_real x) n)) \<longlonglongrightarrow> rGamma x" unfolding rGamma_real_def |
|
1497 by (intro tendsto_intros) |
|
1498 qed (insert rGamma_series_real, simp add: eq_commute) |
|
1499 thus "let fact' = \<lambda>n. setprod of_nat {1..n}; |
|
1500 exp = \<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x ^ k /\<^sub>R fact k) \<longlonglongrightarrow> e; |
|
1501 pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n |
|
1502 in (\<lambda>n. pochhammer' x n / (fact' n * exp (x * ln (real_of_nat n) *\<^sub>R 1))) \<longlonglongrightarrow> rGamma x" |
|
1503 by (simp add: fact_setprod pochhammer_Suc_setprod rGamma_series_def [abs_def] exp_def |
|
1504 of_real_def [symmetric] suminf_def sums_def [abs_def] atLeast0AtMost) |
|
1505 qed |
|
1506 |
|
1507 end |
|
1508 |
|
1509 |
|
1510 lemma rGamma_complex_of_real: "rGamma (complex_of_real x) = complex_of_real (rGamma x)" |
|
1511 unfolding rGamma_real_def using rGamma_complex_real by simp |
|
1512 |
|
1513 lemma Gamma_complex_of_real: "Gamma (complex_of_real x) = complex_of_real (Gamma x)" |
|
1514 unfolding Gamma_def by (simp add: rGamma_complex_of_real) |
|
1515 |
|
1516 lemma rGamma_real_altdef: "rGamma x = lim (rGamma_series (x :: real))" |
|
1517 by (rule sym, rule limI, rule tendsto_intros) |
|
1518 |
|
1519 lemma Gamma_real_altdef1: "Gamma x = lim (Gamma_series (x :: real))" |
|
1520 by (rule sym, rule limI, rule tendsto_intros) |
|
1521 |
|
1522 lemma Gamma_real_altdef2: "Gamma x = Re (Gamma (of_real x))" |
|
1523 using rGamma_complex_real[OF Reals_of_real[of x]] |
|
1524 by (elim Reals_cases) |
|
1525 (simp only: Gamma_def rGamma_real_def of_real_inverse[symmetric] Re_complex_of_real) |
|
1526 |
|
1527 lemma ln_Gamma_series_complex_of_real: |
|
1528 "x > 0 \<Longrightarrow> n > 0 \<Longrightarrow> ln_Gamma_series (complex_of_real x) n = of_real (ln_Gamma_series x n)" |
|
1529 proof - |
|
1530 assume xn: "x > 0" "n > 0" |
|
1531 have "Ln (complex_of_real x / of_nat k + 1) = of_real (ln (x / of_nat k + 1))" if "k \<ge> 1" for k |
|
1532 using that xn by (subst Ln_of_real [symmetric]) (auto intro!: add_nonneg_pos simp: field_simps) |
|
1533 with xn show ?thesis by (simp add: ln_Gamma_series_def Ln_of_nat Ln_of_real) |
|
1534 qed |
|
1535 |
|
1536 lemma ln_Gamma_real_converges: |
|
1537 assumes "(x::real) > 0" |
|
1538 shows "convergent (ln_Gamma_series x)" |
|
1539 proof - |
|
1540 have "(\<lambda>n. ln_Gamma_series (complex_of_real x) n) \<longlonglongrightarrow> ln_Gamma (of_real x)" using assms |
|
1541 by (intro ln_Gamma_complex_LIMSEQ) (auto simp: of_real_in_nonpos_Ints_iff) |
|
1542 moreover from eventually_gt_at_top[of "0::nat"] |
|
1543 have "eventually (\<lambda>n. complex_of_real (ln_Gamma_series x n) = |
|
1544 ln_Gamma_series (complex_of_real x) n) sequentially" |
|
1545 by eventually_elim (simp add: ln_Gamma_series_complex_of_real assms) |
|
1546 ultimately have "(\<lambda>n. complex_of_real (ln_Gamma_series x n)) \<longlonglongrightarrow> ln_Gamma (of_real x)" |
|
1547 by (subst tendsto_cong) assumption+ |
|
1548 from tendsto_Re[OF this] show ?thesis by (auto simp: convergent_def) |
|
1549 qed |
|
1550 |
|
1551 lemma ln_Gamma_real_LIMSEQ: "(x::real) > 0 \<Longrightarrow> ln_Gamma_series x \<longlonglongrightarrow> ln_Gamma x" |
|
1552 using ln_Gamma_real_converges[of x] unfolding ln_Gamma_def by (simp add: convergent_LIMSEQ_iff) |
|
1553 |
|
1554 lemma ln_Gamma_complex_of_real: "x > 0 \<Longrightarrow> ln_Gamma (complex_of_real x) = of_real (ln_Gamma x)" |
|
1555 proof (unfold ln_Gamma_def, rule limI, rule Lim_transform_eventually) |
|
1556 assume x: "x > 0" |
|
1557 show "eventually (\<lambda>n. of_real (ln_Gamma_series x n) = |
|
1558 ln_Gamma_series (complex_of_real x) n) sequentially" |
|
1559 using eventually_gt_at_top[of "0::nat"] |
|
1560 by eventually_elim (simp add: ln_Gamma_series_complex_of_real x) |
|
1561 qed (intro tendsto_of_real, insert ln_Gamma_real_LIMSEQ[of x], simp add: ln_Gamma_def) |
|
1562 |
|
1563 lemma Gamma_real_pos_exp: "x > (0 :: real) \<Longrightarrow> Gamma x = exp (ln_Gamma x)" |
|
1564 by (auto simp: Gamma_real_altdef2 Gamma_complex_altdef of_real_in_nonpos_Ints_iff |
|
1565 ln_Gamma_complex_of_real exp_of_real) |
|
1566 |
|
1567 lemma ln_Gamma_real_pos: "x > 0 \<Longrightarrow> ln_Gamma x = ln (Gamma x :: real)" |
|
1568 unfolding Gamma_real_pos_exp by simp |
|
1569 |
|
1570 lemma Gamma_real_pos: "x > (0::real) \<Longrightarrow> Gamma x > 0" |
|
1571 by (simp add: Gamma_real_pos_exp) |
|
1572 |
|
1573 lemma has_field_derivative_ln_Gamma_real [derivative_intros]: |
|
1574 assumes x: "x > (0::real)" |
|
1575 shows "(ln_Gamma has_field_derivative Digamma x) (at x)" |
|
1576 proof (subst DERIV_cong_ev[OF refl _ refl]) |
|
1577 from assms show "((Re \<circ> ln_Gamma \<circ> complex_of_real) has_field_derivative Digamma x) (at x)" |
|
1578 by (auto intro!: derivative_eq_intros has_vector_derivative_real_complex |
|
1579 simp: Polygamma_of_real o_def) |
|
1580 from eventually_nhds_in_nhd[of x "{0<..}"] assms |
|
1581 show "eventually (\<lambda>y. ln_Gamma y = (Re \<circ> ln_Gamma \<circ> of_real) y) (nhds x)" |
|
1582 by (auto elim!: eventually_mono simp: ln_Gamma_complex_of_real interior_open) |
|
1583 qed |
|
1584 |
|
1585 declare has_field_derivative_ln_Gamma_real[THEN DERIV_chain2, derivative_intros] |
|
1586 |
|
1587 |
|
1588 lemma has_field_derivative_rGamma_real' [derivative_intros]: |
|
1589 "(rGamma has_field_derivative (if x \<in> \<int>\<^sub>\<le>\<^sub>0 then (-1)^(nat \<lfloor>-x\<rfloor>) * fact (nat \<lfloor>-x\<rfloor>) else |
|
1590 -rGamma x * Digamma x)) (at x within A)" |
|
1591 using has_field_derivative_rGamma[of x] by (force elim!: nonpos_Ints_cases') |
|
1592 |
|
1593 declare has_field_derivative_rGamma_real'[THEN DERIV_chain2, derivative_intros] |
|
1594 |
|
1595 lemma Polygamma_real_odd_pos: |
|
1596 assumes "(x::real) \<notin> \<int>\<^sub>\<le>\<^sub>0" "odd n" |
|
1597 shows "Polygamma n x > 0" |
|
1598 proof - |
|
1599 from assms have "x \<noteq> 0" by auto |
|
1600 with assms show ?thesis |
|
1601 unfolding Polygamma_def using Polygamma_converges'[of x "Suc n"] |
|
1602 by (auto simp: zero_less_power_eq simp del: power_Suc |
|
1603 dest: plus_of_nat_eq_0_imp intro!: mult_pos_pos suminf_pos) |
|
1604 qed |
|
1605 |
|
1606 lemma Polygamma_real_even_neg: |
|
1607 assumes "(x::real) > 0" "n > 0" "even n" |
|
1608 shows "Polygamma n x < 0" |
|
1609 using assms unfolding Polygamma_def using Polygamma_converges'[of x "Suc n"] |
|
1610 by (auto intro!: mult_pos_pos suminf_pos) |
|
1611 |
|
1612 lemma Polygamma_real_strict_mono: |
|
1613 assumes "x > 0" "x < (y::real)" "even n" |
|
1614 shows "Polygamma n x < Polygamma n y" |
|
1615 proof - |
|
1616 have "\<exists>\<xi>. x < \<xi> \<and> \<xi> < y \<and> Polygamma n y - Polygamma n x = (y - x) * Polygamma (Suc n) \<xi>" |
|
1617 using assms by (intro MVT2 derivative_intros impI allI) (auto elim!: nonpos_Ints_cases) |
|
1618 then guess \<xi> by (elim exE conjE) note \<xi> = this |
|
1619 note \<xi>(3) |
|
1620 also from \<xi>(1,2) assms have "(y - x) * Polygamma (Suc n) \<xi> > 0" |
|
1621 by (intro mult_pos_pos Polygamma_real_odd_pos) (auto elim!: nonpos_Ints_cases) |
|
1622 finally show ?thesis by simp |
|
1623 qed |
|
1624 |
|
1625 lemma Polygamma_real_strict_antimono: |
|
1626 assumes "x > 0" "x < (y::real)" "odd n" |
|
1627 shows "Polygamma n x > Polygamma n y" |
|
1628 proof - |
|
1629 have "\<exists>\<xi>. x < \<xi> \<and> \<xi> < y \<and> Polygamma n y - Polygamma n x = (y - x) * Polygamma (Suc n) \<xi>" |
|
1630 using assms by (intro MVT2 derivative_intros impI allI) (auto elim!: nonpos_Ints_cases) |
|
1631 then guess \<xi> by (elim exE conjE) note \<xi> = this |
|
1632 note \<xi>(3) |
|
1633 also from \<xi>(1,2) assms have "(y - x) * Polygamma (Suc n) \<xi> < 0" |
|
1634 by (intro mult_pos_neg Polygamma_real_even_neg) simp_all |
|
1635 finally show ?thesis by simp |
|
1636 qed |
|
1637 |
|
1638 lemma Polygamma_real_mono: |
|
1639 assumes "x > 0" "x \<le> (y::real)" "even n" |
|
1640 shows "Polygamma n x \<le> Polygamma n y" |
|
1641 using Polygamma_real_strict_mono[OF assms(1) _ assms(3), of y] assms(2) |
|
1642 by (cases "x = y") simp_all |
|
1643 |
|
1644 lemma Digamma_real_ge_three_halves_pos: |
|
1645 assumes "x \<ge> 3/2" |
|
1646 shows "Digamma (x :: real) > 0" |
|
1647 proof - |
|
1648 have "0 < Digamma (3/2 :: real)" by (fact Digamma_real_three_halves_pos) |
|
1649 also from assms have "\<dots> \<le> Digamma x" by (intro Polygamma_real_mono) simp_all |
|
1650 finally show ?thesis . |
|
1651 qed |
|
1652 |
|
1653 lemma ln_Gamma_real_strict_mono: |
|
1654 assumes "x \<ge> 3/2" "x < y" |
|
1655 shows "ln_Gamma (x :: real) < ln_Gamma y" |
|
1656 proof - |
|
1657 have "\<exists>\<xi>. x < \<xi> \<and> \<xi> < y \<and> ln_Gamma y - ln_Gamma x = (y - x) * Digamma \<xi>" |
|
1658 using assms by (intro MVT2 derivative_intros impI allI) (auto elim!: nonpos_Ints_cases) |
|
1659 then guess \<xi> by (elim exE conjE) note \<xi> = this |
|
1660 note \<xi>(3) |
|
1661 also from \<xi>(1,2) assms have "(y - x) * Digamma \<xi> > 0" |
|
1662 by (intro mult_pos_pos Digamma_real_ge_three_halves_pos) simp_all |
|
1663 finally show ?thesis by simp |
|
1664 qed |
|
1665 |
|
1666 lemma Gamma_real_strict_mono: |
|
1667 assumes "x \<ge> 3/2" "x < y" |
|
1668 shows "Gamma (x :: real) < Gamma y" |
|
1669 proof - |
|
1670 from Gamma_real_pos_exp[of x] assms have "Gamma x = exp (ln_Gamma x)" by simp |
|
1671 also have "\<dots> < exp (ln_Gamma y)" by (intro exp_less_mono ln_Gamma_real_strict_mono assms) |
|
1672 also from Gamma_real_pos_exp[of y] assms have "\<dots> = Gamma y" by simp |
|
1673 finally show ?thesis . |
|
1674 qed |
|
1675 |
|
1676 lemma log_convex_Gamma_real: "convex_on {0<..} (ln \<circ> Gamma :: real \<Rightarrow> real)" |
|
1677 by (rule convex_on_realI[of _ _ Digamma]) |
|
1678 (auto intro!: derivative_eq_intros Polygamma_real_mono Gamma_real_pos |
|
1679 simp: o_def Gamma_eq_zero_iff elim!: nonpos_Ints_cases') |
|
1680 |
|
1681 |
|
1682 subsection \<open>Beta function\<close> |
|
1683 |
|
1684 definition Beta where "Beta a b = Gamma a * Gamma b / Gamma (a + b)" |
|
1685 |
|
1686 lemma Beta_altdef: "Beta a b = Gamma a * Gamma b * rGamma (a + b)" |
|
1687 by (simp add: inverse_eq_divide Beta_def Gamma_def) |
|
1688 |
|
1689 lemma Beta_commute: "Beta a b = Beta b a" |
|
1690 unfolding Beta_def by (simp add: ac_simps) |
|
1691 |
|
1692 lemma has_field_derivative_Beta1 [derivative_intros]: |
|
1693 assumes "x \<notin> \<int>\<^sub>\<le>\<^sub>0" "x + y \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
1694 shows "((\<lambda>x. Beta x y) has_field_derivative (Beta x y * (Digamma x - Digamma (x + y)))) |
|
1695 (at x within A)" unfolding Beta_altdef |
|
1696 by (rule DERIV_cong, (rule derivative_intros assms)+) (simp add: algebra_simps) |
|
1697 |
|
1698 lemma Beta_pole1: "x \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Beta x y = 0" |
|
1699 by (auto simp add: Beta_def elim!: nonpos_Ints_cases') |
|
1700 |
|
1701 lemma Beta_pole2: "y \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Beta x y = 0" |
|
1702 by (auto simp add: Beta_def elim!: nonpos_Ints_cases') |
|
1703 |
|
1704 lemma Beta_zero: "x + y \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Beta x y = 0" |
|
1705 by (auto simp add: Beta_def elim!: nonpos_Ints_cases') |
|
1706 |
|
1707 lemma has_field_derivative_Beta2 [derivative_intros]: |
|
1708 assumes "y \<notin> \<int>\<^sub>\<le>\<^sub>0" "x + y \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
1709 shows "((\<lambda>y. Beta x y) has_field_derivative (Beta x y * (Digamma y - Digamma (x + y)))) |
|
1710 (at y within A)" |
|
1711 using has_field_derivative_Beta1[of y x A] assms by (simp add: Beta_commute add_ac) |
|
1712 |
|
1713 lemma Beta_plus1_plus1: |
|
1714 assumes "x \<notin> \<int>\<^sub>\<le>\<^sub>0" "y \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
1715 shows "Beta (x + 1) y + Beta x (y + 1) = Beta x y" |
|
1716 proof - |
|
1717 have "Beta (x + 1) y + Beta x (y + 1) = |
|
1718 (Gamma (x + 1) * Gamma y + Gamma x * Gamma (y + 1)) * rGamma ((x + y) + 1)" |
|
1719 by (simp add: Beta_altdef add_divide_distrib algebra_simps) |
|
1720 also have "\<dots> = (Gamma x * Gamma y) * ((x + y) * rGamma ((x + y) + 1))" |
|
1721 by (subst assms[THEN Gamma_plus1])+ (simp add: algebra_simps) |
|
1722 also from assms have "\<dots> = Beta x y" unfolding Beta_altdef by (subst rGamma_plus1) simp |
|
1723 finally show ?thesis . |
|
1724 qed |
|
1725 |
|
1726 lemma Beta_plus1_left: |
|
1727 assumes "x \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
1728 shows "(x + y) * Beta (x + 1) y = x * Beta x y" |
|
1729 proof - |
|
1730 have "(x + y) * Beta (x + 1) y = Gamma (x + 1) * Gamma y * ((x + y) * rGamma ((x + y) + 1))" |
|
1731 unfolding Beta_altdef by (simp only: ac_simps) |
|
1732 also have "\<dots> = x * Beta x y" unfolding Beta_altdef |
|
1733 by (subst assms[THEN Gamma_plus1] rGamma_plus1)+ (simp only: ac_simps) |
|
1734 finally show ?thesis . |
|
1735 qed |
|
1736 |
|
1737 lemma Beta_plus1_right: |
|
1738 assumes "y \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
1739 shows "(x + y) * Beta x (y + 1) = y * Beta x y" |
|
1740 using Beta_plus1_left[of y x] assms by (simp_all add: Beta_commute add.commute) |
|
1741 |
|
1742 lemma Gamma_Gamma_Beta: |
|
1743 assumes "x + y \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
1744 shows "Gamma x * Gamma y = Beta x y * Gamma (x + y)" |
|
1745 unfolding Beta_altdef using assms Gamma_eq_zero_iff[of "x+y"] |
|
1746 by (simp add: rGamma_inverse_Gamma) |
|
1747 |
|
1748 |
|
1749 |
|
1750 subsection \<open>Legendre duplication theorem\<close> |
|
1751 |
|
1752 context |
|
1753 begin |
|
1754 |
|
1755 private lemma Gamma_legendre_duplication_aux: |
|
1756 fixes z :: "'a :: Gamma" |
|
1757 assumes "z \<notin> \<int>\<^sub>\<le>\<^sub>0" "z + 1/2 \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
1758 shows "Gamma z * Gamma (z + 1/2) = exp ((1 - 2*z) * of_real (ln 2)) * Gamma (1/2) * Gamma (2*z)" |
|
1759 proof - |
|
1760 let ?powr = "\<lambda>b a. exp (a * of_real (ln (of_nat b)))" |
|
1761 let ?h = "\<lambda>n. (fact (n-1))\<^sup>2 / fact (2*n-1) * of_nat (2^(2*n)) * |
|
1762 exp (1/2 * of_real (ln (real_of_nat n)))" |
|
1763 { |
|
1764 fix z :: 'a assume z: "z \<notin> \<int>\<^sub>\<le>\<^sub>0" "z + 1/2 \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
1765 let ?g = "\<lambda>n. ?powr 2 (2*z) * Gamma_series' z n * Gamma_series' (z + 1/2) n / |
|
1766 Gamma_series' (2*z) (2*n)" |
|
1767 have "eventually (\<lambda>n. ?g n = ?h n) sequentially" using eventually_gt_at_top |
|
1768 proof eventually_elim |
|
1769 fix n :: nat assume n: "n > 0" |
|
1770 let ?f = "fact (n - 1) :: 'a" and ?f' = "fact (2*n - 1) :: 'a" |
|
1771 have A: "exp t * exp t = exp (2*t :: 'a)" for t by (subst exp_add [symmetric]) simp |
|
1772 have A: "Gamma_series' z n * Gamma_series' (z + 1/2) n = ?f^2 * ?powr n (2*z + 1/2) / |
|
1773 (pochhammer z n * pochhammer (z + 1/2) n)" |
|
1774 by (simp add: Gamma_series'_def exp_add ring_distribs power2_eq_square A mult_ac) |
|
1775 have B: "Gamma_series' (2*z) (2*n) = |
|
1776 ?f' * ?powr 2 (2*z) * ?powr n (2*z) / |
|
1777 (of_nat (2^(2*n)) * pochhammer z n * pochhammer (z+1/2) n)" using n |
|
1778 by (simp add: Gamma_series'_def ln_mult exp_add ring_distribs pochhammer_double) |
|
1779 from z have "pochhammer z n \<noteq> 0" by (auto dest: pochhammer_eq_0_imp_nonpos_Int) |
|
1780 moreover from z have "pochhammer (z + 1/2) n \<noteq> 0" by (auto dest: pochhammer_eq_0_imp_nonpos_Int) |
|
1781 ultimately have "?powr 2 (2*z) * (Gamma_series' z n * Gamma_series' (z + 1/2) n) / Gamma_series' (2*z) (2*n) = |
|
1782 ?f^2 / ?f' * of_nat (2^(2*n)) * (?powr n ((4*z + 1)/2) * ?powr n (-2*z))" |
|
1783 using n unfolding A B by (simp add: divide_simps exp_minus) |
|
1784 also have "?powr n ((4*z + 1)/2) * ?powr n (-2*z) = ?powr n (1/2)" |
|
1785 by (simp add: algebra_simps exp_add[symmetric] add_divide_distrib) |
|
1786 finally show "?g n = ?h n" by (simp only: mult_ac) |
|
1787 qed |
|
1788 |
|
1789 moreover from z double_in_nonpos_Ints_imp[of z] have "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto |
|
1790 hence "?g \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)" |
|
1791 using LIMSEQ_subseq_LIMSEQ[OF Gamma_series'_LIMSEQ, of "op*2" "2*z"] |
|
1792 by (intro tendsto_intros Gamma_series'_LIMSEQ) |
|
1793 (simp_all add: o_def subseq_def Gamma_eq_zero_iff) |
|
1794 ultimately have "?h \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)" |
|
1795 by (rule Lim_transform_eventually) |
|
1796 } note lim = this |
|
1797 |
|
1798 from assms double_in_nonpos_Ints_imp[of z] have z': "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto |
|
1799 from fraction_not_in_ints[of 2 1] have "(1/2 :: 'a) \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
1800 by (intro not_in_Ints_imp_not_in_nonpos_Ints) simp_all |
|
1801 with lim[of "1/2 :: 'a"] have "?h \<longlonglongrightarrow> 2 * Gamma (1 / 2 :: 'a)" by (simp add: exp_of_real) |
|
1802 from LIMSEQ_unique[OF this lim[OF assms]] z' show ?thesis |
|
1803 by (simp add: divide_simps Gamma_eq_zero_iff ring_distribs exp_diff exp_of_real ac_simps) |
|
1804 qed |
|
1805 |
|
1806 (* TODO: perhaps this is unnecessary once we have the fact that a holomorphic function is |
|
1807 infinitely differentiable *) |
|
1808 private lemma Gamma_reflection_aux: |
|
1809 defines "h \<equiv> \<lambda>z::complex. if z \<in> \<int> then 0 else |
|
1810 (of_real pi * cot (of_real pi*z) + Digamma z - Digamma (1 - z))" |
|
1811 defines "a \<equiv> complex_of_real pi" |
|
1812 obtains h' where "continuous_on UNIV h'" "\<And>z. (h has_field_derivative (h' z)) (at z)" |
|
1813 proof - |
|
1814 define f where "f n = a * of_real (cos_coeff (n+1) - sin_coeff (n+2))" for n |
|
1815 define F where "F z = (if z = 0 then 0 else (cos (a*z) - sin (a*z)/(a*z)) / z)" for z |
|
1816 define g where "g n = complex_of_real (sin_coeff (n+1))" for n |
|
1817 define G where "G z = (if z = 0 then 1 else sin (a*z)/(a*z))" for z |
|
1818 have a_nz: "a \<noteq> 0" unfolding a_def by simp |
|
1819 |
|
1820 have "(\<lambda>n. f n * (a*z)^n) sums (F z) \<and> (\<lambda>n. g n * (a*z)^n) sums (G z)" |
|
1821 if "abs (Re z) < 1" for z |
|
1822 proof (cases "z = 0"; rule conjI) |
|
1823 assume "z \<noteq> 0" |
|
1824 note z = this that |
|
1825 |
|
1826 from z have sin_nz: "sin (a*z) \<noteq> 0" unfolding a_def by (auto simp: sin_eq_0) |
|
1827 have "(\<lambda>n. of_real (sin_coeff n) * (a*z)^n) sums (sin (a*z))" using sin_converges[of "a*z"] |
|
1828 by (simp add: scaleR_conv_of_real) |
|
1829 from sums_split_initial_segment[OF this, of 1] |
|
1830 have "(\<lambda>n. (a*z) * of_real (sin_coeff (n+1)) * (a*z)^n) sums (sin (a*z))" by (simp add: mult_ac) |
|
1831 from sums_mult[OF this, of "inverse (a*z)"] z a_nz |
|
1832 have A: "(\<lambda>n. g n * (a*z)^n) sums (sin (a*z)/(a*z))" |
|
1833 by (simp add: field_simps g_def) |
|
1834 with z show "(\<lambda>n. g n * (a*z)^n) sums (G z)" by (simp add: G_def) |
|
1835 from A z a_nz sin_nz have g_nz: "(\<Sum>n. g n * (a*z)^n) \<noteq> 0" by (simp add: sums_iff g_def) |
|
1836 |
|
1837 have [simp]: "sin_coeff (Suc 0) = 1" by (simp add: sin_coeff_def) |
|
1838 from sums_split_initial_segment[OF sums_diff[OF cos_converges[of "a*z"] A], of 1] |
|
1839 have "(\<lambda>n. z * f n * (a*z)^n) sums (cos (a*z) - sin (a*z) / (a*z))" |
|
1840 by (simp add: mult_ac scaleR_conv_of_real ring_distribs f_def g_def) |
|
1841 from sums_mult[OF this, of "inverse z"] z assms |
|
1842 show "(\<lambda>n. f n * (a*z)^n) sums (F z)" by (simp add: divide_simps mult_ac f_def F_def) |
|
1843 next |
|
1844 assume z: "z = 0" |
|
1845 have "(\<lambda>n. f n * (a * z) ^ n) sums f 0" using powser_sums_zero[of f] z by simp |
|
1846 with z show "(\<lambda>n. f n * (a * z) ^ n) sums (F z)" |
|
1847 by (simp add: f_def F_def sin_coeff_def cos_coeff_def) |
|
1848 have "(\<lambda>n. g n * (a * z) ^ n) sums g 0" using powser_sums_zero[of g] z by simp |
|
1849 with z show "(\<lambda>n. g n * (a * z) ^ n) sums (G z)" |
|
1850 by (simp add: g_def G_def sin_coeff_def cos_coeff_def) |
|
1851 qed |
|
1852 note sums = conjunct1[OF this] conjunct2[OF this] |
|
1853 |
|
1854 define h2 where [abs_def]: |
|
1855 "h2 z = (\<Sum>n. f n * (a*z)^n) / (\<Sum>n. g n * (a*z)^n) + Digamma (1 + z) - Digamma (1 - z)" for z |
|
1856 define POWSER where [abs_def]: "POWSER f z = (\<Sum>n. f n * (z^n :: complex))" for f z |
|
1857 define POWSER' where [abs_def]: "POWSER' f z = (\<Sum>n. diffs f n * (z^n))" for f and z :: complex |
|
1858 define h2' where [abs_def]: |
|
1859 "h2' z = a * (POWSER g (a*z) * POWSER' f (a*z) - POWSER f (a*z) * POWSER' g (a*z)) / |
|
1860 (POWSER g (a*z))^2 + Polygamma 1 (1 + z) + Polygamma 1 (1 - z)" for z |
|
1861 |
|
1862 have h_eq: "h t = h2 t" if "abs (Re t) < 1" for t |
|
1863 proof - |
|
1864 from that have t: "t \<in> \<int> \<longleftrightarrow> t = 0" by (auto elim!: Ints_cases simp: dist_0_norm) |
|
1865 hence "h t = a*cot (a*t) - 1/t + Digamma (1 + t) - Digamma (1 - t)" |
|
1866 unfolding h_def using Digamma_plus1[of t] by (force simp: field_simps a_def) |
|
1867 also have "a*cot (a*t) - 1/t = (F t) / (G t)" |
|
1868 using t by (auto simp add: divide_simps sin_eq_0 cot_def a_def F_def G_def) |
|
1869 also have "\<dots> = (\<Sum>n. f n * (a*t)^n) / (\<Sum>n. g n * (a*t)^n)" |
|
1870 using sums[of t] that by (simp add: sums_iff dist_0_norm) |
|
1871 finally show "h t = h2 t" by (simp only: h2_def) |
|
1872 qed |
|
1873 |
|
1874 let ?A = "{z. abs (Re z) < 1}" |
|
1875 have "open ({z. Re z < 1} \<inter> {z. Re z > -1})" |
|
1876 using open_halfspace_Re_gt open_halfspace_Re_lt by auto |
|
1877 also have "({z. Re z < 1} \<inter> {z. Re z > -1}) = {z. abs (Re z) < 1}" by auto |
|
1878 finally have open_A: "open ?A" . |
|
1879 hence [simp]: "interior ?A = ?A" by (simp add: interior_open) |
|
1880 |
|
1881 have summable_f: "summable (\<lambda>n. f n * z^n)" for z |
|
1882 by (rule powser_inside, rule sums_summable, rule sums[of "\<i> * of_real (norm z + 1) / a"]) |
|
1883 (simp_all add: norm_mult a_def del: of_real_add) |
|
1884 have summable_g: "summable (\<lambda>n. g n * z^n)" for z |
|
1885 by (rule powser_inside, rule sums_summable, rule sums[of "\<i> * of_real (norm z + 1) / a"]) |
|
1886 (simp_all add: norm_mult a_def del: of_real_add) |
|
1887 have summable_fg': "summable (\<lambda>n. diffs f n * z^n)" "summable (\<lambda>n. diffs g n * z^n)" for z |
|
1888 by (intro termdiff_converges_all summable_f summable_g)+ |
|
1889 have "(POWSER f has_field_derivative (POWSER' f z)) (at z)" |
|
1890 "(POWSER g has_field_derivative (POWSER' g z)) (at z)" for z |
|
1891 unfolding POWSER_def POWSER'_def |
|
1892 by (intro termdiffs_strong_converges_everywhere summable_f summable_g)+ |
|
1893 note derivs = this[THEN DERIV_chain2[OF _ DERIV_cmult[OF DERIV_ident]], unfolded POWSER_def] |
|
1894 have "isCont (POWSER f) z" "isCont (POWSER g) z" "isCont (POWSER' f) z" "isCont (POWSER' g) z" |
|
1895 for z unfolding POWSER_def POWSER'_def |
|
1896 by (intro isCont_powser_converges_everywhere summable_f summable_g summable_fg')+ |
|
1897 note cont = this[THEN isCont_o2[rotated], unfolded POWSER_def POWSER'_def] |
|
1898 |
|
1899 { |
|
1900 fix z :: complex assume z: "abs (Re z) < 1" |
|
1901 define d where "d = \<i> * of_real (norm z + 1)" |
|
1902 have d: "abs (Re d) < 1" "norm z < norm d" by (simp_all add: d_def norm_mult del: of_real_add) |
|
1903 have "eventually (\<lambda>z. h z = h2 z) (nhds z)" |
|
1904 using eventually_nhds_in_nhd[of z ?A] using h_eq z |
|
1905 by (auto elim!: eventually_mono simp: dist_0_norm) |
|
1906 |
|
1907 moreover from sums(2)[OF z] z have nz: "(\<Sum>n. g n * (a * z) ^ n) \<noteq> 0" |
|
1908 unfolding G_def by (auto simp: sums_iff sin_eq_0 a_def) |
|
1909 have A: "z \<in> \<int> \<longleftrightarrow> z = 0" using z by (auto elim!: Ints_cases) |
|
1910 have no_int: "1 + z \<in> \<int> \<longleftrightarrow> z = 0" using z Ints_diff[of "1+z" 1] A |
|
1911 by (auto elim!: nonpos_Ints_cases) |
|
1912 have no_int': "1 - z \<in> \<int> \<longleftrightarrow> z = 0" using z Ints_diff[of 1 "1-z"] A |
|
1913 by (auto elim!: nonpos_Ints_cases) |
|
1914 from no_int no_int' have no_int: "1 - z \<notin> \<int>\<^sub>\<le>\<^sub>0" "1 + z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto |
|
1915 have "(h2 has_field_derivative h2' z) (at z)" unfolding h2_def |
|
1916 by (rule DERIV_cong, (rule derivative_intros refl derivs[unfolded POWSER_def] nz no_int)+) |
|
1917 (auto simp: h2'_def POWSER_def field_simps power2_eq_square) |
|
1918 ultimately have deriv: "(h has_field_derivative h2' z) (at z)" |
|
1919 by (subst DERIV_cong_ev[OF refl _ refl]) |
|
1920 |
|
1921 from sums(2)[OF z] z have "(\<Sum>n. g n * (a * z) ^ n) \<noteq> 0" |
|
1922 unfolding G_def by (auto simp: sums_iff a_def sin_eq_0) |
|
1923 hence "isCont h2' z" using no_int unfolding h2'_def[abs_def] POWSER_def POWSER'_def |
|
1924 by (intro continuous_intros cont |
|
1925 continuous_on_compose2[OF _ continuous_on_Polygamma[of "{z. Re z > 0}"]]) auto |
|
1926 note deriv and this |
|
1927 } note A = this |
|
1928 |
|
1929 interpret h: periodic_fun_simple' h |
|
1930 proof |
|
1931 fix z :: complex |
|
1932 show "h (z + 1) = h z" |
|
1933 proof (cases "z \<in> \<int>") |
|
1934 assume z: "z \<notin> \<int>" |
|
1935 hence A: "z + 1 \<notin> \<int>" "z \<noteq> 0" using Ints_diff[of "z+1" 1] by auto |
|
1936 hence "Digamma (z + 1) - Digamma (-z) = Digamma z - Digamma (-z + 1)" |
|
1937 by (subst (1 2) Digamma_plus1) simp_all |
|
1938 with A z show "h (z + 1) = h z" |
|
1939 by (simp add: h_def sin_plus_pi cos_plus_pi ring_distribs cot_def) |
|
1940 qed (simp add: h_def) |
|
1941 qed |
|
1942 |
|
1943 have h2'_eq: "h2' (z - 1) = h2' z" if z: "Re z > 0" "Re z < 1" for z |
|
1944 proof - |
|
1945 have "((\<lambda>z. h (z - 1)) has_field_derivative h2' (z - 1)) (at z)" |
|
1946 by (rule DERIV_cong, rule DERIV_chain'[OF _ A(1)]) |
|
1947 (insert z, auto intro!: derivative_eq_intros) |
|
1948 hence "(h has_field_derivative h2' (z - 1)) (at z)" by (subst (asm) h.minus_1) |
|
1949 moreover from z have "(h has_field_derivative h2' z) (at z)" by (intro A) simp_all |
|
1950 ultimately show "h2' (z - 1) = h2' z" by (rule DERIV_unique) |
|
1951 qed |
|
1952 |
|
1953 define h2'' where "h2'' z = h2' (z - of_int \<lfloor>Re z\<rfloor>)" for z |
|
1954 have deriv: "(h has_field_derivative h2'' z) (at z)" for z |
|
1955 proof - |
|
1956 fix z :: complex |
|
1957 have B: "\<bar>Re z - real_of_int \<lfloor>Re z\<rfloor>\<bar> < 1" by linarith |
|
1958 have "((\<lambda>t. h (t - of_int \<lfloor>Re z\<rfloor>)) has_field_derivative h2'' z) (at z)" |
|
1959 unfolding h2''_def by (rule DERIV_cong, rule DERIV_chain'[OF _ A(1)]) |
|
1960 (insert B, auto intro!: derivative_intros) |
|
1961 thus "(h has_field_derivative h2'' z) (at z)" by (simp add: h.minus_of_int) |
|
1962 qed |
|
1963 |
|
1964 have cont: "continuous_on UNIV h2''" |
|
1965 proof (intro continuous_at_imp_continuous_on ballI) |
|
1966 fix z :: complex |
|
1967 define r where "r = \<lfloor>Re z\<rfloor>" |
|
1968 define A where "A = {t. of_int r - 1 < Re t \<and> Re t < of_int r + 1}" |
|
1969 have "continuous_on A (\<lambda>t. h2' (t - of_int r))" unfolding A_def |
|
1970 by (intro continuous_at_imp_continuous_on isCont_o2[OF _ A(2)] ballI continuous_intros) |
|
1971 (simp_all add: abs_real_def) |
|
1972 moreover have "h2'' t = h2' (t - of_int r)" if t: "t \<in> A" for t |
|
1973 proof (cases "Re t \<ge> of_int r") |
|
1974 case True |
|
1975 from t have "of_int r - 1 < Re t" "Re t < of_int r + 1" by (simp_all add: A_def) |
|
1976 with True have "\<lfloor>Re t\<rfloor> = \<lfloor>Re z\<rfloor>" unfolding r_def by linarith |
|
1977 thus ?thesis by (auto simp: r_def h2''_def) |
|
1978 next |
|
1979 case False |
|
1980 from t have t: "of_int r - 1 < Re t" "Re t < of_int r + 1" by (simp_all add: A_def) |
|
1981 with False have t': "\<lfloor>Re t\<rfloor> = \<lfloor>Re z\<rfloor> - 1" unfolding r_def by linarith |
|
1982 moreover from t False have "h2' (t - of_int r + 1 - 1) = h2' (t - of_int r + 1)" |
|
1983 by (intro h2'_eq) simp_all |
|
1984 ultimately show ?thesis by (auto simp: r_def h2''_def algebra_simps t') |
|
1985 qed |
|
1986 ultimately have "continuous_on A h2''" by (subst continuous_on_cong[OF refl]) |
|
1987 moreover { |
|
1988 have "open ({t. of_int r - 1 < Re t} \<inter> {t. of_int r + 1 > Re t})" |
|
1989 by (intro open_Int open_halfspace_Re_gt open_halfspace_Re_lt) |
|
1990 also have "{t. of_int r - 1 < Re t} \<inter> {t. of_int r + 1 > Re t} = A" |
|
1991 unfolding A_def by blast |
|
1992 finally have "open A" . |
|
1993 } |
|
1994 ultimately have C: "isCont h2'' t" if "t \<in> A" for t using that |
|
1995 by (subst (asm) continuous_on_eq_continuous_at) auto |
|
1996 have "of_int r - 1 < Re z" "Re z < of_int r + 1" unfolding r_def by linarith+ |
|
1997 thus "isCont h2'' z" by (intro C) (simp_all add: A_def) |
|
1998 qed |
|
1999 |
|
2000 from that[OF cont deriv] show ?thesis . |
|
2001 qed |
|
2002 |
|
2003 lemma Gamma_reflection_complex: |
|
2004 fixes z :: complex |
|
2005 shows "Gamma z * Gamma (1 - z) = of_real pi / sin (of_real pi * z)" |
|
2006 proof - |
|
2007 let ?g = "\<lambda>z::complex. Gamma z * Gamma (1 - z) * sin (of_real pi * z)" |
|
2008 define g where [abs_def]: "g z = (if z \<in> \<int> then of_real pi else ?g z)" for z :: complex |
|
2009 let ?h = "\<lambda>z::complex. (of_real pi * cot (of_real pi*z) + Digamma z - Digamma (1 - z))" |
|
2010 define h where [abs_def]: "h z = (if z \<in> \<int> then 0 else ?h z)" for z :: complex |
|
2011 |
|
2012 \<comment> \<open>@{term g} is periodic with period 1.\<close> |
|
2013 interpret g: periodic_fun_simple' g |
|
2014 proof |
|
2015 fix z :: complex |
|
2016 show "g (z + 1) = g z" |
|
2017 proof (cases "z \<in> \<int>") |
|
2018 case False |
|
2019 hence "z * g z = z * Beta z (- z + 1) * sin (of_real pi * z)" by (simp add: g_def Beta_def) |
|
2020 also have "z * Beta z (- z + 1) = (z + 1 + -z) * Beta (z + 1) (- z + 1)" |
|
2021 using False Ints_diff[of 1 "1 - z"] nonpos_Ints_subset_Ints |
|
2022 by (subst Beta_plus1_left [symmetric]) auto |
|
2023 also have "\<dots> * sin (of_real pi * z) = z * (Beta (z + 1) (-z) * sin (of_real pi * (z + 1)))" |
|
2024 using False Ints_diff[of "z+1" 1] Ints_minus[of "-z"] nonpos_Ints_subset_Ints |
|
2025 by (subst Beta_plus1_right) (auto simp: ring_distribs sin_plus_pi) |
|
2026 also from False have "Beta (z + 1) (-z) * sin (of_real pi * (z + 1)) = g (z + 1)" |
|
2027 using Ints_diff[of "z+1" 1] by (auto simp: g_def Beta_def) |
|
2028 finally show "g (z + 1) = g z" using False by (subst (asm) mult_left_cancel) auto |
|
2029 qed (simp add: g_def) |
|
2030 qed |
|
2031 |
|
2032 \<comment> \<open>@{term g} is entire.\<close> |
|
2033 have g_g': "(g has_field_derivative (h z * g z)) (at z)" for z :: complex |
|
2034 proof (cases "z \<in> \<int>") |
|
2035 let ?h' = "\<lambda>z. Beta z (1 - z) * ((Digamma z - Digamma (1 - z)) * sin (z * of_real pi) + |
|
2036 of_real pi * cos (z * of_real pi))" |
|
2037 case False |
|
2038 from False have "eventually (\<lambda>t. t \<in> UNIV - \<int>) (nhds z)" |
|
2039 by (intro eventually_nhds_in_open) (auto simp: open_Diff) |
|
2040 hence "eventually (\<lambda>t. g t = ?g t) (nhds z)" by eventually_elim (simp add: g_def) |
|
2041 moreover { |
|
2042 from False Ints_diff[of 1 "1-z"] have "1 - z \<notin> \<int>" by auto |
|
2043 hence "(?g has_field_derivative ?h' z) (at z)" using nonpos_Ints_subset_Ints |
|
2044 by (auto intro!: derivative_eq_intros simp: algebra_simps Beta_def) |
|
2045 also from False have "sin (of_real pi * z) \<noteq> 0" by (subst sin_eq_0) auto |
|
2046 hence "?h' z = h z * g z" |
|
2047 using False unfolding g_def h_def cot_def by (simp add: field_simps Beta_def) |
|
2048 finally have "(?g has_field_derivative (h z * g z)) (at z)" . |
|
2049 } |
|
2050 ultimately show ?thesis by (subst DERIV_cong_ev[OF refl _ refl]) |
|
2051 next |
|
2052 case True |
|
2053 then obtain n where z: "z = of_int n" by (auto elim!: Ints_cases) |
|
2054 let ?t = "(\<lambda>z::complex. if z = 0 then 1 else sin z / z) \<circ> (\<lambda>z. of_real pi * z)" |
|
2055 have deriv_0: "(g has_field_derivative 0) (at 0)" |
|
2056 proof (subst DERIV_cong_ev[OF refl _ refl]) |
|
2057 show "eventually (\<lambda>z. g z = of_real pi * Gamma (1 + z) * Gamma (1 - z) * ?t z) (nhds 0)" |
|
2058 using eventually_nhds_ball[OF zero_less_one, of "0::complex"] |
|
2059 proof eventually_elim |
|
2060 fix z :: complex assume z: "z \<in> ball 0 1" |
|
2061 show "g z = of_real pi * Gamma (1 + z) * Gamma (1 - z) * ?t z" |
|
2062 proof (cases "z = 0") |
|
2063 assume z': "z \<noteq> 0" |
|
2064 with z have z'': "z \<notin> \<int>\<^sub>\<le>\<^sub>0" "z \<notin> \<int>" by (auto elim!: Ints_cases simp: dist_0_norm) |
|
2065 from Gamma_plus1[OF this(1)] have "Gamma z = Gamma (z + 1) / z" by simp |
|
2066 with z'' z' show ?thesis by (simp add: g_def ac_simps) |
|
2067 qed (simp add: g_def) |
|
2068 qed |
|
2069 have "(?t has_field_derivative (0 * of_real pi)) (at 0)" |
|
2070 using has_field_derivative_sin_z_over_z[of "UNIV :: complex set"] |
|
2071 by (intro DERIV_chain) simp_all |
|
2072 thus "((\<lambda>z. of_real pi * Gamma (1 + z) * Gamma (1 - z) * ?t z) has_field_derivative 0) (at 0)" |
|
2073 by (auto intro!: derivative_eq_intros simp: o_def) |
|
2074 qed |
|
2075 |
|
2076 have "((g \<circ> (\<lambda>x. x - of_int n)) has_field_derivative 0 * 1) (at (of_int n))" |
|
2077 using deriv_0 by (intro DERIV_chain) (auto intro!: derivative_eq_intros) |
|
2078 also have "g \<circ> (\<lambda>x. x - of_int n) = g" by (intro ext) (simp add: g.minus_of_int) |
|
2079 finally show "(g has_field_derivative (h z * g z)) (at z)" by (simp add: z h_def) |
|
2080 qed |
|
2081 |
|
2082 have g_eq: "g (z/2) * g ((z+1)/2) = Gamma (1/2)^2 * g z" if "Re z > -1" "Re z < 2" for z |
|
2083 proof (cases "z \<in> \<int>") |
|
2084 case True |
|
2085 with that have "z = 0 \<or> z = 1" by (force elim!: Ints_cases) |
|
2086 moreover have "g 0 * g (1/2) = Gamma (1/2)^2 * g 0" |
|
2087 using fraction_not_in_ints[where 'a = complex, of 2 1] by (simp add: g_def power2_eq_square) |
|
2088 moreover have "g (1/2) * g 1 = Gamma (1/2)^2 * g 1" |
|
2089 using fraction_not_in_ints[where 'a = complex, of 2 1] |
|
2090 by (simp add: g_def power2_eq_square Beta_def algebra_simps) |
|
2091 ultimately show ?thesis by force |
|
2092 next |
|
2093 case False |
|
2094 hence z: "z/2 \<notin> \<int>" "(z+1)/2 \<notin> \<int>" using Ints_diff[of "z+1" 1] by (auto elim!: Ints_cases) |
|
2095 hence z': "z/2 \<notin> \<int>\<^sub>\<le>\<^sub>0" "(z+1)/2 \<notin> \<int>\<^sub>\<le>\<^sub>0" by (auto elim!: nonpos_Ints_cases) |
|
2096 from z have "1-z/2 \<notin> \<int>" "1-((z+1)/2) \<notin> \<int>" |
|
2097 using Ints_diff[of 1 "1-z/2"] Ints_diff[of 1 "1-((z+1)/2)"] by auto |
|
2098 hence z'': "1-z/2 \<notin> \<int>\<^sub>\<le>\<^sub>0" "1-((z+1)/2) \<notin> \<int>\<^sub>\<le>\<^sub>0" by (auto elim!: nonpos_Ints_cases) |
|
2099 from z have "g (z/2) * g ((z+1)/2) = |
|
2100 (Gamma (z/2) * Gamma ((z+1)/2)) * (Gamma (1-z/2) * Gamma (1-((z+1)/2))) * |
|
2101 (sin (of_real pi * z/2) * sin (of_real pi * (z+1)/2))" |
|
2102 by (simp add: g_def) |
|
2103 also from z' Gamma_legendre_duplication_aux[of "z/2"] |
|
2104 have "Gamma (z/2) * Gamma ((z+1)/2) = exp ((1-z) * of_real (ln 2)) * Gamma (1/2) * Gamma z" |
|
2105 by (simp add: add_divide_distrib) |
|
2106 also from z'' Gamma_legendre_duplication_aux[of "1-(z+1)/2"] |
|
2107 have "Gamma (1-z/2) * Gamma (1-(z+1)/2) = |
|
2108 Gamma (1-z) * Gamma (1/2) * exp (z * of_real (ln 2))" |
|
2109 by (simp add: add_divide_distrib ac_simps) |
|
2110 finally have "g (z/2) * g ((z+1)/2) = Gamma (1/2)^2 * (Gamma z * Gamma (1-z) * |
|
2111 (2 * (sin (of_real pi*z/2) * sin (of_real pi*(z+1)/2))))" |
|
2112 by (simp add: add_ac power2_eq_square exp_add ring_distribs exp_diff exp_of_real) |
|
2113 also have "sin (of_real pi*(z+1)/2) = cos (of_real pi*z/2)" |
|
2114 using cos_sin_eq[of "- of_real pi * z/2", symmetric] |
|
2115 by (simp add: ring_distribs add_divide_distrib ac_simps) |
|
2116 also have "2 * (sin (of_real pi*z/2) * cos (of_real pi*z/2)) = sin (of_real pi * z)" |
|
2117 by (subst sin_times_cos) (simp add: field_simps) |
|
2118 also have "Gamma z * Gamma (1 - z) * sin (complex_of_real pi * z) = g z" |
|
2119 using \<open>z \<notin> \<int>\<close> by (simp add: g_def) |
|
2120 finally show ?thesis . |
|
2121 qed |
|
2122 have g_eq: "g (z/2) * g ((z+1)/2) = Gamma (1/2)^2 * g z" for z |
|
2123 proof - |
|
2124 define r where "r = \<lfloor>Re z / 2\<rfloor>" |
|
2125 have "Gamma (1/2)^2 * g z = Gamma (1/2)^2 * g (z - of_int (2*r))" by (simp only: g.minus_of_int) |
|
2126 also have "of_int (2*r) = 2 * of_int r" by simp |
|
2127 also have "Re z - 2 * of_int r > -1" "Re z - 2 * of_int r < 2" unfolding r_def by linarith+ |
|
2128 hence "Gamma (1/2)^2 * g (z - 2 * of_int r) = |
|
2129 g ((z - 2 * of_int r)/2) * g ((z - 2 * of_int r + 1)/2)" |
|
2130 unfolding r_def by (intro g_eq[symmetric]) simp_all |
|
2131 also have "(z - 2 * of_int r) / 2 = z/2 - of_int r" by simp |
|
2132 also have "g \<dots> = g (z/2)" by (rule g.minus_of_int) |
|
2133 also have "(z - 2 * of_int r + 1) / 2 = (z + 1)/2 - of_int r" by simp |
|
2134 also have "g \<dots> = g ((z+1)/2)" by (rule g.minus_of_int) |
|
2135 finally show ?thesis .. |
|
2136 qed |
|
2137 |
|
2138 have g_nz [simp]: "g z \<noteq> 0" for z :: complex |
|
2139 unfolding g_def using Ints_diff[of 1 "1 - z"] |
|
2140 by (auto simp: Gamma_eq_zero_iff sin_eq_0 dest!: nonpos_Ints_Int) |
|
2141 |
|
2142 have h_eq: "h z = (h (z/2) + h ((z+1)/2)) / 2" for z |
|
2143 proof - |
|
2144 have "((\<lambda>t. g (t/2) * g ((t+1)/2)) has_field_derivative |
|
2145 (g (z/2) * g ((z+1)/2)) * ((h (z/2) + h ((z+1)/2)) / 2)) (at z)" |
|
2146 by (auto intro!: derivative_eq_intros g_g'[THEN DERIV_chain2] simp: field_simps) |
|
2147 hence "((\<lambda>t. Gamma (1/2)^2 * g t) has_field_derivative |
|
2148 Gamma (1/2)^2 * g z * ((h (z/2) + h ((z+1)/2)) / 2)) (at z)" |
|
2149 by (subst (1 2) g_eq[symmetric]) simp |
|
2150 from DERIV_cmult[OF this, of "inverse ((Gamma (1/2))^2)"] |
|
2151 have "(g has_field_derivative (g z * ((h (z/2) + h ((z+1)/2))/2))) (at z)" |
|
2152 using fraction_not_in_ints[where 'a = complex, of 2 1] |
|
2153 by (simp add: divide_simps Gamma_eq_zero_iff not_in_Ints_imp_not_in_nonpos_Ints) |
|
2154 moreover have "(g has_field_derivative (g z * h z)) (at z)" |
|
2155 using g_g'[of z] by (simp add: ac_simps) |
|
2156 ultimately have "g z * h z = g z * ((h (z/2) + h ((z+1)/2))/2)" |
|
2157 by (intro DERIV_unique) |
|
2158 thus "h z = (h (z/2) + h ((z+1)/2)) / 2" by simp |
|
2159 qed |
|
2160 |
|
2161 obtain h' where h'_cont: "continuous_on UNIV h'" and |
|
2162 h_h': "\<And>z. (h has_field_derivative h' z) (at z)" |
|
2163 unfolding h_def by (erule Gamma_reflection_aux) |
|
2164 |
|
2165 have h'_eq: "h' z = (h' (z/2) + h' ((z+1)/2)) / 4" for z |
|
2166 proof - |
|
2167 have "((\<lambda>t. (h (t/2) + h ((t+1)/2)) / 2) has_field_derivative |
|
2168 ((h' (z/2) + h' ((z+1)/2)) / 4)) (at z)" |
|
2169 by (fastforce intro!: derivative_eq_intros h_h'[THEN DERIV_chain2]) |
|
2170 hence "(h has_field_derivative ((h' (z/2) + h' ((z+1)/2))/4)) (at z)" |
|
2171 by (subst (asm) h_eq[symmetric]) |
|
2172 from h_h' and this show "h' z = (h' (z/2) + h' ((z+1)/2)) / 4" by (rule DERIV_unique) |
|
2173 qed |
|
2174 |
|
2175 have h'_zero: "h' z = 0" for z |
|
2176 proof - |
|
2177 define m where "m = max 1 \<bar>Re z\<bar>" |
|
2178 define B where "B = {t. abs (Re t) \<le> m \<and> abs (Im t) \<le> abs (Im z)}" |
|
2179 have "closed ({t. Re t \<ge> -m} \<inter> {t. Re t \<le> m} \<inter> |
|
2180 {t. Im t \<ge> -\<bar>Im z\<bar>} \<inter> {t. Im t \<le> \<bar>Im z\<bar>})" |
|
2181 (is "closed ?B") by (intro closed_Int closed_halfspace_Re_ge closed_halfspace_Re_le |
|
2182 closed_halfspace_Im_ge closed_halfspace_Im_le) |
|
2183 also have "?B = B" unfolding B_def by fastforce |
|
2184 finally have "closed B" . |
|
2185 moreover have "bounded B" unfolding bounded_iff |
|
2186 proof (intro ballI exI) |
|
2187 fix t assume t: "t \<in> B" |
|
2188 have "norm t \<le> \<bar>Re t\<bar> + \<bar>Im t\<bar>" by (rule cmod_le) |
|
2189 also from t have "\<bar>Re t\<bar> \<le> m" unfolding B_def by blast |
|
2190 also from t have "\<bar>Im t\<bar> \<le> \<bar>Im z\<bar>" unfolding B_def by blast |
|
2191 finally show "norm t \<le> m + \<bar>Im z\<bar>" by - simp |
|
2192 qed |
|
2193 ultimately have compact: "compact B" by (subst compact_eq_bounded_closed) blast |
|
2194 |
|
2195 define M where "M = (SUP z:B. norm (h' z))" |
|
2196 have "compact (h' ` B)" |
|
2197 by (intro compact_continuous_image continuous_on_subset[OF h'_cont] compact) blast+ |
|
2198 hence bdd: "bdd_above ((\<lambda>z. norm (h' z)) ` B)" |
|
2199 using bdd_above_norm[of "h' ` B"] by (simp add: image_comp o_def compact_imp_bounded) |
|
2200 have "norm (h' z) \<le> M" unfolding M_def by (intro cSUP_upper bdd) (simp_all add: B_def m_def) |
|
2201 also have "M \<le> M/2" |
|
2202 proof (subst M_def, subst cSUP_le_iff) |
|
2203 have "z \<in> B" unfolding B_def m_def by simp |
|
2204 thus "B \<noteq> {}" by auto |
|
2205 next |
|
2206 show "\<forall>z\<in>B. norm (h' z) \<le> M/2" |
|
2207 proof |
|
2208 fix t :: complex assume t: "t \<in> B" |
|
2209 from h'_eq[of t] t have "h' t = (h' (t/2) + h' ((t+1)/2)) / 4" by (simp add: dist_0_norm) |
|
2210 also have "norm \<dots> = norm (h' (t/2) + h' ((t+1)/2)) / 4" by simp |
|
2211 also have "norm (h' (t/2) + h' ((t+1)/2)) \<le> norm (h' (t/2)) + norm (h' ((t+1)/2))" |
|
2212 by (rule norm_triangle_ineq) |
|
2213 also from t have "abs (Re ((t + 1)/2)) \<le> m" unfolding m_def B_def by auto |
|
2214 with t have "t/2 \<in> B" "(t+1)/2 \<in> B" unfolding B_def by auto |
|
2215 hence "norm (h' (t/2)) + norm (h' ((t+1)/2)) \<le> M + M" unfolding M_def |
|
2216 by (intro add_mono cSUP_upper bdd) (auto simp: B_def) |
|
2217 also have "(M + M) / 4 = M / 2" by simp |
|
2218 finally show "norm (h' t) \<le> M/2" by - simp_all |
|
2219 qed |
|
2220 qed (insert bdd, auto simp: cball_eq_empty) |
|
2221 hence "M \<le> 0" by simp |
|
2222 finally show "h' z = 0" by simp |
|
2223 qed |
|
2224 have h_h'_2: "(h has_field_derivative 0) (at z)" for z |
|
2225 using h_h'[of z] h'_zero[of z] by simp |
|
2226 |
|
2227 have g_real: "g z \<in> \<real>" if "z \<in> \<real>" for z |
|
2228 unfolding g_def using that by (auto intro!: Reals_mult Gamma_complex_real) |
|
2229 have h_real: "h z \<in> \<real>" if "z \<in> \<real>" for z |
|
2230 unfolding h_def using that by (auto intro!: Reals_mult Reals_add Reals_diff Polygamma_Real) |
|
2231 have g_nz: "g z \<noteq> 0" for z unfolding g_def using Ints_diff[of 1 "1-z"] |
|
2232 by (auto simp: Gamma_eq_zero_iff sin_eq_0) |
|
2233 |
|
2234 from h'_zero h_h'_2 have "\<exists>c. \<forall>z\<in>UNIV. h z = c" |
|
2235 by (intro has_field_derivative_zero_constant) (simp_all add: dist_0_norm) |
|
2236 then obtain c where c: "\<And>z. h z = c" by auto |
|
2237 have "\<exists>u. u \<in> closed_segment 0 1 \<and> Re (g 1) - Re (g 0) = Re (h u * g u * (1 - 0))" |
|
2238 by (intro complex_mvt_line g_g') |
|
2239 find_theorems name:deriv Reals |
|
2240 then guess u by (elim exE conjE) note u = this |
|
2241 from u(1) have u': "u \<in> \<real>" unfolding closed_segment_def |
|
2242 by (auto simp: scaleR_conv_of_real) |
|
2243 from u' g_real[of u] g_nz[of u] have "Re (g u) \<noteq> 0" by (auto elim!: Reals_cases) |
|
2244 with u(2) c[of u] g_real[of u] g_nz[of u] u' |
|
2245 have "Re c = 0" by (simp add: complex_is_Real_iff g.of_1) |
|
2246 with h_real[of 0] c[of 0] have "c = 0" by (auto elim!: Reals_cases) |
|
2247 with c have A: "h z * g z = 0" for z by simp |
|
2248 hence "(g has_field_derivative 0) (at z)" for z using g_g'[of z] by simp |
|
2249 hence "\<exists>c'. \<forall>z\<in>UNIV. g z = c'" by (intro has_field_derivative_zero_constant) simp_all |
|
2250 then obtain c' where c: "\<And>z. g z = c'" by (force simp: dist_0_norm) |
|
2251 from this[of 0] have "c' = pi" unfolding g_def by simp |
|
2252 with c have "g z = pi" by simp |
|
2253 |
|
2254 show ?thesis |
|
2255 proof (cases "z \<in> \<int>") |
|
2256 case False |
|
2257 with \<open>g z = pi\<close> show ?thesis by (auto simp: g_def divide_simps) |
|
2258 next |
|
2259 case True |
|
2260 then obtain n where n: "z = of_int n" by (elim Ints_cases) |
|
2261 with sin_eq_0[of "of_real pi * z"] have "sin (of_real pi * z) = 0" by force |
|
2262 moreover have "of_int (1 - n) \<in> \<int>\<^sub>\<le>\<^sub>0" if "n > 0" using that by (intro nonpos_Ints_of_int) simp |
|
2263 ultimately show ?thesis using n |
|
2264 by (cases "n \<le> 0") (auto simp: Gamma_eq_zero_iff nonpos_Ints_of_int) |
|
2265 qed |
|
2266 qed |
|
2267 |
|
2268 lemma rGamma_reflection_complex: |
|
2269 "rGamma z * rGamma (1 - z :: complex) = sin (of_real pi * z) / of_real pi" |
|
2270 using Gamma_reflection_complex[of z] |
|
2271 by (simp add: Gamma_def divide_simps split: if_split_asm) |
|
2272 |
|
2273 lemma rGamma_reflection_complex': |
|
2274 "rGamma z * rGamma (- z :: complex) = -z * sin (of_real pi * z) / of_real pi" |
|
2275 proof - |
|
2276 have "rGamma z * rGamma (-z) = -z * (rGamma z * rGamma (1 - z))" |
|
2277 using rGamma_plus1[of "-z", symmetric] by simp |
|
2278 also have "rGamma z * rGamma (1 - z) = sin (of_real pi * z) / of_real pi" |
|
2279 by (rule rGamma_reflection_complex) |
|
2280 finally show ?thesis by simp |
|
2281 qed |
|
2282 |
|
2283 lemma Gamma_reflection_complex': |
|
2284 "Gamma z * Gamma (- z :: complex) = - of_real pi / (z * sin (of_real pi * z))" |
|
2285 using rGamma_reflection_complex'[of z] by (force simp add: Gamma_def divide_simps mult_ac) |
|
2286 |
|
2287 |
|
2288 |
|
2289 lemma Gamma_one_half_real: "Gamma (1/2 :: real) = sqrt pi" |
|
2290 proof - |
|
2291 from Gamma_reflection_complex[of "1/2"] fraction_not_in_ints[where 'a = complex, of 2 1] |
|
2292 have "Gamma (1/2 :: complex)^2 = of_real pi" by (simp add: power2_eq_square) |
|
2293 hence "of_real pi = Gamma (complex_of_real (1/2))^2" by simp |
|
2294 also have "\<dots> = of_real ((Gamma (1/2))^2)" by (subst Gamma_complex_of_real) simp_all |
|
2295 finally have "Gamma (1/2)^2 = pi" by (subst (asm) of_real_eq_iff) simp_all |
|
2296 moreover have "Gamma (1/2 :: real) \<ge> 0" using Gamma_real_pos[of "1/2"] by simp |
|
2297 ultimately show ?thesis by (rule real_sqrt_unique [symmetric]) |
|
2298 qed |
|
2299 |
|
2300 lemma Gamma_one_half_complex: "Gamma (1/2 :: complex) = of_real (sqrt pi)" |
|
2301 proof - |
|
2302 have "Gamma (1/2 :: complex) = Gamma (of_real (1/2))" by simp |
|
2303 also have "\<dots> = of_real (sqrt pi)" by (simp only: Gamma_complex_of_real Gamma_one_half_real) |
|
2304 finally show ?thesis . |
|
2305 qed |
|
2306 |
|
2307 lemma Gamma_legendre_duplication: |
|
2308 fixes z :: complex |
|
2309 assumes "z \<notin> \<int>\<^sub>\<le>\<^sub>0" "z + 1/2 \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
2310 shows "Gamma z * Gamma (z + 1/2) = |
|
2311 exp ((1 - 2*z) * of_real (ln 2)) * of_real (sqrt pi) * Gamma (2*z)" |
|
2312 using Gamma_legendre_duplication_aux[OF assms] by (simp add: Gamma_one_half_complex) |
|
2313 |
|
2314 end |
|
2315 |
|
2316 |
|
2317 subsection \<open>Limits and residues\<close> |
|
2318 |
|
2319 text \<open> |
|
2320 The inverse of the Gamma function has simple zeros: |
|
2321 \<close> |
|
2322 |
|
2323 lemma rGamma_zeros: |
|
2324 "(\<lambda>z. rGamma z / (z + of_nat n)) \<midarrow> (- of_nat n) \<rightarrow> ((-1)^n * fact n :: 'a :: Gamma)" |
|
2325 proof (subst tendsto_cong) |
|
2326 let ?f = "\<lambda>z. pochhammer z n * rGamma (z + of_nat (Suc n)) :: 'a" |
|
2327 from eventually_at_ball'[OF zero_less_one, of "- of_nat n :: 'a" UNIV] |
|
2328 show "eventually (\<lambda>z. rGamma z / (z + of_nat n) = ?f z) (at (- of_nat n))" |
|
2329 by (subst pochhammer_rGamma[of _ "Suc n"]) |
|
2330 (auto elim!: eventually_mono simp: divide_simps pochhammer_rec' eq_neg_iff_add_eq_0) |
|
2331 have "isCont ?f (- of_nat n)" by (intro continuous_intros) |
|
2332 thus "?f \<midarrow> (- of_nat n) \<rightarrow> (- 1) ^ n * fact n" unfolding isCont_def |
|
2333 by (simp add: pochhammer_same) |
|
2334 qed |
|
2335 |
|
2336 |
|
2337 text \<open> |
|
2338 The simple zeros of the inverse of the Gamma function correspond to simple poles of the Gamma function, |
|
2339 and their residues can easily be computed from the limit we have just proven: |
|
2340 \<close> |
|
2341 |
|
2342 lemma Gamma_poles: "filterlim Gamma at_infinity (at (- of_nat n :: 'a :: Gamma))" |
|
2343 proof - |
|
2344 from eventually_at_ball'[OF zero_less_one, of "- of_nat n :: 'a" UNIV] |
|
2345 have "eventually (\<lambda>z. rGamma z \<noteq> (0 :: 'a)) (at (- of_nat n))" |
|
2346 by (auto elim!: eventually_mono nonpos_Ints_cases' |
|
2347 simp: rGamma_eq_zero_iff dist_of_nat dist_minus) |
|
2348 with isCont_rGamma[of "- of_nat n :: 'a", OF continuous_ident] |
|
2349 have "filterlim (\<lambda>z. inverse (rGamma z) :: 'a) at_infinity (at (- of_nat n))" |
|
2350 unfolding isCont_def by (intro filterlim_compose[OF filterlim_inverse_at_infinity]) |
|
2351 (simp_all add: filterlim_at) |
|
2352 moreover have "(\<lambda>z. inverse (rGamma z) :: 'a) = Gamma" |
|
2353 by (intro ext) (simp add: rGamma_inverse_Gamma) |
|
2354 ultimately show ?thesis by (simp only: ) |
|
2355 qed |
|
2356 |
|
2357 lemma Gamma_residues: |
|
2358 "(\<lambda>z. Gamma z * (z + of_nat n)) \<midarrow> (- of_nat n) \<rightarrow> ((-1)^n / fact n :: 'a :: Gamma)" |
|
2359 proof (subst tendsto_cong) |
|
2360 let ?c = "(- 1) ^ n / fact n :: 'a" |
|
2361 from eventually_at_ball'[OF zero_less_one, of "- of_nat n :: 'a" UNIV] |
|
2362 show "eventually (\<lambda>z. Gamma z * (z + of_nat n) = inverse (rGamma z / (z + of_nat n))) |
|
2363 (at (- of_nat n))" |
|
2364 by (auto elim!: eventually_mono simp: divide_simps rGamma_inverse_Gamma) |
|
2365 have "(\<lambda>z. inverse (rGamma z / (z + of_nat n))) \<midarrow> (- of_nat n) \<rightarrow> |
|
2366 inverse ((- 1) ^ n * fact n :: 'a)" |
|
2367 by (intro tendsto_intros rGamma_zeros) simp_all |
|
2368 also have "inverse ((- 1) ^ n * fact n) = ?c" |
|
2369 by (simp_all add: field_simps power_mult_distrib [symmetric] del: power_mult_distrib) |
|
2370 finally show "(\<lambda>z. inverse (rGamma z / (z + of_nat n))) \<midarrow> (- of_nat n) \<rightarrow> ?c" . |
|
2371 qed |
|
2372 |
|
2373 |
|
2374 |
|
2375 subsection \<open>Alternative definitions\<close> |
|
2376 |
|
2377 |
|
2378 subsubsection \<open>Variant of the Euler form\<close> |
|
2379 |
|
2380 |
|
2381 definition Gamma_series_euler' where |
|
2382 "Gamma_series_euler' z n = |
|
2383 inverse z * (\<Prod>k=1..n. exp (z * of_real (ln (1 + inverse (of_nat k)))) / (1 + z / of_nat k))" |
|
2384 |
|
2385 context |
|
2386 begin |
|
2387 private lemma Gamma_euler'_aux1: |
|
2388 fixes z :: "'a :: {real_normed_field,banach}" |
|
2389 assumes n: "n > 0" |
|
2390 shows "exp (z * of_real (ln (of_nat n + 1))) = (\<Prod>k=1..n. exp (z * of_real (ln (1 + 1 / of_nat k))))" |
|
2391 proof - |
|
2392 have "(\<Prod>k=1..n. exp (z * of_real (ln (1 + 1 / of_nat k)))) = |
|
2393 exp (z * of_real (\<Sum>k = 1..n. ln (1 + 1 / real_of_nat k)))" |
|
2394 by (subst exp_setsum [symmetric]) (simp_all add: setsum_right_distrib) |
|
2395 also have "(\<Sum>k=1..n. ln (1 + 1 / of_nat k) :: real) = ln (\<Prod>k=1..n. 1 + 1 / real_of_nat k)" |
|
2396 by (subst ln_setprod [symmetric]) (auto intro!: add_pos_nonneg) |
|
2397 also have "(\<Prod>k=1..n. 1 + 1 / of_nat k :: real) = (\<Prod>k=1..n. (of_nat k + 1) / of_nat k)" |
|
2398 by (intro setprod.cong) (simp_all add: divide_simps) |
|
2399 also have "(\<Prod>k=1..n. (of_nat k + 1) / of_nat k :: real) = of_nat n + 1" |
|
2400 by (induction n) (simp_all add: setprod_nat_ivl_Suc' divide_simps) |
|
2401 finally show ?thesis .. |
|
2402 qed |
|
2403 |
|
2404 lemma Gamma_series_euler': |
|
2405 assumes z: "(z :: 'a :: Gamma) \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
2406 shows "(\<lambda>n. Gamma_series_euler' z n) \<longlonglongrightarrow> Gamma z" |
|
2407 proof (rule Gamma_seriesI, rule Lim_transform_eventually) |
|
2408 let ?f = "\<lambda>n. fact n * exp (z * of_real (ln (of_nat n + 1))) / pochhammer z (n + 1)" |
|
2409 let ?r = "\<lambda>n. ?f n / Gamma_series z n" |
|
2410 let ?r' = "\<lambda>n. exp (z * of_real (ln (of_nat (Suc n) / of_nat n)))" |
|
2411 from z have z': "z \<noteq> 0" by auto |
|
2412 |
|
2413 have "eventually (\<lambda>n. ?r' n = ?r n) sequentially" using eventually_gt_at_top[of "0::nat"] |
|
2414 using z by (auto simp: divide_simps Gamma_series_def ring_distribs exp_diff ln_div add_ac |
|
2415 elim!: eventually_mono dest: pochhammer_eq_0_imp_nonpos_Int) |
|
2416 moreover have "?r' \<longlonglongrightarrow> exp (z * of_real (ln 1))" |
|
2417 by (intro tendsto_intros LIMSEQ_Suc_n_over_n) simp_all |
|
2418 ultimately show "?r \<longlonglongrightarrow> 1" by (force dest!: Lim_transform_eventually) |
|
2419 |
|
2420 from eventually_gt_at_top[of "0::nat"] |
|
2421 show "eventually (\<lambda>n. ?r n = Gamma_series_euler' z n / Gamma_series z n) sequentially" |
|
2422 proof eventually_elim |
|
2423 fix n :: nat assume n: "n > 0" |
|
2424 from n z' have "Gamma_series_euler' z n = |
|
2425 exp (z * of_real (ln (of_nat n + 1))) / (z * (\<Prod>k=1..n. (1 + z / of_nat k)))" |
|
2426 by (subst Gamma_euler'_aux1) |
|
2427 (simp_all add: Gamma_series_euler'_def setprod.distrib |
|
2428 setprod_inversef[symmetric] divide_inverse) |
|
2429 also have "(\<Prod>k=1..n. (1 + z / of_nat k)) = pochhammer (z + 1) n / fact n" |
|
2430 by (cases n) (simp_all add: pochhammer_setprod fact_setprod atLeastLessThanSuc_atLeastAtMost |
|
2431 setprod_dividef [symmetric] field_simps setprod.atLeast_Suc_atMost_Suc_shift) |
|
2432 also have "z * \<dots> = pochhammer z (Suc n) / fact n" by (simp add: pochhammer_rec) |
|
2433 finally show "?r n = Gamma_series_euler' z n / Gamma_series z n" by simp |
|
2434 qed |
|
2435 qed |
|
2436 |
|
2437 end |
|
2438 |
|
2439 |
|
2440 |
|
2441 subsubsection \<open>Weierstrass form\<close> |
|
2442 |
|
2443 definition Gamma_series_weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where |
|
2444 "Gamma_series_weierstrass z n = |
|
2445 exp (-euler_mascheroni * z) / z * (\<Prod>k=1..n. exp (z / of_nat k) / (1 + z / of_nat k))" |
|
2446 |
|
2447 definition rGamma_series_weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where |
|
2448 "rGamma_series_weierstrass z n = |
|
2449 exp (euler_mascheroni * z) * z * (\<Prod>k=1..n. (1 + z / of_nat k) * exp (-z / of_nat k))" |
|
2450 |
|
2451 lemma Gamma_series_weierstrass_nonpos_Ints: |
|
2452 "eventually (\<lambda>k. Gamma_series_weierstrass (- of_nat n) k = 0) sequentially" |
|
2453 using eventually_ge_at_top[of n] by eventually_elim (auto simp: Gamma_series_weierstrass_def) |
|
2454 |
|
2455 lemma rGamma_series_weierstrass_nonpos_Ints: |
|
2456 "eventually (\<lambda>k. rGamma_series_weierstrass (- of_nat n) k = 0) sequentially" |
|
2457 using eventually_ge_at_top[of n] by eventually_elim (auto simp: rGamma_series_weierstrass_def) |
|
2458 |
|
2459 lemma Gamma_weierstrass_complex: "Gamma_series_weierstrass z \<longlonglongrightarrow> Gamma (z :: complex)" |
|
2460 proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0") |
|
2461 case True |
|
2462 then obtain n where "z = - of_nat n" by (elim nonpos_Ints_cases') |
|
2463 also from True have "Gamma_series_weierstrass \<dots> \<longlonglongrightarrow> Gamma z" |
|
2464 by (simp add: tendsto_cong[OF Gamma_series_weierstrass_nonpos_Ints] Gamma_nonpos_Int) |
|
2465 finally show ?thesis . |
|
2466 next |
|
2467 case False |
|
2468 hence z: "z \<noteq> 0" by auto |
|
2469 let ?f = "(\<lambda>x. \<Prod>x = Suc 0..x. exp (z / of_nat x) / (1 + z / of_nat x))" |
|
2470 have A: "exp (ln (1 + z / of_nat n)) = (1 + z / of_nat n)" if "n \<ge> 1" for n :: nat |
|
2471 using False that by (subst exp_Ln) (auto simp: field_simps dest!: plus_of_nat_eq_0_imp) |
|
2472 have "(\<lambda>n. \<Sum>k=1..n. z / of_nat k - ln (1 + z / of_nat k)) \<longlonglongrightarrow> ln_Gamma z + euler_mascheroni * z + ln z" |
|
2473 using ln_Gamma_series'_aux[OF False] |
|
2474 by (simp only: atLeastLessThanSuc_atLeastAtMost [symmetric] One_nat_def |
|
2475 setsum_shift_bounds_Suc_ivl sums_def atLeast0LessThan) |
|
2476 from tendsto_exp[OF this] False z have "?f \<longlonglongrightarrow> z * exp (euler_mascheroni * z) * Gamma z" |
|
2477 by (simp add: exp_add exp_setsum exp_diff mult_ac Gamma_complex_altdef A) |
|
2478 from tendsto_mult[OF tendsto_const[of "exp (-euler_mascheroni * z) / z"] this] z |
|
2479 show "Gamma_series_weierstrass z \<longlonglongrightarrow> Gamma z" |
|
2480 by (simp add: exp_minus divide_simps Gamma_series_weierstrass_def [abs_def]) |
|
2481 qed |
|
2482 |
|
2483 lemma tendsto_complex_of_real_iff: "((\<lambda>x. complex_of_real (f x)) \<longlongrightarrow> of_real c) F = (f \<longlongrightarrow> c) F" |
|
2484 by (rule tendsto_of_real_iff) |
|
2485 |
|
2486 lemma Gamma_weierstrass_real: "Gamma_series_weierstrass x \<longlonglongrightarrow> Gamma (x :: real)" |
|
2487 using Gamma_weierstrass_complex[of "of_real x"] unfolding Gamma_series_weierstrass_def[abs_def] |
|
2488 by (subst tendsto_complex_of_real_iff [symmetric]) |
|
2489 (simp_all add: exp_of_real[symmetric] Gamma_complex_of_real) |
|
2490 |
|
2491 lemma rGamma_weierstrass_complex: "rGamma_series_weierstrass z \<longlonglongrightarrow> rGamma (z :: complex)" |
|
2492 proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0") |
|
2493 case True |
|
2494 then obtain n where "z = - of_nat n" by (elim nonpos_Ints_cases') |
|
2495 also from True have "rGamma_series_weierstrass \<dots> \<longlonglongrightarrow> rGamma z" |
|
2496 by (simp add: tendsto_cong[OF rGamma_series_weierstrass_nonpos_Ints] rGamma_nonpos_Int) |
|
2497 finally show ?thesis . |
|
2498 next |
|
2499 case False |
|
2500 have "rGamma_series_weierstrass z = (\<lambda>n. inverse (Gamma_series_weierstrass z n))" |
|
2501 by (simp add: rGamma_series_weierstrass_def[abs_def] Gamma_series_weierstrass_def |
|
2502 exp_minus divide_inverse setprod_inversef[symmetric] mult_ac) |
|
2503 also from False have "\<dots> \<longlonglongrightarrow> inverse (Gamma z)" |
|
2504 by (intro tendsto_intros Gamma_weierstrass_complex) (simp add: Gamma_eq_zero_iff) |
|
2505 finally show ?thesis by (simp add: Gamma_def) |
|
2506 qed |
|
2507 |
|
2508 subsubsection \<open>Binomial coefficient form\<close> |
|
2509 |
|
2510 lemma Gamma_gbinomial: |
|
2511 "(\<lambda>n. ((z + of_nat n) gchoose n) * exp (-z * of_real (ln (of_nat n)))) \<longlonglongrightarrow> rGamma (z+1)" |
|
2512 proof (cases "z = 0") |
|
2513 case False |
|
2514 show ?thesis |
|
2515 proof (rule Lim_transform_eventually) |
|
2516 let ?powr = "\<lambda>a b. exp (b * of_real (ln (of_nat a)))" |
|
2517 show "eventually (\<lambda>n. rGamma_series z n / z = |
|
2518 ((z + of_nat n) gchoose n) * ?powr n (-z)) sequentially" |
|
2519 proof (intro always_eventually allI) |
|
2520 fix n :: nat |
|
2521 from False have "((z + of_nat n) gchoose n) = pochhammer z (Suc n) / z / fact n" |
|
2522 by (simp add: gbinomial_pochhammer' pochhammer_rec) |
|
2523 also have "pochhammer z (Suc n) / z / fact n * ?powr n (-z) = rGamma_series z n / z" |
|
2524 by (simp add: rGamma_series_def divide_simps exp_minus) |
|
2525 finally show "rGamma_series z n / z = ((z + of_nat n) gchoose n) * ?powr n (-z)" .. |
|
2526 qed |
|
2527 |
|
2528 from False have "(\<lambda>n. rGamma_series z n / z) \<longlonglongrightarrow> rGamma z / z" by (intro tendsto_intros) |
|
2529 also from False have "rGamma z / z = rGamma (z + 1)" using rGamma_plus1[of z] |
|
2530 by (simp add: field_simps) |
|
2531 finally show "(\<lambda>n. rGamma_series z n / z) \<longlonglongrightarrow> rGamma (z+1)" . |
|
2532 qed |
|
2533 qed (simp_all add: binomial_gbinomial [symmetric]) |
|
2534 |
|
2535 lemma gbinomial_minus': "(a + of_nat b) gchoose b = (- 1) ^ b * (- (a + 1) gchoose b)" |
|
2536 by (subst gbinomial_minus) (simp add: power_mult_distrib [symmetric]) |
|
2537 |
|
2538 lemma gbinomial_asymptotic: |
|
2539 fixes z :: "'a :: Gamma" |
|
2540 shows "(\<lambda>n. (z gchoose n) / ((-1)^n / exp ((z+1) * of_real (ln (real n))))) \<longlonglongrightarrow> |
|
2541 inverse (Gamma (- z))" |
|
2542 unfolding rGamma_inverse_Gamma [symmetric] using Gamma_gbinomial[of "-z-1"] |
|
2543 by (subst (asm) gbinomial_minus') |
|
2544 (simp add: add_ac mult_ac divide_inverse power_inverse [symmetric]) |
|
2545 |
|
2546 lemma fact_binomial_limit: |
|
2547 "(\<lambda>n. of_nat ((k + n) choose n) / of_nat (n ^ k) :: 'a :: Gamma) \<longlonglongrightarrow> 1 / fact k" |
|
2548 proof (rule Lim_transform_eventually) |
|
2549 have "(\<lambda>n. of_nat ((k + n) choose n) / of_real (exp (of_nat k * ln (real_of_nat n)))) |
|
2550 \<longlonglongrightarrow> 1 / Gamma (of_nat (Suc k) :: 'a)" (is "?f \<longlonglongrightarrow> _") |
|
2551 using Gamma_gbinomial[of "of_nat k :: 'a"] |
|
2552 by (simp add: binomial_gbinomial add_ac Gamma_def divide_simps exp_of_real [symmetric] exp_minus) |
|
2553 also have "Gamma (of_nat (Suc k)) = fact k" by (simp add: Gamma_fact) |
|
2554 finally show "?f \<longlonglongrightarrow> 1 / fact k" . |
|
2555 |
|
2556 show "eventually (\<lambda>n. ?f n = of_nat ((k + n) choose n) / of_nat (n ^ k)) sequentially" |
|
2557 using eventually_gt_at_top[of "0::nat"] |
|
2558 proof eventually_elim |
|
2559 fix n :: nat assume n: "n > 0" |
|
2560 from n have "exp (real_of_nat k * ln (real_of_nat n)) = real_of_nat (n^k)" |
|
2561 by (simp add: exp_of_nat_mult) |
|
2562 thus "?f n = of_nat ((k + n) choose n) / of_nat (n ^ k)" by simp |
|
2563 qed |
|
2564 qed |
|
2565 |
|
2566 lemma binomial_asymptotic': |
|
2567 "(\<lambda>n. of_nat ((k + n) choose n) / (of_nat (n ^ k) / fact k) :: 'a :: Gamma) \<longlonglongrightarrow> 1" |
|
2568 using tendsto_mult[OF fact_binomial_limit[of k] tendsto_const[of "fact k :: 'a"]] by simp |
|
2569 |
|
2570 lemma gbinomial_Beta: |
|
2571 assumes "z + 1 \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
2572 shows "((z::'a::Gamma) gchoose n) = inverse ((z + 1) * Beta (z - of_nat n + 1) (of_nat n + 1))" |
|
2573 using assms |
|
2574 proof (induction n arbitrary: z) |
|
2575 case 0 |
|
2576 hence "z + 2 \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
2577 using plus_one_in_nonpos_Ints_imp[of "z+1"] by (auto simp: add.commute) |
|
2578 with 0 show ?case |
|
2579 by (auto simp: Beta_def Gamma_eq_zero_iff Gamma_plus1 [symmetric] add.commute) |
|
2580 next |
|
2581 case (Suc n z) |
|
2582 show ?case |
|
2583 proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0") |
|
2584 case True |
|
2585 with Suc.prems have "z = 0" |
|
2586 by (auto elim!: nonpos_Ints_cases simp: algebra_simps one_plus_of_int_in_nonpos_Ints_iff) |
|
2587 show ?thesis |
|
2588 proof (cases "n = 0") |
|
2589 case True |
|
2590 with \<open>z = 0\<close> show ?thesis |
|
2591 by (simp add: Beta_def Gamma_eq_zero_iff Gamma_plus1 [symmetric]) |
|
2592 next |
|
2593 case False |
|
2594 with \<open>z = 0\<close> show ?thesis |
|
2595 by (simp_all add: Beta_pole1 one_minus_of_nat_in_nonpos_Ints_iff gbinomial_1) |
|
2596 qed |
|
2597 next |
|
2598 case False |
|
2599 have "(z gchoose (Suc n)) = ((z - 1 + 1) gchoose (Suc n))" by simp |
|
2600 also have "\<dots> = (z - 1 gchoose n) * ((z - 1) + 1) / of_nat (Suc n)" |
|
2601 by (subst gbinomial_factors) (simp add: field_simps) |
|
2602 also from False have "\<dots> = inverse (of_nat (Suc n) * Beta (z - of_nat n) (of_nat (Suc n)))" |
|
2603 (is "_ = inverse ?x") by (subst Suc.IH) (simp_all add: field_simps Beta_pole1) |
|
2604 also have "of_nat (Suc n) \<notin> (\<int>\<^sub>\<le>\<^sub>0 :: 'a set)" by (subst of_nat_in_nonpos_Ints_iff) simp_all |
|
2605 hence "?x = (z + 1) * Beta (z - of_nat (Suc n) + 1) (of_nat (Suc n) + 1)" |
|
2606 by (subst Beta_plus1_right [symmetric]) simp_all |
|
2607 finally show ?thesis . |
|
2608 qed |
|
2609 qed |
|
2610 |
|
2611 lemma gbinomial_Gamma: |
|
2612 assumes "z + 1 \<notin> \<int>\<^sub>\<le>\<^sub>0" |
|
2613 shows "(z gchoose n) = Gamma (z + 1) / (fact n * Gamma (z - of_nat n + 1))" |
|
2614 proof - |
|
2615 have "(z gchoose n) = Gamma (z + 2) / (z + 1) / (fact n * Gamma (z - of_nat n + 1))" |
|
2616 by (subst gbinomial_Beta[OF assms]) (simp_all add: Beta_def Gamma_fact [symmetric] add_ac) |
|
2617 also from assms have "Gamma (z + 2) / (z + 1) = Gamma (z + 1)" |
|
2618 using Gamma_plus1[of "z+1"] by (auto simp add: divide_simps mult_ac add_ac) |
|
2619 finally show ?thesis . |
|
2620 qed |
|
2621 |
|
2622 |
|
2623 subsubsection \<open>Integral form\<close> |
|
2624 |
|
2625 lemma integrable_Gamma_integral_bound: |
|
2626 fixes a c :: real |
|
2627 assumes a: "a > -1" and c: "c \<ge> 0" |
|
2628 defines "f \<equiv> \<lambda>x. if x \<in> {0..c} then x powr a else exp (-x/2)" |
|
2629 shows "f integrable_on {0..}" |
|
2630 proof - |
|
2631 have "f integrable_on {0..c}" |
|
2632 by (rule integrable_spike_finite[of "{}", OF _ _ integrable_on_powr_from_0[of a c]]) |
|
2633 (insert a c, simp_all add: f_def) |
|
2634 moreover have A: "(\<lambda>x. exp (-x/2)) integrable_on {c..}" |
|
2635 using integrable_on_exp_minus_to_infinity[of "1/2"] by simp |
|
2636 have "f integrable_on {c..}" |
|
2637 by (rule integrable_spike_finite[of "{c}", OF _ _ A]) (simp_all add: f_def) |
|
2638 ultimately show "f integrable_on {0..}" |
|
2639 by (rule integrable_union') (insert c, auto simp: max_def) |
|
2640 qed |
|
2641 |
|
2642 lemma Gamma_integral_complex: |
|
2643 assumes z: "Re z > 0" |
|
2644 shows "((\<lambda>t. of_real t powr (z - 1) / of_real (exp t)) has_integral Gamma z) {0..}" |
|
2645 proof - |
|
2646 have A: "((\<lambda>t. (of_real t) powr (z - 1) * of_real ((1 - t) ^ n)) |
|
2647 has_integral (fact n / pochhammer z (n+1))) {0..1}" |
|
2648 if "Re z > 0" for n z using that |
|
2649 proof (induction n arbitrary: z) |
|
2650 case 0 |
|
2651 have "((\<lambda>t. complex_of_real t powr (z - 1)) has_integral |
|
2652 (of_real 1 powr z / z - of_real 0 powr z / z)) {0..1}" using 0 |
|
2653 by (intro fundamental_theorem_of_calculus_interior) |
|
2654 (auto intro!: continuous_intros derivative_eq_intros has_vector_derivative_real_complex) |
|
2655 thus ?case by simp |
|
2656 next |
|
2657 case (Suc n) |
|
2658 let ?f = "\<lambda>t. complex_of_real t powr z / z" |
|
2659 let ?f' = "\<lambda>t. complex_of_real t powr (z - 1)" |
|
2660 let ?g = "\<lambda>t. (1 - complex_of_real t) ^ Suc n" |
|
2661 let ?g' = "\<lambda>t. - ((1 - complex_of_real t) ^ n) * of_nat (Suc n)" |
|
2662 have "((\<lambda>t. ?f' t * ?g t) has_integral |
|
2663 (of_nat (Suc n)) * fact n / pochhammer z (n+2)) {0..1}" |
|
2664 (is "(_ has_integral ?I) _") |
|
2665 proof (rule integration_by_parts_interior[where f' = ?f' and g = ?g]) |
|
2666 from Suc.prems show "continuous_on {0..1} ?f" "continuous_on {0..1} ?g" |
|
2667 by (auto intro!: continuous_intros) |
|
2668 next |
|
2669 fix t :: real assume t: "t \<in> {0<..<1}" |
|
2670 show "(?f has_vector_derivative ?f' t) (at t)" using t Suc.prems |
|
2671 by (auto intro!: derivative_eq_intros has_vector_derivative_real_complex) |
|
2672 show "(?g has_vector_derivative ?g' t) (at t)" |
|
2673 by (rule has_vector_derivative_real_complex derivative_eq_intros refl)+ simp_all |
|
2674 next |
|
2675 from Suc.prems have [simp]: "z \<noteq> 0" by auto |
|
2676 from Suc.prems have A: "Re (z + of_nat n) > 0" for n by simp |
|
2677 have [simp]: "z + of_nat n \<noteq> 0" "z + 1 + of_nat n \<noteq> 0" for n |
|
2678 using A[of n] A[of "Suc n"] by (auto simp add: add.assoc simp del: plus_complex.sel) |
|
2679 have "((\<lambda>x. of_real x powr z * of_real ((1 - x) ^ n) * (- of_nat (Suc n) / z)) has_integral |
|
2680 fact n / pochhammer (z+1) (n+1) * (- of_nat (Suc n) / z)) {0..1}" |
|
2681 (is "(?A has_integral ?B) _") |
|
2682 using Suc.IH[of "z+1"] Suc.prems by (intro has_integral_mult_left) (simp_all add: add_ac pochhammer_rec) |
|
2683 also have "?A = (\<lambda>t. ?f t * ?g' t)" by (intro ext) (simp_all add: field_simps) |
|
2684 also have "?B = - (of_nat (Suc n) * fact n / pochhammer z (n+2))" |
|
2685 by (simp add: divide_simps pochhammer_rec |
|
2686 setprod_shift_bounds_cl_Suc_ivl del: of_nat_Suc) |
|
2687 finally show "((\<lambda>t. ?f t * ?g' t) has_integral (?f 1 * ?g 1 - ?f 0 * ?g 0 - ?I)) {0..1}" |
|
2688 by simp |
|
2689 qed (simp_all add: bounded_bilinear_mult) |
|
2690 thus ?case by simp |
|
2691 qed |
|
2692 |
|
2693 have B: "((\<lambda>t. if t \<in> {0..of_nat n} then |
|
2694 of_real t powr (z - 1) * (1 - of_real t / of_nat n) ^ n else 0) |
|
2695 has_integral (of_nat n powr z * fact n / pochhammer z (n+1))) {0..}" for n |
|
2696 proof (cases "n > 0") |
|
2697 case [simp]: True |
|
2698 hence [simp]: "n \<noteq> 0" by auto |
|
2699 with has_integral_affinity01[OF A[OF z, of n], of "inverse (of_nat n)" 0] |
|
2700 have "((\<lambda>x. (of_nat n - of_real x) ^ n * (of_real x / of_nat n) powr (z - 1) / of_nat n ^ n) |
|
2701 has_integral fact n * of_nat n / pochhammer z (n+1)) ((\<lambda>x. real n * x)`{0..1})" |
|
2702 (is "(?f has_integral ?I) ?ivl") by (simp add: field_simps scaleR_conv_of_real) |
|
2703 also from True have "((\<lambda>x. real n*x)`{0..1}) = {0..real n}" |
|
2704 by (subst image_mult_atLeastAtMost) simp_all |
|
2705 also have "?f = (\<lambda>x. (of_real x / of_nat n) powr (z - 1) * (1 - of_real x / of_nat n) ^ n)" |
|
2706 using True by (intro ext) (simp add: field_simps) |
|
2707 finally have "((\<lambda>x. (of_real x / of_nat n) powr (z - 1) * (1 - of_real x / of_nat n) ^ n) |
|
2708 has_integral ?I) {0..real n}" (is ?P) . |
|
2709 also have "?P \<longleftrightarrow> ((\<lambda>x. exp ((z - 1) * of_real (ln (x / of_nat n))) * (1 - of_real x / of_nat n) ^ n) |
|
2710 has_integral ?I) {0..real n}" |
|
2711 by (intro has_integral_spike_finite_eq[of "{0}"]) (auto simp: powr_def Ln_of_real [symmetric]) |
|
2712 also have "\<dots> \<longleftrightarrow> ((\<lambda>x. exp ((z - 1) * of_real (ln x - ln (of_nat n))) * (1 - of_real x / of_nat n) ^ n) |
|
2713 has_integral ?I) {0..real n}" |
|
2714 by (intro has_integral_spike_finite_eq[of "{0}"]) (simp_all add: ln_div) |
|
2715 finally have \<dots> . |
|
2716 note B = has_integral_mult_right[OF this, of "exp ((z - 1) * ln (of_nat n))"] |
|
2717 have "((\<lambda>x. exp ((z - 1) * of_real (ln x)) * (1 - of_real x / of_nat n) ^ n) |
|
2718 has_integral (?I * exp ((z - 1) * ln (of_nat n)))) {0..real n}" (is ?P) |
|
2719 by (insert B, subst (asm) mult.assoc [symmetric], subst (asm) exp_add [symmetric]) |
|
2720 (simp add: Ln_of_nat algebra_simps) |
|
2721 also have "?P \<longleftrightarrow> ((\<lambda>x. of_real x powr (z - 1) * (1 - of_real x / of_nat n) ^ n) |
|
2722 has_integral (?I * exp ((z - 1) * ln (of_nat n)))) {0..real n}" |
|
2723 by (intro has_integral_spike_finite_eq[of "{0}"]) (simp_all add: powr_def Ln_of_real) |
|
2724 also have "fact n * of_nat n / pochhammer z (n+1) * exp ((z - 1) * Ln (of_nat n)) = |
|
2725 (of_nat n powr z * fact n / pochhammer z (n+1))" |
|
2726 by (auto simp add: powr_def algebra_simps exp_diff) |
|
2727 finally show ?thesis by (subst has_integral_restrict) simp_all |
|
2728 next |
|
2729 case False |
|
2730 thus ?thesis by (subst has_integral_restrict) (simp_all add: has_integral_refl) |
|
2731 qed |
|
2732 |
|
2733 have "eventually (\<lambda>n. Gamma_series z n = |
|
2734 of_nat n powr z * fact n / pochhammer z (n+1)) sequentially" |
|
2735 using eventually_gt_at_top[of "0::nat"] |
|
2736 by eventually_elim (simp add: powr_def algebra_simps Ln_of_nat Gamma_series_def) |
|
2737 from this and Gamma_series_LIMSEQ[of z] |
|
2738 have C: "(\<lambda>k. of_nat k powr z * fact k / pochhammer z (k+1)) \<longlonglongrightarrow> Gamma z" |
|
2739 by (rule Lim_transform_eventually) |
|
2740 |
|
2741 { |
|
2742 fix x :: real assume x: "x \<ge> 0" |
|
2743 have lim_exp: "(\<lambda>k. (1 - x / real k) ^ k) \<longlonglongrightarrow> exp (-x)" |
|
2744 using tendsto_exp_limit_sequentially[of "-x"] by simp |
|
2745 have "(\<lambda>k. of_real x powr (z - 1) * of_real ((1 - x / of_nat k) ^ k)) |
|
2746 \<longlonglongrightarrow> of_real x powr (z - 1) * of_real (exp (-x))" (is ?P) |
|
2747 by (intro tendsto_intros lim_exp) |
|
2748 also from eventually_gt_at_top[of "nat \<lceil>x\<rceil>"] |
|
2749 have "eventually (\<lambda>k. of_nat k > x) sequentially" by eventually_elim linarith |
|
2750 hence "?P \<longleftrightarrow> (\<lambda>k. if x \<le> of_nat k then |
|
2751 of_real x powr (z - 1) * of_real ((1 - x / of_nat k) ^ k) else 0) |
|
2752 \<longlonglongrightarrow> of_real x powr (z - 1) * of_real (exp (-x))" |
|
2753 by (intro tendsto_cong) (auto elim!: eventually_mono) |
|
2754 finally have \<dots> . |
|
2755 } |
|
2756 hence D: "\<forall>x\<in>{0..}. (\<lambda>k. if x \<in> {0..real k} then |
|
2757 of_real x powr (z - 1) * (1 - of_real x / of_nat k) ^ k else 0) |
|
2758 \<longlonglongrightarrow> of_real x powr (z - 1) / of_real (exp x)" |
|
2759 by (simp add: exp_minus field_simps cong: if_cong) |
|
2760 |
|
2761 have "((\<lambda>x. (Re z - 1) * (ln x / x)) \<longlongrightarrow> (Re z - 1) * 0) at_top" |
|
2762 by (intro tendsto_intros ln_x_over_x_tendsto_0) |
|
2763 hence "((\<lambda>x. ((Re z - 1) * ln x) / x) \<longlongrightarrow> 0) at_top" by simp |
|
2764 from order_tendstoD(2)[OF this, of "1/2"] |
|
2765 have "eventually (\<lambda>x. (Re z - 1) * ln x / x < 1/2) at_top" by simp |
|
2766 from eventually_conj[OF this eventually_gt_at_top[of 0]] |
|
2767 obtain x0 where "\<forall>x\<ge>x0. (Re z - 1) * ln x / x < 1/2 \<and> x > 0" |
|
2768 by (auto simp: eventually_at_top_linorder) |
|
2769 hence x0: "x0 > 0" "\<And>x. x \<ge> x0 \<Longrightarrow> (Re z - 1) * ln x < x / 2" by auto |
|
2770 |
|
2771 define h where "h = (\<lambda>x. if x \<in> {0..x0} then x powr (Re z - 1) else exp (-x/2))" |
|
2772 have le_h: "x powr (Re z - 1) * exp (-x) \<le> h x" if x: "x \<ge> 0" for x |
|
2773 proof (cases "x > x0") |
|
2774 case True |
|
2775 from True x0(1) have "x powr (Re z - 1) * exp (-x) = exp ((Re z - 1) * ln x - x)" |
|
2776 by (simp add: powr_def exp_diff exp_minus field_simps exp_add) |
|
2777 also from x0(2)[of x] True have "\<dots> < exp (-x/2)" |
|
2778 by (simp add: field_simps) |
|
2779 finally show ?thesis using True by (auto simp add: h_def) |
|
2780 next |
|
2781 case False |
|
2782 from x have "x powr (Re z - 1) * exp (- x) \<le> x powr (Re z - 1) * 1" |
|
2783 by (intro mult_left_mono) simp_all |
|
2784 with False show ?thesis by (auto simp add: h_def) |
|
2785 qed |
|
2786 |
|
2787 have E: "\<forall>x\<in>{0..}. cmod (if x \<in> {0..real k} then of_real x powr (z - 1) * |
|
2788 (1 - complex_of_real x / of_nat k) ^ k else 0) \<le> h x" |
|
2789 (is "\<forall>x\<in>_. ?f x \<le> _") for k |
|
2790 proof safe |
|
2791 fix x :: real assume x: "x \<ge> 0" |
|
2792 { |
|
2793 fix x :: real and n :: nat assume x: "x \<le> of_nat n" |
|
2794 have "(1 - complex_of_real x / of_nat n) = complex_of_real ((1 - x / of_nat n))" by simp |
|
2795 also have "norm \<dots> = \<bar>(1 - x / real n)\<bar>" by (subst norm_of_real) (rule refl) |
|
2796 also from x have "\<dots> = (1 - x / real n)" by (intro abs_of_nonneg) (simp_all add: divide_simps) |
|
2797 finally have "cmod (1 - complex_of_real x / of_nat n) = 1 - x / real n" . |
|
2798 } note D = this |
|
2799 from D[of x k] x |
|
2800 have "?f x \<le> (if of_nat k \<ge> x \<and> k > 0 then x powr (Re z - 1) * (1 - x / real k) ^ k else 0)" |
|
2801 by (auto simp: norm_mult norm_powr_real_powr norm_power intro!: mult_nonneg_nonneg) |
|
2802 also have "\<dots> \<le> x powr (Re z - 1) * exp (-x)" |
|
2803 by (auto intro!: mult_left_mono exp_ge_one_minus_x_over_n_power_n) |
|
2804 also from x have "\<dots> \<le> h x" by (rule le_h) |
|
2805 finally show "?f x \<le> h x" . |
|
2806 qed |
|
2807 |
|
2808 have F: "h integrable_on {0..}" unfolding h_def |
|
2809 by (rule integrable_Gamma_integral_bound) (insert assms x0(1), simp_all) |
|
2810 show ?thesis |
|
2811 by (rule has_integral_dominated_convergence[OF B F E D C]) |
|
2812 qed |
|
2813 |
|
2814 lemma Gamma_integral_real: |
|
2815 assumes x: "x > (0 :: real)" |
|
2816 shows "((\<lambda>t. t powr (x - 1) / exp t) has_integral Gamma x) {0..}" |
|
2817 proof - |
|
2818 have A: "((\<lambda>t. complex_of_real t powr (complex_of_real x - 1) / |
|
2819 complex_of_real (exp t)) has_integral complex_of_real (Gamma x)) {0..}" |
|
2820 using Gamma_integral_complex[of x] assms by (simp_all add: Gamma_complex_of_real powr_of_real) |
|
2821 have "((\<lambda>t. complex_of_real (t powr (x - 1) / exp t)) has_integral of_real (Gamma x)) {0..}" |
|
2822 by (rule has_integral_eq[OF _ A]) (simp_all add: powr_of_real [symmetric]) |
|
2823 from has_integral_linear[OF this bounded_linear_Re] show ?thesis by (simp add: o_def) |
|
2824 qed |
|
2825 |
|
2826 |
|
2827 |
|
2828 subsection \<open>The Weierstraß product formula for the sine\<close> |
|
2829 |
|
2830 lemma sin_product_formula_complex: |
|
2831 fixes z :: complex |
|
2832 shows "(\<lambda>n. of_real pi * z * (\<Prod>k=1..n. 1 - z^2 / of_nat k^2)) \<longlonglongrightarrow> sin (of_real pi * z)" |
|
2833 proof - |
|
2834 let ?f = "rGamma_series_weierstrass" |
|
2835 have "(\<lambda>n. (- of_real pi * inverse z) * (?f z n * ?f (- z) n)) |
|
2836 \<longlonglongrightarrow> (- of_real pi * inverse z) * (rGamma z * rGamma (- z))" |
|
2837 by (intro tendsto_intros rGamma_weierstrass_complex) |
|
2838 also have "(\<lambda>n. (- of_real pi * inverse z) * (?f z n * ?f (-z) n)) = |
|
2839 (\<lambda>n. of_real pi * z * (\<Prod>k=1..n. 1 - z^2 / of_nat k ^ 2))" |
|
2840 proof |
|
2841 fix n :: nat |
|
2842 have "(- of_real pi * inverse z) * (?f z n * ?f (-z) n) = |
|
2843 of_real pi * z * (\<Prod>k=1..n. (of_nat k - z) * (of_nat k + z) / of_nat k ^ 2)" |
|
2844 by (simp add: rGamma_series_weierstrass_def mult_ac exp_minus |
|
2845 divide_simps setprod.distrib[symmetric] power2_eq_square) |
|
2846 also have "(\<Prod>k=1..n. (of_nat k - z) * (of_nat k + z) / of_nat k ^ 2) = |
|
2847 (\<Prod>k=1..n. 1 - z^2 / of_nat k ^ 2)" |
|
2848 by (intro setprod.cong) (simp_all add: power2_eq_square field_simps) |
|
2849 finally show "(- of_real pi * inverse z) * (?f z n * ?f (-z) n) = of_real pi * z * \<dots>" |
|
2850 by (simp add: divide_simps) |
|
2851 qed |
|
2852 also have "(- of_real pi * inverse z) * (rGamma z * rGamma (- z)) = sin (of_real pi * z)" |
|
2853 by (subst rGamma_reflection_complex') (simp add: divide_simps) |
|
2854 finally show ?thesis . |
|
2855 qed |
|
2856 |
|
2857 lemma sin_product_formula_real: |
|
2858 "(\<lambda>n. pi * (x::real) * (\<Prod>k=1..n. 1 - x^2 / of_nat k^2)) \<longlonglongrightarrow> sin (pi * x)" |
|
2859 proof - |
|
2860 from sin_product_formula_complex[of "of_real x"] |
|
2861 have "(\<lambda>n. of_real pi * of_real x * (\<Prod>k=1..n. 1 - (of_real x)^2 / (of_nat k)^2)) |
|
2862 \<longlonglongrightarrow> sin (of_real pi * of_real x :: complex)" (is "?f \<longlonglongrightarrow> ?y") . |
|
2863 also have "?f = (\<lambda>n. of_real (pi * x * (\<Prod>k=1..n. 1 - x^2 / (of_nat k^2))))" by simp |
|
2864 also have "?y = of_real (sin (pi * x))" by (simp only: sin_of_real [symmetric] of_real_mult) |
|
2865 finally show ?thesis by (subst (asm) tendsto_of_real_iff) |
|
2866 qed |
|
2867 |
|
2868 lemma sin_product_formula_real': |
|
2869 assumes "x \<noteq> (0::real)" |
|
2870 shows "(\<lambda>n. (\<Prod>k=1..n. 1 - x^2 / of_nat k^2)) \<longlonglongrightarrow> sin (pi * x) / (pi * x)" |
|
2871 using tendsto_divide[OF sin_product_formula_real[of x] tendsto_const[of "pi * x"]] assms |
|
2872 by simp |
|
2873 |
|
2874 |
|
2875 subsection \<open>The Solution to the Basel problem\<close> |
|
2876 |
|
2877 theorem inverse_squares_sums: "(\<lambda>n. 1 / (n + 1)\<^sup>2) sums (pi\<^sup>2 / 6)" |
|
2878 proof - |
|
2879 define P where "P x n = (\<Prod>k=1..n. 1 - x^2 / of_nat k^2)" for x :: real and n |
|
2880 define K where "K = (\<Sum>n. inverse (real_of_nat (Suc n))^2)" |
|
2881 define f where [abs_def]: "f x = (\<Sum>n. P x n / of_nat (Suc n)^2)" for x |
|
2882 define g where [abs_def]: "g x = (1 - sin (pi * x) / (pi * x))" for x |
|
2883 |
|
2884 have sums: "(\<lambda>n. P x n / of_nat (Suc n)^2) sums (if x = 0 then K else g x / x^2)" for x |
|
2885 proof (cases "x = 0") |
|
2886 assume x: "x = 0" |
|
2887 have "summable (\<lambda>n. inverse ((real_of_nat (Suc n))\<^sup>2))" |
|
2888 using inverse_power_summable[of 2] by (subst summable_Suc_iff) simp |
|
2889 thus ?thesis by (simp add: x g_def P_def K_def inverse_eq_divide power_divide summable_sums) |
|
2890 next |
|
2891 assume x: "x \<noteq> 0" |
|
2892 have "(\<lambda>n. P x n - P x (Suc n)) sums (P x 0 - sin (pi * x) / (pi * x))" |
|
2893 unfolding P_def using x by (intro telescope_sums' sin_product_formula_real') |
|
2894 also have "(\<lambda>n. P x n - P x (Suc n)) = (\<lambda>n. (x^2 / of_nat (Suc n)^2) * P x n)" |
|
2895 unfolding P_def by (simp add: setprod_nat_ivl_Suc' algebra_simps) |
|
2896 also have "P x 0 = 1" by (simp add: P_def) |
|
2897 finally have "(\<lambda>n. x\<^sup>2 / (of_nat (Suc n))\<^sup>2 * P x n) sums (1 - sin (pi * x) / (pi * x))" . |
|
2898 from sums_divide[OF this, of "x^2"] x show ?thesis unfolding g_def by simp |
|
2899 qed |
|
2900 |
|
2901 have "continuous_on (ball 0 1) f" |
|
2902 proof (rule uniform_limit_theorem; (intro always_eventually allI)?) |
|
2903 show "uniform_limit (ball 0 1) (\<lambda>n x. \<Sum>k<n. P x k / of_nat (Suc k)^2) f sequentially" |
|
2904 proof (unfold f_def, rule weierstrass_m_test) |
|
2905 fix n :: nat and x :: real assume x: "x \<in> ball 0 1" |
|
2906 { |
|
2907 fix k :: nat assume k: "k \<ge> 1" |
|
2908 from x have "x^2 < 1" by (auto simp: dist_0_norm abs_square_less_1) |
|
2909 also from k have "\<dots> \<le> of_nat k^2" by simp |
|
2910 finally have "(1 - x^2 / of_nat k^2) \<in> {0..1}" using k |
|
2911 by (simp_all add: field_simps del: of_nat_Suc) |
|
2912 } |
|
2913 hence "(\<Prod>k=1..n. abs (1 - x^2 / of_nat k^2)) \<le> (\<Prod>k=1..n. 1)" by (intro setprod_mono) simp |
|
2914 thus "norm (P x n / (of_nat (Suc n)^2)) \<le> 1 / of_nat (Suc n)^2" |
|
2915 unfolding P_def by (simp add: field_simps abs_setprod del: of_nat_Suc) |
|
2916 qed (subst summable_Suc_iff, insert inverse_power_summable[of 2], simp add: inverse_eq_divide) |
|
2917 qed (auto simp: P_def intro!: continuous_intros) |
|
2918 hence "isCont f 0" by (subst (asm) continuous_on_eq_continuous_at) simp_all |
|
2919 hence "(f \<midarrow> 0 \<rightarrow> f 0)" by (simp add: isCont_def) |
|
2920 also have "f 0 = K" unfolding f_def P_def K_def by (simp add: inverse_eq_divide power_divide) |
|
2921 finally have "f \<midarrow> 0 \<rightarrow> K" . |
|
2922 |
|
2923 moreover have "f \<midarrow> 0 \<rightarrow> pi^2 / 6" |
|
2924 proof (rule Lim_transform_eventually) |
|
2925 define f' where [abs_def]: "f' x = (\<Sum>n. - sin_coeff (n+3) * pi ^ (n+2) * x^n)" for x |
|
2926 have "eventually (\<lambda>x. x \<noteq> (0::real)) (at 0)" |
|
2927 by (auto simp add: eventually_at intro!: exI[of _ 1]) |
|
2928 thus "eventually (\<lambda>x. f' x = f x) (at 0)" |
|
2929 proof eventually_elim |
|
2930 fix x :: real assume x: "x \<noteq> 0" |
|
2931 have "sin_coeff 1 = (1 :: real)" "sin_coeff 2 = (0::real)" by (simp_all add: sin_coeff_def) |
|
2932 with sums_split_initial_segment[OF sums_minus[OF sin_converges], of 3 "pi*x"] |
|
2933 have "(\<lambda>n. - (sin_coeff (n+3) * (pi*x)^(n+3))) sums (pi * x - sin (pi*x))" |
|
2934 by (simp add: eval_nat_numeral) |
|
2935 from sums_divide[OF this, of "x^3 * pi"] x |
|
2936 have "(\<lambda>n. - (sin_coeff (n+3) * pi^(n+2) * x^n)) sums ((1 - sin (pi*x) / (pi*x)) / x^2)" |
|
2937 by (simp add: divide_simps eval_nat_numeral power_mult_distrib mult_ac) |
|
2938 with x have "(\<lambda>n. - (sin_coeff (n+3) * pi^(n+2) * x^n)) sums (g x / x^2)" |
|
2939 by (simp add: g_def) |
|
2940 hence "f' x = g x / x^2" by (simp add: sums_iff f'_def) |
|
2941 also have "\<dots> = f x" using sums[of x] x by (simp add: sums_iff g_def f_def) |
|
2942 finally show "f' x = f x" . |
|
2943 qed |
|
2944 |
|
2945 have "isCont f' 0" unfolding f'_def |
|
2946 proof (intro isCont_powser_converges_everywhere) |
|
2947 fix x :: real show "summable (\<lambda>n. -sin_coeff (n+3) * pi^(n+2) * x^n)" |
|
2948 proof (cases "x = 0") |
|
2949 assume x: "x \<noteq> 0" |
|
2950 from summable_divide[OF sums_summable[OF sums_split_initial_segment[OF |
|
2951 sin_converges[of "pi*x"]], of 3], of "-pi*x^3"] x |
|
2952 show ?thesis by (simp add: mult_ac power_mult_distrib divide_simps eval_nat_numeral) |
|
2953 qed (simp only: summable_0_powser) |
|
2954 qed |
|
2955 hence "f' \<midarrow> 0 \<rightarrow> f' 0" by (simp add: isCont_def) |
|
2956 also have "f' 0 = pi * pi / fact 3" unfolding f'_def |
|
2957 by (subst powser_zero) (simp add: sin_coeff_def) |
|
2958 finally show "f' \<midarrow> 0 \<rightarrow> pi^2 / 6" by (simp add: eval_nat_numeral) |
|
2959 qed |
|
2960 |
|
2961 ultimately have "K = pi^2 / 6" by (rule LIM_unique) |
|
2962 moreover from inverse_power_summable[of 2] |
|
2963 have "summable (\<lambda>n. (inverse (real_of_nat (Suc n)))\<^sup>2)" |
|
2964 by (subst summable_Suc_iff) (simp add: power_inverse) |
|
2965 ultimately show ?thesis unfolding K_def |
|
2966 by (auto simp add: sums_iff power_divide inverse_eq_divide) |
|
2967 qed |
|
2968 |
|
2969 end |