more defer/prefer
authorpaulson <lp15@cam.ac.uk>
Sun Apr 29 14:46:11 2018 +0100 (12 months ago)
changeset 680552cab37094fc4
parent 68054 ebd179b82e20
child 68056 9e077a905209
more defer/prefer
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Derivative.thy
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat Apr 28 21:37:45 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Apr 29 14:46:11 2018 +0100
     1.3 @@ -837,15 +837,13 @@
     1.4      qed
     1.5    } note ** = this
     1.6    show ?thesis
     1.7 -  unfolding has_field_derivative_def
     1.8 +    unfolding has_field_derivative_def
     1.9    proof (rule has_derivative_sequence [OF cvs _ _ x])
    1.10 -    show "\<forall>n. \<forall>x\<in>s. (f n has_derivative (( * ) (f' n x))) (at x within s)"
    1.11 -      by (metis has_field_derivative_def df)
    1.12 -  next show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
    1.13 +  show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
    1.14      by (rule tf)
    1.15 -  next show "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
    1.16 +  next show "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
    1.17      by (blast intro: **)
    1.18 -  qed
    1.19 +  qed (metis has_field_derivative_def df)
    1.20  qed
    1.21  
    1.22  lemma has_complex_derivative_series:
    1.23 @@ -884,7 +882,7 @@
    1.24        by (metis df has_field_derivative_def mult_commute_abs)
    1.25    next show " ((\<lambda>n. f n x) sums l)"
    1.26      by (rule sf)
    1.27 -  next show "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
    1.28 +  next show "\<And>e. e>0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
    1.29      by (blast intro: **)
    1.30    qed
    1.31  qed
    1.32 @@ -896,7 +894,7 @@
    1.33    assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
    1.34    assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
    1.35    assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
    1.36 -  shows   "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)"
    1.37 +  shows  "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)"
    1.38  proof -
    1.39    from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
    1.40      unfolding uniformly_convergent_on_def by blast
    1.41 @@ -905,7 +903,6 @@
    1.42      by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within)
    1.43    then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
    1.44      "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
    1.45 -  from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
    1.46    from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)"
    1.47      by (simp add: has_field_derivative_def s)
    1.48    have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)"
    1.49 @@ -915,15 +912,6 @@
    1.50      by (auto simp: summable_def field_differentiable_def has_field_derivative_def)
    1.51  qed
    1.52  
    1.53 -lemma field_differentiable_series':
    1.54 -  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach} \<Rightarrow> 'a"
    1.55 -  assumes "convex s" "open s"
    1.56 -  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
    1.57 -  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
    1.58 -  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
    1.59 -  shows   "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x0)"
    1.60 -  using field_differentiable_series[OF assms, of x0] \<open>x0 \<in> s\<close> by blast+
    1.61 -
    1.62  subsection\<open>Bound theorem\<close>
    1.63  
    1.64  lemma field_differentiable_bound:
     2.1 --- a/src/HOL/Analysis/Derivative.thy	Sat Apr 28 21:37:45 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Derivative.thy	Sun Apr 29 14:46:11 2018 +0100
     2.3 @@ -1197,13 +1197,13 @@
     2.4  
     2.5  lemma has_derivative_inverse_basic:
     2.6    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     2.7 -  assumes "(f has_derivative f') (at (g y))"
     2.8 -    and "bounded_linear g'"
     2.9 +  assumes derf: "(f has_derivative f') (at (g y))"
    2.10 +    and ling': "bounded_linear g'"
    2.11      and "g' \<circ> f' = id"
    2.12 -    and "continuous (at y) g"
    2.13 -    and "open t"
    2.14 -    and "y \<in> t"
    2.15 -    and "\<forall>z\<in>t. f (g z) = z"
    2.16 +    and contg: "continuous (at y) g"
    2.17 +    and "open T"
    2.18 +    and "y \<in> T"
    2.19 +    and fg: "\<And>z. z \<in> T \<Longrightarrow> f (g z) = z"
    2.20    shows "(g has_derivative g') (at y)"
    2.21  proof -
    2.22    interpret f': bounded_linear f'
    2.23 @@ -1214,70 +1214,48 @@
    2.24      using bounded_linear.pos_bounded[OF assms(2)] by blast
    2.25    have lem1: "\<forall>e>0. \<exists>d>0. \<forall>z.
    2.26      norm (z - y) < d \<longrightarrow> norm (g z - g y - g'(z - y)) \<le> e * norm (g z - g y)"
    2.27 -  proof (rule, rule)
    2.28 +  proof (intro allI impI)
    2.29      fix e :: real
    2.30      assume "e > 0"
    2.31      with C(1) have *: "e / C > 0" by auto
    2.32 -    obtain d0 where d0:
    2.33 -        "0 < d0"
    2.34 -        "\<forall>ya. norm (ya - g y) < d0 \<longrightarrow> norm (f ya - f (g y) - f' (ya - g y)) \<le> e / C * norm (ya - g y)"
    2.35 -      using assms(1)
    2.36 -      unfolding has_derivative_at_alt
    2.37 -      using * by blast
    2.38 -    obtain d1 where d1:
    2.39 -        "0 < d1"
    2.40 -        "\<forall>x. 0 < dist x y \<and> dist x y < d1 \<longrightarrow> dist (g x) (g y) < d0"
    2.41 -      using assms(4)
    2.42 -      unfolding continuous_at Lim_at
    2.43 -      using d0(1) by blast
    2.44 -    obtain d2 where d2:
    2.45 -        "0 < d2"
    2.46 -        "\<forall>ya. dist ya y < d2 \<longrightarrow> ya \<in> t"
    2.47 -      using assms(5)
    2.48 -      unfolding open_dist
    2.49 -      using assms(6) by blast
    2.50 +    obtain d0 where  "0 < d0" and d0:
    2.51 +        "\<And>u. norm (u - g y) < d0 \<Longrightarrow> norm (f u - f (g y) - f' (u - g y)) \<le> e / C * norm (u - g y)"
    2.52 +      using derf * unfolding has_derivative_at_alt by blast
    2.53 +    obtain d1 where "0 < d1" and d1: "\<And>x. \<lbrakk>0 < dist x y; dist x y < d1\<rbrakk> \<Longrightarrow> dist (g x) (g y) < d0"
    2.54 +      using contg \<open>0 < d0\<close> unfolding continuous_at Lim_at by blast
    2.55 +    obtain d2 where "0 < d2" and d2: "\<And>u. dist u y < d2 \<Longrightarrow> u \<in> T"
    2.56 +      using \<open>open T\<close> \<open>y \<in> T\<close> unfolding open_dist by blast
    2.57      obtain d where d: "0 < d" "d < d1" "d < d2"
    2.58 -      using real_lbound_gt_zero[OF d1(1) d2(1)] by blast
    2.59 -    then show "\<exists>d>0. \<forall>z. norm (z - y) < d \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e * norm (g z - g y)"
    2.60 -      apply (rule_tac x=d in exI)
    2.61 -      apply rule
    2.62 -      defer
    2.63 -      apply rule
    2.64 -      apply rule
    2.65 -    proof -
    2.66 +      using real_lbound_gt_zero[OF \<open>0 < d1\<close> \<open>0 < d2\<close>] by blast
    2.67 +    show "\<exists>d>0. \<forall>z. norm (z - y) < d \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e * norm (g z - g y)"
    2.68 +    proof (intro exI allI impI conjI)
    2.69        fix z
    2.70        assume as: "norm (z - y) < d"
    2.71 -      then have "z \<in> t"
    2.72 +      then have "z \<in> T"
    2.73          using d2 d unfolding dist_norm by auto
    2.74        have "norm (g z - g y - g' (z - y)) \<le> norm (g' (f (g z) - y - f' (g z - g y)))"
    2.75          unfolding g'.diff f'.diff
    2.76 -        unfolding assms(3)[unfolded o_def id_def, THEN fun_cong]
    2.77 -        unfolding assms(7)[rule_format,OF \<open>z\<in>t\<close>]
    2.78 -        apply (subst norm_minus_cancel[symmetric])
    2.79 -        apply auto
    2.80 -        done
    2.81 +        unfolding assms(3)[unfolded o_def id_def, THEN fun_cong] fg[OF \<open>z\<in>T\<close>]
    2.82 +        by (simp add: norm_minus_commute)
    2.83        also have "\<dots> \<le> norm (f (g z) - y - f' (g z - g y)) * C"
    2.84          by (rule C(2))
    2.85        also have "\<dots> \<le> (e / C) * norm (g z - g y) * C"
    2.86 -        apply (rule mult_right_mono)
    2.87 -        apply (rule d0(2)[rule_format,unfolded assms(7)[rule_format,OF \<open>y\<in>t\<close>]])
    2.88 -        apply (cases "z = y")
    2.89 -        defer
    2.90 -        apply (rule d1(2)[unfolded dist_norm,rule_format])
    2.91 -        using as d C d0
    2.92 -        apply auto
    2.93 -        done
    2.94 +      proof -
    2.95 +        have "norm (g z - g y) < d0"
    2.96 +          by (metis as cancel_comm_monoid_add_class.diff_cancel d(2) \<open>0 < d0\<close> d1 diff_gt_0_iff_gt diff_strict_mono dist_norm dist_self zero_less_dist_iff)
    2.97 +        then show ?thesis
    2.98 +          by (metis C(1) \<open>y \<in> T\<close> d0 fg real_mult_le_cancel_iff1)
    2.99 +      qed
   2.100        also have "\<dots> \<le> e * norm (g z - g y)"
   2.101          using C by (auto simp add: field_simps)
   2.102        finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (g z - g y)"
   2.103          by simp
   2.104 -    qed auto
   2.105 +    qed (use d in auto)
   2.106    qed
   2.107    have *: "(0::real) < 1 / 2"
   2.108      by auto
   2.109 -  obtain d where d:
   2.110 -      "0 < d"
   2.111 -      "\<forall>z. norm (z - y) < d \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> 1 / 2 * norm (g z - g y)"
   2.112 +  obtain d where "0 < d" and d:
   2.113 +      "\<And>z. norm (z - y) < d \<Longrightarrow> norm (g z - g y - g' (z - y)) \<le> 1/2 * norm (g z - g y)"
   2.114      using lem1 * by blast
   2.115    define B where "B = C * 2"
   2.116    have "B > 0"
   2.117 @@ -1287,51 +1265,37 @@
   2.118      have "norm (g z - g y) \<le> norm(g' (z - y)) + norm ((g z - g y) - g'(z - y))"
   2.119        by (rule norm_triangle_sub)
   2.120      also have "\<dots> \<le> norm (g' (z - y)) + 1 / 2 * norm (g z - g y)"
   2.121 -      apply (rule add_left_mono)
   2.122 -      using d and z
   2.123 -      apply auto
   2.124 -      done
   2.125 +      by (rule add_left_mono) (use d z in auto)
   2.126      also have "\<dots> \<le> norm (z - y) * C + 1 / 2 * norm (g z - g y)"
   2.127 -      apply (rule add_right_mono)
   2.128 -      using C
   2.129 -      apply auto
   2.130 -      done
   2.131 +      by (rule add_right_mono) (use C in auto)
   2.132      finally show "norm (g z - g y) \<le> B * norm (z - y)"
   2.133        unfolding B_def
   2.134        by (auto simp add: field_simps)
   2.135    qed
   2.136    show ?thesis
   2.137      unfolding has_derivative_at_alt
   2.138 -    apply rule
   2.139 -    apply (rule assms)
   2.140 -    apply rule
   2.141 -    apply rule
   2.142 -  proof -
   2.143 +  proof (intro conjI assms allI impI)
   2.144      fix e :: real
   2.145      assume "e > 0"
   2.146      then have *: "e / B > 0" by (metis \<open>B > 0\<close> divide_pos_pos)
   2.147 -    obtain d' where d':
   2.148 -        "0 < d'"
   2.149 -        "\<forall>z. norm (z - y) < d' \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e / B * norm (g z - g y)"
   2.150 +    obtain d' where "0 < d'" and d':
   2.151 +        "\<And>z. norm (z - y) < d' \<Longrightarrow> norm (g z - g y - g' (z - y)) \<le> e / B * norm (g z - g y)"
   2.152        using lem1 * by blast
   2.153      obtain k where k: "0 < k" "k < d" "k < d'"
   2.154 -      using real_lbound_gt_zero[OF d(1) d'(1)] by blast
   2.155 +      using real_lbound_gt_zero[OF \<open>0 < d\<close> \<open>0 < d'\<close>] by blast
   2.156      show "\<exists>d>0. \<forall>ya. norm (ya - y) < d \<longrightarrow> norm (g ya - g y - g' (ya - y)) \<le> e * norm (ya - y)"
   2.157 -      apply (rule_tac x=k in exI)
   2.158 -      apply auto
   2.159 -    proof -
   2.160 +    proof (intro exI allI impI conjI)
   2.161        fix z
   2.162        assume as: "norm (z - y) < k"
   2.163        then have "norm (g z - g y - g' (z - y)) \<le> e / B * norm(g z - g y)"
   2.164          using d' k by auto
   2.165        also have "\<dots> \<le> e * norm (z - y)"
   2.166          unfolding times_divide_eq_left pos_divide_le_eq[OF \<open>B>0\<close>]
   2.167 -        using lem2[of z]
   2.168 -        using k as using \<open>e > 0\<close>
   2.169 +        using lem2[of z] k as \<open>e > 0\<close>
   2.170          by (auto simp add: field_simps)
   2.171        finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (z - y)"
   2.172          by simp
   2.173 -    qed(insert k, auto)
   2.174 +    qed (use k in auto)
   2.175    qed
   2.176  qed
   2.177  
   2.178 @@ -1344,25 +1308,22 @@
   2.179      and "g' \<circ> f' = id"
   2.180      and "continuous (at (f x)) g"
   2.181      and "g (f x) = x"
   2.182 -    and "open t"
   2.183 -    and "f x \<in> t"
   2.184 -    and "\<forall>y\<in>t. f (g y) = y"
   2.185 +    and "open T"
   2.186 +    and "f x \<in> T"
   2.187 +    and "\<And>y. y \<in> T \<Longrightarrow> f (g y) = y"
   2.188    shows "(g has_derivative g') (at (f x))"
   2.189 -  apply (rule has_derivative_inverse_basic)
   2.190 -  using assms
   2.191 -  apply auto
   2.192 -  done
   2.193 +  by (rule has_derivative_inverse_basic) (use assms in auto)
   2.194  
   2.195  text \<open>This is the version in Dieudonne', assuming continuity of f and g.\<close>
   2.196  
   2.197  lemma has_derivative_inverse_dieudonne:
   2.198    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   2.199 -  assumes "open s"
   2.200 -    and "open (f ` s)"
   2.201 -    and "continuous_on s f"
   2.202 -    and "continuous_on (f ` s) g"
   2.203 -    and "\<forall>x\<in>s. g (f x) = x"
   2.204 -    and "x \<in> s"
   2.205 +  assumes "open S"
   2.206 +    and "open (f ` S)"
   2.207 +    and "continuous_on S f"
   2.208 +    and "continuous_on (f ` S) g"
   2.209 +    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
   2.210 +    and "x \<in> S"
   2.211      and "(f has_derivative f') (at x)"
   2.212      and "bounded_linear g'"
   2.213      and "g' \<circ> f' = id"
   2.214 @@ -1377,11 +1338,11 @@
   2.215  
   2.216  lemma has_derivative_inverse:
   2.217    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   2.218 -  assumes "compact s"
   2.219 -    and "x \<in> s"
   2.220 -    and "f x \<in> interior (f ` s)"
   2.221 -    and "continuous_on s f"
   2.222 -    and "\<forall>y\<in>s. g (f y) = y"
   2.223 +  assumes "compact S"
   2.224 +    and "x \<in> S"
   2.225 +    and fx: "f x \<in> interior (f ` S)"
   2.226 +    and "continuous_on S f"
   2.227 +    and "\<And>y. y \<in> S \<Longrightarrow> g (f y) = y"
   2.228      and "(f has_derivative f') (at x)"
   2.229      and "bounded_linear g'"
   2.230      and "g' \<circ> f' = id"
   2.231 @@ -1389,20 +1350,17 @@
   2.232  proof -
   2.233    {
   2.234      fix y
   2.235 -    assume "y \<in> interior (f ` s)"
   2.236 -    then obtain x where "x \<in> s" and *: "y = f x"
   2.237 -      unfolding image_iff
   2.238 -      using interior_subset
   2.239 -      by auto
   2.240 +    assume "y \<in> interior (f ` S)"
   2.241 +    then obtain x where "x \<in> S" and *: "y = f x"
   2.242 +      by (meson imageE interior_subset subsetCE)
   2.243      have "f (g y) = y"
   2.244 -      unfolding * and assms(5)[rule_format,OF \<open>x\<in>s\<close>] ..
   2.245 +      unfolding * and assms(5)[rule_format,OF \<open>x\<in>S\<close>] ..
   2.246    } note * = this
   2.247    show ?thesis
   2.248 -    apply (rule has_derivative_inverse_basic_x[OF assms(6-8)])
   2.249 -    apply (rule continuous_on_interior[OF _ assms(3)])
   2.250 -    apply (rule continuous_on_inv[OF assms(4,1)])
   2.251 -    apply (rule assms(2,5) assms(5)[rule_format] open_interior assms(3))+
   2.252 -    apply (metis *)
   2.253 +    apply (rule has_derivative_inverse_basic_x[OF assms(6-8), where T = "interior (f ` S)"])
   2.254 +    apply (rule continuous_on_interior[OF _ fx])
   2.255 +    apply (rule continuous_on_inv)
   2.256 +    apply (simp_all add: assms *)
   2.257      done
   2.258  qed
   2.259  
   2.260 @@ -1411,13 +1369,13 @@
   2.261  
   2.262  lemma brouwer_surjective:
   2.263    fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
   2.264 -  assumes "compact t"
   2.265 -    and "convex t"
   2.266 -    and "t \<noteq> {}"
   2.267 -    and "continuous_on t f"
   2.268 -    and "\<forall>x\<in>s. \<forall>y\<in>t. x + (y - f y) \<in> t"
   2.269 -    and "x \<in> s"
   2.270 -  shows "\<exists>y\<in>t. f y = x"
   2.271 +  assumes "compact T"
   2.272 +    and "convex T"
   2.273 +    and "T \<noteq> {}"
   2.274 +    and "continuous_on T f"
   2.275 +    and "\<And>x y. \<lbrakk>x\<in>S; y\<in>T\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> T"
   2.276 +    and "x \<in> S"
   2.277 +  shows "\<exists>y\<in>T. f y = x"
   2.278  proof -
   2.279    have *: "\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y"
   2.280      by (auto simp add: algebra_simps)
   2.281 @@ -1432,10 +1390,10 @@
   2.282  
   2.283  lemma brouwer_surjective_cball:
   2.284    fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
   2.285 -  assumes "e > 0"
   2.286 -    and "continuous_on (cball a e) f"
   2.287 -    and "\<forall>x\<in>s. \<forall>y\<in>cball a e. x + (y - f y) \<in> cball a e"
   2.288 -    and "x \<in> s"
   2.289 +  assumes "continuous_on (cball a e) f"
   2.290 +    and "e > 0"
   2.291 +    and "x \<in> S"
   2.292 +    and "\<And>x y. \<lbrakk>x\<in>S; y\<in>cball a e\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> cball a e"
   2.293    shows "\<exists>y\<in>cball a e. f y = x"
   2.294    apply (rule brouwer_surjective)
   2.295    apply (rule compact_cball convex_cball)+
   2.296 @@ -1448,14 +1406,14 @@
   2.297  
   2.298  lemma sussmann_open_mapping:
   2.299    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
   2.300 -  assumes "open s"
   2.301 -    and "continuous_on s f"
   2.302 -    and "x \<in> s"
   2.303 +  assumes "open S"
   2.304 +    and "continuous_on S f"
   2.305 +    and "x \<in> S"
   2.306      and "(f has_derivative f') (at x)"
   2.307      and "bounded_linear g'" "f' \<circ> g' = id"
   2.308 -    and "t \<subseteq> s"
   2.309 -    and "x \<in> interior t"
   2.310 -  shows "f x \<in> interior (f ` t)"
   2.311 +    and "T \<subseteq> S"
   2.312 +    and "x \<in> interior T"
   2.313 +  shows "f x \<in> interior (f ` T)"
   2.314  proof -
   2.315    interpret f': bounded_linear f'
   2.316      using assms
   2.317 @@ -1473,31 +1431,17 @@
   2.318      using assms(4)
   2.319      unfolding has_derivative_at_alt
   2.320      using * by blast
   2.321 -  obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> t"
   2.322 +  obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> T"
   2.323      using assms(8)
   2.324      unfolding mem_interior_cball
   2.325      by blast
   2.326    have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
   2.327    obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
   2.328      using real_lbound_gt_zero[OF *] by blast
   2.329 -  have "\<forall>z\<in>cball (f x) (e / 2). \<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z"
   2.330 -    apply rule
   2.331 -    apply (rule brouwer_surjective_cball[where s="cball (f x) (e/2)"])
   2.332 -    prefer 3
   2.333 -    apply rule
   2.334 -    apply rule
   2.335 -  proof-
   2.336 -    show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
   2.337 -      unfolding g'.diff
   2.338 -      apply (rule continuous_on_compose[of _ _ f, unfolded o_def])
   2.339 -      apply (rule continuous_intros linear_continuous_on[OF assms(5)])+
   2.340 -      apply (rule continuous_on_subset[OF assms(2)])
   2.341 -      apply rule
   2.342 -      apply (unfold image_iff)
   2.343 -      apply (erule bexE)
   2.344 +  have lem: "\<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z" if "z\<in>cball (f x) (e / 2)" for z
   2.345 +  proof (rule brouwer_surjective_cball)
   2.346 +    have z: "z \<in> S" if as: "y \<in>cball (f x) e" "z = x + (g' y - g' (f x))" for y z
   2.347      proof-
   2.348 -      fix y z
   2.349 -      assume as: "y \<in>cball (f x) e" "z = x + (g' y - g' (f x))"
   2.350        have "dist x z = norm (g' (f x) - g' y)"
   2.351          unfolding as(2) and dist_norm by auto
   2.352        also have "\<dots> \<le> norm (f x - y) * B"
   2.353 @@ -1516,9 +1460,16 @@
   2.354        finally have "z \<in> cball x e1"
   2.355          unfolding mem_cball
   2.356          by force
   2.357 -      then show "z \<in> s"
   2.358 +      then show "z \<in> S"
   2.359          using e1 assms(7) by auto
   2.360      qed
   2.361 +    show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
   2.362 +      unfolding g'.diff
   2.363 +      apply (rule continuous_on_compose[of _ _ f, unfolded o_def])
   2.364 +       apply (rule continuous_intros linear_continuous_on[OF assms(5)])+
   2.365 +      apply (rule continuous_on_subset[OF assms(2)])
   2.366 +      using z
   2.367 +      by blast
   2.368    next
   2.369      fix y z
   2.370      assume as: "y \<in> cball (f x) (e / 2)" "z \<in> cball (f x) e"
   2.371 @@ -1528,7 +1479,7 @@
   2.372        apply (rule mult_right_mono)
   2.373        using as(2)[unfolded mem_cball dist_norm] and B
   2.374        unfolding norm_minus_commute
   2.375 -      apply auto
   2.376 +       apply auto
   2.377        done
   2.378      also have "\<dots> < e0"
   2.379        using e and B
   2.380 @@ -1563,7 +1514,7 @@
   2.381      finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e"
   2.382        unfolding mem_cball dist_norm
   2.383        by auto
   2.384 -  qed (insert e, auto) note lem = this
   2.385 +  qed (use e that in auto) 
   2.386    show ?thesis
   2.387      unfolding mem_interior
   2.388      apply (rule_tac x="e/2" in exI)
   2.389 @@ -1589,13 +1540,13 @@
   2.390        done
   2.391      also have "\<dots> \<le> e1"
   2.392        using e B unfolding less_divide_eq by auto
   2.393 -    finally have "x + g'(z - f x) \<in> t"
   2.394 +    finally have "x + g'(z - f x) \<in> T"
   2.395        apply -
   2.396        apply (rule e1(2)[unfolded subset_eq,rule_format])
   2.397        unfolding mem_cball dist_norm
   2.398        apply auto
   2.399        done
   2.400 -    then show "y \<in> f ` t"
   2.401 +    then show "y \<in> f ` T"
   2.402        using z by auto
   2.403    qed (insert e, auto)
   2.404  qed
   2.405 @@ -1750,9 +1701,9 @@
   2.406    fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   2.407    assumes "a \<in> s"
   2.408        and "open s"
   2.409 -      and "bounded_linear g'"
   2.410 +      and bling: "bounded_linear g'"
   2.411        and "g' \<circ> f' a = id"
   2.412 -      and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x)"
   2.413 +      and derf: "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x)"
   2.414        and "\<And>e. e > 0 \<Longrightarrow> \<exists>d>0. \<forall>x. dist a x < d \<longrightarrow> onorm (\<lambda>v. f' x v - f' a v) < e"
   2.415    obtains r where "r > 0" "ball a r \<subseteq> s" "inj_on f (ball a r)"
   2.416  proof -
   2.417 @@ -1760,11 +1711,7 @@
   2.418      using assms by auto
   2.419    note f'g' = assms(4)[unfolded id_def o_def,THEN cong]
   2.420    have "g' (f' a (\<Sum>Basis)) = (\<Sum>Basis)" "(\<Sum>Basis) \<noteq> (0::'n)"
   2.421 -    defer
   2.422 -    apply (subst euclidean_eq_iff)
   2.423 -    using f'g'
   2.424 -    apply auto
   2.425 -    done
   2.426 +    using f'g' by auto
   2.427    then have *: "0 < onorm g'"
   2.428      unfolding onorm_pos_lt[OF assms(3)]
   2.429      by fastforce
   2.430 @@ -1812,17 +1759,11 @@
   2.431          have *: "(\<lambda>v. v - g' (f' u v)) = g' \<circ> (\<lambda>w. f' a w - f' u w)"
   2.432            unfolding o_def and diff
   2.433            using f'g' by auto
   2.434 +        have blin: "bounded_linear (f' a)"
   2.435 +          using \<open>a \<in> s\<close> derf by blast
   2.436          show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)"
   2.437 -          unfolding ph' *
   2.438 -          apply (simp add: comp_def)
   2.439 -          apply (rule bounded_linear.has_derivative[OF assms(3)])
   2.440 -          apply (rule derivative_intros)
   2.441 -          defer
   2.442 -          apply (rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
   2.443 -          apply (rule has_derivative_at_withinI)
   2.444 -          using assms(5) and \<open>u \<in> s\<close> \<open>a \<in> s\<close>
   2.445 -          apply (auto intro!: derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] has_derivative_bounded_linear)
   2.446 -          done
   2.447 +          unfolding ph' * comp_def
   2.448 +          by (rule \<open>u \<in> s\<close> derivative_eq_intros has_derivative_at_withinI [OF derf] bounded_linear.has_derivative [OF blin]  bounded_linear.has_derivative [OF bling] |simp)+
   2.449          have **: "bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>x. f' a x - f' u x)"
   2.450            apply (rule_tac[!] bounded_linear_sub)
   2.451            apply (rule_tac[!] has_derivative_bounded_linear)
   2.452 @@ -1896,21 +1837,20 @@
   2.453    qed
   2.454  qed
   2.455  
   2.456 -lemma has_derivative_sequence_lipschitz:
   2.457 +lemma has_derivative_sequence_Lipschitz:
   2.458    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   2.459 -  assumes "convex s"
   2.460 -    and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
   2.461 -    and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
   2.462 -  shows "\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s.
   2.463 +  assumes "convex S"
   2.464 +    and "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
   2.465 +    and "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
   2.466 +    and "e > 0"
   2.467 +  shows "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S.
   2.468      norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)"
   2.469 -proof (rule, rule)
   2.470 -  fix e :: real
   2.471 -  assume "e > 0"
   2.472 -  then have *: "2 * (1/2* e) = e" "1/2 * e >0"
   2.473 -    by auto
   2.474 -  obtain N where "\<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> 1 / 2 * e * norm h"
   2.475 +proof -
   2.476 +  have *: "2 * (1/2* e) = e" "1/2 * e >0"
   2.477 +    using \<open>e>0\<close> by auto
   2.478 +  obtain N where "\<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> 1 / 2 * e * norm h"
   2.479      using assms(3) *(2) by blast
   2.480 -  then show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm (f m x - f n x - (f m y - f n y)) \<le> e * norm (x - y)"
   2.481 +  then show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S. norm (f m x - f n x - (f m y - f n y)) \<le> e * norm (x - y)"
   2.482      apply (rule_tac x=N in exI)
   2.483      apply (rule has_derivative_sequence_lipschitz_lemma[where e="1/2 *e", unfolded *])
   2.484      using assms \<open>e > 0\<close>
   2.485 @@ -1920,22 +1860,22 @@
   2.486  
   2.487  lemma has_derivative_sequence:
   2.488    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
   2.489 -  assumes "convex s"
   2.490 -    and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
   2.491 -    and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
   2.492 -    and "x0 \<in> s"
   2.493 +  assumes "convex S"
   2.494 +    and "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
   2.495 +    and "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
   2.496 +    and "x0 \<in> S"
   2.497      and "((\<lambda>n. f n x0) \<longlongrightarrow> l) sequentially"
   2.498 -  shows "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g'(x)) (at x within s)"
   2.499 +  shows "\<exists>g. \<forall>x\<in>S. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g'(x)) (at x within S)"
   2.500  proof -
   2.501 -  have lem1: "\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s.
   2.502 +  have lem1: "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S.
   2.503        norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)"
   2.504 -    using assms(1,2,3) by (rule has_derivative_sequence_lipschitz)
   2.505 -  have "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
   2.506 +    using assms(1,2,3) by (rule has_derivative_sequence_Lipschitz)
   2.507 +  have "\<exists>g. \<forall>x\<in>S. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
   2.508      apply (rule bchoice)
   2.509      unfolding convergent_eq_Cauchy
   2.510    proof
   2.511      fix x
   2.512 -    assume "x \<in> s"
   2.513 +    assume "x \<in> S"
   2.514      show "Cauchy (\<lambda>n. f n x)"
   2.515      proof (cases "x = x0")
   2.516        case True
   2.517 @@ -1945,7 +1885,7 @@
   2.518        case False
   2.519        show ?thesis
   2.520          unfolding Cauchy_def
   2.521 -      proof (rule, rule)
   2.522 +      proof (intro allI impI)
   2.523          fix e :: real
   2.524          assume "e > 0"
   2.525          hence *: "e / 2 > 0" "e / 2 / norm (x - x0) > 0" using False by auto
   2.526 @@ -1955,12 +1895,11 @@
   2.527            using *(1) by blast
   2.528          obtain N where N:
   2.529            "\<forall>m\<ge>N. \<forall>n\<ge>N.
   2.530 -            \<forall>xa\<in>s. \<forall>y\<in>s. norm (f m xa - f n xa - (f m y - f n y)) \<le>
   2.531 +            \<forall>xa\<in>S. \<forall>y\<in>S. norm (f m xa - f n xa - (f m y - f n y)) \<le>
   2.532                e / 2 / norm (x - x0) * norm (xa - y)"
   2.533          using lem1 *(2) by blast
   2.534          show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e"
   2.535 -          apply (rule_tac x="max M N" in exI)
   2.536 -        proof rule+
   2.537 +        proof (intro exI allI impI)
   2.538            fix m n
   2.539            assume as: "max M N \<le>m" "max M N\<le>n"
   2.540            have "dist (f m x) (f n x) \<le>
   2.541 @@ -1968,7 +1907,7 @@
   2.542              unfolding dist_norm
   2.543              by (rule norm_triangle_sub)
   2.544            also have "\<dots> \<le> norm (f m x0 - f n x0) + e / 2"
   2.545 -            using N[rule_format,OF _ _ \<open>x\<in>s\<close> \<open>x0\<in>s\<close>, of m n] and as and False
   2.546 +            using N[rule_format,OF _ _ \<open>x\<in>S\<close> \<open>x0\<in>S\<close>, of m n] and as and False
   2.547              by auto
   2.548            also have "\<dots> < e / 2 + e / 2"
   2.549              apply (rule add_strict_right_mono)
   2.550 @@ -1982,27 +1921,24 @@
   2.551        qed
   2.552      qed
   2.553    qed
   2.554 -  then obtain g where g: "\<forall>x\<in>s. (\<lambda>n. f n x) \<longlonglongrightarrow> g x" ..
   2.555 -  have lem2: "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm ((f n x - f n y) - (g x - g y)) \<le> e * norm (x - y)"
   2.556 +  then obtain g where g: "\<forall>x\<in>S. (\<lambda>n. f n x) \<longlonglongrightarrow> g x" ..
   2.557 +  have lem2: "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S. norm ((f n x - f n y) - (g x - g y)) \<le> e * norm (x - y)"
   2.558    proof (rule, rule)
   2.559      fix e :: real
   2.560      assume *: "e > 0"
   2.561      obtain N where
   2.562 -      N: "\<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm (f m x - f n x - (f m y - f n y)) \<le> e * norm (x - y)"
   2.563 +      N: "\<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S. norm (f m x - f n x - (f m y - f n y)) \<le> e * norm (x - y)"
   2.564        using lem1 * by blast
   2.565 -    show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)"
   2.566 +    show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S. norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)"
   2.567        apply (rule_tac x=N in exI)
   2.568      proof rule+
   2.569        fix n x y
   2.570 -      assume as: "N \<le> n" "x \<in> s" "y \<in> s"
   2.571 +      assume as: "N \<le> n" "x \<in> S" "y \<in> S"
   2.572        have "((\<lambda>m. norm (f n x - f n y - (f m x - f m y))) \<longlongrightarrow> norm (f n x - f n y - (g x - g y))) sequentially"
   2.573          by (intro tendsto_intros g[rule_format] as)
   2.574        moreover have "eventually (\<lambda>m. norm (f n x - f n y - (f m x - f m y)) \<le> e * norm (x - y)) sequentially"
   2.575          unfolding eventually_sequentially
   2.576 -        apply (rule_tac x=N in exI)
   2.577 -        apply rule
   2.578 -        apply rule
   2.579 -      proof -
   2.580 +      proof (intro exI allI impI)
   2.581          fix m
   2.582          assume "N \<le> m"
   2.583          then show "norm (f n x - f n y - (f m x - f m y)) \<le> e * norm (x - y)"
   2.584 @@ -2013,11 +1949,11 @@
   2.585          by (simp add: tendsto_upperbound)
   2.586      qed
   2.587    qed
   2.588 -  have "\<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g' x) (at x within s)"
   2.589 +  have "\<forall>x\<in>S. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g' x) (at x within S)"
   2.590      unfolding has_derivative_within_alt2
   2.591    proof (intro ballI conjI)
   2.592      fix x
   2.593 -    assume "x \<in> s"
   2.594 +    assume "x \<in> S"
   2.595      then show "((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
   2.596        by (simp add: g)
   2.597      have lem3: "\<forall>u. ((\<lambda>n. f' n x u) \<longlongrightarrow> g' x u) sequentially"
   2.598 @@ -2030,7 +1966,7 @@
   2.599        proof (cases "u = 0")
   2.600          case True
   2.601          have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e * norm u) sequentially"
   2.602 -          using assms(3)[folded eventually_sequentially] and \<open>0 < e\<close> and \<open>x \<in> s\<close>
   2.603 +          using assms(3)[folded eventually_sequentially] and \<open>0 < e\<close> and \<open>x \<in> S\<close>
   2.604            by (fast elim: eventually_mono)
   2.605          then show ?thesis
   2.606            using \<open>u = 0\<close> and \<open>0 < e\<close> by (auto elim: eventually_mono)
   2.607 @@ -2038,7 +1974,7 @@
   2.608          case False
   2.609          with \<open>0 < e\<close> have "0 < e / norm u" by simp
   2.610          then have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e / norm u * norm u) sequentially"
   2.611 -          using assms(3)[folded eventually_sequentially] and \<open>x \<in> s\<close>
   2.612 +          using assms(3)[folded eventually_sequentially] and \<open>x \<in> S\<close>
   2.613            by (fast elim: eventually_mono)
   2.614          then show ?thesis
   2.615            using \<open>u \<noteq> 0\<close> by simp
   2.616 @@ -2048,7 +1984,7 @@
   2.617      proof
   2.618        fix x' y z :: 'a
   2.619        fix c :: real
   2.620 -      note lin = assms(2)[rule_format,OF \<open>x\<in>s\<close>,THEN has_derivative_bounded_linear]
   2.621 +      note lin = assms(2)[rule_format,OF \<open>x\<in>S\<close>,THEN has_derivative_bounded_linear]
   2.622        show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'"
   2.623          apply (rule tendsto_unique[OF trivial_limit_sequentially])
   2.624          apply (rule lem3[rule_format])
   2.625 @@ -2064,9 +2000,9 @@
   2.626          apply (rule lem3[rule_format])+
   2.627          done
   2.628        obtain N where N: "\<forall>h. norm (f' N x h - g' x h) \<le> 1 * norm h"
   2.629 -        using assms(3) \<open>x \<in> s\<close> by (fast intro: zero_less_one)
   2.630 +        using assms(3) \<open>x \<in> S\<close> by (fast intro: zero_less_one)
   2.631        have "bounded_linear (f' N x)"
   2.632 -        using assms(2) \<open>x \<in> s\<close> by fast
   2.633 +        using assms(2) \<open>x \<in> S\<close> by fast
   2.634        from bounded_linear.bounded [OF this]
   2.635        obtain K where K: "\<forall>h. norm (f' N x h) \<le> norm h * K" ..
   2.636        {
   2.637 @@ -2082,36 +2018,36 @@
   2.638        }
   2.639        then show "\<exists>K. \<forall>h. norm (g' x h) \<le> norm h * K" by fast
   2.640      qed
   2.641 -    show "\<forall>e>0. eventually (\<lambda>y. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)) (at x within s)"
   2.642 +    show "\<forall>e>0. eventually (\<lambda>y. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)) (at x within S)"
   2.643      proof (rule, rule)
   2.644        fix e :: real
   2.645        assume "e > 0"
   2.646        then have *: "e / 3 > 0"
   2.647          by auto
   2.648 -      obtain N1 where N1: "\<forall>n\<ge>N1. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e / 3 * norm h"
   2.649 +      obtain N1 where N1: "\<forall>n\<ge>N1. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e / 3 * norm h"
   2.650          using assms(3) * by blast
   2.651        obtain N2 where
   2.652 -          N2: "\<forall>n\<ge>N2. \<forall>x\<in>s. \<forall>y\<in>s. norm (f n x - f n y - (g x - g y)) \<le> e / 3 * norm (x - y)"
   2.653 +          N2: "\<forall>n\<ge>N2. \<forall>x\<in>S. \<forall>y\<in>S. norm (f n x - f n y - (g x - g y)) \<le> e / 3 * norm (x - y)"
   2.654          using lem2 * by blast
   2.655        let ?N = "max N1 N2"
   2.656 -      have "eventually (\<lambda>y. norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)) (at x within s)"
   2.657 -        using assms(2)[unfolded has_derivative_within_alt2] and \<open>x \<in> s\<close> and * by fast
   2.658 -      moreover have "eventually (\<lambda>y. y \<in> s) (at x within s)"
   2.659 +      have "eventually (\<lambda>y. norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)) (at x within S)"
   2.660 +        using assms(2)[unfolded has_derivative_within_alt2] and \<open>x \<in> S\<close> and * by fast
   2.661 +      moreover have "eventually (\<lambda>y. y \<in> S) (at x within S)"
   2.662          unfolding eventually_at by (fast intro: zero_less_one)
   2.663 -      ultimately show "\<forall>\<^sub>F y in at x within s. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
   2.664 +      ultimately show "\<forall>\<^sub>F y in at x within S. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
   2.665        proof (rule eventually_elim2)
   2.666          fix y
   2.667 -        assume "y \<in> s"
   2.668 +        assume "y \<in> S"
   2.669          assume "norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)"
   2.670          moreover have "norm (g y - g x - (f ?N y - f ?N x)) \<le> e / 3 * norm (y - x)"
   2.671 -          using N2[rule_format, OF _ \<open>y \<in> s\<close> \<open>x \<in> s\<close>]
   2.672 +          using N2[rule_format, OF _ \<open>y \<in> S\<close> \<open>x \<in> S\<close>]
   2.673            by (simp add: norm_minus_commute)
   2.674          ultimately have "norm (g y - g x - f' ?N x (y - x)) \<le> 2 * e / 3 * norm (y - x)"
   2.675            using norm_triangle_le[of "g y - g x - (f ?N y - f ?N x)" "f ?N y - f ?N x - f' ?N x (y - x)" "2 * e / 3 * norm (y - x)"]
   2.676            by (auto simp add: algebra_simps)
   2.677          moreover
   2.678          have " norm (f' ?N x (y - x) - g' x (y - x)) \<le> e / 3 * norm (y - x)"
   2.679 -          using N1 \<open>x \<in> s\<close> by auto
   2.680 +          using N1 \<open>x \<in> S\<close> by auto
   2.681          ultimately show "norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
   2.682            using norm_triangle_le[of "g y - g x - f' (max N1 N2) x (y - x)" "f' (max N1 N2) x (y - x) - g' x (y - x)"]
   2.683            by (auto simp add: algebra_simps)
   2.684 @@ -2125,77 +2061,63 @@
   2.685  
   2.686  lemma has_antiderivative_sequence:
   2.687    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
   2.688 -  assumes "convex s"
   2.689 -    and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
   2.690 -    and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
   2.691 -  shows "\<exists>g. \<forall>x\<in>s. (g has_derivative g' x) (at x within s)"
   2.692 -proof (cases "s = {}")
   2.693 +  assumes "convex S"
   2.694 +    and der: "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
   2.695 +    and no: "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
   2.696 +  shows "\<exists>g. \<forall>x\<in>S. (g has_derivative g' x) (at x within S)"
   2.697 +proof (cases "S = {}")
   2.698    case False
   2.699 -  then obtain a where "a \<in> s"
   2.700 +  then obtain a where "a \<in> S"
   2.701      by auto
   2.702 -  have *: "\<And>P Q. \<exists>g. \<forall>x\<in>s. P g x \<and> Q g x \<Longrightarrow> \<exists>g. \<forall>x\<in>s. Q g x"
   2.703 +  have *: "\<And>P Q. \<exists>g. \<forall>x\<in>S. P g x \<and> Q g x \<Longrightarrow> \<exists>g. \<forall>x\<in>S. Q g x"
   2.704      by auto
   2.705    show ?thesis
   2.706      apply (rule *)
   2.707 -    apply (rule has_derivative_sequence[OF assms(1) _ assms(3), of "\<lambda>n x. f n x + (f 0 a - f n a)"])
   2.708 -    apply (metis assms(2) has_derivative_add_const)
   2.709 -    apply (rule \<open>a \<in> s\<close>)
   2.710 +    apply (rule has_derivative_sequence [OF \<open>convex S\<close> _ no, of "\<lambda>n x. f n x + (f 0 a - f n a)"])
   2.711 +       apply (metis assms(2) has_derivative_add_const)
   2.712 +    using \<open>a \<in> S\<close> 
   2.713      apply auto
   2.714      done
   2.715  qed auto
   2.716  
   2.717  lemma has_antiderivative_limit:
   2.718    fixes g' :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'b::banach"
   2.719 -  assumes "convex s"
   2.720 -    and "\<forall>e>0. \<exists>f f'. \<forall>x\<in>s.
   2.721 -      (f has_derivative (f' x)) (at x within s) \<and> (\<forall>h. norm (f' x h - g' x h) \<le> e * norm h)"
   2.722 -  shows "\<exists>g. \<forall>x\<in>s. (g has_derivative g' x) (at x within s)"
   2.723 +  assumes "convex S"
   2.724 +    and "\<And>e. e>0 \<Longrightarrow> \<exists>f f'. \<forall>x\<in>S.
   2.725 +           (f has_derivative (f' x)) (at x within S) \<and> (\<forall>h. norm (f' x h - g' x h) \<le> e * norm h)"
   2.726 +  shows "\<exists>g. \<forall>x\<in>S. (g has_derivative g' x) (at x within S)"
   2.727  proof -
   2.728 -  have *: "\<forall>n. \<exists>f f'. \<forall>x\<in>s.
   2.729 -    (f has_derivative (f' x)) (at x within s) \<and>
   2.730 +  have *: "\<forall>n. \<exists>f f'. \<forall>x\<in>S.
   2.731 +    (f has_derivative (f' x)) (at x within S) \<and>
   2.732      (\<forall>h. norm(f' x h - g' x h) \<le> inverse (real (Suc n)) * norm h)"
   2.733      by (simp add: assms(2))
   2.734    obtain f where
   2.735 -    *: "\<forall>x. \<exists>f'. \<forall>xa\<in>s. (f x has_derivative f' xa) (at xa within s) \<and>
   2.736 -      (\<forall>h. norm (f' xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
   2.737 -    using *[THEN choice] ..
   2.738 +    *: "\<And>x. \<exists>f'. \<forall>xa\<in>S. (f x has_derivative f' xa) (at xa within S) \<and>
   2.739 +        (\<forall>h. norm (f' xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
   2.740 +    using * by metis
   2.741    obtain f' where
   2.742 -    f: "\<forall>x. \<forall>xa\<in>s. (f x has_derivative f' x xa) (at xa within s) \<and>
   2.743 -      (\<forall>h. norm (f' x xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
   2.744 -    using *[THEN choice] ..
   2.745 +    f': "\<And>x. \<forall>z\<in>S. (f x has_derivative f' x z) (at z within S) \<and>
   2.746 +            (\<forall>h. norm (f' x z h - g' z h) \<le> inverse (real (Suc x)) * norm h)"
   2.747 +    using * by metis
   2.748    show ?thesis
   2.749 -    apply (rule has_antiderivative_sequence[OF assms(1), of f f'])
   2.750 -    defer
   2.751 -    apply rule
   2.752 -    apply rule
   2.753 -  proof -
   2.754 +  proof (rule has_antiderivative_sequence[OF \<open>convex S\<close>, of f f'])
   2.755      fix e :: real
   2.756      assume "e > 0"
   2.757      obtain N where N: "inverse (real (Suc N)) < e"
   2.758        using reals_Archimedean[OF \<open>e>0\<close>] ..
   2.759 -    show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
   2.760 -      apply (rule_tac x=N in exI)
   2.761 -      apply rule
   2.762 -      apply rule
   2.763 -      apply rule
   2.764 -      apply rule
   2.765 -    proof -
   2.766 +    show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
   2.767 +    proof (intro exI allI ballI impI)
   2.768        fix n x h
   2.769 -      assume n: "N \<le> n" and x: "x \<in> s"
   2.770 +      assume n: "N \<le> n" and x: "x \<in> S"
   2.771        have *: "inverse (real (Suc n)) \<le> e"
   2.772          apply (rule order_trans[OF _ N[THEN less_imp_le]])
   2.773          using n
   2.774          apply (auto simp add: field_simps)
   2.775          done
   2.776        show "norm (f' n x h - g' x h) \<le> e * norm h"
   2.777 -        using f[rule_format,THEN conjunct2, OF x, of n, THEN spec[where x=h]]
   2.778 -        apply (rule order_trans)
   2.779 -        using N *
   2.780 -        apply (cases "h = 0")
   2.781 -        apply auto
   2.782 -        done
   2.783 +        by (meson "*" mult_right_mono norm_ge_zero order.trans x f')
   2.784      qed
   2.785 -  qed (insert f, auto)
   2.786 +  qed (use f' in auto)
   2.787  qed
   2.788  
   2.789  
   2.790 @@ -2203,12 +2125,12 @@
   2.791  
   2.792  lemma has_derivative_series:
   2.793    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
   2.794 -  assumes "convex s"
   2.795 -    and "\<And>n x. x \<in> s \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within s)"
   2.796 -    and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (sum (\<lambda>i. f' i x h) {..<n} - g' x h) \<le> e * norm h"
   2.797 -    and "x \<in> s"
   2.798 +  assumes "convex S"
   2.799 +    and "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
   2.800 +    and "\<And>e. e>0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (sum (\<lambda>i. f' i x h) {..<n} - g' x h) \<le> e * norm h"
   2.801 +    and "x \<in> S"
   2.802      and "(\<lambda>n. f n x) sums l"
   2.803 -  shows "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums (g x) \<and> (g has_derivative g' x) (at x within s)"
   2.804 +  shows "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) sums (g x) \<and> (g has_derivative g' x) (at x within S)"
   2.805    unfolding sums_def
   2.806    apply (rule has_derivative_sequence[OF assms(1) _ assms(3)])
   2.807    apply (metis assms(2) has_derivative_sum)
   2.808 @@ -2219,20 +2141,19 @@
   2.809  
   2.810  lemma has_field_derivative_series:
   2.811    fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
   2.812 -  assumes "convex s"
   2.813 -  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
   2.814 -  assumes "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
   2.815 -  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
   2.816 -  shows   "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within s)"
   2.817 +  assumes "convex S"
   2.818 +  assumes "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x within S)"
   2.819 +  assumes "uniform_limit S (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
   2.820 +  assumes "x0 \<in> S" "summable (\<lambda>n. f n x0)"
   2.821 +  shows   "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within S)"
   2.822  unfolding has_field_derivative_def
   2.823  proof (rule has_derivative_series)
   2.824 -  show "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h"
   2.825 -  proof (intro allI impI)
   2.826 -    fix e :: real assume "e > 0"
   2.827 -    with assms(3) obtain N where N: "\<And>n x. n \<ge> N \<Longrightarrow> x \<in> s \<Longrightarrow> norm ((\<Sum>i<n. f' i x) - g' x) < e"
   2.828 +  show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" if "e > 0" for e
   2.829 +  proof -
   2.830 +    from that assms(3) obtain N where N: "\<And>n x. n \<ge> N \<Longrightarrow> x \<in> S \<Longrightarrow> norm ((\<Sum>i<n. f' i x) - g' x) < e"
   2.831        unfolding uniform_limit_iff eventually_at_top_linorder dist_norm by blast
   2.832      {
   2.833 -      fix n :: nat and x h :: 'a assume nx: "n \<ge> N" "x \<in> s"
   2.834 +      fix n :: nat and x h :: 'a assume nx: "n \<ge> N" "x \<in> S"
   2.835        have "norm ((\<Sum>i<n. f' i x * h) - g' x * h) = norm ((\<Sum>i<n. f' i x) - g' x) * norm h"
   2.836          by (simp add: norm_mult [symmetric] ring_distribs sum_distrib_right)
   2.837        also from N[OF nx] have "norm ((\<Sum>i<n. f' i x) - g' x) \<le> e" by simp
   2.838 @@ -2240,55 +2161,55 @@
   2.839          by (intro mult_right_mono) simp_all
   2.840        finally have "norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" .
   2.841      }
   2.842 -    thus "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" by blast
   2.843 +    thus "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" by blast
   2.844    qed
   2.845 -qed (insert assms, auto simp: has_field_derivative_def)
   2.846 +qed (use assms in \<open>auto simp: has_field_derivative_def\<close>)
   2.847  
   2.848  lemma has_field_derivative_series':
   2.849    fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
   2.850 -  assumes "convex s"
   2.851 -  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
   2.852 -  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
   2.853 -  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" "x \<in> interior s"
   2.854 +  assumes "convex S"
   2.855 +  assumes "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x within S)"
   2.856 +  assumes "uniformly_convergent_on S (\<lambda>n x. \<Sum>i<n. f' i x)"
   2.857 +  assumes "x0 \<in> S" "summable (\<lambda>n. f n x0)" "x \<in> interior S"
   2.858    shows   "summable (\<lambda>n. f n x)" "((\<lambda>x. \<Sum>n. f n x) has_field_derivative (\<Sum>n. f' n x)) (at x)"
   2.859  proof -
   2.860 -  from \<open>x \<in> interior s\<close> have "x \<in> s" using interior_subset by blast
   2.861 +  from \<open>x \<in> interior S\<close> have "x \<in> S" using interior_subset by blast
   2.862    define g' where [abs_def]: "g' x = (\<Sum>i. f' i x)" for x
   2.863 -  from assms(3) have "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
   2.864 +  from assms(3) have "uniform_limit S (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
   2.865      by (simp add: uniformly_convergent_uniform_limit_iff suminf_eq_lim g'_def)
   2.866    from has_field_derivative_series[OF assms(1,2) this assms(4,5)] obtain g where g:
   2.867 -    "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
   2.868 -    "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
   2.869 -  from g(1)[OF \<open>x \<in> s\<close>] show "summable (\<lambda>n. f n x)" by (simp add: sums_iff)
   2.870 -  from g(2)[OF \<open>x \<in> s\<close>] \<open>x \<in> interior s\<close> have "(g has_field_derivative g' x) (at x)"
   2.871 -    by (simp add: at_within_interior[of x s])
   2.872 +    "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x"
   2.873 +    "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast
   2.874 +  from g(1)[OF \<open>x \<in> S\<close>] show "summable (\<lambda>n. f n x)" by (simp add: sums_iff)
   2.875 +  from g(2)[OF \<open>x \<in> S\<close>] \<open>x \<in> interior S\<close> have "(g has_field_derivative g' x) (at x)"
   2.876 +    by (simp add: at_within_interior[of x S])
   2.877    also have "(g has_field_derivative g' x) (at x) \<longleftrightarrow>
   2.878                  ((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)"
   2.879 -    using eventually_nhds_in_nhd[OF \<open>x \<in> interior s\<close>] interior_subset[of s] g(1)
   2.880 +    using eventually_nhds_in_nhd[OF \<open>x \<in> interior S\<close>] interior_subset[of S] g(1)
   2.881      by (intro DERIV_cong_ev) (auto elim!: eventually_mono simp: sums_iff)
   2.882    finally show "((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)" .
   2.883  qed
   2.884  
   2.885  lemma differentiable_series:
   2.886    fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
   2.887 -  assumes "convex s" "open s"
   2.888 -  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   2.889 -  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
   2.890 -  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
   2.891 +  assumes "convex S" "open S"
   2.892 +  assumes "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   2.893 +  assumes "uniformly_convergent_on S (\<lambda>n x. \<Sum>i<n. f' i x)"
   2.894 +  assumes "x0 \<in> S" "summable (\<lambda>n. f n x0)" and x: "x \<in> S"
   2.895    shows   "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)"
   2.896  proof -
   2.897 -  from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
   2.898 +  from assms(4) obtain g' where A: "uniform_limit S (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
   2.899      unfolding uniformly_convergent_on_def by blast
   2.900 -  from x and \<open>open s\<close> have s: "at x within s = at x" by (rule at_within_open)
   2.901 -  have "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within s)"
   2.902 -    by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within)
   2.903 -  then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
   2.904 -    "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
   2.905 +  from x and \<open>open S\<close> have S: "at x within S = at x" by (rule at_within_open)
   2.906 +  have "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within S)"
   2.907 +    by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within)
   2.908 +  then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x"
   2.909 +    "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast
   2.910    from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
   2.911    from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)"
   2.912 -    by (simp add: has_field_derivative_def s)
   2.913 +    by (simp add: has_field_derivative_def S)
   2.914    have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)"
   2.915 -    by (rule has_derivative_transform_within_open[OF g' \<open>open s\<close> x])
   2.916 +    by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x])
   2.917         (insert g, auto simp: sums_iff)
   2.918    thus "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)" unfolding differentiable_def
   2.919      by (auto simp: summable_def differentiable_def has_field_derivative_def)
   2.920 @@ -2296,32 +2217,32 @@
   2.921  
   2.922  lemma differentiable_series':
   2.923    fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
   2.924 -  assumes "convex s" "open s"
   2.925 -  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   2.926 -  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
   2.927 -  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
   2.928 +  assumes "convex S" "open S"
   2.929 +  assumes "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   2.930 +  assumes "uniformly_convergent_on S (\<lambda>n x. \<Sum>i<n. f' i x)"
   2.931 +  assumes "x0 \<in> S" "summable (\<lambda>n. f n x0)"
   2.932    shows   "(\<lambda>x. \<Sum>n. f n x) differentiable (at x0)"
   2.933 -  using differentiable_series[OF assms, of x0] \<open>x0 \<in> s\<close> by blast+
   2.934 +  using differentiable_series[OF assms, of x0] \<open>x0 \<in> S\<close> by blast+
   2.935  
   2.936  text \<open>Considering derivative @{typ "real \<Rightarrow> 'b::real_normed_vector"} as a vector.\<close>
   2.937  
   2.938  definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
   2.939  
   2.940  lemma vector_derivative_unique_within:
   2.941 -  assumes not_bot: "at x within s \<noteq> bot"
   2.942 -    and f': "(f has_vector_derivative f') (at x within s)"
   2.943 -    and f'': "(f has_vector_derivative f'') (at x within s)"
   2.944 +  assumes not_bot: "at x within S \<noteq> bot"
   2.945 +    and f': "(f has_vector_derivative f') (at x within S)"
   2.946 +    and f'': "(f has_vector_derivative f'') (at x within S)"
   2.947    shows "f' = f''"
   2.948  proof -
   2.949    have "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
   2.950    proof (rule frechet_derivative_unique_within)
   2.951 -    show "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> s"
   2.952 +    show "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> S"
   2.953      proof clarsimp
   2.954        fix e :: real assume "0 < e"
   2.955 -      with islimpt_approachable_real[of x s] not_bot
   2.956 -      obtain x' where "x' \<in> s" "x' \<noteq> x" "\<bar>x' - x\<bar> < e"
   2.957 +      with islimpt_approachable_real[of x S] not_bot
   2.958 +      obtain x' where "x' \<in> S" "x' \<noteq> x" "\<bar>x' - x\<bar> < e"
   2.959          by (auto simp add: trivial_limit_within)
   2.960 -      then show "\<exists>d. d \<noteq> 0 \<and> \<bar>d\<bar> < e \<and> x + d \<in> s"
   2.961 +      then show "\<exists>d. d \<noteq> 0 \<and> \<bar>d\<bar> < e \<and> x + d \<in> S"
   2.962          by (intro exI[of _ "x' - x"]) auto
   2.963      qed
   2.964    qed (insert f' f'', auto simp: has_vector_derivative_def)
   2.965 @@ -2351,8 +2272,8 @@
   2.966  qed (auto simp: vector_derivative_def has_vector_derivative_def differentiable_def)
   2.967  
   2.968  lemma vector_derivative_within:
   2.969 -  assumes not_bot: "at x within s \<noteq> bot" and y: "(f has_vector_derivative y) (at x within s)"
   2.970 -  shows "vector_derivative f (at x within s) = y"
   2.971 +  assumes not_bot: "at x within S \<noteq> bot" and y: "(f has_vector_derivative y) (at x within S)"
   2.972 +  shows "vector_derivative f (at x within S) = y"
   2.973    using y
   2.974    by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y])
   2.975       (auto simp: differentiable_def has_vector_derivative_def)
   2.976 @@ -2381,11 +2302,11 @@
   2.977    by (metis has_field_derivative_def has_real_derivative)
   2.978  
   2.979  lemma has_vector_derivative_cong_ev:
   2.980 -  assumes *: "eventually (\<lambda>x. x \<in> s \<longrightarrow> f x = g x) (nhds x)" "f x = g x"
   2.981 -  shows "(f has_vector_derivative f') (at x within s) = (g has_vector_derivative f') (at x within s)"
   2.982 +  assumes *: "eventually (\<lambda>x. x \<in> S \<longrightarrow> f x = g x) (nhds x)" "f x = g x"
   2.983 +  shows "(f has_vector_derivative f') (at x within S) = (g has_vector_derivative f') (at x within S)"
   2.984    unfolding has_vector_derivative_def has_derivative_def
   2.985    using *
   2.986 -  apply (cases "at x within s \<noteq> bot")
   2.987 +  apply (cases "at x within S \<noteq> bot")
   2.988    apply (intro refl conj_cong filterlim_cong)
   2.989    apply (auto simp: netlimit_within eventually_at_filter elim: eventually_mono)
   2.990    done