author Manuel Eberl Fri Jul 13 16:54:36 2018 +0100 (10 months ago) changeset 68624 205d352ed727 parent 68623 b942da0962c2 child 68625 2ec84498f562
Tagged Ball_Volume and Gamma_Function in HOL-Analysis
```     1.1 --- a/src/HOL/Analysis/Ball_Volume.thy	Fri Jul 13 15:42:18 2018 +0200
1.2 +++ b/src/HOL/Analysis/Ball_Volume.thy	Fri Jul 13 16:54:36 2018 +0100
1.3 @@ -1,9 +1,9 @@
1.4  (*
1.5 -   File:     HOL/Analysis/Gamma_Function.thy
1.6 +   File:     HOL/Analysis/Ball_Volume.thy
1.7     Author:   Manuel Eberl, TU München
1.8  *)
1.9
1.10 -section \<open>The volume (Lebesgue measure) of an \$n\$-dimensional ball\<close>
1.11 +section \<open>The volume of an \$n\$-dimensional ball\<close>
1.12
1.13  theory Ball_Volume
1.14    imports Gamma_Function Lebesgue_Integral_Substitution
1.15 @@ -14,7 +14,7 @@
1.16    dimension need not be an integer; we also allow fractional dimensions, although we do
1.17    not use this case or prove anything about it for now.
1.18  \<close>
1.19 -definition unit_ball_vol :: "real \<Rightarrow> real" where
1.20 +definition%important unit_ball_vol :: "real \<Rightarrow> real" where
1.21    "unit_ball_vol n = pi powr (n / 2) / Gamma (n / 2 + 1)"
1.22
1.23  lemma unit_ball_vol_pos [simp]: "n \<ge> 0 \<Longrightarrow> unit_ball_vol n > 0"
1.24 @@ -177,7 +177,7 @@
1.25    assumes r: "r \<ge> 0"
1.26  begin
1.27
1.28 -theorem emeasure_cball:
1.29 +theorem%unimportant emeasure_cball:
1.30    "emeasure lborel (cball c r) = ennreal (unit_ball_vol (DIM('a)) * r ^ DIM('a))"
1.31  proof (cases "r = 0")
1.32    case False
1.33 @@ -202,11 +202,11 @@
1.34    finally show ?thesis .
1.35  qed auto
1.36
1.37 -corollary content_cball:
1.38 +corollary%unimportant content_cball:
1.39    "content (cball c r) = unit_ball_vol (DIM('a)) * r ^ DIM('a)"
1.40    by (simp add: measure_def emeasure_cball r)
1.41
1.42 -corollary emeasure_ball:
1.43 +corollary%unimportant emeasure_ball:
1.44    "emeasure lborel (ball c r) = ennreal (unit_ball_vol (DIM('a)) * r ^ DIM('a))"
1.45  proof -
1.46    from negligible_sphere[of c r] have "sphere c r \<in> null_sets lborel"
1.47 @@ -219,7 +219,7 @@
1.48    finally show ?thesis ..
1.49  qed
1.50
1.51 -corollary content_ball:
1.52 +corollary%important content_ball:
1.53    "content (ball c r) = unit_ball_vol (DIM('a)) * r ^ DIM('a)"
1.54    by (simp add: measure_def r emeasure_ball)
1.55
1.56 @@ -289,22 +289,25 @@
1.57  lemma unit_ball_vol_1 [simp]: "unit_ball_vol 1 = 2"
1.58    using unit_ball_vol_odd[of 0] by simp
1.59
1.60 -corollary unit_ball_vol_2: "unit_ball_vol 2 = pi"
1.61 +corollary%unimportant
1.62 +          unit_ball_vol_2: "unit_ball_vol 2 = pi"
1.63        and unit_ball_vol_3: "unit_ball_vol 3 = 4 / 3 * pi"
1.64        and unit_ball_vol_4: "unit_ball_vol 4 = pi\<^sup>2 / 2"
1.65        and unit_ball_vol_5: "unit_ball_vol 5 = 8 / 15 * pi\<^sup>2"
1.67
1.68 -corollary circle_area: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 2) set) = r ^ 2 * pi"
1.69 +corollary%unimportant circle_area:
1.70 +  "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 2) set) = r ^ 2 * pi"
1.71    by (simp add: content_ball unit_ball_vol_2)
1.72
1.73 -corollary sphere_volume: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 3) set) = 4 / 3 * r ^ 3 * pi"
1.74 +corollary%unimportant sphere_volume:
1.75 +  "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 3) set) = 4 / 3 * r ^ 3 * pi"
1.76    by (simp add: content_ball unit_ball_vol_3)
1.77
1.78  text \<open>
1.79    Useful equivalent forms
1.80  \<close>
1.81 -corollary content_ball_eq_0_iff [simp]: "content (ball c r) = 0 \<longleftrightarrow> r \<le> 0"
1.82 +corollary%unimportant content_ball_eq_0_iff [simp]: "content (ball c r) = 0 \<longleftrightarrow> r \<le> 0"
1.83  proof -
1.84    have "r > 0 \<Longrightarrow> content (ball c r) > 0"
1.85      by (simp add: content_ball unit_ball_vol_def)
1.86 @@ -312,10 +315,10 @@
1.87      by (fastforce simp: ball_empty)
1.88  qed
1.89
1.90 -corollary content_ball_gt_0_iff [simp]: "0 < content (ball z r) \<longleftrightarrow> 0 < r"
1.91 +corollary%unimportant content_ball_gt_0_iff [simp]: "0 < content (ball z r) \<longleftrightarrow> 0 < r"
1.92    by (auto simp: zero_less_measure_iff)
1.93
1.94 -corollary content_cball_eq_0_iff [simp]: "content (cball c r) = 0 \<longleftrightarrow> r \<le> 0"
1.95 +corollary%unimportant content_cball_eq_0_iff [simp]: "content (cball c r) = 0 \<longleftrightarrow> r \<le> 0"
1.96  proof (cases "r = 0")
1.97    case False
1.98    moreover have "r > 0 \<Longrightarrow> content (cball c r) > 0"
1.99 @@ -324,7 +327,7 @@
1.100      by fastforce
1.101  qed auto
1.102
1.103 -corollary content_cball_gt_0_iff [simp]: "0 < content (cball z r) \<longleftrightarrow> 0 < r"
1.104 +corollary%unimportant content_cball_gt_0_iff [simp]: "0 < content (cball z r) \<longleftrightarrow> 0 < r"
1.105    by (auto simp: zero_less_measure_iff)
1.106
1.107  end
```
```     2.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Fri Jul 13 15:42:18 2018 +0200
2.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Fri Jul 13 16:54:36 2018 +0100
2.3 @@ -230,22 +230,22 @@
2.4  qed
2.5
2.6
2.7 -subsection \<open>Definitions\<close>
2.8 +subsection \<open>The Euler form and the logarithmic Gamma function\<close>
2.9
2.10  text \<open>
2.11 -  We define the Gamma function by first defining its multiplicative inverse @{term "Gamma_inv"}.
2.12 -  This is more convenient because @{term "Gamma_inv"} is entire, which makes proofs of its
2.13 +  We define the Gamma function by first defining its multiplicative inverse \<open>rGamma\<close>.
2.14 +  This is more convenient because \<open>rGamma\<close> is entire, which makes proofs of its
2.15    properties more convenient because one does not have to watch out for discontinuities.
2.16 -  (e.g. @{term "Gamma_inv"} fulfils @{term "rGamma z = z * rGamma (z + 1)"} everywhere,
2.17 -  whereas @{term "Gamma"} does not fulfil the analogous equation on the non-positive integers)
2.18 -
2.19 -  We define the Gamma function (resp. its inverse) in the Euler form. This form has the advantage
2.20 +  (e.g. \<open>rGamma\<close> fulfils \<open>rGamma z = z * rGamma (z + 1)\<close> everywhere, whereas the \<open>\<Gamma>\<close> function
2.21 +  does not fulfil the analogous equation on the non-positive integers)
2.22 +
2.23 +  We define the \<open>\<Gamma>\<close> function (resp.\ its reciprocale) in the Euler form. This form has the advantage
2.24    that it is a relatively simple limit that converges everywhere. The limit at the poles is 0
2.25 -  (due to division by 0). The functional equation @{term "Gamma (z + 1) = z * Gamma z"} follows
2.26 +  (due to division by 0). The functional equation \<open>Gamma (z + 1) = z * Gamma z\<close> follows
2.27    immediately from the definition.
2.28  \<close>
2.29
2.30 -definition Gamma_series :: "('a :: {banach,real_normed_field}) \<Rightarrow> nat \<Rightarrow> 'a" where
2.31 +definition%important Gamma_series :: "('a :: {banach,real_normed_field}) \<Rightarrow> nat \<Rightarrow> 'a" where
2.32    "Gamma_series z n = fact n * exp (z * of_real (ln (of_nat n))) / pochhammer z (n+1)"
2.33
2.34  definition Gamma_series' :: "('a :: {banach,real_normed_field}) \<Rightarrow> nat \<Rightarrow> 'a" where
2.35 @@ -304,11 +304,8 @@
2.36    from tendsto_add[OF this tendsto_const[of 1]] show "(\<lambda>n. z / of_nat n + 1) \<longlonglongrightarrow> 1" by simp
2.37  qed
2.38
2.39 -
2.40 -subsection \<open>Convergence of the Euler series form\<close>
2.41 -
2.42  text \<open>
2.43 -  We now show that the series that defines the Gamma function in the Euler form converges
2.44 +  We now show that the series that defines the \<open>\<Gamma>\<close> function in the Euler form converges
2.45    and that the function defined by it is continuous on the complex halfspace with positive
2.46    real part.
2.47
2.48 @@ -320,10 +317,10 @@
2.49    function to the inverse of the Gamma function, and from that to the Gamma function itself.
2.50  \<close>
2.51
2.52 -definition ln_Gamma_series :: "('a :: {banach,real_normed_field,ln}) \<Rightarrow> nat \<Rightarrow> 'a" where
2.53 +definition%important ln_Gamma_series :: "('a :: {banach,real_normed_field,ln}) \<Rightarrow> nat \<Rightarrow> 'a" where
2.54    "ln_Gamma_series z n = z * ln (of_nat n) - ln z - (\<Sum>k=1..n. ln (z / of_nat k + 1))"
2.55
2.56 -definition ln_Gamma_series' :: "('a :: {banach,real_normed_field,ln}) \<Rightarrow> nat \<Rightarrow> 'a" where
2.57 +definition%unimportant ln_Gamma_series' :: "('a :: {banach,real_normed_field,ln}) \<Rightarrow> nat \<Rightarrow> 'a" where
2.58    "ln_Gamma_series' z n =
2.59       - euler_mascheroni*z - ln z + (\<Sum>k=1..n. z / of_nat n - ln (z / of_nat k + 1))"
2.60
2.61 @@ -333,9 +330,7 @@
2.62
2.63  text \<open>
2.64    We now show that the log-Gamma series converges locally uniformly for all complex numbers except
2.65 -  the non-positive integers. We do this by proving that the series is locally Cauchy, adapting this
2.66 -  proof:
2.67 -  https://math.stackexchange.com/questions/887158/convergence-of-gammaz-lim-n-to-infty-fracnzn-prod-m-0nzm
2.68 +  the non-positive integers. We do this by proving that the series is locally Cauchy.
2.69  \<close>
2.70
2.71  context
2.72 @@ -497,7 +492,7 @@
2.73  lemma ln_Gamma_series_complex_converges'': "(z :: complex) \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> convergent (ln_Gamma_series z)"
2.74    by (drule ln_Gamma_series_complex_converges') (auto intro: uniformly_convergent_imp_convergent)
2.75
2.76 -lemma ln_Gamma_complex_LIMSEQ: "(z :: complex) \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln_Gamma_series z \<longlonglongrightarrow> ln_Gamma z"
2.77 +theorem ln_Gamma_complex_LIMSEQ: "(z :: complex) \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln_Gamma_series z \<longlonglongrightarrow> ln_Gamma z"
2.78    using ln_Gamma_series_complex_converges'' by (simp add: convergent_LIMSEQ_iff ln_Gamma_def)
2.79
2.80  lemma exp_ln_Gamma_series_complex:
2.81 @@ -609,6 +604,9 @@
2.82      by (subst summable_Suc_iff) (simp add: summable_mult inverse_power_summable)
2.83  qed
2.84
2.85 +
2.86 +subsection \<open>The Polygamma functions\<close>
2.87 +
2.88  lemma summable_deriv_ln_Gamma:
2.89    "z \<noteq> (0 :: 'a :: {real_normed_field,banach}) \<Longrightarrow>
2.90       summable (\<lambda>n. inverse (of_nat (Suc n)) - inverse (z + of_nat (Suc n)))"
2.91 @@ -616,13 +614,12 @@
2.92    by (rule uniformly_convergent_imp_convergent,
2.93        rule uniformly_summable_deriv_ln_Gamma[of z "norm z/2"]) simp_all
2.94
2.95 -
2.96 -definition Polygamma :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a" where
2.97 +definition%important Polygamma :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a" where
2.98    "Polygamma n z = (if n = 0 then
2.99        (\<Sum>k. inverse (of_nat (Suc k)) - inverse (z + of_nat k)) - euler_mascheroni else
2.100        (-1)^Suc n * fact n * (\<Sum>k. inverse ((z + of_nat k)^Suc n)))"
2.101
2.102 -abbreviation Digamma :: "('a :: {real_normed_field,banach}) \<Rightarrow> 'a" where
2.103 +abbreviation%important Digamma :: "('a :: {real_normed_field,banach}) \<Rightarrow> 'a" where
2.104    "Digamma \<equiv> Polygamma 0"
2.105
2.106  lemma Digamma_def:
2.107 @@ -708,7 +705,7 @@
2.108    using uniformly_convergent_imp_convergent[OF Polygamma_converges[OF assms, of 1], of z]
2.110
2.111 -lemma Digamma_LIMSEQ:
2.112 +theorem Digamma_LIMSEQ:
2.113    fixes z :: "'a :: {banach,real_normed_field}"
2.114    assumes z: "z \<noteq> 0"
2.115    shows   "(\<lambda>m. of_real (ln (real m)) - (\<Sum>n<m. inverse (z + of_nat n))) \<longlonglongrightarrow> Digamma z"
2.116 @@ -739,7 +736,14 @@
2.117    finally show ?thesis by (rule Lim_transform) (insert lim, simp)
2.118  qed
2.119
2.120 -lemma has_field_derivative_ln_Gamma_complex [derivative_intros]:
2.121 +theorem Polygamma_LIMSEQ:
2.122 +  fixes z :: "'a :: {banach,real_normed_field}"
2.123 +  assumes "z \<noteq> 0" and "n > 0"
2.124 +  shows   "(\<lambda>k. inverse ((z + of_nat k)^Suc n)) sums ((-1) ^ Suc n * Polygamma n z / fact n)"
2.125 +  using Polygamma_converges'[OF assms(1), of "Suc n"] assms(2)
2.126 +  by (simp add: sums_iff Polygamma_def)
2.127 +
2.128 +theorem has_field_derivative_ln_Gamma_complex [derivative_intros]:
2.129    fixes z :: complex
2.130    assumes z: "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
2.131    shows   "(ln_Gamma has_field_derivative Digamma z) (at z)"
2.132 @@ -814,7 +818,7 @@
2.133    finally show ?thesis by (simp add: Digamma_def[of z])
2.134  qed
2.135
2.136 -lemma Polygamma_plus1:
2.137 +theorem Polygamma_plus1:
2.138    assumes "z \<noteq> 0"
2.139    shows   "Polygamma n (z + 1) = Polygamma n z + (-1)^n * fact n / (z ^ Suc n)"
2.140  proof (cases "n = 0")
2.141 @@ -832,7 +836,7 @@
2.142    finally show ?thesis .
2.143  qed (insert assms, simp add: Digamma_plus1 inverse_eq_divide)
2.144
2.145 -lemma Digamma_of_nat:
2.146 +theorem Digamma_of_nat:
2.147    "Digamma (of_nat (Suc n) :: 'a :: {real_normed_field,banach}) = harm n - euler_mascheroni"
2.148  proof (induction n)
2.149    case (Suc n)
2.150 @@ -897,7 +901,7 @@
2.151  qed
2.152
2.153
2.154 -lemma has_field_derivative_Polygamma [derivative_intros]:
2.155 +theorem has_field_derivative_Polygamma [derivative_intros]:
2.156    fixes z :: "'a :: {real_normed_field,euclidean_space}"
2.157    assumes z: "z \<notin> \<int>\<^sub>\<le>\<^sub>0"
2.158    shows "(Polygamma n has_field_derivative Polygamma (Suc n) z) (at z within A)"
2.159 @@ -1017,7 +1021,7 @@
2.160    the reals and for the complex numbers with a minimal amount of proof duplication.
2.161  \<close>
2.162
2.163 -class Gamma = real_normed_field + complete_space +
2.164 +class%unimportant Gamma = real_normed_field + complete_space +
2.165    fixes rGamma :: "'a \<Rightarrow> 'a"
2.166    assumes rGamma_eq_zero_iff_aux: "rGamma z = 0 \<longleftrightarrow> (\<exists>n. z = - of_nat n)"
2.167    assumes differentiable_rGamma_aux1:
2.168 @@ -1070,7 +1074,7 @@
2.169                    exp_def of_real_def[symmetric] suminf_def sums_def[abs_def] atLeast0AtMost)
2.170  qed (insert rGamma_eq_zero_iff[of z], simp_all add: rGamma_series_nonpos_Ints_LIMSEQ)
2.171
2.172 -lemma Gamma_series_LIMSEQ [tendsto_intros]:
2.173 +theorem Gamma_series_LIMSEQ [tendsto_intros]:
2.174    "Gamma_series z \<longlonglongrightarrow> Gamma z"
2.175  proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0")
2.176    case False
2.177 @@ -1128,10 +1132,10 @@
2.179  qed simp_all
2.180
2.181 -lemma Gamma_plus1: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Gamma (z + 1) = z * Gamma z"
2.182 +theorem Gamma_plus1: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Gamma (z + 1) = z * Gamma z"
2.183    using rGamma_plus1[of z] by (simp add: rGamma_inverse_Gamma field_simps Gamma_eq_zero_iff)
2.184
2.185 -lemma pochhammer_Gamma: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> pochhammer z n = Gamma (z + of_nat n) / Gamma z"
2.186 +theorem pochhammer_Gamma: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> pochhammer z n = Gamma (z + of_nat n) / Gamma z"
2.187    using pochhammer_rGamma[of z]
2.188    by (simp add: rGamma_inverse_Gamma Gamma_eq_zero_iff field_simps)
2.189
2.190 @@ -1147,7 +1151,7 @@
2.191
2.192  lemma Gamma_1 [simp]: "Gamma 1 = 1" unfolding Gamma_def by simp
2.193
2.194 -lemma Gamma_fact: "Gamma (1 + of_nat n) = fact n"
2.195 +theorem Gamma_fact: "Gamma (1 + of_nat n) = fact n"
2.196    by (simp add: pochhammer_fact pochhammer_Gamma of_nat_in_nonpos_Ints_iff flip: of_nat_Suc)
2.197
2.198  lemma Gamma_numeral: "Gamma (numeral n) = fact (pred_numeral n)"
2.199 @@ -1230,8 +1234,7 @@
2.200  declare has_field_derivative_rGamma_no_nonpos_int [derivative_intros]
2.201  declare has_field_derivative_rGamma [derivative_intros]
2.202
2.203 -
2.204 -lemma has_field_derivative_Gamma [derivative_intros]:
2.205 +theorem has_field_derivative_Gamma [derivative_intros]:
2.206    "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> (Gamma has_field_derivative Gamma z * Digamma z) (at z within A)"
2.207    unfolding Gamma_def [abs_def]
2.208    by (fastforce intro!: derivative_eq_intros simp: rGamma_eq_zero_iff)
2.209 @@ -1242,13 +1245,6 @@
2.210  hide_fact rGamma_eq_zero_iff_aux differentiable_rGamma_aux1 differentiable_rGamma_aux2
2.211            differentiable_rGamma_aux2 rGamma_series_aux Gamma_class.rGamma_eq_zero_iff_aux
2.212
2.213 -
2.214 -
2.215 -(* TODO: differentiable etc. *)
2.216 -
2.217 -
2.218 -subsection \<open>Continuity\<close>
2.219 -
2.220  lemma continuous_on_rGamma [continuous_intros]: "continuous_on A rGamma"
2.221    by (rule DERIV_continuous_on has_field_derivative_rGamma)+
2.222
2.223 @@ -1263,14 +1259,12 @@
2.224    "isCont f z \<Longrightarrow> f z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> isCont (\<lambda>x. Gamma (f x)) z"
2.225    by (rule isCont_o2[OF _  DERIV_isCont[OF has_field_derivative_Gamma]])
2.226
2.227 -
2.228 -
2.229 -text \<open>The complex Gamma function\<close>
2.230 -
2.231 -instantiation complex :: Gamma
2.232 +subsection%unimportant \<open>The complex Gamma function\<close>
2.233 +
2.234 +instantiation%unimportant complex :: Gamma
2.235  begin
2.236
2.237 -definition rGamma_complex :: "complex \<Rightarrow> complex" where
2.238 +definition%unimportant rGamma_complex :: "complex \<Rightarrow> complex" where
2.239    "rGamma_complex z = lim (rGamma_series z)"
2.240
2.241  lemma rGamma_series_complex_converges:
2.242 @@ -1305,7 +1299,7 @@
2.243    thus "?thesis1" "?thesis2" by blast+
2.244  qed
2.245
2.246 -context
2.247 +context%unimportant
2.248  begin
2.249
2.250  (* TODO: duplication *)
2.251 @@ -1514,7 +1508,7 @@
2.252
2.253
2.254
2.255 -text \<open>The real Gamma function\<close>
2.256 +subsection%unimportant \<open>The real Gamma function\<close>
2.257
2.258  lemma rGamma_series_real:
2.259    "eventually (\<lambda>n. rGamma_series x n = Re (rGamma_series (of_real x) n)) sequentially"
2.260 @@ -1532,7 +1526,7 @@
2.261    finally show "rGamma_series x n = Re (rGamma_series (of_real x) n)" ..
2.262  qed
2.263
2.264 -instantiation real :: Gamma
2.265 +instantiation%unimportant real :: Gamma
2.266  begin
2.267
2.268  definition "rGamma_real x = Re (rGamma (of_real x :: complex))"
2.269 @@ -1777,7 +1771,7 @@
2.270    finally show ?thesis .
2.271  qed
2.272
2.273 -lemma log_convex_Gamma_real: "convex_on {0<..} (ln \<circ> Gamma :: real \<Rightarrow> real)"
2.274 +theorem log_convex_Gamma_real: "convex_on {0<..} (ln \<circ> Gamma :: real \<Rightarrow> real)"
2.275    by (rule convex_on_realI[of _ _ Digamma])
2.276       (auto intro!: derivative_eq_intros Polygamma_real_mono Gamma_real_pos
2.277             simp: o_def Gamma_eq_zero_iff elim!: nonpos_Ints_cases')
2.278 @@ -1795,7 +1789,7 @@
2.279    integers, where the Gamma function is not defined).
2.280  \<close>
2.281
2.282 -context
2.283 +context%unimportant
2.284    fixes G :: "real \<Rightarrow> real"
2.285    assumes G_1: "G 1 = 1"
2.286    assumes G_plus1: "x > 0 \<Longrightarrow> G (x + 1) = x * G x"
2.287 @@ -1928,7 +1922,7 @@
2.288  end
2.289
2.290
2.291 -subsection \<open>Beta function\<close>
2.292 +subsection \<open>The Beta function\<close>
2.293
2.294  definition Beta where "Beta a b = Gamma a * Gamma b / Gamma (a + b)"
2.295
2.296 @@ -1959,7 +1953,7 @@
2.297                 (at y within A)"
2.298    using has_field_derivative_Beta1[of y x A] assms by (simp add: Beta_commute add_ac)
2.299
2.300 -lemma Beta_plus1_plus1:
2.301 +theorem Beta_plus1_plus1:
2.302    assumes "x \<notin> \<int>\<^sub>\<le>\<^sub>0" "y \<notin> \<int>\<^sub>\<le>\<^sub>0"
2.303    shows   "Beta (x + 1) y + Beta x (y + 1) = Beta x y"
2.304  proof -
2.305 @@ -1972,7 +1966,7 @@
2.306    finally show ?thesis .
2.307  qed
2.308
2.309 -lemma Beta_plus1_left:
2.310 +theorem Beta_plus1_left:
2.311    assumes "x \<notin> \<int>\<^sub>\<le>\<^sub>0"
2.312    shows   "(x + y) * Beta (x + 1) y = x * Beta x y"
2.313  proof -
2.314 @@ -1983,7 +1977,7 @@
2.315    finally show ?thesis .
2.316  qed
2.317
2.318 -lemma Beta_plus1_right:
2.319 +theorem Beta_plus1_right:
2.320    assumes "y \<notin> \<int>\<^sub>\<le>\<^sub>0"
2.321    shows   "(x + y) * Beta x (y + 1) = y * Beta x y"
2.323 @@ -2052,7 +2046,7 @@
2.324      by (simp add: divide_simps Gamma_eq_zero_iff ring_distribs exp_diff exp_of_real ac_simps)
2.325  qed
2.326
2.327 -lemma Gamma_reflection_complex:
2.328 +theorem Gamma_reflection_complex:
2.329    fixes z :: complex
2.330    shows "Gamma z * Gamma (1 - z) = of_real pi / sin (of_real pi * z)"
2.331  proof -
2.332 @@ -2367,7 +2361,7 @@
2.333    finally show ?thesis .
2.334  qed
2.335
2.336 -lemma Gamma_legendre_duplication:
2.337 +theorem Gamma_legendre_duplication:
2.338    fixes z :: complex
2.339    assumes "z \<notin> \<int>\<^sub>\<le>\<^sub>0" "z + 1/2 \<notin> \<int>\<^sub>\<le>\<^sub>0"
2.340    shows "Gamma z * Gamma (z + 1/2) =
2.341 @@ -2377,7 +2371,7 @@
2.342  end
2.343
2.344
2.345 -subsection \<open>Limits and residues\<close>
2.346 +subsection%unimportant \<open>Limits and residues\<close>
2.347
2.348  text \<open>
2.349    The inverse of the Gamma function has simple zeros:
2.350 @@ -2477,7 +2471,7 @@
2.351    finally show ?thesis ..
2.352  qed
2.353
2.354 -lemma Gamma_series_euler':
2.355 +theorem Gamma_series_euler':
2.356    assumes z: "(z :: 'a :: Gamma) \<notin> \<int>\<^sub>\<le>\<^sub>0"
2.357    shows "(\<lambda>n. Gamma_series_euler' z n) \<longlonglongrightarrow> Gamma z"
2.358  proof (rule Gamma_seriesI, rule Lim_transform_eventually)
2.359 @@ -2520,7 +2514,8 @@
2.360    "Gamma_series_weierstrass z n =
2.361       exp (-euler_mascheroni * z) / z * (\<Prod>k=1..n. exp (z / of_nat k) / (1 + z / of_nat k))"
2.362
2.363 -definition rGamma_series_weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
2.364 +definition%unimportant
2.365 +  rGamma_series_weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
2.366    "rGamma_series_weierstrass z n =
2.367       exp (euler_mascheroni * z) * z * (\<Prod>k=1..n. (1 + z / of_nat k) * exp (-z / of_nat k))"
2.368
2.369 @@ -2532,7 +2527,7 @@
2.370    "eventually (\<lambda>k. rGamma_series_weierstrass (- of_nat n) k = 0) sequentially"
2.371    using eventually_ge_at_top[of n] by eventually_elim (auto simp: rGamma_series_weierstrass_def)
2.372
2.373 -lemma Gamma_weierstrass_complex: "Gamma_series_weierstrass z \<longlonglongrightarrow> Gamma (z :: complex)"
2.374 +theorem Gamma_weierstrass_complex: "Gamma_series_weierstrass z \<longlonglongrightarrow> Gamma (z :: complex)"
2.375  proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0")
2.376    case True
2.377    then obtain n where "z = - of_nat n" by (elim nonpos_Ints_cases')
2.378 @@ -2684,7 +2679,7 @@
2.379    qed
2.380  qed
2.381
2.382 -lemma gbinomial_Gamma:
2.383 +theorem gbinomial_Gamma:
2.384    assumes "z + 1 \<notin> \<int>\<^sub>\<le>\<^sub>0"
2.385    shows   "(z gchoose n) = Gamma (z + 1) / (fact n * Gamma (z - of_nat n + 1))"
2.386  proof -
2.387 @@ -2785,7 +2780,7 @@
2.388      by (rule integrable_Un') (insert c, auto simp: max_def)
2.389  qed
2.390
2.391 -lemma Gamma_integral_complex:
2.392 +theorem Gamma_integral_complex:
2.393    assumes z: "Re z > 0"
2.394    shows   "((\<lambda>t. of_real t powr (z - 1) / of_real (exp t)) has_integral Gamma z) {0..}"
2.395  proof -
2.396 @@ -3067,7 +3062,7 @@
2.397    shows   "(\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1)) integrable_on {0..1}"
2.398    using integrable_Beta[OF assms] by (rule set_borel_integral_eq_integral)
2.399
2.400 -lemma has_integral_Beta_real:
2.401 +theorem has_integral_Beta_real:
2.402    assumes a: "a > 0" and b: "b > (0 :: real)"
2.403    shows "((\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1)) has_integral Beta a b) {0..1}"
2.404  proof -
2.405 @@ -3158,7 +3153,7 @@
2.406
2.407  subsection \<open>The Weierstraß product formula for the sine\<close>
2.408
2.409 -lemma sin_product_formula_complex:
2.410 +theorem sin_product_formula_complex:
2.411    fixes z :: complex
2.412    shows "(\<lambda>n. of_real pi * z * (\<Prod>k=1..n. 1 - z^2 / of_nat k^2)) \<longlonglongrightarrow> sin (of_real pi * z)"
2.413  proof -
```