Tagged Ball_Volume and Gamma_Function in HOL-Analysis
authorManuel Eberl <eberlm@in.tum.de>
Fri Jul 13 16:54:36 2018 +0100 (4 months ago)
changeset 68624205d352ed727
parent 68623 b942da0962c2
child 68625 2ec84498f562
Tagged Ball_Volume and Gamma_Function in HOL-Analysis
src/HOL/Analysis/Ball_Volume.thy
src/HOL/Analysis/Gamma_Function.thy
     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.66    by (simp_all add: eval_unit_ball_vol)
    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.109    by (simp add: summable_iff_convergent)
   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.178    finally show ?case by (simp add: add_ac pochhammer_rec')
   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.322    using Beta_plus1_left[of y x] assms by (simp_all add: Beta_commute add.commute)
   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 -