author paulson Sun Apr 29 14:46:11 2018 +0100 (12 months ago) changeset 68055 2cab37094fc4 parent 68054 ebd179b82e20 child 68056 9e077a905209
more defer/prefer
```     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
```