added many small lemmas about setsum/setprod/powr/...
authoreberlm
Thu Oct 29 15:40:52 2015 +0100 (2015-10-29)
changeset 61524f2e51e704a96
parent 61523 9ad1fccbba96
child 61525 87244a9cfe40
child 61526 c04295685936
child 61531 ab2e862263e7
added many small lemmas about setsum/setprod/powr/...
src/HOL/Groups_Big.thy
src/HOL/Int.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Set_Interval.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Groups_Big.thy	Tue Oct 27 23:18:32 2015 +0100
     1.2 +++ b/src/HOL/Groups_Big.thy	Thu Oct 29 15:40:52 2015 +0100
     1.3 @@ -930,6 +930,14 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 +lemma setsum_cong_Suc:
     1.8 +  assumes "0 \<notin> A" "\<And>x. Suc x \<in> A \<Longrightarrow> f (Suc x) = g (Suc x)"
     1.9 +  shows   "setsum f A = setsum g A"
    1.10 +proof (rule setsum.cong)
    1.11 +  fix x assume "x \<in> A"
    1.12 +  with assms(1) show "f x = g x" by (cases x) (auto intro!: assms(2))
    1.13 +qed simp_all
    1.14 +
    1.15  
    1.16  subsubsection \<open>Cardinality as special case of @{const setsum}\<close>
    1.17  
     2.1 --- a/src/HOL/Int.thy	Tue Oct 27 23:18:32 2015 +0100
     2.2 +++ b/src/HOL/Int.thy	Thu Oct 29 15:40:52 2015 +0100
     2.3 @@ -724,8 +724,36 @@
     2.4    "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
     2.5    by (rule Ints_cases) auto
     2.6  
     2.7 +lemma Nats_subset_Ints: "\<nat> \<subseteq> \<int>"
     2.8 +  unfolding Nats_def Ints_def
     2.9 +  by (rule subsetI, elim imageE, hypsubst, subst of_int_of_nat_eq[symmetric], rule imageI) simp_all
    2.10 +
    2.11 +lemma Nats_altdef1: "\<nat> = {of_int n |n. n \<ge> 0}"
    2.12 +proof (intro subsetI equalityI)
    2.13 +  fix x :: 'a assume "x \<in> {of_int n |n. n \<ge> 0}"
    2.14 +  then obtain n where "x = of_int n" "n \<ge> 0" by (auto elim!: Ints_cases)
    2.15 +  hence "x = of_nat (nat n)" by (subst of_nat_nat) simp_all
    2.16 +  thus "x \<in> \<nat>" by simp
    2.17 +next
    2.18 +  fix x :: 'a assume "x \<in> \<nat>"
    2.19 +  then obtain n where "x = of_nat n" by (auto elim!: Nats_cases)
    2.20 +  hence "x = of_int (int n)" by simp
    2.21 +  also have "int n \<ge> 0" by simp
    2.22 +  hence "of_int (int n) \<in> {of_int n |n. n \<ge> 0}" by blast
    2.23 +  finally show "x \<in> {of_int n |n. n \<ge> 0}" .
    2.24 +qed
    2.25 +
    2.26  end
    2.27  
    2.28 +lemma (in linordered_idom) Nats_altdef2: "\<nat> = {n \<in> \<int>. n \<ge> 0}"
    2.29 +proof (intro subsetI equalityI)
    2.30 +  fix x :: 'a assume "x \<in> {n \<in> \<int>. n \<ge> 0}"
    2.31 +  then obtain n where "x = of_int n" "n \<ge> 0" by (auto elim!: Ints_cases)
    2.32 +  hence "x = of_nat (nat n)" by (subst of_nat_nat) simp_all
    2.33 +  thus "x \<in> \<nat>" by simp
    2.34 +qed (auto elim!: Nats_cases)
    2.35 +
    2.36 +
    2.37  text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close>
    2.38  
    2.39  lemma Ints_double_eq_0_iff:
     3.1 --- a/src/HOL/Limits.thy	Tue Oct 27 23:18:32 2015 +0100
     3.2 +++ b/src/HOL/Limits.thy	Thu Oct 29 15:40:52 2015 +0100
     3.3 @@ -1436,6 +1436,39 @@
     3.4    using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
     3.5    by auto
     3.6  
     3.7 +lemma lim_1_over_n: "((\<lambda>n. 1 / of_nat n) ---> (0::'a::real_normed_field)) sequentially"
     3.8 +proof (subst lim_sequentially, intro allI impI exI)
     3.9 +  fix e :: real assume e: "e > 0"
    3.10 +  fix n :: nat assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
    3.11 +  have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
    3.12 +  also note n
    3.13 +  finally show "dist (1 / of_nat n :: 'a) 0 < e" using e 
    3.14 +    by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
    3.15 +qed
    3.16 +
    3.17 +lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) ---> (0::'a::real_normed_field)) sequentially"
    3.18 +  using lim_1_over_n by (simp add: inverse_eq_divide)
    3.19 +
    3.20 +lemma LIMSEQ_Suc_n_over_n: "(\<lambda>n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) ----> 1"
    3.21 +proof (rule Lim_transform_eventually)
    3.22 +  show "eventually (\<lambda>n. 1 + inverse (of_nat n :: 'a) = of_nat (Suc n) / of_nat n) sequentially"
    3.23 +    using eventually_gt_at_top[of "0::nat"] by eventually_elim (simp add: field_simps)
    3.24 +  have "(\<lambda>n. 1 + inverse (of_nat n) :: 'a) ----> 1 + 0"
    3.25 +    by (intro tendsto_add tendsto_const lim_inverse_n)
    3.26 +  thus "(\<lambda>n. 1 + inverse (of_nat n) :: 'a) ----> 1" by simp
    3.27 +qed
    3.28 +
    3.29 +lemma LIMSEQ_n_over_Suc_n: "(\<lambda>n. of_nat n / of_nat (Suc n) :: 'a :: real_normed_field) ----> 1"
    3.30 +proof (rule Lim_transform_eventually)
    3.31 +  show "eventually (\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a) = 
    3.32 +                        of_nat n / of_nat (Suc n)) sequentially"
    3.33 +    using eventually_gt_at_top[of "0::nat"] 
    3.34 +    by eventually_elim (simp add: field_simps del: of_nat_Suc)
    3.35 +  have "(\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a)) ----> inverse 1"
    3.36 +    by (intro tendsto_inverse LIMSEQ_Suc_n_over_n) simp_all
    3.37 +  thus "(\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a)) ----> 1" by simp
    3.38 +qed
    3.39 +
    3.40  subsection \<open>Convergence on sequences\<close>
    3.41  
    3.42  lemma convergent_add:
     4.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Oct 27 23:18:32 2015 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Oct 29 15:40:52 2015 +0100
     4.3 @@ -977,7 +977,6 @@
     4.4    apply (auto simp: exp_of_nat_mult [symmetric])
     4.5    done
     4.6  
     4.7 -
     4.8  subsection\<open>The Unwinding Number and the Ln-product Formula\<close>
     4.9  
    4.10  text\<open>Note that in this special case the unwinding number is -1, 0 or 1.\<close>
    4.11 @@ -1262,6 +1261,21 @@
    4.12          Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
    4.13    by (auto simp: of_real_numeral Ln_times)
    4.14  
    4.15 +lemma Ln_of_nat: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
    4.16 +  by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all
    4.17 +
    4.18 +lemma Ln_of_nat_over_of_nat: 
    4.19 +  assumes "m > 0" "n > 0"
    4.20 +  shows   "Ln (of_nat m / of_nat n) = of_real (ln (of_nat m) - ln (of_nat n))"
    4.21 +proof -
    4.22 +  have "of_nat m / of_nat n = (of_real (of_nat m / of_nat n) :: complex)" by simp
    4.23 +  also from assms have "Ln ... = of_real (ln (of_nat m / of_nat n))"
    4.24 +    by (simp add: Ln_of_real[symmetric])
    4.25 +  also from assms have "... = of_real (ln (of_nat m) - ln (of_nat n))"
    4.26 +    by (simp add: ln_div)
    4.27 +  finally show ?thesis .
    4.28 +qed
    4.29 +
    4.30  
    4.31  subsection\<open>Relation between Ln and Arg, and hence continuity of Arg\<close>
    4.32  
    4.33 @@ -1445,6 +1459,15 @@
    4.34    using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
    4.35    by auto
    4.36  
    4.37 +lemma cnj_powr:
    4.38 +  assumes "Im a = 0 \<Longrightarrow> Re a \<ge> 0"
    4.39 +  shows   "cnj (a powr b) = cnj a powr cnj b"
    4.40 +proof (cases "a = 0")
    4.41 +  case False
    4.42 +  with assms have "Im a = 0 \<Longrightarrow> Re a > 0" by (auto simp: complex_eq_iff)
    4.43 +  with False show ?thesis by (simp add: powr_def exp_cnj cnj_Ln)
    4.44 +qed simp
    4.45 +
    4.46  lemma powr_real_real:
    4.47      "\<lbrakk>w \<in> \<real>; z \<in> \<real>; 0 < Re w\<rbrakk> \<Longrightarrow> w powr z = exp(Re z * ln(Re w))"
    4.48    apply (simp add: powr_def)
    4.49 @@ -1466,6 +1489,19 @@
    4.50             \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
    4.51    by (auto simp: Reals_def powr_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
    4.52  
    4.53 +lemma powr_neg_real_complex:
    4.54 +  shows   "(- of_real x) powr a = (-1) powr (of_real (sgn x) * a) * of_real x powr (a :: complex)"
    4.55 +proof (cases "x = 0")
    4.56 +  assume x: "x \<noteq> 0"
    4.57 +  hence "(-x) powr a = exp (a * ln (-of_real x))" by (simp add: powr_def)
    4.58 +  also from x have "ln (-of_real x) = Ln (of_real x) + of_real (sgn x) * pi * \<i>"
    4.59 +    by (simp add: Ln_minus Ln_of_real)
    4.60 +  also from x assms have "exp (a * ...) = cis pi powr (of_real (sgn x) * a) * of_real x powr a"
    4.61 +    by (simp add: powr_def exp_add algebra_simps Ln_of_real cis_conv_exp)
    4.62 +  also note cis_pi
    4.63 +  finally show ?thesis by simp
    4.64 +qed simp_all
    4.65 +
    4.66  lemma has_field_derivative_powr:
    4.67      "(Im z = 0 \<Longrightarrow> 0 < Re z)
    4.68       \<Longrightarrow> ((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
    4.69 @@ -1477,6 +1513,25 @@
    4.70    apply (simp add: field_simps exp_diff)
    4.71    done
    4.72  
    4.73 +lemma has_field_derivative_powr_complex':
    4.74 +  assumes "Im z \<noteq> 0 \<or> Re z > 0"
    4.75 +  shows "((\<lambda>z. z powr r :: complex) has_field_derivative r * z powr (r - 1)) (at z)"
    4.76 +proof (subst DERIV_cong_ev[OF refl _ refl])
    4.77 +  from assms have "eventually (\<lambda>z. z \<noteq> 0) (nhds z)" by (intro t1_space_nhds) auto
    4.78 +  thus "eventually (\<lambda>z. z powr r = Exp (r * Ln z)) (nhds z)"
    4.79 +    unfolding powr_def by eventually_elim simp
    4.80 +
    4.81 +  have "((\<lambda>z. Exp (r * Ln z)) has_field_derivative Exp (r * Ln z) * (inverse z * r)) (at z)" 
    4.82 +    using assms by (auto intro!: derivative_eq_intros has_field_derivative_powr)
    4.83 +  also have "Exp (r * Ln z) * (inverse z * r) = r * z powr (r - 1)"
    4.84 +    unfolding powr_def by (simp add: assms exp_diff field_simps)
    4.85 +  finally show "((\<lambda>z. Exp (r * Ln z)) has_field_derivative r * z powr (r - 1)) (at z)" 
    4.86 +    by simp
    4.87 +qed
    4.88 +
    4.89 +declare has_field_derivative_powr_complex'[THEN DERIV_chain2, derivative_intros]
    4.90 +
    4.91 +
    4.92  lemma has_field_derivative_powr_right:
    4.93      "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
    4.94    apply (simp add: powr_def)
     5.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Oct 27 23:18:32 2015 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Oct 29 15:40:52 2015 +0100
     5.3 @@ -1135,6 +1135,15 @@
     5.4      by metis
     5.5  qed
     5.6  
     5.7 +lemma has_field_derivative_zero_constant:
     5.8 +  assumes "convex s" "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative 0) (at x within s)"
     5.9 +  shows   "\<exists>c. \<forall>x\<in>s. f (x) = (c :: 'a :: real_normed_field)"
    5.10 +proof (rule has_derivative_zero_constant)
    5.11 +  have A: "op * 0 = (\<lambda>_. 0 :: 'a)" by (intro ext) simp
    5.12 +  fix x assume "x \<in> s" thus "(f has_derivative (\<lambda>h. 0)) (at x within s)"
    5.13 +    using assms(2)[of x] by (simp add: has_field_derivative_def A)
    5.14 +qed fact
    5.15 +
    5.16  lemma has_derivative_zero_unique:
    5.17    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
    5.18    assumes "convex s"
     6.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Oct 27 23:18:32 2015 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Oct 29 15:40:52 2015 +0100
     6.3 @@ -6019,12 +6019,6 @@
     6.4  
     6.5  subsection \<open>Taylor series expansion\<close>
     6.6  
     6.7 -lemma
     6.8 -  setsum_telescope:
     6.9 -  fixes f::"nat \<Rightarrow> 'a::ab_group_add"
    6.10 -  shows "setsum (\<lambda>i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)"
    6.11 -  by (induct i) simp_all
    6.12 -
    6.13  lemma (in bounded_bilinear) setsum_prod_derivatives_has_vector_derivative:
    6.14    assumes "p>0"
    6.15    and f0: "Df 0 = f"
     7.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Oct 27 23:18:32 2015 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Oct 29 15:40:52 2015 +0100
     7.3 @@ -1506,6 +1506,18 @@
     7.4      by (metis islimpt_approachable closed_limpt [where 'a='a])
     7.5  qed
     7.6  
     7.7 +lemma closed_of_nat_image: "closed (of_nat ` A :: 'a :: real_normed_algebra_1 set)"
     7.8 +  by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_nat)
     7.9 +
    7.10 +lemma closed_of_int_image: "closed (of_int ` A :: 'a :: real_normed_algebra_1 set)"
    7.11 +  by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_int)
    7.12 +
    7.13 +lemma closed_Nats [simp]: "closed (\<nat> :: 'a :: real_normed_algebra_1 set)"
    7.14 +  unfolding Nats_def by (rule closed_of_nat_image)
    7.15 +
    7.16 +lemma closed_Ints [simp]: "closed (\<int> :: 'a :: real_normed_algebra_1 set)"
    7.17 +  unfolding Ints_def by (rule closed_of_int_image)
    7.18 +
    7.19  
    7.20  subsection \<open>Interior of a Set\<close>
    7.21  
     8.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Oct 27 23:18:32 2015 +0100
     8.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Thu Oct 29 15:40:52 2015 +0100
     8.3 @@ -735,6 +735,9 @@
     8.4    thus ?thesis by simp
     8.5  qed
     8.6  
     8.7 +lemma norm_uminus_minus: "norm (-x - y :: 'a :: real_normed_vector) = norm (x + y)"
     8.8 +  by (subst (2) norm_minus_cancel[symmetric], subst minus_add_distrib) simp
     8.9 +
    8.10  lemma norm_triangle_ineq2:
    8.11    fixes a b :: "'a::real_normed_vector"
    8.12    shows "norm a - norm b \<le> norm (a - b)"
    8.13 @@ -1281,6 +1284,18 @@
    8.14  lemma dist_diff [simp]: "dist a (a - b) = norm b"  "dist (a - b) a = norm b"
    8.15    by (simp_all add: dist_norm)
    8.16    
    8.17 +lemma dist_of_int: "dist (of_int m) (of_int n :: 'a :: real_normed_algebra_1) = of_int \<bar>m - n\<bar>"
    8.18 +proof -
    8.19 +  have "dist (of_int m) (of_int n :: 'a) = dist (of_int m :: 'a) (of_int m - (of_int (m - n)))"
    8.20 +    by simp
    8.21 +  also have "\<dots> = of_int \<bar>m - n\<bar>" by (subst dist_diff, subst norm_of_int) simp
    8.22 +  finally show ?thesis .
    8.23 +qed
    8.24 +
    8.25 +lemma dist_of_nat: 
    8.26 +  "dist (of_nat m) (of_nat n :: 'a :: real_normed_algebra_1) = of_int \<bar>int m - int n\<bar>"
    8.27 +  by (subst (1 2) of_int_of_nat_eq [symmetric]) (rule dist_of_int)
    8.28 +  
    8.29  subsection \<open>Bounded Linear and Bilinear Operators\<close>
    8.30  
    8.31  locale linear = additive f for f :: "'a::real_vector \<Rightarrow> 'b::real_vector" +
     9.1 --- a/src/HOL/Set_Interval.thy	Tue Oct 27 23:18:32 2015 +0100
     9.2 +++ b/src/HOL/Set_Interval.thy	Thu Oct 29 15:40:52 2015 +0100
     9.3 @@ -409,6 +409,11 @@
     9.4    "{a .. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)"
     9.5    using dense[of "max a d" "b"]
     9.6    by (force simp: subset_eq Ball_def not_less[symmetric])
     9.7 +  
     9.8 +lemma greaterThanLessThan_subseteq_greaterThanLessThan:
     9.9 +  "{a <..< b} \<subseteq> {c <..< d} \<longleftrightarrow> (a < b \<longrightarrow> a \<ge> c \<and> b \<le> d)"
    9.10 +  using dense[of "a" "min c b"] dense[of "max a d" "b"]
    9.11 +  by (force simp: subset_eq Ball_def not_less[symmetric])
    9.12  
    9.13  lemma greaterThanAtMost_subseteq_atLeastLessThan_iff:
    9.14    "{a <.. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b < d)"
    9.15 @@ -1648,6 +1653,18 @@
    9.16    by auto
    9.17  
    9.18  
    9.19 +subsection \<open>Telescoping\<close>
    9.20 +
    9.21 +lemma setsum_telescope:
    9.22 +  fixes f::"nat \<Rightarrow> 'a::ab_group_add"
    9.23 +  shows "setsum (\<lambda>i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)"
    9.24 +  by (induct i) simp_all
    9.25 +
    9.26 +lemma setsum_telescope'':
    9.27 +  assumes "m \<le> n"
    9.28 +  shows   "(\<Sum>k\<in>{Suc m..n}. f k - f (k - 1)) = f n - (f m :: 'a :: ab_group_add)"
    9.29 +  by (rule dec_induct[OF assms]) (simp_all add: algebra_simps)
    9.30 +
    9.31  subsection \<open>The formula for geometric sums\<close>
    9.32  
    9.33  lemma geometric_sum:
    9.34 @@ -1845,4 +1862,38 @@
    9.35      by auto
    9.36  qed
    9.37  
    9.38 +
    9.39 +subsection \<open>Shifting bounds\<close>
    9.40 +
    9.41 +lemma setprod_shift_bounds_nat_ivl:
    9.42 +  "setprod f {m+k..<n+k} = setprod (%i. f(i + k)){m..<n::nat}"
    9.43 +by (induct "n", auto simp:atLeastLessThanSuc)
    9.44 +
    9.45 +lemma setprod_shift_bounds_cl_nat_ivl:
    9.46 +  "setprod f {m+k..n+k} = setprod (%i. f(i + k)){m..n::nat}"
    9.47 +  by (rule setprod.reindex_bij_witness[where i="\<lambda>i. i + k" and j="\<lambda>i. i - k"]) auto
    9.48 +
    9.49 +corollary setprod_shift_bounds_cl_Suc_ivl:
    9.50 +  "setprod f {Suc m..Suc n} = setprod (%i. f(Suc i)){m..n}"
    9.51 +by (simp add:setprod_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
    9.52 +
    9.53 +corollary setprod_shift_bounds_Suc_ivl:
    9.54 +  "setprod f {Suc m..<Suc n} = setprod (%i. f(Suc i)){m..<n}"
    9.55 +by (simp add:setprod_shift_bounds_nat_ivl[where k="Suc 0", simplified])
    9.56 +
    9.57 +lemma setprod_lessThan_Suc: "setprod f {..<Suc n} = setprod f {..<n} * f n"
    9.58 +  by (simp add: lessThan_Suc mult.commute)
    9.59 +
    9.60 +lemma setprod_atLeastLessThan_Suc: "a \<le> b \<Longrightarrow> setprod f {a..<Suc b} = setprod f {a..<b} * f b"
    9.61 +  by (simp add: atLeastLessThanSuc mult.commute)
    9.62 +
    9.63 +lemma setprod_nat_ivl_Suc':
    9.64 +  assumes "m \<le> Suc n"
    9.65 +  shows   "setprod f {m..Suc n} = f (Suc n) * setprod f {m..n}"
    9.66 +proof -
    9.67 +  from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto
    9.68 +  also have "setprod f \<dots> = f (Suc n) * setprod f {m..n}" by simp
    9.69 +  finally show ?thesis .
    9.70 +qed
    9.71 +
    9.72  end
    10.1 --- a/src/HOL/Transcendental.thy	Tue Oct 27 23:18:32 2015 +0100
    10.2 +++ b/src/HOL/Transcendental.thy	Thu Oct 29 15:40:52 2015 +0100
    10.3 @@ -25,6 +25,14 @@
    10.4  lemma real_fact_int [simp]: "real (fact n :: int) = fact n"
    10.5    by (metis of_int_of_nat_eq of_nat_fact real_of_int_def)
    10.6  
    10.7 +lemma norm_fact [simp]:
    10.8 +  "norm (fact n :: 'a :: {real_normed_algebra_1}) = fact n"
    10.9 +proof -
   10.10 +  have "(fact n :: 'a) = of_real (fact n)" by simp
   10.11 +  also have "norm \<dots> = fact n" by (subst norm_of_real) simp
   10.12 +  finally show ?thesis .
   10.13 +qed
   10.14 +
   10.15  lemma root_test_convergence:
   10.16    fixes f :: "nat \<Rightarrow> 'a::banach"
   10.17    assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
   10.18 @@ -2431,6 +2439,14 @@
   10.19    apply (metis dual_order.strict_iff_order powr_less_mono2)
   10.20    done
   10.21  
   10.22 +lemma powr_mono2':
   10.23 +  assumes "a \<le> 0" "x > 0" "x \<le> (y::real)"
   10.24 +  shows   "x powr a \<ge> y powr a"
   10.25 +proof -
   10.26 +  from assms have "x powr -a \<le> y powr -a" by (intro powr_mono2) simp_all
   10.27 +  with assms show ?thesis by (auto simp add: powr_minus field_simps)
   10.28 +qed
   10.29 +
   10.30  lemma powr_inj:
   10.31    fixes x::real shows "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
   10.32    unfolding powr_def exp_inj_iff by simp
   10.33 @@ -2542,6 +2558,19 @@
   10.34    using DERIV_powr[OF g pos DERIV_const, of r] pos
   10.35    by (simp add: powr_divide2[symmetric] field_simps)
   10.36  
   10.37 +lemma has_real_derivative_powr:
   10.38 +  assumes "z > 0"
   10.39 +  shows "((\<lambda>z. z powr r) has_real_derivative r * z powr (r - 1)) (at z)"
   10.40 +proof (subst DERIV_cong_ev[OF refl _ refl])
   10.41 +  from assms have "eventually (\<lambda>z. z \<noteq> 0) (nhds z)" by (intro t1_space_nhds) auto
   10.42 +  thus "eventually (\<lambda>z. z powr r = exp (r * ln z)) (nhds z)"
   10.43 +    unfolding powr_def by eventually_elim simp
   10.44 +  from assms show "((\<lambda>z. exp (r * ln z)) has_real_derivative r * z powr (r - 1)) (at z)"
   10.45 +    by (auto intro!: derivative_eq_intros simp: powr_def field_simps exp_diff)
   10.46 +qed
   10.47 +
   10.48 +declare has_real_derivative_powr[THEN DERIV_chain2, derivative_intros]
   10.49 +
   10.50  lemma tendsto_zero_powrI:
   10.51    assumes "(f ---> (0::real)) F" "(g ---> b) F" "\<forall>\<^sub>F x in F. 0 \<le> f x" "0 < b"
   10.52    shows "((\<lambda>x. f x powr g x) ---> 0) F"