--- a/src/HOL/Analysis/Analysis.thy Fri Jul 13 17:27:05 2018 +0100
+++ b/src/HOL/Analysis/Analysis.thy Fri Jul 13 22:10:05 2018 +0100
@@ -25,6 +25,7 @@
Gamma_Function
Change_Of_Vars
Lipschitz
+ Simplex_Content
begin
end
--- a/src/HOL/Analysis/Ball_Volume.thy Fri Jul 13 17:27:05 2018 +0100
+++ b/src/HOL/Analysis/Ball_Volume.thy Fri Jul 13 22:10:05 2018 +0100
@@ -1,9 +1,9 @@
(*
- File: HOL/Analysis/Gamma_Function.thy
+ File: HOL/Analysis/Ball_Volume.thy
Author: Manuel Eberl, TU München
*)
-section \<open>The volume (Lebesgue measure) of an $n$-dimensional ball\<close>
+section \<open>The volume of an $n$-dimensional ball\<close>
theory Ball_Volume
imports Gamma_Function Lebesgue_Integral_Substitution
@@ -14,7 +14,7 @@
dimension need not be an integer; we also allow fractional dimensions, although we do
not use this case or prove anything about it for now.
\<close>
-definition unit_ball_vol :: "real \<Rightarrow> real" where
+definition%important unit_ball_vol :: "real \<Rightarrow> real" where
"unit_ball_vol n = pi powr (n / 2) / Gamma (n / 2 + 1)"
lemma unit_ball_vol_pos [simp]: "n \<ge> 0 \<Longrightarrow> unit_ball_vol n > 0"
@@ -177,7 +177,7 @@
assumes r: "r \<ge> 0"
begin
-theorem emeasure_cball:
+theorem%unimportant emeasure_cball:
"emeasure lborel (cball c r) = ennreal (unit_ball_vol (DIM('a)) * r ^ DIM('a))"
proof (cases "r = 0")
case False
@@ -202,11 +202,11 @@
finally show ?thesis .
qed auto
-corollary content_cball:
+corollary%unimportant content_cball:
"content (cball c r) = unit_ball_vol (DIM('a)) * r ^ DIM('a)"
by (simp add: measure_def emeasure_cball r)
-corollary emeasure_ball:
+corollary%unimportant emeasure_ball:
"emeasure lborel (ball c r) = ennreal (unit_ball_vol (DIM('a)) * r ^ DIM('a))"
proof -
from negligible_sphere[of c r] have "sphere c r \<in> null_sets lborel"
@@ -219,7 +219,7 @@
finally show ?thesis ..
qed
-corollary content_ball:
+corollary%important content_ball:
"content (ball c r) = unit_ball_vol (DIM('a)) * r ^ DIM('a)"
by (simp add: measure_def r emeasure_ball)
@@ -289,22 +289,25 @@
lemma unit_ball_vol_1 [simp]: "unit_ball_vol 1 = 2"
using unit_ball_vol_odd[of 0] by simp
-corollary unit_ball_vol_2: "unit_ball_vol 2 = pi"
+corollary%unimportant
+ unit_ball_vol_2: "unit_ball_vol 2 = pi"
and unit_ball_vol_3: "unit_ball_vol 3 = 4 / 3 * pi"
and unit_ball_vol_4: "unit_ball_vol 4 = pi\<^sup>2 / 2"
and unit_ball_vol_5: "unit_ball_vol 5 = 8 / 15 * pi\<^sup>2"
by (simp_all add: eval_unit_ball_vol)
-corollary circle_area: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 2) set) = r ^ 2 * pi"
+corollary%unimportant circle_area:
+ "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 2) set) = r ^ 2 * pi"
by (simp add: content_ball unit_ball_vol_2)
-corollary sphere_volume: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 3) set) = 4 / 3 * r ^ 3 * pi"
+corollary%unimportant sphere_volume:
+ "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 3) set) = 4 / 3 * r ^ 3 * pi"
by (simp add: content_ball unit_ball_vol_3)
text \<open>
Useful equivalent forms
\<close>
-corollary content_ball_eq_0_iff [simp]: "content (ball c r) = 0 \<longleftrightarrow> r \<le> 0"
+corollary%unimportant content_ball_eq_0_iff [simp]: "content (ball c r) = 0 \<longleftrightarrow> r \<le> 0"
proof -
have "r > 0 \<Longrightarrow> content (ball c r) > 0"
by (simp add: content_ball unit_ball_vol_def)
@@ -312,10 +315,10 @@
by (fastforce simp: ball_empty)
qed
-corollary content_ball_gt_0_iff [simp]: "0 < content (ball z r) \<longleftrightarrow> 0 < r"
+corollary%unimportant content_ball_gt_0_iff [simp]: "0 < content (ball z r) \<longleftrightarrow> 0 < r"
by (auto simp: zero_less_measure_iff)
-corollary content_cball_eq_0_iff [simp]: "content (cball c r) = 0 \<longleftrightarrow> r \<le> 0"
+corollary%unimportant content_cball_eq_0_iff [simp]: "content (cball c r) = 0 \<longleftrightarrow> r \<le> 0"
proof (cases "r = 0")
case False
moreover have "r > 0 \<Longrightarrow> content (cball c r) > 0"
@@ -324,7 +327,7 @@
by fastforce
qed auto
-corollary content_cball_gt_0_iff [simp]: "0 < content (cball z r) \<longleftrightarrow> 0 < r"
+corollary%unimportant content_cball_gt_0_iff [simp]: "0 < content (cball z r) \<longleftrightarrow> 0 < r"
by (auto simp: zero_less_measure_iff)
end
--- a/src/HOL/Analysis/Gamma_Function.thy Fri Jul 13 17:27:05 2018 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy Fri Jul 13 22:10:05 2018 +0100
@@ -230,22 +230,22 @@
qed
-subsection \<open>Definitions\<close>
+subsection \<open>The Euler form and the logarithmic Gamma function\<close>
text \<open>
- We define the Gamma function by first defining its multiplicative inverse @{term "Gamma_inv"}.
- This is more convenient because @{term "Gamma_inv"} is entire, which makes proofs of its
+ We define the Gamma function by first defining its multiplicative inverse \<open>rGamma\<close>.
+ This is more convenient because \<open>rGamma\<close> is entire, which makes proofs of its
properties more convenient because one does not have to watch out for discontinuities.
- (e.g. @{term "Gamma_inv"} fulfils @{term "rGamma z = z * rGamma (z + 1)"} everywhere,
- whereas @{term "Gamma"} does not fulfil the analogous equation on the non-positive integers)
-
- We define the Gamma function (resp. its inverse) in the Euler form. This form has the advantage
+ (e.g. \<open>rGamma\<close> fulfils \<open>rGamma z = z * rGamma (z + 1)\<close> everywhere, whereas the \<open>\<Gamma>\<close> function
+ does not fulfil the analogous equation on the non-positive integers)
+
+ We define the \<open>\<Gamma>\<close> function (resp.\ its reciprocale) in the Euler form. This form has the advantage
that it is a relatively simple limit that converges everywhere. The limit at the poles is 0
- (due to division by 0). The functional equation @{term "Gamma (z + 1) = z * Gamma z"} follows
+ (due to division by 0). The functional equation \<open>Gamma (z + 1) = z * Gamma z\<close> follows
immediately from the definition.
\<close>
-definition Gamma_series :: "('a :: {banach,real_normed_field}) \<Rightarrow> nat \<Rightarrow> 'a" where
+definition%important Gamma_series :: "('a :: {banach,real_normed_field}) \<Rightarrow> nat \<Rightarrow> 'a" where
"Gamma_series z n = fact n * exp (z * of_real (ln (of_nat n))) / pochhammer z (n+1)"
definition Gamma_series' :: "('a :: {banach,real_normed_field}) \<Rightarrow> nat \<Rightarrow> 'a" where
@@ -304,11 +304,8 @@
from tendsto_add[OF this tendsto_const[of 1]] show "(\<lambda>n. z / of_nat n + 1) \<longlonglongrightarrow> 1" by simp
qed
-
-subsection \<open>Convergence of the Euler series form\<close>
-
text \<open>
- We now show that the series that defines the Gamma function in the Euler form converges
+ We now show that the series that defines the \<open>\<Gamma>\<close> function in the Euler form converges
and that the function defined by it is continuous on the complex halfspace with positive
real part.
@@ -320,10 +317,10 @@
function to the inverse of the Gamma function, and from that to the Gamma function itself.
\<close>
-definition ln_Gamma_series :: "('a :: {banach,real_normed_field,ln}) \<Rightarrow> nat \<Rightarrow> 'a" where
+definition%important ln_Gamma_series :: "('a :: {banach,real_normed_field,ln}) \<Rightarrow> nat \<Rightarrow> 'a" where
"ln_Gamma_series z n = z * ln (of_nat n) - ln z - (\<Sum>k=1..n. ln (z / of_nat k + 1))"
-definition ln_Gamma_series' :: "('a :: {banach,real_normed_field,ln}) \<Rightarrow> nat \<Rightarrow> 'a" where
+definition%unimportant ln_Gamma_series' :: "('a :: {banach,real_normed_field,ln}) \<Rightarrow> nat \<Rightarrow> 'a" where
"ln_Gamma_series' z n =
- euler_mascheroni*z - ln z + (\<Sum>k=1..n. z / of_nat n - ln (z / of_nat k + 1))"
@@ -333,9 +330,7 @@
text \<open>
We now show that the log-Gamma series converges locally uniformly for all complex numbers except
- the non-positive integers. We do this by proving that the series is locally Cauchy, adapting this
- proof:
- https://math.stackexchange.com/questions/887158/convergence-of-gammaz-lim-n-to-infty-fracnzn-prod-m-0nzm
+ the non-positive integers. We do this by proving that the series is locally Cauchy.
\<close>
context
@@ -497,7 +492,7 @@
lemma ln_Gamma_series_complex_converges'': "(z :: complex) \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> convergent (ln_Gamma_series z)"
by (drule ln_Gamma_series_complex_converges') (auto intro: uniformly_convergent_imp_convergent)
-lemma ln_Gamma_complex_LIMSEQ: "(z :: complex) \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln_Gamma_series z \<longlonglongrightarrow> ln_Gamma z"
+theorem ln_Gamma_complex_LIMSEQ: "(z :: complex) \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln_Gamma_series z \<longlonglongrightarrow> ln_Gamma z"
using ln_Gamma_series_complex_converges'' by (simp add: convergent_LIMSEQ_iff ln_Gamma_def)
lemma exp_ln_Gamma_series_complex:
@@ -609,6 +604,9 @@
by (subst summable_Suc_iff) (simp add: summable_mult inverse_power_summable)
qed
+
+subsection \<open>The Polygamma functions\<close>
+
lemma summable_deriv_ln_Gamma:
"z \<noteq> (0 :: 'a :: {real_normed_field,banach}) \<Longrightarrow>
summable (\<lambda>n. inverse (of_nat (Suc n)) - inverse (z + of_nat (Suc n)))"
@@ -616,13 +614,12 @@
by (rule uniformly_convergent_imp_convergent,
rule uniformly_summable_deriv_ln_Gamma[of z "norm z/2"]) simp_all
-
-definition Polygamma :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a" where
+definition%important Polygamma :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a" where
"Polygamma n z = (if n = 0 then
(\<Sum>k. inverse (of_nat (Suc k)) - inverse (z + of_nat k)) - euler_mascheroni else
(-1)^Suc n * fact n * (\<Sum>k. inverse ((z + of_nat k)^Suc n)))"
-abbreviation Digamma :: "('a :: {real_normed_field,banach}) \<Rightarrow> 'a" where
+abbreviation%important Digamma :: "('a :: {real_normed_field,banach}) \<Rightarrow> 'a" where
"Digamma \<equiv> Polygamma 0"
lemma Digamma_def:
@@ -708,7 +705,7 @@
using uniformly_convergent_imp_convergent[OF Polygamma_converges[OF assms, of 1], of z]
by (simp add: summable_iff_convergent)
-lemma Digamma_LIMSEQ:
+theorem Digamma_LIMSEQ:
fixes z :: "'a :: {banach,real_normed_field}"
assumes z: "z \<noteq> 0"
shows "(\<lambda>m. of_real (ln (real m)) - (\<Sum>n<m. inverse (z + of_nat n))) \<longlonglongrightarrow> Digamma z"
@@ -739,7 +736,14 @@
finally show ?thesis by (rule Lim_transform) (insert lim, simp)
qed
-lemma has_field_derivative_ln_Gamma_complex [derivative_intros]:
+theorem Polygamma_LIMSEQ:
+ fixes z :: "'a :: {banach,real_normed_field}"
+ assumes "z \<noteq> 0" and "n > 0"
+ shows "(\<lambda>k. inverse ((z + of_nat k)^Suc n)) sums ((-1) ^ Suc n * Polygamma n z / fact n)"
+ using Polygamma_converges'[OF assms(1), of "Suc n"] assms(2)
+ by (simp add: sums_iff Polygamma_def)
+
+theorem has_field_derivative_ln_Gamma_complex [derivative_intros]:
fixes z :: complex
assumes z: "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
shows "(ln_Gamma has_field_derivative Digamma z) (at z)"
@@ -814,7 +818,7 @@
finally show ?thesis by (simp add: Digamma_def[of z])
qed
-lemma Polygamma_plus1:
+theorem Polygamma_plus1:
assumes "z \<noteq> 0"
shows "Polygamma n (z + 1) = Polygamma n z + (-1)^n * fact n / (z ^ Suc n)"
proof (cases "n = 0")
@@ -832,7 +836,7 @@
finally show ?thesis .
qed (insert assms, simp add: Digamma_plus1 inverse_eq_divide)
-lemma Digamma_of_nat:
+theorem Digamma_of_nat:
"Digamma (of_nat (Suc n) :: 'a :: {real_normed_field,banach}) = harm n - euler_mascheroni"
proof (induction n)
case (Suc n)
@@ -897,7 +901,7 @@
qed
-lemma has_field_derivative_Polygamma [derivative_intros]:
+theorem has_field_derivative_Polygamma [derivative_intros]:
fixes z :: "'a :: {real_normed_field,euclidean_space}"
assumes z: "z \<notin> \<int>\<^sub>\<le>\<^sub>0"
shows "(Polygamma n has_field_derivative Polygamma (Suc n) z) (at z within A)"
@@ -1017,7 +1021,7 @@
the reals and for the complex numbers with a minimal amount of proof duplication.
\<close>
-class Gamma = real_normed_field + complete_space +
+class%unimportant Gamma = real_normed_field + complete_space +
fixes rGamma :: "'a \<Rightarrow> 'a"
assumes rGamma_eq_zero_iff_aux: "rGamma z = 0 \<longleftrightarrow> (\<exists>n. z = - of_nat n)"
assumes differentiable_rGamma_aux1:
@@ -1070,7 +1074,7 @@
exp_def of_real_def[symmetric] suminf_def sums_def[abs_def] atLeast0AtMost)
qed (insert rGamma_eq_zero_iff[of z], simp_all add: rGamma_series_nonpos_Ints_LIMSEQ)
-lemma Gamma_series_LIMSEQ [tendsto_intros]:
+theorem Gamma_series_LIMSEQ [tendsto_intros]:
"Gamma_series z \<longlonglongrightarrow> Gamma z"
proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0")
case False
@@ -1128,10 +1132,10 @@
finally show ?case by (simp add: add_ac pochhammer_rec')
qed simp_all
-lemma Gamma_plus1: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Gamma (z + 1) = z * Gamma z"
+theorem Gamma_plus1: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Gamma (z + 1) = z * Gamma z"
using rGamma_plus1[of z] by (simp add: rGamma_inverse_Gamma field_simps Gamma_eq_zero_iff)
-lemma pochhammer_Gamma: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> pochhammer z n = Gamma (z + of_nat n) / Gamma z"
+theorem pochhammer_Gamma: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> pochhammer z n = Gamma (z + of_nat n) / Gamma z"
using pochhammer_rGamma[of z]
by (simp add: rGamma_inverse_Gamma Gamma_eq_zero_iff field_simps)
@@ -1147,7 +1151,7 @@
lemma Gamma_1 [simp]: "Gamma 1 = 1" unfolding Gamma_def by simp
-lemma Gamma_fact: "Gamma (1 + of_nat n) = fact n"
+theorem Gamma_fact: "Gamma (1 + of_nat n) = fact n"
by (simp add: pochhammer_fact pochhammer_Gamma of_nat_in_nonpos_Ints_iff flip: of_nat_Suc)
lemma Gamma_numeral: "Gamma (numeral n) = fact (pred_numeral n)"
@@ -1230,8 +1234,7 @@
declare has_field_derivative_rGamma_no_nonpos_int [derivative_intros]
declare has_field_derivative_rGamma [derivative_intros]
-
-lemma has_field_derivative_Gamma [derivative_intros]:
+theorem has_field_derivative_Gamma [derivative_intros]:
"z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> (Gamma has_field_derivative Gamma z * Digamma z) (at z within A)"
unfolding Gamma_def [abs_def]
by (fastforce intro!: derivative_eq_intros simp: rGamma_eq_zero_iff)
@@ -1242,13 +1245,6 @@
hide_fact rGamma_eq_zero_iff_aux differentiable_rGamma_aux1 differentiable_rGamma_aux2
differentiable_rGamma_aux2 rGamma_series_aux Gamma_class.rGamma_eq_zero_iff_aux
-
-
-(* TODO: differentiable etc. *)
-
-
-subsection \<open>Continuity\<close>
-
lemma continuous_on_rGamma [continuous_intros]: "continuous_on A rGamma"
by (rule DERIV_continuous_on has_field_derivative_rGamma)+
@@ -1263,14 +1259,12 @@
"isCont f z \<Longrightarrow> f z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> isCont (\<lambda>x. Gamma (f x)) z"
by (rule isCont_o2[OF _ DERIV_isCont[OF has_field_derivative_Gamma]])
-
-
-text \<open>The complex Gamma function\<close>
-
-instantiation complex :: Gamma
+subsection%unimportant \<open>The complex Gamma function\<close>
+
+instantiation%unimportant complex :: Gamma
begin
-definition rGamma_complex :: "complex \<Rightarrow> complex" where
+definition%unimportant rGamma_complex :: "complex \<Rightarrow> complex" where
"rGamma_complex z = lim (rGamma_series z)"
lemma rGamma_series_complex_converges:
@@ -1305,7 +1299,7 @@
thus "?thesis1" "?thesis2" by blast+
qed
-context
+context%unimportant
begin
(* TODO: duplication *)
@@ -1514,7 +1508,7 @@
-text \<open>The real Gamma function\<close>
+subsection%unimportant \<open>The real Gamma function\<close>
lemma rGamma_series_real:
"eventually (\<lambda>n. rGamma_series x n = Re (rGamma_series (of_real x) n)) sequentially"
@@ -1532,7 +1526,7 @@
finally show "rGamma_series x n = Re (rGamma_series (of_real x) n)" ..
qed
-instantiation real :: Gamma
+instantiation%unimportant real :: Gamma
begin
definition "rGamma_real x = Re (rGamma (of_real x :: complex))"
@@ -1777,7 +1771,7 @@
finally show ?thesis .
qed
-lemma log_convex_Gamma_real: "convex_on {0<..} (ln \<circ> Gamma :: real \<Rightarrow> real)"
+theorem log_convex_Gamma_real: "convex_on {0<..} (ln \<circ> Gamma :: real \<Rightarrow> real)"
by (rule convex_on_realI[of _ _ Digamma])
(auto intro!: derivative_eq_intros Polygamma_real_mono Gamma_real_pos
simp: o_def Gamma_eq_zero_iff elim!: nonpos_Ints_cases')
@@ -1795,7 +1789,7 @@
integers, where the Gamma function is not defined).
\<close>
-context
+context%unimportant
fixes G :: "real \<Rightarrow> real"
assumes G_1: "G 1 = 1"
assumes G_plus1: "x > 0 \<Longrightarrow> G (x + 1) = x * G x"
@@ -1928,7 +1922,7 @@
end
-subsection \<open>Beta function\<close>
+subsection \<open>The Beta function\<close>
definition Beta where "Beta a b = Gamma a * Gamma b / Gamma (a + b)"
@@ -1959,7 +1953,7 @@
(at y within A)"
using has_field_derivative_Beta1[of y x A] assms by (simp add: Beta_commute add_ac)
-lemma Beta_plus1_plus1:
+theorem Beta_plus1_plus1:
assumes "x \<notin> \<int>\<^sub>\<le>\<^sub>0" "y \<notin> \<int>\<^sub>\<le>\<^sub>0"
shows "Beta (x + 1) y + Beta x (y + 1) = Beta x y"
proof -
@@ -1972,7 +1966,7 @@
finally show ?thesis .
qed
-lemma Beta_plus1_left:
+theorem Beta_plus1_left:
assumes "x \<notin> \<int>\<^sub>\<le>\<^sub>0"
shows "(x + y) * Beta (x + 1) y = x * Beta x y"
proof -
@@ -1983,7 +1977,7 @@
finally show ?thesis .
qed
-lemma Beta_plus1_right:
+theorem Beta_plus1_right:
assumes "y \<notin> \<int>\<^sub>\<le>\<^sub>0"
shows "(x + y) * Beta x (y + 1) = y * Beta x y"
using Beta_plus1_left[of y x] assms by (simp_all add: Beta_commute add.commute)
@@ -2052,7 +2046,7 @@
by (simp add: divide_simps Gamma_eq_zero_iff ring_distribs exp_diff exp_of_real ac_simps)
qed
-lemma Gamma_reflection_complex:
+theorem Gamma_reflection_complex:
fixes z :: complex
shows "Gamma z * Gamma (1 - z) = of_real pi / sin (of_real pi * z)"
proof -
@@ -2367,7 +2361,7 @@
finally show ?thesis .
qed
-lemma Gamma_legendre_duplication:
+theorem Gamma_legendre_duplication:
fixes z :: complex
assumes "z \<notin> \<int>\<^sub>\<le>\<^sub>0" "z + 1/2 \<notin> \<int>\<^sub>\<le>\<^sub>0"
shows "Gamma z * Gamma (z + 1/2) =
@@ -2377,7 +2371,7 @@
end
-subsection \<open>Limits and residues\<close>
+subsection%unimportant \<open>Limits and residues\<close>
text \<open>
The inverse of the Gamma function has simple zeros:
@@ -2477,7 +2471,7 @@
finally show ?thesis ..
qed
-lemma Gamma_series_euler':
+theorem Gamma_series_euler':
assumes z: "(z :: 'a :: Gamma) \<notin> \<int>\<^sub>\<le>\<^sub>0"
shows "(\<lambda>n. Gamma_series_euler' z n) \<longlonglongrightarrow> Gamma z"
proof (rule Gamma_seriesI, rule Lim_transform_eventually)
@@ -2520,7 +2514,8 @@
"Gamma_series_weierstrass z n =
exp (-euler_mascheroni * z) / z * (\<Prod>k=1..n. exp (z / of_nat k) / (1 + z / of_nat k))"
-definition rGamma_series_weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
+definition%unimportant
+ rGamma_series_weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
"rGamma_series_weierstrass z n =
exp (euler_mascheroni * z) * z * (\<Prod>k=1..n. (1 + z / of_nat k) * exp (-z / of_nat k))"
@@ -2532,7 +2527,7 @@
"eventually (\<lambda>k. rGamma_series_weierstrass (- of_nat n) k = 0) sequentially"
using eventually_ge_at_top[of n] by eventually_elim (auto simp: rGamma_series_weierstrass_def)
-lemma Gamma_weierstrass_complex: "Gamma_series_weierstrass z \<longlonglongrightarrow> Gamma (z :: complex)"
+theorem Gamma_weierstrass_complex: "Gamma_series_weierstrass z \<longlonglongrightarrow> Gamma (z :: complex)"
proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0")
case True
then obtain n where "z = - of_nat n" by (elim nonpos_Ints_cases')
@@ -2684,7 +2679,7 @@
qed
qed
-lemma gbinomial_Gamma:
+theorem gbinomial_Gamma:
assumes "z + 1 \<notin> \<int>\<^sub>\<le>\<^sub>0"
shows "(z gchoose n) = Gamma (z + 1) / (fact n * Gamma (z - of_nat n + 1))"
proof -
@@ -2785,7 +2780,7 @@
by (rule integrable_Un') (insert c, auto simp: max_def)
qed
-lemma Gamma_integral_complex:
+theorem Gamma_integral_complex:
assumes z: "Re z > 0"
shows "((\<lambda>t. of_real t powr (z - 1) / of_real (exp t)) has_integral Gamma z) {0..}"
proof -
@@ -3067,7 +3062,7 @@
shows "(\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1)) integrable_on {0..1}"
using integrable_Beta[OF assms] by (rule set_borel_integral_eq_integral)
-lemma has_integral_Beta_real:
+theorem has_integral_Beta_real:
assumes a: "a > 0" and b: "b > (0 :: real)"
shows "((\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1)) has_integral Beta a b) {0..1}"
proof -
@@ -3158,7 +3153,7 @@
subsection \<open>The Weierstraß product formula for the sine\<close>
-lemma sin_product_formula_complex:
+theorem sin_product_formula_complex:
fixes z :: complex
shows "(\<lambda>n. of_real pi * z * (\<Prod>k=1..n. 1 - z^2 / of_nat k^2)) \<longlonglongrightarrow> sin (of_real pi * z)"
proof -
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Simplex_Content.thy Fri Jul 13 22:10:05 2018 +0100
@@ -0,0 +1,263 @@
+(*
+ File: Analysis/Simplex_Content.thy
+ Author: Manuel Eberl <eberlm@in.tum.de>
+
+ The content of an n-dimensional simplex, including the formula for the content of a
+ triangle and Heron's formula.
+*)
+section \<open>Volume of a simplex\<close>
+theory Simplex_Content
+ imports Change_Of_Vars
+begin
+
+lemma fact_neq_top_ennreal [simp]: "fact n \<noteq> (top :: ennreal)"
+ by (induction n) (auto simp: ennreal_mult_eq_top_iff)
+
+lemma ennreal_fact: "ennreal (fact n) = fact n"
+ by (induction n) (auto simp: ennreal_mult algebra_simps ennreal_of_nat_eq_real_of_nat)
+
+context
+ fixes S :: "'a set \<Rightarrow> real \<Rightarrow> ('a \<Rightarrow> real) set"
+ defines "S \<equiv> (\<lambda>A t. {x. (\<forall>i\<in>A. 0 \<le> x i) \<and> sum x A \<le> t})"
+begin
+
+lemma emeasure_std_simplex_aux_step:
+ assumes "b \<notin> A" "finite A"
+ shows "x(b := y) \<in> S (insert b A) t \<longleftrightarrow> y \<in> {0..t} \<and> x \<in> S A (t - y)"
+ using assms sum_nonneg[of A x] unfolding S_def
+ by (force simp: sum_delta_notmem algebra_simps)
+
+lemma emeasure_std_simplex_aux:
+ fixes t :: real
+ assumes "finite (A :: 'a set)" "t \<ge> 0"
+ shows "emeasure (Pi\<^sub>M A (\<lambda>_. lborel))
+ (S A t \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) = t ^ card A / fact (card A)"
+ using assms(1,2)
+proof (induction arbitrary: t rule: finite_induct)
+ case (empty t)
+ thus ?case by (simp add: PiM_empty S_def)
+next
+ case (insert b A t)
+ define n where "n = Suc (card A)"
+ have n_pos: "n > 0" by (simp add: n_def)
+ let ?M = "\<lambda>A. (Pi\<^sub>M A (\<lambda>_. lborel))"
+ {
+ fix A :: "'a set" and t :: real assume "finite A"
+ have "S A t \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel)) =
+ Pi\<^sub>E A (\<lambda>_. {0..}) \<inter> (\<lambda>x. sum x A) -` {..t} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))"
+ by (auto simp: S_def space_PiM)
+ also have "\<dots> \<in> sets (Pi\<^sub>M A (\<lambda>_. lborel))"
+ using \<open>finite A\<close> by measurable
+ finally have "S A t \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel)) \<in> sets (Pi\<^sub>M A (\<lambda>_. lborel))" .
+ } note meas [measurable] = this
+
+ interpret product_sigma_finite "\<lambda>_. lborel"
+ by standard
+ have "emeasure (?M (insert b A)) (S (insert b A) t \<inter> space (?M (insert b A))) =
+ nn_integral (?M (insert b A))
+ (\<lambda>x. indicator (S (insert b A) t \<inter> space (?M (insert b A))) x)"
+ using insert.hyps by (subst nn_integral_indicator) auto
+ also have "\<dots> = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. indicator (S (insert b A) t \<inter> space (?M (insert b A)))
+ (x(b := y)) \<partial>?M A \<partial>lborel)"
+ using insert.prems insert.hyps by (intro product_nn_integral_insert_rev) auto
+ also have "\<dots> = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. indicator {0..t} y * indicator (S A (t - y) \<inter> space (?M A)) x
+ \<partial>?M A \<partial>lborel)"
+ using insert.hyps insert.prems emeasure_std_simplex_aux_step[of b A]
+ by (intro nn_integral_cong)
+ (auto simp: fun_eq_iff indicator_def space_PiM PiE_def extensional_def)
+ also have "\<dots> = (\<integral>\<^sup>+ y. indicator {0..t} y * (\<integral>\<^sup>+ x. indicator (S A (t - y) \<inter> space (?M A)) x
+ \<partial>?M A) \<partial>lborel)" using \<open>finite A\<close>
+ by (subst nn_integral_cmult) auto
+ also have "\<dots> = (\<integral>\<^sup>+ y. indicator {0..t} y * emeasure (?M A) (S A (t - y) \<inter> space (?M A)) \<partial>lborel)"
+ using \<open>finite A\<close> by (subst nn_integral_indicator) auto
+ also have "\<dots> = (\<integral>\<^sup>+ y. indicator {0..t} y * (t - y) ^ card A / ennreal (fact (card A)) \<partial>lborel)"
+ using insert.IH by (intro nn_integral_cong) (auto simp: indicator_def divide_ennreal)
+ also have "\<dots> = (\<integral>\<^sup>+ y. indicator {0..t} y * (t - y) ^ card A \<partial>lborel) / ennreal (fact (card A))"
+ using \<open>finite A\<close> by (subst nn_integral_divide) auto
+ also have "(\<integral>\<^sup>+ y. indicator {0..t} y * (t - y) ^ card A \<partial>lborel) =
+ (\<integral>\<^sup>+y\<in>{0..t}. ennreal ((t - y) ^ (n - 1)) \<partial>lborel)"
+ by (intro nn_integral_cong) (auto simp: indicator_def n_def)
+ also have "((\<lambda>x. - ((t - x) ^ n / n)) has_real_derivative (t - x) ^ (n - 1)) (at x)"
+ if "x \<in> {0..t}" for x by (rule derivative_eq_intros refl | simp add: n_pos)+
+ hence "(\<integral>\<^sup>+y\<in>{0..t}. ennreal ((t - y) ^ (n - 1)) \<partial>lborel) =
+ ennreal (-((t - t) ^ n / n) - (-((t - 0) ^ n / n)))"
+ using insert.prems insert.hyps by (intro nn_integral_FTC_Icc) auto
+ also have "\<dots> = ennreal (t ^ n / n)" using n_pos by (simp add: zero_power)
+ also have "\<dots> / ennreal (fact (card A)) = ennreal (t ^ n / n / fact (card A))"
+ using n_pos \<open>t \<ge> 0\<close> by (subst divide_ennreal) auto
+ also have "t ^ n / n / fact (card A) = t ^ n / fact n"
+ by (simp add: n_def)
+ also have "n = card (insert b A)"
+ using insert.hyps by (subst card_insert) (auto simp: n_def)
+ finally show ?case .
+qed
+
+end
+
+lemma emeasure_std_simplex:
+ "emeasure lborel (convex hull (insert 0 Basis :: 'a :: euclidean_space set)) =
+ ennreal (1 / fact DIM('a))"
+proof -
+ have "emeasure lborel {x::'a. (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i) \<and> sum ((\<bullet>) x) Basis \<le> 1} =
+ emeasure (distr (Pi\<^sub>M Basis (\<lambda>b. lborel)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b))
+ {x::'a. (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i) \<and> sum ((\<bullet>) x) Basis \<le> 1}"
+ by (subst lborel_eq) simp
+ also have "\<dots> = emeasure (Pi\<^sub>M Basis (\<lambda>b. lborel))
+ ({y::'a \<Rightarrow> real. (\<forall>i\<in>Basis. 0 \<le> y i) \<and> sum y Basis \<le> 1} \<inter>
+ space (Pi\<^sub>M Basis (\<lambda>b. lborel)))"
+ by (subst emeasure_distr) auto
+ also have "\<dots> = ennreal (1 / fact DIM('a))"
+ by (subst emeasure_std_simplex_aux) auto
+ finally show ?thesis by (simp only: std_simplex)
+qed
+
+theorem content_std_simplex:
+ "measure lborel (convex hull (insert 0 Basis :: 'a :: euclidean_space set)) =
+ 1 / fact DIM('a)"
+ by (simp add: measure_def emeasure_std_simplex)
+
+(* TODO: move to Change_of_Vars *)
+lemma measure_lebesgue_linear_transformation:
+ fixes A :: "(real ^ 'n :: {finite, wellorder}) set"
+ fixes f :: "_ \<Rightarrow> real ^ 'n :: {finite, wellorder}"
+ assumes "bounded A" "A \<in> sets lebesgue" "linear f"
+ shows "measure lebesgue (f ` A) = \<bar>det (matrix f)\<bar> * measure lebesgue A"
+proof -
+ from assms have [intro]: "A \<in> lmeasurable"
+ by (intro bounded_set_imp_lmeasurable) auto
+ hence [intro]: "f ` A \<in> lmeasurable"
+ by (intro lmeasure_integral measurable_linear_image assms)
+ have "measure lebesgue (f ` A) = integral (f ` A) (\<lambda>_. 1)"
+ by (intro lmeasure_integral measurable_linear_image assms) auto
+ also have "\<dots> = integral (f ` A) (\<lambda>_. 1 :: real ^ 1) $ 0"
+ by (subst integral_component_eq_cart [symmetric]) (auto intro: integrable_on_const)
+ also have "\<dots> = \<bar>det (matrix f)\<bar> * integral A (\<lambda>x. 1 :: real ^ 1) $ 0"
+ using assms
+ by (subst integral_change_of_variables_linear)
+ (auto simp: o_def absolutely_integrable_on_def intro: integrable_on_const)
+ also have "integral A (\<lambda>x. 1 :: real ^ 1) $ 0 = integral A (\<lambda>x. 1)"
+ by (subst integral_component_eq_cart [symmetric]) (auto intro: integrable_on_const)
+ also have "\<dots> = measure lebesgue A"
+ by (intro lmeasure_integral [symmetric]) auto
+ finally show ?thesis .
+qed
+
+theorem content_simplex:
+ fixes X :: "(real ^ 'n :: {finite, wellorder}) set" and f :: "'n :: _ \<Rightarrow> real ^ ('n :: _)"
+ assumes "finite X" "card X = Suc CARD('n)" and x0: "x0 \<in> X" and bij: "bij_betw f UNIV (X - {x0})"
+ defines "M \<equiv> (\<chi> i. \<chi> j. f j $ i - x0 $ i)"
+ shows "content (convex hull X) = \<bar>det M\<bar> / fact (CARD('n))"
+proof -
+ define g where "g = (\<lambda>x. M *v x)"
+ have [simp]: "M *v axis i 1 = f i - x0" for i :: 'n
+ by (simp add: M_def matrix_vector_mult_basis column_def vec_eq_iff)
+ define std where "std = (convex hull insert 0 Basis :: (real ^ 'n :: _) set)"
+ have compact: "compact std" unfolding std_def
+ by (intro finite_imp_compact_convex_hull) auto
+
+ have "measure lebesgue (convex hull X) = measure lebesgue (((+) (-x0)) ` (convex hull X))"
+ by (rule measure_translation [symmetric])
+ also have "((+) (-x0)) ` (convex hull X) = convex hull (((+) (-x0)) ` X)"
+ by (rule convex_hull_translation [symmetric])
+ also have "((+) (-x0)) ` X = insert 0 ((\<lambda>x. x - x0) ` (X - {x0}))"
+ using x0 by (auto simp: image_iff)
+ finally have eq: "measure lebesgue (convex hull X) = measure lebesgue (convex hull \<dots>)" .
+
+ from compact have "measure lebesgue (g ` std) = \<bar>det M\<bar> * measure lebesgue std"
+ by (subst measure_lebesgue_linear_transformation)
+ (auto intro: finite_imp_bounded_convex_hull dest: compact_imp_closed simp: g_def std_def)
+ also have "measure lebesgue std = content std" using compact
+ by (intro measure_completion) (auto dest: compact_imp_closed)
+ also have "content std = 1 / fact CARD('n)" unfolding std_def
+ by (simp add: content_std_simplex)
+ also have "g ` std = convex hull (g ` insert 0 Basis)" unfolding std_def
+ by (rule convex_hull_linear_image) (auto simp: g_def)
+ also have "g ` insert 0 Basis = insert 0 (g ` Basis)"
+ by (auto simp: g_def)
+ also have "g ` Basis = (\<lambda>x. x - x0) ` range f"
+ by (auto simp: g_def Basis_vec_def image_iff)
+ also have "range f = X - {x0}" using bij
+ using bij_betw_imp_surj_on by blast
+ also note eq [symmetric]
+ finally show ?thesis
+ using finite_imp_compact_convex_hull[OF \<open>finite X\<close>] by (auto dest: compact_imp_closed)
+qed
+
+theorem content_triangle:
+ fixes A B C :: "real ^ 2"
+ shows "content (convex hull {A, B, C}) =
+ \<bar>(C $ 1 - A $ 1) * (B $ 2 - A $ 2) - (B $ 1 - A $ 1) * (C $ 2 - A $ 2)\<bar> / 2"
+proof -
+ define M :: "real ^ 2 ^ 2" where "M \<equiv> (\<chi> i. \<chi> j. (if j = 1 then B else C) $ i - A $ i)"
+ define g where "g = (\<lambda>x. M *v x)"
+ define std where "std = (convex hull insert 0 Basis :: (real ^ 2) set)"
+ have [simp]: "M *v axis i 1 = (if i = 1 then B - A else C - A)" for i
+ by (auto simp: M_def matrix_vector_mult_basis column_def vec_eq_iff)
+ have compact: "compact std" unfolding std_def
+ by (intro finite_imp_compact_convex_hull) auto
+
+ have "measure lebesgue (convex hull {A, B, C}) =
+ measure lebesgue (((+) (-A)) ` (convex hull {A, B, C}))"
+ by (rule measure_translation [symmetric])
+ also have "((+) (-A)) ` (convex hull {A, B, C}) = convex hull (((+) (-A)) ` {A, B, C})"
+ by (rule convex_hull_translation [symmetric])
+ also have "((+) (-A)) ` {A, B, C} = {0, B - A, C - A}"
+ by (auto simp: image_iff)
+ finally have eq: "measure lebesgue (convex hull {A, B, C}) =
+ measure lebesgue (convex hull {0, B - A, C - A})" .
+
+ from compact have "measure lebesgue (g ` std) = \<bar>det M\<bar> * measure lebesgue std"
+ by (subst measure_lebesgue_linear_transformation)
+ (auto intro: finite_imp_bounded_convex_hull dest: compact_imp_closed simp: g_def std_def)
+ also have "measure lebesgue std = content std" using compact
+ by (intro measure_completion) (auto dest: compact_imp_closed)
+ also have "content std = 1 / 2" unfolding std_def
+ by (simp add: content_std_simplex)
+ also have "g ` std = convex hull (g ` insert 0 Basis)" unfolding std_def
+ by (rule convex_hull_linear_image) (auto simp: g_def)
+ also have "g ` insert 0 Basis = insert 0 (g ` Basis)"
+ by (auto simp: g_def)
+ also have "(2 :: 2) \<noteq> 1" by auto
+ hence "\<not>(\<forall>y::2. y = 1)" by blast
+ hence "g ` Basis = {B - A, C - A}"
+ by (auto simp: g_def Basis_vec_def image_iff)
+ also note eq [symmetric]
+ finally show ?thesis
+ using finite_imp_compact_convex_hull[of "{A, B, C}"]
+ by (auto dest!: compact_imp_closed simp: det_2 M_def)
+qed
+
+theorem heron:
+ fixes A B C :: "real ^ 2"
+ defines "a \<equiv> dist B C" and "b \<equiv> dist A C" and "c \<equiv> dist A B"
+ defines "s \<equiv> (a + b + c) / 2"
+ shows "content (convex hull {A, B, C}) = sqrt (s * (s - a) * (s - b) * (s - c))"
+proof -
+ have [simp]: "(UNIV :: 2 set) = {1, 2}"
+ using exhaust_2 by auto
+ have dist_eq: "dist (A :: real ^ 2) B ^ 2 = (A $ 1 - B $ 1) ^ 2 + (A $ 2 - B $ 2) ^ 2"
+ for A B by (simp add: dist_vec_def dist_real_def)
+ have nonneg: "s * (s - a) * (s - b) * (s - c) \<ge> 0"
+ using dist_triangle[of A B C] dist_triangle[of A C B] dist_triangle[of B C A]
+ by (intro mult_nonneg_nonneg) (auto simp: s_def a_def b_def c_def dist_commute)
+
+ have "16 * content (convex hull {A, B, C}) ^ 2 =
+ 4 * ((C $ 1 - A $ 1) * (B $ 2 - A $ 2) - (B $ 1 - A $ 1) * (C $ 2 - A $ 2)) ^ 2"
+ by (subst content_triangle) (simp add: power_divide)
+ also have "\<dots> = (2 * (dist A B ^ 2 * dist A C ^ 2 + dist A B ^ 2 * dist B C ^ 2 +
+ dist A C ^ 2 * dist B C ^ 2) - (dist A B ^ 2) ^ 2 - (dist A C ^ 2) ^ 2 - (dist B C ^ 2) ^ 2)"
+ unfolding dist_eq unfolding power2_eq_square by algebra
+ also have "\<dots> = (a + b + c) * ((a + b + c) - 2 * a) * ((a + b + c) - 2 * b) *
+ ((a + b + c) - 2 * c)"
+ unfolding power2_eq_square by (simp add: s_def a_def b_def c_def algebra_simps)
+ also have "\<dots> = 16 * s * (s - a) * (s - b) * (s - c)"
+ by (simp add: s_def divide_simps mult_ac)
+ finally have "content (convex hull {A, B, C}) ^ 2 = s * (s - a) * (s - b) * (s - c)"
+ by simp
+ also have "\<dots> = sqrt (s * (s - a) * (s - b) * (s - c)) ^ 2"
+ by (intro real_sqrt_pow2 [symmetric] nonneg)
+ finally show ?thesis using nonneg
+ by (subst (asm) power2_eq_iff_nonneg) auto
+qed
+
+end