author eberlm Thu Oct 29 15:40:52 2015 +0100 (2015-10-29) changeset 61524 f2e51e704a96 parent 61523 9ad1fccbba96 child 61525 87244a9cfe40 child 61526 c04295685936 child 61531 ab2e862263e7
 src/HOL/Groups_Big.thy file | annotate | diff | revisions src/HOL/Int.thy file | annotate | diff | revisions src/HOL/Limits.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Complex_Transcendental.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Derivative.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Integration.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy file | annotate | diff | revisions src/HOL/Real_Vector_Spaces.thy file | annotate | diff | revisions src/HOL/Set_Interval.thy file | annotate | diff | revisions src/HOL/Transcendental.thy file | annotate | diff | revisions
```     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
```
```     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.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.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)"
```
```     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.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"
```