author paulson Sun May 20 22:10:30 2018 +0100 (21 months ago) changeset 68242 4acc029f69e9 parent 68238 eb57621568bb parent 68241 39a311f50344 child 68243 ddf1ead7b182
merged
```     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun May 20 22:04:46 2018 +0200
1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun May 20 22:10:30 2018 +0100
1.3 @@ -1154,7 +1154,7 @@
1.4            vector_derivative (shiftpath (1 - a) (shiftpath a g)) (at x within {0..1})"
1.5        apply (rule vector_derivative_at_within_ivl
1.6                    [OF has_vector_derivative_transform_within_open
1.7 -                      [where f = "(shiftpath (1 - a) (shiftpath a g))" and s = "{0<..<1}-s"]])
1.8 +                      [where f = "(shiftpath (1 - a) (shiftpath a g))" and S = "{0<..<1}-s"]])
1.9        using s g assms x
1.10        apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath
1.11                          vector_derivative_within_interior vector_derivative_works [symmetric])
1.12 @@ -4453,7 +4453,7 @@
1.13      case True then show ?thesis
1.15        apply (rule Lim_transform_away_within [of _ "z+1" _ "\<lambda>w::complex. (f w - f z)/(w - z)"])
1.16 -      using has_field_derivative_at_within DERIV_within_iff f'
1.17 +      using has_field_derivative_at_within has_field_derivative_iff f'
1.19        done
1.20    next
1.21 @@ -5554,7 +5554,7 @@
1.22      apply (rule w)
1.23      done
1.24    show ?thes2
1.25 -    apply (simp add: DERIV_within_iff del: power_Suc)
1.26 +    apply (simp add: has_field_derivative_iff del: power_Suc)
1.27      apply (rule Lim_transform_within [OF tendsto_mult_left [OF *] \<open>0 < d\<close> ])
1.28      apply (simp add: \<open>k \<noteq> 0\<close> **)
1.29      done
```
```     2.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun May 20 22:04:46 2018 +0200
2.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun May 20 22:10:30 2018 +0100
2.3 @@ -17,7 +17,7 @@
2.4  lemma has_derivative_mult_right:
2.5    fixes c:: "'a :: real_normed_algebra"
2.6    shows "((( * ) c) has_derivative (( * ) c)) F"
2.7 -by (rule has_derivative_mult_right [OF has_derivative_id])
2.8 +by (rule has_derivative_mult_right [OF has_derivative_ident])
2.9
2.10  lemma has_derivative_of_real[derivative_intros, simp]:
2.11    "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_derivative (\<lambda>x. of_real (f' x))) F"
2.12 @@ -382,7 +382,7 @@
2.13  lemma holomorphic_on_Un [holomorphic_intros]:
2.14    assumes "f holomorphic_on A" "f holomorphic_on B" "open A" "open B"
2.15    shows   "f holomorphic_on (A \<union> B)"
2.16 -  using assms by (auto simp: holomorphic_on_def  at_within_open[of _ A]
2.17 +  using assms by (auto simp: holomorphic_on_def  at_within_open[of _ A]
2.18                               at_within_open[of _ B]  at_within_open[of _ "A \<union> B"] open_Un)
2.19
2.20  lemma holomorphic_on_If_Un [holomorphic_intros]:
2.21 @@ -839,10 +839,10 @@
2.22    show ?thesis
2.23      unfolding has_field_derivative_def
2.24    proof (rule has_derivative_sequence [OF cvs _ _ x])
2.25 -  show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
2.26 -    by (rule tf)
2.27 -  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"
2.28 -    by (blast intro: **)
2.29 +    show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
2.30 +      by (rule tf)
2.31 +  next show "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
2.32 +      unfolding eventually_sequentially by (blast intro: **)
2.33    qed (metis has_field_derivative_def df)
2.34  qed
2.35
2.36 @@ -882,8 +882,8 @@
2.37        by (metis df has_field_derivative_def mult_commute_abs)
2.38    next show " ((\<lambda>n. f n x) sums l)"
2.39      by (rule sf)
2.40 -  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"
2.41 -    by (blast intro: **)
2.42 +  next show "\<And>e. e>0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
2.43 +      unfolding eventually_sequentially by (blast intro: **)
2.44    qed
2.45  qed
2.46
2.47 @@ -922,10 +922,8 @@
2.48        and "x \<in> s"  "y \<in> s"
2.49      shows "norm(f x - f y) \<le> B * norm(x - y)"
2.50    apply (rule differentiable_bound [OF cvs])
2.51 -  apply (rule ballI, erule df [unfolded has_field_derivative_def])
2.52 -  apply (rule ballI, rule onorm_le, simp add: norm_mult mult_right_mono dn)
2.53 -  apply fact
2.54 -  apply fact
2.55 +  apply (erule df [unfolded has_field_derivative_def])
2.56 +  apply (rule onorm_le, simp_all add: norm_mult mult_right_mono assms)
2.57    done
2.58
2.59  subsection\<open>Inverse function theorem for complex derivatives\<close>
```
```     3.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Sun May 20 22:04:46 2018 +0200
3.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Sun May 20 22:10:30 2018 +0100
3.3 @@ -864,7 +864,7 @@
3.4    proof -
3.5      define h where [abs_def]: "h z = (z - \<xi>)^2 * f z" for z
3.6      have h0: "(h has_field_derivative 0) (at \<xi>)"
3.7 -      apply (simp add: h_def Derivative.DERIV_within_iff)
3.8 +      apply (simp add: h_def has_field_derivative_iff)
3.9        apply (rule Lim_transform_within [OF that, of 1])
3.10        apply (auto simp: divide_simps power2_eq_square)
3.11        done
3.12 @@ -879,7 +879,7 @@
3.13          case False
3.14          then have "f field_differentiable at z within S"
3.15            using holomorphic_onD [OF holf, of z] \<open>z \<in> S\<close>
3.16 -          unfolding field_differentiable_def DERIV_within_iff
3.17 +          unfolding field_differentiable_def has_field_derivative_iff
3.18            by (force intro: exI [where x="dist \<xi> z"] elim: Lim_transform_within_set [unfolded eventually_at])
3.19          then show ?thesis
3.20            by (simp add: h_def power2_eq_square derivative_intros)
3.21 @@ -1719,7 +1719,7 @@
3.22    have "cnj \<circ> f \<circ> cnj field_differentiable at x within S \<inter> {z. Im z < 0}"
3.23          if "x \<in> S" "Im x < 0" "f field_differentiable at (cnj x) within S \<inter> {z. 0 < Im z}" for x
3.24      using that
3.25 -    apply (simp add: field_differentiable_def Derivative.DERIV_within_iff Lim_within dist_norm, clarify)
3.26 +    apply (simp add: field_differentiable_def has_field_derivative_iff Lim_within dist_norm, clarify)
3.27      apply (rule_tac x="cnj f'" in exI)
3.28      apply (elim all_forward ex_forward conj_forward imp_forward asm_rl, clarify)
3.29      apply (drule_tac x="cnj xa" in bspec)
```
```     4.1 --- a/src/HOL/Analysis/Derivative.thy	Sun May 20 22:04:46 2018 +0200
4.2 +++ b/src/HOL/Analysis/Derivative.thy	Sun May 20 22:10:30 2018 +0100
4.3 @@ -1,6 +1,6 @@
4.4  (*  Title:      HOL/Analysis/Derivative.thy
4.5      Author:     John Harrison
4.6 -    Author:     Robert Himmelmann, TU Muenchen (translation from HOL Light)
4.7 +    Author:     Robert Himmelmann, TU Muenchen (translation from HOL Light); tidied by LCP
4.8  *)
4.9
4.10  section \<open>Multivariate calculus in Euclidean space\<close>
4.11 @@ -15,18 +15,6 @@
4.12
4.13  subsection \<open>Derivatives\<close>
4.14
4.15 -subsubsection \<open>Combining theorems\<close>
4.16 -
4.17 -lemmas has_derivative_id = has_derivative_ident
4.18 -lemmas has_derivative_neg = has_derivative_minus
4.19 -lemmas has_derivative_sub = has_derivative_diff
4.20 -lemmas scaleR_right_has_derivative = has_derivative_scaleR_right
4.21 -lemmas scaleR_left_has_derivative = has_derivative_scaleR_left
4.22 -lemmas inner_right_has_derivative = has_derivative_inner_right
4.23 -lemmas inner_left_has_derivative = has_derivative_inner_left
4.24 -lemmas mult_right_has_derivative = has_derivative_mult_right
4.25 -lemmas mult_left_has_derivative = has_derivative_mult_left
4.26 -
4.28    "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
4.29    by (intro derivative_eq_intros) auto
4.30 @@ -34,20 +22,6 @@
4.31
4.32  subsection \<open>Derivative with composed bilinear function\<close>
4.33
4.34 -lemma has_derivative_bilinear_within:
4.35 -  assumes "(f has_derivative f') (at x within s)"
4.36 -    and "(g has_derivative g') (at x within s)"
4.37 -    and "bounded_bilinear h"
4.38 -  shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)"
4.39 -  using bounded_bilinear.FDERIV[OF assms(3,1,2)] .
4.40 -
4.41 -lemma has_derivative_bilinear_at:
4.42 -  assumes "(f has_derivative f') (at x)"
4.43 -    and "(g has_derivative g') (at x)"
4.44 -    and "bounded_bilinear h"
4.45 -  shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
4.46 -  using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
4.47 -
4.48  text \<open>More explicit epsilon-delta forms.\<close>
4.49
4.50  lemma has_derivative_within':
4.51 @@ -56,15 +30,14 @@
4.52      (\<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
4.53        norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
4.54    unfolding has_derivative_within Lim_within dist_norm
4.55 -  unfolding diff_0_right
4.57
4.58  lemma has_derivative_at':
4.59 -  "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and>
4.60 -    (\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
4.61 -      norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
4.62 -  using has_derivative_within' [of f f' x UNIV]
4.63 -  by simp
4.64 +  "(f has_derivative f') (at x)
4.65 +   \<longleftrightarrow> bounded_linear f' \<and>
4.66 +       (\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
4.67 +        norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
4.68 +  using has_derivative_within' [of f f' x UNIV] by simp
4.69
4.70  lemma has_derivative_at_withinI:
4.71    "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
4.72 @@ -80,7 +53,7 @@
4.73    fixes f :: "real \<Rightarrow> real"
4.74      and y :: "real"
4.75    shows "(f has_derivative (( * ) y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
4.76 -    ((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x <..} \<inter> I))"
4.77 +         ((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x <..} \<inter> I))"
4.78  proof -
4.79    have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
4.80      ((\<lambda>t. (f t - f x) / (t - x) - y) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I))"
4.81 @@ -95,8 +68,6 @@
4.82
4.83  subsubsection \<open>Caratheodory characterization\<close>
4.84
4.85 -lemmas DERIV_within_iff = has_field_derivative_iff
4.86 -
4.87  lemma DERIV_caratheodory_within:
4.88    "(f has_field_derivative l) (at x within S) \<longleftrightarrow>
4.89     (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within S) g \<and> g x = l)"
4.90 @@ -108,7 +79,7 @@
4.91      let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
4.92      show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
4.93      show "continuous (at x within S) ?g" using \<open>?lhs\<close>
4.94 -      by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
4.95 +      by (auto simp add: continuous_within has_field_derivative_iff cong: Lim_cong_within)
4.96      show "?g x = l" by simp
4.97    qed
4.98  next
4.99 @@ -116,7 +87,7 @@
4.100    then obtain g where
4.101      "(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within S) g" and "g x = l" by blast
4.102    thus ?lhs
4.103 -    by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
4.104 +    by (auto simp add: continuous_within has_field_derivative_iff cong: Lim_cong_within)
4.105  qed
4.106
4.107  subsection \<open>Differentiability\<close>
4.108 @@ -173,7 +144,7 @@
4.109  lemma differentiable_on_mult [simp, derivative_intros]:
4.110    fixes f :: "'M::real_normed_vector \<Rightarrow> 'a::real_normed_algebra"
4.111    shows "\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>z. f z * g z) differentiable_on S"
4.112 -  apply (simp add: differentiable_on_def differentiable_def)
4.113 +  unfolding differentiable_on_def differentiable_def
4.114    using differentiable_def differentiable_mult by blast
4.115
4.116  lemma differentiable_on_compose:
4.117 @@ -211,9 +182,9 @@
4.118    by (blast intro: differentiable_scaleR)
4.119
4.120  lemma has_derivative_sqnorm_at [derivative_intros, simp]:
4.121 -   "((\<lambda>x. (norm x)\<^sup>2) has_derivative (\<lambda>x. 2 *\<^sub>R (a \<bullet> x))) (at a)"
4.122 -using has_derivative_bilinear_at [of id id a id id "(\<bullet>)"]
4.123 -by (auto simp: inner_commute dot_square_norm bounded_bilinear_inner)
4.124 +  "((\<lambda>x. (norm x)\<^sup>2) has_derivative (\<lambda>x. 2 *\<^sub>R (a \<bullet> x))) (at a)"
4.125 +  using bounded_bilinear.FDERIV  [of "(\<bullet>)" id id a _ id id]
4.126 +  by (auto simp: inner_commute dot_square_norm bounded_bilinear_inner)
4.127
4.128  lemma differentiable_sqnorm_at [derivative_intros, simp]:
4.129    fixes a :: "'a :: {real_normed_vector,real_inner}"
4.130 @@ -378,29 +349,24 @@
4.131
4.132  lemma frechet_derivative_unique_within:
4.133    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
4.134 -  assumes "(f has_derivative f') (at x within S)"
4.135 -    and "(f has_derivative f'') (at x within S)"
4.136 -    and "\<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"
4.137 +  assumes 1: "(f has_derivative f') (at x within S)"
4.138 +    and 2: "(f has_derivative f'') (at x within S)"
4.139 +    and S: "\<And>i e. \<lbrakk>i\<in>Basis; e>0\<rbrakk> \<Longrightarrow> \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> (x + d *\<^sub>R i) \<in> S"
4.140    shows "f' = f''"
4.141  proof -
4.142    note as = assms(1,2)[unfolded has_derivative_def]
4.143    then interpret f': bounded_linear f' by auto
4.144    from as interpret f'': bounded_linear f'' by auto
4.145    have "x islimpt S" unfolding islimpt_approachable
4.146 -  proof (rule, rule)
4.147 +  proof (intro allI impI)
4.148      fix e :: real
4.149      assume "e > 0"
4.150      obtain d where "0 < \<bar>d\<bar>" and "\<bar>d\<bar> < e" and "x + d *\<^sub>R (SOME i. i \<in> Basis) \<in> S"
4.151        using assms(3) SOME_Basis \<open>e>0\<close> by blast
4.152      then show "\<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
4.153 -      apply (rule_tac x="x + d *\<^sub>R (SOME i. i \<in> Basis)" in bexI)
4.154 -      unfolding dist_norm
4.155 -      apply (auto simp: SOME_Basis nonzero_Basis)
4.156 -      done
4.157 -  qed
4.158 +      by (rule_tac x="x + d *\<^sub>R (SOME i. i \<in> Basis)" in bexI) (auto simp: dist_norm SOME_Basis nonzero_Basis)  qed
4.159    then have *: "netlimit (at x within S) = x"
4.160 -    apply (auto intro!: netlimit_within)
4.161 -    by (metis trivial_limit_within)
4.162 +    by (simp add: Lim_ident_at trivial_limit_within)
4.163    show ?thesis
4.164    proof (rule linear_eq_stdbasis)
4.165      show "linear f'" "linear f''"
4.166 @@ -450,81 +416,65 @@
4.167
4.168  lemma frechet_derivative_unique_within_closed_interval:
4.169    fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
4.170 -  assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
4.171 -    and "x \<in> cbox a b"
4.172 +  assumes ab: "\<And>i. i\<in>Basis \<Longrightarrow> a\<bullet>i < b\<bullet>i"
4.173 +    and x: "x \<in> cbox a b"
4.174      and "(f has_derivative f' ) (at x within cbox a b)"
4.175      and "(f has_derivative f'') (at x within cbox a b)"
4.176    shows "f' = f''"
4.177 -  apply(rule frechet_derivative_unique_within)
4.178 -  apply(rule assms(3,4))+
4.179 -proof (rule, rule, rule)
4.180 +proof (rule frechet_derivative_unique_within)
4.181    fix e :: real
4.182    fix i :: 'a
4.183    assume "e > 0" and i: "i \<in> Basis"
4.184    then show "\<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> cbox a b"
4.185    proof (cases "x\<bullet>i = a\<bullet>i")
4.186      case True
4.187 -    then show ?thesis
4.188 -      apply (rule_tac x="(min (b\<bullet>i - a\<bullet>i)  e) / 2" in exI)
4.189 -      using assms(1)[THEN bspec[where x=i]] and \<open>e>0\<close> and assms(2)
4.190 -      unfolding mem_box
4.191 -      using i
4.192 -      apply (auto simp add: field_simps inner_simps inner_Basis)
4.193 -      done
4.194 +    with ab[of i] \<open>e>0\<close> x i show ?thesis
4.195 +      by (rule_tac x="(min (b\<bullet>i - a\<bullet>i) e) / 2" in exI)
4.196 +         (auto simp add: mem_box field_simps inner_simps inner_Basis)
4.197    next
4.198 -    note * = assms(2)[unfolded mem_box, THEN bspec, OF i]
4.199      case False
4.200      moreover have "a \<bullet> i < x \<bullet> i"
4.201 -      using False * by auto
4.202 +      using False i mem_box(2) x by force
4.203      moreover {
4.204        have "a \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e \<le> a\<bullet>i *2 + x\<bullet>i - a\<bullet>i"
4.205          by auto
4.206        also have "\<dots> = a\<bullet>i + x\<bullet>i"
4.207          by auto
4.208        also have "\<dots> \<le> 2 * (x\<bullet>i)"
4.209 -        using * by auto
4.210 +        using \<open>a \<bullet> i < x \<bullet> i\<close> by auto
4.211        finally have "a \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e \<le> x \<bullet> i * 2"
4.212          by auto
4.213      }
4.214      moreover have "min (x \<bullet> i - a \<bullet> i) e \<ge> 0"
4.215 -      using * and \<open>e>0\<close> by auto
4.216 +      by (simp add: \<open>0 < e\<close> \<open>a \<bullet> i < x \<bullet> i\<close> less_eq_real_def)
4.217      then have "x \<bullet> i * 2 \<le> b \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e"
4.218 -      using * by auto
4.219 +      using i mem_box(2) x by force
4.220      ultimately show ?thesis
4.221 -      apply (rule_tac x="- (min (x\<bullet>i - a\<bullet>i) e) / 2" in exI)
4.222 -      using assms(1)[THEN bspec, OF i] and \<open>e>0\<close> and assms(2)
4.223 -      unfolding mem_box
4.224 -      using i
4.225 -      apply (auto simp add: field_simps inner_simps inner_Basis)
4.226 -      done
4.227 +    using ab[of i] \<open>e>0\<close> x i
4.228 +      by (rule_tac x="- (min (x\<bullet>i - a\<bullet>i) e) / 2" in exI)
4.229 +         (auto simp add: mem_box field_simps inner_simps inner_Basis)
4.230    qed
4.231 -qed
4.232 +qed (use assms in auto)
4.233
4.234  lemma frechet_derivative_unique_within_open_interval:
4.235    fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
4.236 -  assumes "x \<in> box a b"
4.237 -    and "(f has_derivative f' ) (at x within box a b)"
4.238 -    and "(f has_derivative f'') (at x within box a b)"
4.239 +  assumes x: "x \<in> box a b"
4.240 +    and f: "(f has_derivative f' ) (at x within box a b)" "(f has_derivative f'') (at x within box a b)"
4.241    shows "f' = f''"
4.242  proof -
4.243 -  from assms(1) have *: "at x within box a b = at x"
4.244 -    by (metis at_within_interior interior_open open_box)
4.245 -  from assms(2,3) [unfolded *] show "f' = f''"
4.246 -    by (rule has_derivative_unique)
4.247 +  have "at x within box a b = at x"
4.248 +    by (metis x at_within_interior interior_open open_box)
4.249 +  with f show "f' = f''"
4.250 +    by (simp add: has_derivative_unique)
4.251  qed
4.252
4.253  lemma frechet_derivative_at:
4.254    "(f has_derivative f') (at x) \<Longrightarrow> f' = frechet_derivative f (at x)"
4.255 -  apply (rule has_derivative_unique[of f])
4.256 -  apply assumption
4.257 -  unfolding frechet_derivative_works[symmetric]
4.258 -  using differentiable_def
4.259 -  apply auto
4.260 -  done
4.261 +  using differentiable_def frechet_derivative_works has_derivative_unique by blast
4.262
4.263  lemma frechet_derivative_within_cbox:
4.264    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
4.265 -  assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
4.266 +  assumes "\<And>i. i\<in>Basis \<Longrightarrow> a\<bullet>i < b\<bullet>i"
4.267      and "x \<in> cbox a b"
4.268      and "(f has_derivative f') (at x within cbox a b)"
4.269    shows "frechet_derivative f (at x within cbox a b) = f'"
4.270 @@ -547,7 +497,7 @@
4.271      using deriv by (rule has_derivative_bounded_linear)
4.272    show "f' h = 0"
4.273    proof (cases "h = 0")
4.274 -    assume "h \<noteq> 0"
4.275 +    case False
4.276      from min obtain d where d1: "0 < d" and d2: "\<forall>y\<in>ball x d. f x \<le> f y"
4.277        unfolding eventually_at by (force simp: dist_commute)
4.278      have "FDERIV (\<lambda>r. x + r *\<^sub>R h) 0 :> (\<lambda>r. r *\<^sub>R h)"
4.279 @@ -561,7 +511,7 @@
4.280        using \<open>h \<noteq> 0\<close> by (auto simp add: d2 dist_norm pos_less_divide_eq)
4.281      ultimately show "f' h = 0"
4.282        by (rule DERIV_local_min)
4.283 -  qed (simp add: f'.zero)
4.284 +  qed simp
4.285  qed
4.286
4.287  lemma has_derivative_local_max:
4.288 @@ -574,21 +524,21 @@
4.289
4.290  lemma differential_zero_maxmin:
4.291    fixes f::"'a::real_normed_vector \<Rightarrow> real"
4.292 -  assumes "x \<in> s"
4.293 -    and "open s"
4.294 +  assumes "x \<in> S"
4.295 +    and "open S"
4.296      and deriv: "(f has_derivative f') (at x)"
4.297 -    and mono: "(\<forall>y\<in>s. f y \<le> f x) \<or> (\<forall>y\<in>s. f x \<le> f y)"
4.298 +    and mono: "(\<forall>y\<in>S. f y \<le> f x) \<or> (\<forall>y\<in>S. f x \<le> f y)"
4.299    shows "f' = (\<lambda>v. 0)"
4.300    using mono
4.301  proof
4.302 -  assume "\<forall>y\<in>s. f y \<le> f x"
4.303 -  with \<open>x \<in> s\<close> and \<open>open s\<close> have "eventually (\<lambda>y. f y \<le> f x) (at x)"
4.304 +  assume "\<forall>y\<in>S. f y \<le> f x"
4.305 +  with \<open>x \<in> S\<close> and \<open>open S\<close> have "eventually (\<lambda>y. f y \<le> f x) (at x)"
4.306      unfolding eventually_at_topological by auto
4.307    with deriv show ?thesis
4.308      by (rule has_derivative_local_max)
4.309  next
4.310 -  assume "\<forall>y\<in>s. f x \<le> f y"
4.311 -  with \<open>x \<in> s\<close> and \<open>open s\<close> have "eventually (\<lambda>y. f x \<le> f y) (at x)"
4.312 +  assume "\<forall>y\<in>S. f x \<le> f y"
4.313 +  with \<open>x \<in> S\<close> and \<open>open S\<close> have "eventually (\<lambda>y. f x \<le> f y) (at x)"
4.314      unfolding eventually_at_topological by auto
4.315    with deriv show ?thesis
4.316      by (rule has_derivative_local_min)
4.317 @@ -613,28 +563,24 @@
4.318      unfolding fun_eq_iff by simp
4.319  qed
4.320
4.321 -lemma rolle:
4.322 +theorem Rolle:
4.323    fixes f :: "real \<Rightarrow> real"
4.324    assumes "a < b"
4.325 -    and "f a = f b"
4.326 -    and "continuous_on {a .. b} f"
4.327 -    and "\<forall>x\<in>{a <..< b}. (f has_derivative f' x) (at x)"
4.328 +    and fab: "f a = f b"
4.329 +    and contf: "continuous_on {a..b} f"
4.330 +    and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
4.331    shows "\<exists>x\<in>{a <..< b}. f' x = (\<lambda>v. 0)"
4.332  proof -
4.333    have "\<exists>x\<in>box a b. (\<forall>y\<in>box a b. f x \<le> f y) \<or> (\<forall>y\<in>box a b. f y \<le> f x)"
4.334    proof -
4.335 -    have "(a + b) / 2 \<in> {a .. b}"
4.336 +    have "(a + b) / 2 \<in> {a..b}"
4.337        using assms(1) by auto
4.338 -    then have *: "{a .. b} \<noteq> {}"
4.339 +    then have *: "{a..b} \<noteq> {}"
4.340        by auto
4.341 -    obtain d where d:
4.342 -        "d \<in>cbox a b"
4.343 -        "\<forall>y\<in>cbox a b. f y \<le> f d"
4.344 -      using continuous_attains_sup[OF compact_Icc * assms(3)] by auto
4.345 -    obtain c where c:
4.346 -        "c \<in> cbox a b"
4.347 -        "\<forall>y\<in>cbox a b. f c \<le> f y"
4.348 -      using continuous_attains_inf[OF compact_Icc * assms(3)] by auto
4.349 +    obtain d where d: "d \<in>cbox a b" "\<forall>y\<in>cbox a b. f y \<le> f d"
4.350 +      using continuous_attains_sup[OF compact_Icc * contf] by auto
4.351 +    obtain c where c: "c \<in> cbox a b" "\<forall>y\<in>cbox a b. f c \<le> f y"
4.352 +      using continuous_attains_inf[OF compact_Icc * contf] by auto
4.353      show ?thesis
4.354      proof (cases "d \<in> box a b \<or> c \<in> box a b")
4.355        case True
4.356 @@ -644,16 +590,11 @@
4.357        define e where "e = (a + b) /2"
4.358        case False
4.359        then have "f d = f c"
4.360 -        using d c assms(2) by auto
4.361 -      then have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d"
4.362 -        using c d
4.363 +        using d c fab by auto
4.364 +      with c d have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d"
4.365          by force
4.366        then show ?thesis
4.367 -        apply (rule_tac x=e in bexI)
4.368 -        unfolding e_def
4.369 -        using assms(1)
4.370 -        apply auto
4.371 -        done
4.372 +        by (rule_tac x=e in bexI) (auto simp: e_def \<open>a < b\<close>)
4.373      qed
4.374    qed
4.375    then obtain x where x: "x \<in> {a <..< b}" "(\<forall>y\<in>{a <..< b}. f x \<le> f y) \<or> (\<forall>y\<in>{a <..< b}. f y \<le> f x)"
4.376 @@ -673,18 +614,18 @@
4.377  lemma mvt:
4.378    fixes f :: "real \<Rightarrow> real"
4.379    assumes "a < b"
4.380 -    and "continuous_on {a..b} f"
4.381 -  assumes "\<forall>x\<in>{a<..<b}. (f has_derivative (f' x)) (at x)"
4.382 +    and contf: "continuous_on {a..b} f"
4.383 +    and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
4.384    shows "\<exists>x\<in>{a<..<b}. f b - f a = (f' x) (b - a)"
4.385  proof -
4.386    have "\<exists>x\<in>{a <..< b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
4.387 -  proof (intro rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
4.388 +  proof (intro Rolle[OF \<open>a < b\<close>, of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
4.389      fix x
4.390 -    assume x: "x \<in> {a <..< b}"
4.391 +    assume x: "a < x" "x < b"
4.392      show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative
4.393          (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
4.394 -      by (intro derivative_intros assms(3)[rule_format,OF x])
4.395 -  qed (insert assms(1,2), auto intro!: continuous_intros simp: field_simps)
4.396 +      by (intro derivative_intros derf[OF x])
4.397 +  qed (use assms in \<open>auto intro!: continuous_intros simp: field_simps\<close>)
4.398    then obtain x where
4.399      "x \<in> {a <..< b}"
4.400      "(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
4.401 @@ -697,50 +638,33 @@
4.402  lemma mvt_simple:
4.403    fixes f :: "real \<Rightarrow> real"
4.404    assumes "a < b"
4.405 -    and "\<forall>x\<in>{a..b}. (f has_derivative f' x) (at x within {a..b})"
4.406 +    and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x within {a..b})"
4.407    shows "\<exists>x\<in>{a<..<b}. f b - f a = f' x (b - a)"
4.408  proof (rule mvt)
4.409    have "f differentiable_on {a..b}"
4.410 -    using assms(2) unfolding differentiable_on_def differentiable_def by fast
4.411 +    using derf unfolding differentiable_on_def differentiable_def by force
4.412    then show "continuous_on {a..b} f"
4.413      by (rule differentiable_imp_continuous_on)
4.414 -  show "\<forall>x\<in>{a<..<b}. (f has_derivative f' x) (at x)"
4.415 -  proof
4.416 -    fix x
4.417 -    assume x: "x \<in> {a <..< b}"
4.418 -    show "(f has_derivative f' x) (at x)"
4.419 -      unfolding at_within_open[OF x open_greaterThanLessThan,symmetric]
4.420 -      apply (rule has_derivative_within_subset)
4.421 -      apply (rule assms(2)[rule_format])
4.422 -      using x
4.423 -      apply auto
4.424 -      done
4.425 -  qed
4.426 -qed (rule assms(1))
4.427 +  show "(f has_derivative f' x) (at x)" if "a < x" "x < b" for x
4.428 +    by (metis at_within_Icc_at derf leI order.asym that)
4.429 +qed (rule assms)
4.430
4.431  lemma mvt_very_simple:
4.432    fixes f :: "real \<Rightarrow> real"
4.433    assumes "a \<le> b"
4.434 -    and "\<forall>x\<in>{a .. b}. (f has_derivative f' x) (at x within {a .. b})"
4.435 -  shows "\<exists>x\<in>{a .. b}. f b - f a = f' x (b - a)"
4.436 +    and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x within {a..b})"
4.437 +  shows "\<exists>x\<in>{a..b}. f b - f a = f' x (b - a)"
4.438  proof (cases "a = b")
4.439    interpret bounded_linear "f' b"
4.440      using assms(2) assms(1) by auto
4.441    case True
4.442    then show ?thesis
4.443 -    apply (rule_tac x=a in bexI)
4.444 -    using assms(2)[THEN bspec[where x=a]]
4.445 -    unfolding has_derivative_def
4.446 -    unfolding True
4.447 -    using zero
4.448 -    apply auto
4.449 -    done
4.450 +    by force
4.451  next
4.452    case False
4.453    then show ?thesis
4.454 -    using mvt_simple[OF _ assms(2)]
4.455 -    using assms(1)
4.456 -    by auto
4.457 +    using mvt_simple[OF _ derf]
4.458 +    by (metis \<open>a \<le> b\<close> atLeastAtMost_iff dual_order.order_iff_strict greaterThanLessThan_iff)
4.459  qed
4.460
4.461  text \<open>A nice generalization (see Havin's proof of 5.19 from Rudin's book).\<close>
4.462 @@ -748,19 +672,16 @@
4.463  lemma mvt_general:
4.464    fixes f :: "real \<Rightarrow> 'a::real_inner"
4.465    assumes "a < b"
4.466 -    and "continuous_on {a .. b} f"
4.467 -    and "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
4.468 +    and contf: "continuous_on {a..b} f"
4.469 +    and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
4.470    shows "\<exists>x\<in>{a<..<b}. norm (f b - f a) \<le> norm (f' x (b - a))"
4.471  proof -
4.472    have "\<exists>x\<in>{a<..<b}. (f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)"
4.473 -    apply (rule mvt)
4.474 -    apply (rule assms(1))
4.475 -    apply (intro continuous_intros assms(2))
4.476 -    using assms(3)
4.477 -    apply (fast intro: has_derivative_inner_right)
4.478 +    apply (rule mvt [OF \<open>a < b\<close>])
4.479 +    apply (intro continuous_intros contf)
4.480 +    using derf apply (blast intro: has_derivative_inner_right)
4.481      done
4.482 -  then obtain x where x:
4.483 -    "x \<in> {a<..<b}"
4.484 +  then obtain x where x: "x \<in> {a<..<b}"
4.485      "(f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)" ..
4.486    show ?thesis
4.487    proof (cases "f a = f b")
4.488 @@ -779,21 +700,18 @@
4.489    next
4.490      case True
4.491      then show ?thesis
4.492 -      using assms(1)
4.493 -      apply (rule_tac x="(a + b) /2" in bexI)
4.494 -      apply auto
4.495 -      done
4.496 +      using \<open>a < b\<close> by (rule_tac x="(a + b) /2" in bexI) auto
4.497    qed
4.498  qed
4.499
4.500
4.501  subsection \<open>More general bound theorems\<close>
4.502
4.503 -lemma differentiable_bound_general:
4.504 +proposition differentiable_bound_general:
4.505    fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
4.506    assumes "a < b"
4.507 -    and f_cont: "continuous_on {a .. b} f"
4.508 -    and phi_cont: "continuous_on {a .. b} \<phi>"
4.509 +    and f_cont: "continuous_on {a..b} f"
4.510 +    and phi_cont: "continuous_on {a..b} \<phi>"
4.511      and f': "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
4.512      and phi': "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (\<phi> has_vector_derivative \<phi>' x) (at x)"
4.513      and bnd: "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> norm (f' x) \<le> \<phi>' x"
4.514 @@ -813,7 +731,7 @@
4.515      with \<open>e > 0\<close> have "e2 > 0" by simp
4.516      let ?le = "\<lambda>x1. norm (f x1 - f a) \<le> \<phi> x1 - \<phi> a + e * (x1 - a) + e"
4.517      define A where "A = {x2. a \<le> x2 \<and> x2 \<le> b \<and> (\<forall>x1\<in>{a ..< x2}. ?le x1)}"
4.518 -    have A_subset: "A \<subseteq> {a .. b}" by (auto simp: A_def)
4.519 +    have A_subset: "A \<subseteq> {a..b}" by (auto simp: A_def)
4.520      {
4.521        fix x2
4.522        assume a: "a \<le> x2" "x2 \<le> b" and le: "\<forall>x1\<in>{a..<x2}. ?le x1"
4.523 @@ -828,7 +746,7 @@
4.524            "((\<lambda>x1. norm (f x1 - f a)) \<longlongrightarrow> norm (f x2 - f a)) (at x2 within {a <..<x2})"
4.525            using a
4.526            by (auto intro!: tendsto_eq_intros f_tendsto phi_tendsto
4.527 -            intro: tendsto_within_subset[where S="{a .. b}"])
4.528 +            intro: tendsto_within_subset[where S="{a..b}"])
4.529          moreover
4.530          have "eventually (\<lambda>x. x > a) (at x2 within {a <..<x2})"
4.531            by (auto simp: eventually_at_filter)
4.532 @@ -860,85 +778,11 @@
4.533        using y_all_le \<open>a \<le> y\<close> \<open>y \<le> b\<close>
4.534        by (auto simp: A_def)
4.535      hence "A = {a .. y}"
4.536 -      using A_subset
4.537 -      by (auto simp: subset_iff y_def cSup_upper intro: A_ivl)
4.538 +      using A_subset by (auto simp: subset_iff y_def cSup_upper intro: A_ivl)
4.539      from le_cont[OF \<open>a \<le> y\<close> \<open>y \<le> b\<close> y_all_le] have le_y: "?le y" .
4.540 -    {
4.541 -      assume "a \<noteq> y" with \<open>a \<le> y\<close> have "a < y" by simp
4.542 -      have "y = b"
4.543 -      proof (rule ccontr)
4.544 -        assume "y \<noteq> b"
4.545 -        hence "y < b" using \<open>y \<le> b\<close> by simp
4.546 -        let ?F = "at y within {y..<b}"
4.547 -        from f' phi'
4.548 -        have "(f has_vector_derivative f' y) ?F"
4.549 -          and "(\<phi> has_vector_derivative \<phi>' y) ?F"
4.550 -          using \<open>a < y\<close> \<open>y < b\<close>
4.551 -          by (auto simp add: at_within_open[of _ "{a<..<b}"] has_vector_derivative_def
4.552 -            intro!: has_derivative_subset[where s="{a<..<b}" and t="{y..<b}"])
4.553 -        hence "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y - (x1 - y) *\<^sub>R f' y) \<le> e2 * \<bar>x1 - y\<bar>"
4.554 -            "\<forall>\<^sub>F x1 in ?F. norm (\<phi> x1 - \<phi> y - (x1 - y) *\<^sub>R \<phi>' y) \<le> e2 * \<bar>x1 - y\<bar>"
4.555 -          using \<open>e2 > 0\<close>
4.556 -          by (auto simp: has_derivative_within_alt2 has_vector_derivative_def)
4.557 -        moreover
4.558 -        have "\<forall>\<^sub>F x1 in ?F. y \<le> x1" "\<forall>\<^sub>F x1 in ?F. x1 < b"
4.559 -          by (auto simp: eventually_at_filter)
4.560 -        ultimately
4.561 -        have "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y) \<le> (\<phi> x1 - \<phi> y) + e * \<bar>x1 - y\<bar>"
4.562 -          (is "\<forall>\<^sub>F x1 in ?F. ?le' x1")
4.563 -        proof eventually_elim
4.564 -          case (elim x1)
4.565 -          from norm_triangle_ineq2[THEN order_trans, OF elim(1)]
4.566 -          have "norm (f x1 - f y) \<le> norm (f' y) * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
4.567 -            by (simp add: ac_simps)
4.568 -          also have "norm (f' y) \<le> \<phi>' y" using bnd \<open>a < y\<close> \<open>y < b\<close> by simp
4.569 -          also
4.570 -          from elim have "\<phi>' y * \<bar>x1 - y\<bar> \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar>"
4.571 -            by (simp add: ac_simps)
4.572 -          finally
4.573 -          have "norm (f x1 - f y) \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
4.574 -            by (auto simp: mult_right_mono)
4.575 -          thus ?case by (simp add: e2_def)
4.576 -        qed
4.577 -        moreover have "?le' y" by simp
4.578 -        ultimately obtain S
4.579 -        where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..<b} \<Longrightarrow> ?le' x"
4.580 -          unfolding eventually_at_topological
4.581 -          by metis
4.582 -        from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
4.583 -          by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
4.584 -        define d' where "d' = min ((y + b)/2) (y + (d/2))"
4.585 -        have "d' \<in> A"
4.586 -          unfolding A_def
4.587 -        proof safe
4.588 -          show "a \<le> d'" using \<open>a < y\<close> \<open>0 < d\<close> \<open>y < b\<close> by (simp add: d'_def)
4.589 -          show "d' \<le> b" using \<open>y < b\<close> by (simp add: d'_def min_def)
4.590 -          fix x1
4.591 -          assume x1: "x1 \<in> {a..<d'}"
4.592 -          {
4.593 -            assume "x1 < y"
4.594 -            hence "?le x1"
4.595 -              using \<open>x1 \<in> {a..<d'}\<close> y_all_le by auto
4.596 -          } moreover {
4.597 -            assume "x1 \<ge> y"
4.598 -            hence x1': "x1 \<in> S" "x1 \<in> {y..<b}" using x1
4.599 -              by (auto simp: d'_def dist_real_def intro!: d)
4.600 -            have "norm (f x1 - f a) \<le> norm (f x1 - f y) + norm (f y - f a)"
4.601 -              by (rule order_trans[OF _ norm_triangle_ineq]) simp
4.602 -            also note S(3)[OF x1']
4.603 -            also note le_y
4.604 -            finally have "?le x1"
4.605 -              using \<open>x1 \<ge> y\<close> by (auto simp: algebra_simps)
4.606 -          } ultimately show "?le x1" by arith
4.607 -        qed
4.608 -        hence "d' \<le> y"
4.609 -          unfolding y_def
4.610 -          by (rule cSup_upper) simp
4.611 -        thus False using \<open>d > 0\<close> \<open>y < b\<close>
4.612 -          by (simp add: d'_def min_def split: if_split_asm)
4.613 -      qed
4.614 -    } moreover {
4.615 -      assume "a = y"
4.616 +    have "y = b"
4.617 +    proof (cases "a = y")
4.618 +      case True
4.619        with \<open>a < b\<close> have "y < b" by simp
4.620        with \<open>a = y\<close> f_cont phi_cont \<open>e2 > 0\<close>
4.621        have 1: "\<forall>\<^sub>F x in at y within {y..b}. dist (f x) (f y) < e2"
4.622 @@ -966,8 +810,7 @@
4.623          finally show "?le x1" .
4.624        qed
4.625        from this[unfolded eventually_at_topological] \<open>?le y\<close>
4.626 -      obtain S
4.627 -      where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..b} \<Longrightarrow> ?le x"
4.628 +      obtain S where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..b} \<Longrightarrow> ?le x"
4.629          by metis
4.630        from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
4.631          by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
4.632 @@ -987,81 +830,140 @@
4.633        hence "d' \<le> y"
4.634          unfolding y_def
4.635          by (rule cSup_upper) simp
4.636 -      hence "y = b" using \<open>d > 0\<close> \<open>y < b\<close>
4.637 +      then show "y = b" using \<open>d > 0\<close> \<open>y < b\<close>
4.639 -    } ultimately have "y = b"
4.640 -      by auto
4.641 +    next
4.642 +      case False
4.643 +      with \<open>a \<le> y\<close> have "a < y" by simp
4.644 +      show "y = b"
4.645 +      proof (rule ccontr)
4.646 +        assume "y \<noteq> b"
4.647 +        hence "y < b" using \<open>y \<le> b\<close> by simp
4.648 +        let ?F = "at y within {y..<b}"
4.649 +        from f' phi'
4.650 +        have "(f has_vector_derivative f' y) ?F"
4.651 +          and "(\<phi> has_vector_derivative \<phi>' y) ?F"
4.652 +          using \<open>a < y\<close> \<open>y < b\<close>
4.653 +          by (auto simp add: at_within_open[of _ "{a<..<b}"] has_vector_derivative_def
4.654 +            intro!: has_derivative_subset[where s="{a<..<b}" and t="{y..<b}"])
4.655 +        hence "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y - (x1 - y) *\<^sub>R f' y) \<le> e2 * \<bar>x1 - y\<bar>"
4.656 +            "\<forall>\<^sub>F x1 in ?F. norm (\<phi> x1 - \<phi> y - (x1 - y) *\<^sub>R \<phi>' y) \<le> e2 * \<bar>x1 - y\<bar>"
4.657 +          using \<open>e2 > 0\<close>
4.658 +          by (auto simp: has_derivative_within_alt2 has_vector_derivative_def)
4.659 +        moreover
4.660 +        have "\<forall>\<^sub>F x1 in ?F. y \<le> x1" "\<forall>\<^sub>F x1 in ?F. x1 < b"
4.661 +          by (auto simp: eventually_at_filter)
4.662 +        ultimately
4.663 +        have "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y) \<le> (\<phi> x1 - \<phi> y) + e * \<bar>x1 - y\<bar>"
4.664 +          (is "\<forall>\<^sub>F x1 in ?F. ?le' x1")
4.665 +        proof eventually_elim
4.666 +          case (elim x1)
4.667 +          from norm_triangle_ineq2[THEN order_trans, OF elim(1)]
4.668 +          have "norm (f x1 - f y) \<le> norm (f' y) * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
4.669 +            by (simp add: ac_simps)
4.670 +          also have "norm (f' y) \<le> \<phi>' y" using bnd \<open>a < y\<close> \<open>y < b\<close> by simp
4.671 +          also have "\<phi>' y * \<bar>x1 - y\<bar> \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar>"
4.672 +            using elim by (simp add: ac_simps)
4.673 +          finally
4.674 +          have "norm (f x1 - f y) \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
4.675 +            by (auto simp: mult_right_mono)
4.676 +          thus ?case by (simp add: e2_def)
4.677 +        qed
4.678 +        moreover have "?le' y" by simp
4.679 +        ultimately obtain S
4.680 +        where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..<b} \<Longrightarrow> ?le' x"
4.681 +          unfolding eventually_at_topological
4.682 +          by metis
4.683 +        from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
4.684 +          by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
4.685 +        define d' where "d' = min ((y + b)/2) (y + (d/2))"
4.686 +        have "d' \<in> A"
4.687 +          unfolding A_def
4.688 +        proof safe
4.689 +          show "a \<le> d'" using \<open>a < y\<close> \<open>0 < d\<close> \<open>y < b\<close> by (simp add: d'_def)
4.690 +          show "d' \<le> b" using \<open>y < b\<close> by (simp add: d'_def min_def)
4.691 +          fix x1
4.692 +          assume x1: "x1 \<in> {a..<d'}"
4.693 +          show "?le x1"
4.694 +          proof (cases "x1 < y")
4.695 +            case True
4.696 +            then show ?thesis
4.697 +              using \<open>y \<in> A\<close> local.leI x1 by auto
4.698 +          next
4.699 +            case False
4.700 +            hence x1': "x1 \<in> S" "x1 \<in> {y..<b}" using x1
4.701 +              by (auto simp: d'_def dist_real_def intro!: d)
4.702 +            have "norm (f x1 - f a) \<le> norm (f x1 - f y) + norm (f y - f a)"
4.703 +              by (rule order_trans[OF _ norm_triangle_ineq]) simp
4.704 +            also note S(3)[OF x1']
4.705 +            also note le_y
4.706 +            finally show "?le x1"
4.707 +              using False by (auto simp: algebra_simps)
4.708 +          qed
4.709 +        qed
4.710 +        hence "d' \<le> y"
4.711 +          unfolding y_def by (rule cSup_upper) simp
4.712 +        thus False using \<open>d > 0\<close> \<open>y < b\<close>
4.713 +          by (simp add: d'_def min_def split: if_split_asm)
4.714 +      qed
4.715 +    qed
4.716      with le_y have "norm (f b - f a) \<le> \<phi> b - \<phi> a + e * (b - a + 1)"
4.718    } note * = this
4.719 -  {
4.720 +  show ?thesis
4.721 +  proof (rule field_le_epsilon)
4.722      fix e::real assume "e > 0"
4.723 -    hence "norm (f b - f a) \<le> \<phi> b - \<phi> a + e"
4.724 +    then show "norm (f b - f a) \<le> \<phi> b - \<phi> a + e"
4.725        using *[of "e / (b - a + 1)"] \<open>a < b\<close> by simp
4.726 -  } thus ?thesis
4.727 -    by (rule field_le_epsilon)
4.728 +  qed
4.729  qed
4.730
4.731  lemma differentiable_bound:
4.732    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
4.733 -  assumes "convex s"
4.734 -    and "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)"
4.735 -    and "\<forall>x\<in>s. onorm (f' x) \<le> B"
4.736 -    and x: "x \<in> s"
4.737 -    and y: "y \<in> s"
4.738 +  assumes "convex S"
4.739 +    and derf: "\<And>x. x\<in>S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
4.740 +    and B: "\<And>x. x \<in> S \<Longrightarrow> onorm (f' x) \<le> B"
4.741 +    and x: "x \<in> S"
4.742 +    and y: "y \<in> S"
4.743    shows "norm (f x - f y) \<le> B * norm (x - y)"
4.744  proof -
4.745    let ?p = "\<lambda>u. x + u *\<^sub>R (y - x)"
4.746    let ?\<phi> = "\<lambda>h. h * B * norm (x - y)"
4.747 -  have *: "\<And>u. u\<in>{0..1} \<Longrightarrow> x + u *\<^sub>R (y - x) \<in> s"
4.748 -    using assms(1)[unfolded convex_alt,rule_format,OF x y]
4.749 -    unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib
4.750 -    by (auto simp add: algebra_simps)
4.751 -  have 0: "continuous_on (?p ` {0..1}) f"
4.752 -    using *
4.753 +  have *: "x + u *\<^sub>R (y - x) \<in> S" if "u \<in> {0..1}" for u
4.754 +  proof -
4.755 +    have "u *\<^sub>R y = u *\<^sub>R (y - x) + u *\<^sub>R x"
4.756 +      by (simp add: scale_right_diff_distrib)
4.757 +    then show "x + u *\<^sub>R (y - x) \<in> S"
4.758 +      using that \<open>convex S\<close> unfolding convex_alt by (metis (no_types) atLeastAtMost_iff linordered_field_class.sign_simps(2) pth_c(3) scaleR_collapse x y)
4.759 +  qed
4.760 +  have "\<And>z. z \<in> (\<lambda>u. x + u *\<^sub>R (y - x)) ` {0..1} \<Longrightarrow>
4.761 +          (f has_derivative f' z) (at z within (\<lambda>u. x + u *\<^sub>R (y - x)) ` {0..1})"
4.762 +    by (auto intro: * has_derivative_within_subset [OF derf])
4.763 +  then have "continuous_on (?p ` {0..1}) f"
4.764      unfolding continuous_on_eq_continuous_within
4.765 -    apply -
4.766 -    apply rule
4.767 -    apply (rule differentiable_imp_continuous_within)
4.768 -    unfolding differentiable_def
4.769 -    apply (rule_tac x="f' xa" in exI)
4.770 -    apply (rule has_derivative_within_subset)
4.771 -    apply (rule assms(2)[rule_format])
4.772 -    apply auto
4.773 -    done
4.774 -  from * have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
4.775 -    by (intro continuous_intros 0)+
4.776 +    by (meson has_derivative_continuous)
4.777 +  with * have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
4.778 +    by (intro continuous_intros)+
4.779    {
4.780      fix u::real assume u: "u \<in>{0 <..< 1}"
4.781      let ?u = "?p u"
4.782      interpret linear "(f' ?u)"
4.783 -      using u by (auto intro!: has_derivative_linear assms(2)[rule_format] *)
4.784 +      using u by (auto intro!: has_derivative_linear derf *)
4.785      have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within box 0 1)"
4.786 -      apply (rule diff_chain_within)
4.787 -      apply (rule derivative_intros)+
4.788 -      apply (rule has_derivative_within_subset)
4.789 -      apply (rule assms(2)[rule_format])
4.790 -      using u *
4.791 -      apply auto
4.792 -      done
4.793 +      by (intro derivative_intros has_derivative_within_subset [OF derf]) (use u * in auto)
4.794      hence "((f \<circ> ?p) has_vector_derivative f' ?u (y - x)) (at u)"
4.795        by (simp add: has_derivative_within_open[OF u open_greaterThanLessThan]
4.796          scaleR has_vector_derivative_def o_def)
4.797    } note 2 = this
4.798 -  {
4.799 -    have "continuous_on {0..1} ?\<phi>"
4.800 -      by (rule continuous_intros)+
4.801 -  } note 3 = this
4.802 -  {
4.803 -    fix u::real assume u: "u \<in>{0 <..< 1}"
4.804 -    have "(?\<phi> has_vector_derivative B * norm (x - y)) (at u)"
4.805 -      by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
4.806 -  } note 4 = this
4.807 +  have 3: "continuous_on {0..1} ?\<phi>"
4.808 +    by (rule continuous_intros)+
4.809 +  have 4: "(?\<phi> has_vector_derivative B * norm (x - y)) (at u)" for u
4.810 +    by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
4.811    {
4.812      fix u::real assume u: "u \<in>{0 <..< 1}"
4.813      let ?u = "?p u"
4.814      interpret bounded_linear "(f' ?u)"
4.815 -      using u by (auto intro!: has_derivative_bounded_linear assms(2)[rule_format] *)
4.816 +      using u by (auto intro!: has_derivative_bounded_linear derf *)
4.817      have "norm (f' ?u (y - x)) \<le> onorm (f' ?u) * norm (y - x)"
4.818        by (rule onorm) (rule bounded_linear)
4.819      also have "onorm (f' ?u) \<le> B"
4.820 @@ -1083,7 +985,7 @@
4.821    fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
4.822    assumes "\<And>t. t \<in> {0..1} \<Longrightarrow> x0 + t *\<^sub>R a \<in> G"
4.823    assumes f': "\<And>x. x \<in> G \<Longrightarrow> (f has_derivative f' x) (at x within G)"
4.824 -  assumes B: "\<forall>x\<in>{0..1}. onorm (f' (x0 + x *\<^sub>R a)) \<le> B"
4.825 +  assumes B: "\<And>x. x \<in> {0..1} \<Longrightarrow> onorm (f' (x0 + x *\<^sub>R a)) \<le> B"
4.826    shows "norm (f (x0 + a) - f x0) \<le> norm a * B"
4.827  proof -
4.828    let ?G = "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}"
4.829 @@ -1095,14 +997,14 @@
4.830    ultimately show ?thesis
4.831      using has_derivative_subset[OF f' \<open>?G \<subseteq> G\<close>] B
4.832        differentiable_bound[of "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}" f f' B "x0 + a" x0]
4.833 -    by (auto simp: ac_simps)
4.834 +    by (force simp: ac_simps)
4.835  qed
4.836
4.837  lemma differentiable_bound_linearization:
4.838    fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
4.839 -  assumes "\<And>t. t \<in> {0..1} \<Longrightarrow> a + t *\<^sub>R (b - a) \<in> S"
4.840 +  assumes S: "\<And>t. t \<in> {0..1} \<Longrightarrow> a + t *\<^sub>R (b - a) \<in> S"
4.841    assumes f'[derivative_intros]: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
4.842 -  assumes B: "\<forall>x\<in>S. onorm (f' x - f' x0) \<le> B"
4.843 +  assumes B: "\<And>x. x \<in> S \<Longrightarrow> onorm (f' x - f' x0) \<le> B"
4.844    assumes "x0 \<in> S"
4.845    shows "norm (f b - f a - f' x0 (b - a)) \<le> norm (b - a) * B"
4.846  proof -
4.847 @@ -1111,9 +1013,9 @@
4.848      unfolding g_def using assms
4.849      by (auto intro!: derivative_eq_intros
4.850        bounded_linear.has_derivative[OF has_derivative_bounded_linear, OF f'])
4.851 -  from B have B: "\<forall>x\<in>{0..1}. onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> B"
4.852 -     using assms by (auto simp: fun_diff_def)
4.853 -  from differentiable_bound_segment[OF assms(1) g B] \<open>x0 \<in> S\<close>
4.854 +  from B have "\<forall>x\<in>{0..1}. onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> B"
4.855 +    using assms by (auto simp: fun_diff_def)
4.856 +  with differentiable_bound_segment[OF S g] \<open>x0 \<in> S\<close>
4.857    show ?thesis
4.858      by (simp add: g_def field_simps linear_diff[OF has_derivative_linear[OF f']])
4.859  qed
4.860 @@ -1122,7 +1024,7 @@
4.861    fixes f::"real \<Rightarrow> 'b::real_normed_vector"
4.862    assumes f': "\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)"
4.863    assumes "closed_segment a b \<subseteq> S"
4.864 -  assumes B: "\<forall>x\<in>S. norm (f' x - f' x0) \<le> B"
4.865 +  assumes B: "\<And>x. x \<in> S \<Longrightarrow> norm (f' x - f' x0) \<le> B"
4.866    assumes "x0 \<in> S"
4.867    shows "norm (f b - f a - (b - a) *\<^sub>R f' x0) \<le> norm (b - a) * B"
4.868    using assms
4.869 @@ -1346,20 +1248,14 @@
4.870      and "x \<in> S"
4.871      and fx: "f x \<in> interior (f ` S)"
4.872      and "continuous_on S f"
4.873 -    and "\<And>y. y \<in> S \<Longrightarrow> g (f y) = y"
4.874 +    and gf: "\<And>y. y \<in> S \<Longrightarrow> g (f y) = y"
4.875      and "(f has_derivative f') (at x)"
4.876      and "bounded_linear g'"
4.877      and "g' \<circ> f' = id"
4.878    shows "(g has_derivative g') (at (f x))"
4.879  proof -
4.880 -  {
4.881 -    fix y
4.882 -    assume "y \<in> interior (f ` S)"
4.883 -    then obtain x where "x \<in> S" and *: "y = f x"
4.884 -      by (meson imageE interior_subset subsetCE)
4.885 -    have "f (g y) = y"
4.886 -      unfolding * and assms(5)[rule_format,OF \<open>x\<in>S\<close>] ..
4.887 -  } note * = this
4.888 +  have *: "\<And>y. y \<in> interior (f ` S) \<Longrightarrow> f (g y) = y"
4.889 +    by (metis gf image_iff interior_subset subsetCE)
4.890    show ?thesis
4.891      apply (rule has_derivative_inverse_basic_x[OF assms(6-8), where T = "interior (f ` S)"])
4.892      apply (rule continuous_on_interior[OF _ fx])
4.893 @@ -1386,8 +1282,8 @@
4.894    show ?thesis
4.895      unfolding *
4.896      apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
4.897 -    apply (rule continuous_intros assms)+
4.898 -    using assms(4-6)
4.899 +    apply (intro continuous_intros)
4.900 +    using assms
4.901      apply auto
4.902      done
4.903  qed
4.904 @@ -1411,34 +1307,28 @@
4.905  lemma sussmann_open_mapping:
4.906    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
4.907    assumes "open S"
4.908 -    and "continuous_on S f"
4.909 +    and contf: "continuous_on S f"
4.910      and "x \<in> S"
4.911 -    and "(f has_derivative f') (at x)"
4.912 +    and derf: "(f has_derivative f') (at x)"
4.913      and "bounded_linear g'" "f' \<circ> g' = id"
4.914      and "T \<subseteq> S"
4.915 -    and "x \<in> interior T"
4.916 +    and x: "x \<in> interior T"
4.917    shows "f x \<in> interior (f ` T)"
4.918  proof -
4.919    interpret f': bounded_linear f'
4.920 -    using assms
4.921 -    unfolding has_derivative_def
4.922 -    by auto
4.923 +    using assms unfolding has_derivative_def by auto
4.924    interpret g': bounded_linear g'
4.925 -    using assms
4.926 -    by auto
4.927 +    using assms by auto
4.928    obtain B where B: "0 < B" "\<forall>x. norm (g' x) \<le> norm x * B"
4.929      using bounded_linear.pos_bounded[OF assms(5)] by blast
4.930    hence *: "1 / (2 * B) > 0" by auto
4.931    obtain e0 where e0:
4.932        "0 < e0"
4.933        "\<forall>y. norm (y - x) < e0 \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> 1 / (2 * B) * norm (y - x)"
4.934 -    using assms(4)
4.935 -    unfolding has_derivative_at_alt
4.936 +    using derf unfolding has_derivative_at_alt
4.937      using * by blast
4.938    obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> T"
4.939 -    using assms(8)
4.940 -    unfolding mem_interior_cball
4.941 -    by blast
4.942 +    using mem_interior_cball x by blast
4.943    have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
4.944    obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
4.945      using real_lbound_gt_zero[OF *] by blast
4.946 @@ -1449,83 +1339,59 @@
4.947        have "dist x z = norm (g' (f x) - g' y)"
4.948          unfolding as(2) and dist_norm by auto
4.949        also have "\<dots> \<le> norm (f x - y) * B"
4.950 -        unfolding g'.diff[symmetric]
4.951 -        using B
4.952 -        by auto
4.953 +        by (metis B(2) g'.diff)
4.954        also have "\<dots> \<le> e * B"
4.955 -        using as(1)[unfolded mem_cball dist_norm]
4.956 -        using B
4.957 -        by auto
4.958 +        by (metis B(1) dist_norm mem_cball real_mult_le_cancel_iff1 that(1))
4.959        also have "\<dots> \<le> e1"
4.960 -        using e
4.961 -        unfolding less_divide_eq
4.962 -        using B
4.963 -        by auto
4.964 +        using B(1) e(3) pos_less_divide_eq by fastforce
4.965        finally have "z \<in> cball x e1"
4.966 -        unfolding mem_cball
4.967          by force
4.968        then show "z \<in> S"
4.969          using e1 assms(7) by auto
4.970      qed
4.971      show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
4.972        unfolding g'.diff
4.973 -      apply (rule continuous_on_compose[of _ _ f, unfolded o_def])
4.974 -       apply (rule continuous_intros linear_continuous_on[OF assms(5)])+
4.975 -      apply (rule continuous_on_subset[OF assms(2)])
4.976 -      using z
4.977 -      by blast
4.978 +    proof (rule continuous_on_compose2 [OF _ _ order_refl, of _ _ f])
4.979 +      show "continuous_on ((\<lambda>y. x + (g' y - g' (f x))) ` cball (f x) e) f"
4.980 +        by (rule continuous_on_subset[OF contf]) (use z in blast)
4.981 +      show "continuous_on (cball (f x) e) (\<lambda>y. x + (g' y - g' (f x)))"
4.982 +        by (intro continuous_intros linear_continuous_on[OF \<open>bounded_linear g'\<close>])
4.983 +    qed
4.984    next
4.985      fix y z
4.986 -    assume as: "y \<in> cball (f x) (e / 2)" "z \<in> cball (f x) e"
4.987 +    assume y: "y \<in> cball (f x) (e / 2)" and z: "z \<in> cball (f x) e"
4.988      have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
4.989        using B by auto
4.990      also have "\<dots> \<le> e * B"
4.991 -      apply (rule mult_right_mono)
4.992 -      using as(2)[unfolded mem_cball dist_norm] and B
4.993 -      unfolding norm_minus_commute
4.994 -       apply auto
4.995 -      done
4.996 +      by (metis B(1) z dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1)
4.997      also have "\<dots> < e0"
4.998 -      using e and B
4.999 -      unfolding less_divide_eq
4.1000 -      by auto
4.1001 +      using B(1) e(2) pos_less_divide_eq by blast
4.1002      finally have *: "norm (x + g' (z - f x) - x) < e0"
4.1003        by auto
4.1004      have **: "f x + f' (x + g' (z - f x) - x) = z"
4.1005        using assms(6)[unfolded o_def id_def,THEN cong]
4.1006        by auto
4.1007      have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le>
4.1008 -        norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
4.1009 +          norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
4.1010        using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"]
4.1011        by (auto simp add: algebra_simps)
4.1012      also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)"
4.1013        using e0(2)[rule_format, OF *]
4.1014        by (simp only: algebra_simps **) auto
4.1015      also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2"
4.1016 -      using as(1)[unfolded mem_cball dist_norm]
4.1017 -      by auto
4.1018 +      using y by (auto simp: dist_norm)
4.1019      also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2"
4.1020 -      using * and B
4.1021 -      by (auto simp add: field_simps)
4.1022 +      using * B by (auto simp add: field_simps)
4.1023      also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2"
4.1024        by auto
4.1025      also have "\<dots> \<le> e/2 + e/2"
4.1027 -      using as(2)[unfolded mem_cball dist_norm]
4.1028 -      unfolding norm_minus_commute
4.1029 -      apply auto
4.1030 -      done
4.1031 +      using B(1) \<open>norm (z - f x) * B \<le> e * B\<close> by auto
4.1032      finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e"
4.1033 -      unfolding mem_cball dist_norm
4.1034 -      by auto
4.1035 +      by (auto simp: dist_norm)
4.1036    qed (use e that in auto)
4.1037    show ?thesis
4.1038      unfolding mem_interior
4.1039 -    apply (rule_tac x="e/2" in exI)
4.1040 -    apply rule
4.1041 -    apply (rule divide_pos_pos)
4.1042 -    prefer 3
4.1043 -  proof
4.1044 +  proof (intro exI conjI subsetI)
4.1045      fix y
4.1046      assume "y \<in> ball (f x) (e / 2)"
4.1047      then have *: "y \<in> cball (f x) (e / 2)"
4.1048 @@ -1536,23 +1402,14 @@
4.1049        using B
4.1050        by (auto simp add: field_simps)
4.1051      also have "\<dots> \<le> e * B"
4.1052 -      apply (rule mult_right_mono)
4.1053 -      using z(1)
4.1054 -      unfolding mem_cball dist_norm norm_minus_commute
4.1055 -      using B
4.1056 -      apply auto
4.1057 -      done
4.1058 +      by (metis B(1) dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1 z(1))
4.1059      also have "\<dots> \<le> e1"
4.1060        using e B unfolding less_divide_eq by auto
4.1061      finally have "x + g'(z - f x) \<in> T"
4.1062 -      apply -
4.1063 -      apply (rule e1(2)[unfolded subset_eq,rule_format])
4.1064 -      unfolding mem_cball dist_norm
4.1065 -      apply auto
4.1066 -      done
4.1068      then show "y \<in> f ` T"
4.1069        using z by auto
4.1070 -  qed (insert e, auto)
4.1071 +  qed (use e in auto)
4.1072  qed
4.1073
4.1074  text \<open>Hence the following eccentric variant of the inverse function theorem.
4.1075 @@ -1562,30 +1419,25 @@
4.1076
4.1077  lemma has_derivative_inverse_strong:
4.1078    fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
4.1079 -  assumes "open s"
4.1080 -    and "x \<in> s"
4.1081 -    and "continuous_on s f"
4.1082 -    and "\<forall>x\<in>s. g (f x) = x"
4.1083 -    and "(f has_derivative f') (at x)"
4.1084 -    and "f' \<circ> g' = id"
4.1085 +  assumes "open S"
4.1086 +    and "x \<in> S"
4.1087 +    and contf: "continuous_on S f"
4.1088 +    and gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
4.1089 +    and derf: "(f has_derivative f') (at x)"
4.1090 +    and id: "f' \<circ> g' = id"
4.1091    shows "(g has_derivative g') (at (f x))"
4.1092  proof -
4.1093    have linf: "bounded_linear f'"
4.1094 -    using assms(5) unfolding has_derivative_def by auto
4.1095 +    using derf unfolding has_derivative_def by auto
4.1096    then have ling: "bounded_linear g'"
4.1097      unfolding linear_conv_bounded_linear[symmetric]
4.1098 -    apply -
4.1099 -    apply (rule right_inverse_linear)
4.1100 -    using assms(6)
4.1101 -    apply auto
4.1102 -    done
4.1103 +    using id right_inverse_linear by blast
4.1104    moreover have "g' \<circ> f' = id"
4.1105 -    using assms(6) linf ling
4.1106 +    using id linf ling
4.1107      unfolding linear_conv_bounded_linear[symmetric]
4.1108      using linear_inverse_left
4.1109      by auto
4.1110 -  moreover have *:"\<forall>t\<subseteq>s. x \<in> interior t \<longrightarrow> f x \<in> interior (f ` t)"
4.1111 -    apply clarify
4.1112 +  moreover have *: "\<And>T. \<lbrakk>T \<subseteq> S; x \<in> interior T\<rbrakk> \<Longrightarrow> f x \<in> interior (f ` T)"
4.1113      apply (rule sussmann_open_mapping)
4.1114      apply (rule assms ling)+
4.1115      apply auto
4.1116 @@ -1595,44 +1447,30 @@
4.1117    proof (rule, rule)
4.1118      fix e :: real
4.1119      assume "e > 0"
4.1120 -    then have "f x \<in> interior (f ` (ball x e \<inter> s))"
4.1121 -      using *[rule_format,of "ball x e \<inter> s"] \<open>x \<in> s\<close>
4.1122 +    then have "f x \<in> interior (f ` (ball x e \<inter> S))"
4.1123 +      using *[rule_format,of "ball x e \<inter> S"] \<open>x \<in> S\<close>
4.1124        by (auto simp add: interior_open[OF open_ball] interior_open[OF assms(1)])
4.1125 -    then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> s)"
4.1126 +    then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> S)"
4.1127        unfolding mem_interior by blast
4.1128      show "\<exists>d>0. \<forall>y. 0 < dist y (f x) \<and> dist y (f x) < d \<longrightarrow> dist (g y) (g (f x)) < e"
4.1129 -      apply (rule_tac x=d in exI)
4.1130 -      apply rule
4.1131 -      apply (rule d(1))
4.1132 -      apply rule
4.1133 -      apply rule
4.1134 -    proof -
4.1135 +    proof (intro exI allI impI conjI)
4.1136        fix y
4.1137        assume "0 < dist y (f x) \<and> dist y (f x) < d"
4.1138 -      then have "g y \<in> g ` f ` (ball x e \<inter> s)"
4.1139 -        using d(2)[unfolded subset_eq,THEN bspec[where x=y]]
4.1140 -        by (auto simp add: dist_commute)
4.1141 -      then have "g y \<in> ball x e \<inter> s"
4.1142 -        using assms(4) by auto
4.1143 +      then have "g y \<in> g ` f ` (ball x e \<inter> S)"
4.1144 +        by (metis d(2) dist_commute mem_ball rev_image_eqI subset_iff)
4.1145        then show "dist (g y) (g (f x)) < e"
4.1146 -        using assms(4)[rule_format,OF \<open>x \<in> s\<close>]
4.1147 -        by (auto simp add: dist_commute)
4.1148 -    qed
4.1149 +        using gf[OF \<open>x \<in> S\<close>]
4.1150 +        by (simp add: assms(4) dist_commute image_iff)
4.1151 +    qed (use d in auto)
4.1152    qed
4.1153 -  moreover have "f x \<in> interior (f ` s)"
4.1154 +  moreover have "f x \<in> interior (f ` S)"
4.1155      apply (rule sussmann_open_mapping)
4.1156      apply (rule assms ling)+
4.1157 -    using interior_open[OF assms(1)] and \<open>x \<in> s\<close>
4.1158 +    using interior_open[OF assms(1)] and \<open>x \<in> S\<close>
4.1159      apply auto
4.1160      done
4.1161 -  moreover have "f (g y) = y" if "y \<in> interior (f ` s)" for y
4.1162 -  proof -
4.1163 -    from that have "y \<in> f ` s"
4.1164 -      using interior_subset by auto
4.1165 -    then obtain z where "z \<in> s" "y = f z" unfolding image_iff ..
4.1166 -    then show ?thesis
4.1167 -      using assms(4) by auto
4.1168 -  qed
4.1169 +  moreover have "f (g y) = y" if "y \<in> interior (f ` S)" for y
4.1170 +    by (metis gf imageE interiorE set_mp that)
4.1171    ultimately show ?thesis using assms
4.1172      by (metis has_derivative_inverse_basic_x open_interior)
4.1173  qed
4.1174 @@ -1641,10 +1479,10 @@
4.1175
4.1176  lemma has_derivative_inverse_strong_x:
4.1177    fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
4.1178 -  assumes "open s"
4.1179 -    and "g y \<in> s"
4.1180 -    and "continuous_on s f"
4.1181 -    and "\<forall>x\<in>s. g (f x) = x"
4.1182 +  assumes "open S"
4.1183 +    and "g y \<in> S"
4.1184 +    and "continuous_on S f"
4.1185 +    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
4.1186      and "(f has_derivative f') (at (g y))"
4.1187      and "f' \<circ> g' = id"
4.1188      and "f (g y) = y"
4.1189 @@ -1657,21 +1495,18 @@
4.1190
4.1191  lemma has_derivative_inverse_on:
4.1192    fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
4.1193 -  assumes "open s"
4.1194 -    and "\<forall>x\<in>s. (f has_derivative f'(x)) (at x)"
4.1195 -    and "\<forall>x\<in>s. g (f x) = x"
4.1196 +  assumes "open S"
4.1197 +    and derf: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f'(x)) (at x)"
4.1198 +    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
4.1199      and "f' x \<circ> g' x = id"
4.1200 -    and "x \<in> s"
4.1201 +    and "x \<in> S"
4.1202    shows "(g has_derivative g'(x)) (at (f x))"
4.1203 -  apply (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
4.1204 -  apply (rule assms)+
4.1205 -  unfolding continuous_on_eq_continuous_at[OF assms(1)]
4.1206 -  apply rule
4.1207 -  apply (rule differentiable_imp_continuous_within)
4.1208 -  unfolding differentiable_def
4.1209 -  using assms
4.1210 -  apply auto
4.1211 -  done
4.1212 +proof (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
4.1213 +  show "continuous_on S f"
4.1214 +  unfolding continuous_on_eq_continuous_at[OF \<open>open S\<close>]
4.1215 +  using derf has_derivative_continuous by blast
4.1216 +qed (use assms in auto)
4.1217 +
4.1218
4.1219  text \<open>Invertible derivative continous at a point implies local
4.1220  injectivity. It's only for this we need continuity of the derivative,
4.1221 @@ -1681,13 +1516,13 @@
4.1222
4.1223  proposition has_derivative_locally_injective:
4.1224    fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
4.1225 -  assumes "a \<in> s"
4.1226 -      and "open s"
4.1227 +  assumes "a \<in> S"
4.1228 +      and "open S"
4.1229        and bling: "bounded_linear g'"
4.1230        and "g' \<circ> f' a = id"
4.1231 -      and derf: "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x)"
4.1232 +      and derf: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x)"
4.1233        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"
4.1234 -  obtains r where "r > 0" "ball a r \<subseteq> s" "inj_on f (ball a r)"
4.1235 +  obtains r where "r > 0" "ball a r \<subseteq> S" "inj_on f (ball a r)"
4.1236  proof -
4.1237    interpret bounded_linear g'
4.1238      using assms by auto
4.1239 @@ -1704,21 +1539,17 @@
4.1240        "0 < d1"
4.1241        "\<And>x. dist a x < d1 \<Longrightarrow> onorm (\<lambda>v. f' x v - f' a v) < k"
4.1242      using assms(6) * by blast
4.1243 -  from \<open>open s\<close> obtain d2 where "d2 > 0" "ball a d2 \<subseteq> s"
4.1244 -    using \<open>a\<in>s\<close> ..
4.1245 -  obtain d2 where "d2 > 0" "ball a d2 \<subseteq> s"
4.1246 -    using assms(2,1) ..
4.1247 -  obtain d2 where d2: "0 < d2" "ball a d2 \<subseteq> s"
4.1248 -    using assms(2)
4.1249 -    unfolding open_contains_ball
4.1250 -    using \<open>a\<in>s\<close> by blast
4.1251 +  from \<open>open S\<close> obtain d2 where "d2 > 0" "ball a d2 \<subseteq> S"
4.1252 +    using \<open>a\<in>S\<close> ..
4.1253 +  obtain d2 where d2: "0 < d2" "ball a d2 \<subseteq> S"
4.1254 +    using \<open>0 < d2\<close> \<open>ball a d2 \<subseteq> S\<close> by blast
4.1255    obtain d where d: "0 < d" "d < d1" "d < d2"
4.1256      using real_lbound_gt_zero[OF d1(1) d2(1)] by blast
4.1257    show ?thesis
4.1258    proof
4.1259      show "0 < d" by (fact d)
4.1260 -    show "ball a d \<subseteq> s"
4.1261 -      using \<open>d < d2\<close> \<open>ball a d2 \<subseteq> s\<close> by auto
4.1262 +    show "ball a d \<subseteq> S"
4.1263 +      using \<open>d < d2\<close> \<open>ball a d2 \<subseteq> S\<close> by auto
4.1264      show "inj_on f (ball a d)"
4.1265      unfolding inj_on_def
4.1266      proof (intro strip)
4.1267 @@ -1726,55 +1557,36 @@
4.1268        assume as: "x \<in> ball a d" "y \<in> ball a d" "f x = f y"
4.1269        define ph where [abs_def]: "ph w = w - g' (f w - f x)" for w
4.1270        have ph':"ph = g' \<circ> (\<lambda>w. f' a w - (f w - f x))"
4.1271 -        unfolding ph_def o_def
4.1272 -        unfolding diff
4.1273 -        using f'g'
4.1274 -        by (auto simp: algebra_simps)
4.1275 +        unfolding ph_def o_def  by (simp add: diff f'g')
4.1276        have "norm (ph x - ph y) \<le> (1 / 2) * norm (x - y)"
4.1277 -        apply (rule differentiable_bound[OF convex_ball _ _ as(1-2), where f'="\<lambda>x v. v - g'(f' x v)"])
4.1278 -        apply (rule_tac[!] ballI)
4.1279 -      proof -
4.1280 +      proof (rule differentiable_bound[OF convex_ball _ _ as(1-2)])
4.1281          fix u
4.1282          assume u: "u \<in> ball a d"
4.1283 -        then have "u \<in> s"
4.1284 +        then have "u \<in> S"
4.1285            using d d2 by auto
4.1286          have *: "(\<lambda>v. v - g' (f' u v)) = g' \<circ> (\<lambda>w. f' a w - f' u w)"
4.1287            unfolding o_def and diff
4.1288            using f'g' by auto
4.1289          have blin: "bounded_linear (f' a)"
4.1290 -          using \<open>a \<in> s\<close> derf by blast
4.1291 +          using \<open>a \<in> S\<close> derf by blast
4.1292          show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)"
4.1293            unfolding ph' * comp_def
4.1294 -          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)+
4.1295 +          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)+
4.1296          have **: "bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>x. f' a x - f' u x)"
4.1297 -          apply (rule_tac[!] bounded_linear_sub)
4.1298 -          apply (rule_tac[!] has_derivative_bounded_linear)
4.1299 -          using assms(5) \<open>u \<in> s\<close> \<open>a \<in> s\<close>
4.1300 -          apply auto
4.1301 -          done
4.1302 -        have "onorm (\<lambda>v. v - g' (f' u v)) \<le> onorm g' * onorm (\<lambda>w. f' a w - f' u w)"
4.1303 -          unfolding *
4.1304 -          apply (rule onorm_compose)
4.1305 -          apply (rule assms(3) **)+
4.1306 -          done
4.1307 +          using \<open>u \<in> S\<close> blin bounded_linear_sub derf by auto
4.1308 +        then have "onorm (\<lambda>v. v - g' (f' u v)) \<le> onorm g' * onorm (\<lambda>w. f' a w - f' u w)"
4.1309 +          by (simp add: "*" bounded_linear_axioms onorm_compose)
4.1310          also have "\<dots> \<le> onorm g' * k"
4.1311            apply (rule mult_left_mono)
4.1312            using d1(2)[of u]
4.1313 -          using onorm_neg[where f="\<lambda>x. f' u x - f' a x"]
4.1314 -          using d and u and onorm_pos_le[OF assms(3)]
4.1315 -          apply (auto simp: algebra_simps)
4.1316 +          using onorm_neg[where f="\<lambda>x. f' u x - f' a x"] d u onorm_pos_le[OF bling] apply (auto simp: algebra_simps)
4.1317            done
4.1318          also have "\<dots> \<le> 1 / 2"
4.1319            unfolding k_def by auto
4.1320          finally show "onorm (\<lambda>v. v - g' (f' u v)) \<le> 1 / 2" .
4.1321        qed
4.1322        moreover have "norm (ph y - ph x) = norm (y - x)"
4.1323 -        apply (rule arg_cong[where f=norm])
4.1324 -        unfolding ph_def
4.1325 -        using diff
4.1326 -        unfolding as
4.1327 -        apply auto
4.1328 -        done
4.1329 +        by (simp add: as(3) ph_def)
4.1330        ultimately show "x = y"
4.1331          unfolding norm_minus_commute by auto
4.1332      qed
4.1333 @@ -1786,32 +1598,28 @@
4.1334
4.1335  lemma has_derivative_sequence_lipschitz_lemma:
4.1336    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
4.1337 -  assumes "convex s"
4.1338 -    and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
4.1339 -    and "\<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
4.1340 +  assumes "convex S"
4.1341 +    and derf: "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
4.1342 +    and nle: "\<And>n x h. \<lbrakk>n\<ge>N; x \<in> S\<rbrakk> \<Longrightarrow> norm (f' n x h - g' x h) \<le> e * norm h"
4.1343      and "0 \<le> e"
4.1344 -  shows "\<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> 2 * e * norm (x - y)"
4.1345 -proof rule+
4.1346 +  shows "\<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> 2 * e * norm (x - y)"
4.1347 +proof clarify
4.1348    fix m n x y
4.1349 -  assume as: "N \<le> m" "N \<le> n" "x \<in> s" "y \<in> s"
4.1350 +  assume as: "N \<le> m" "N \<le> n" "x \<in> S" "y \<in> S"
4.1351    show "norm ((f m x - f n x) - (f m y - f n y)) \<le> 2 * e * norm (x - y)"
4.1352 -    apply (rule differentiable_bound[where f'="\<lambda>x h. f' m x h - f' n x h", OF assms(1) _ _ as(3-4)])
4.1353 -    apply (rule_tac[!] ballI)
4.1354 -  proof -
4.1355 +  proof (rule differentiable_bound[where f'="\<lambda>x h. f' m x h - f' n x h", OF \<open>convex S\<close> _ _ as(3-4)])
4.1356      fix x
4.1357 -    assume "x \<in> s"
4.1358 -    show "((\<lambda>a. f m a - f n a) has_derivative (\<lambda>h. f' m x h - f' n x h)) (at x within s)"
4.1359 -      by (rule derivative_intros assms(2)[rule_format] \<open>x\<in>s\<close>)+
4.1360 +    assume "x \<in> S"
4.1361 +    show "((\<lambda>a. f m a - f n a) has_derivative (\<lambda>h. f' m x h - f' n x h)) (at x within S)"
4.1362 +      by (rule derivative_intros derf \<open>x\<in>S\<close>)+
4.1363      show "onorm (\<lambda>h. f' m x h - f' n x h) \<le> 2 * e"
4.1364      proof (rule onorm_bound)
4.1365        fix h
4.1366        have "norm (f' m x h - f' n x h) \<le> norm (f' m x h - g' x h) + norm (f' n x h - g' x h)"
4.1367          using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"]
4.1368 -        unfolding norm_minus_commute
4.1369 -        by (auto simp add: algebra_simps)
4.1370 +        by (auto simp add: algebra_simps norm_minus_commute)
4.1371        also have "\<dots> \<le> e * norm h + e * norm h"
4.1372 -        using assms(3)[rule_format,OF \<open>N \<le> m\<close> \<open>x \<in> s\<close>, of h]
4.1373 -        using assms(3)[rule_format,OF \<open>N \<le> n\<close> \<open>x \<in> s\<close>, of h]
4.1374 +        using nle[OF \<open>N \<le> m\<close> \<open>x \<in> S\<close>, of h] nle[OF \<open>N \<le> n\<close> \<open>x \<in> S\<close>, of h]
4.1375          by (auto simp add: field_simps)
4.1376        finally show "norm (f' m x h - f' n x h) \<le> 2 * e * norm h"
4.1377          by auto
4.1378 @@ -1823,18 +1631,20 @@
4.1379    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
4.1380    assumes "convex S"
4.1381      and "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
4.1382 -    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"
4.1383 +    and nle: "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
4.1384      and "e > 0"
4.1385    shows "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S.
4.1386      norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)"
4.1387  proof -
4.1388 -  have *: "2 * (1/2* e) = e" "1/2 * e >0"
4.1389 -    using \<open>e>0\<close> by auto
4.1390 -  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"
4.1391 -    using assms(3) *(2) by blast
4.1392 +  have *: "2 * (e/2) = e"
4.1393 +    using \<open>e > 0\<close> by auto
4.1394 +  obtain N where "\<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> (e/2) * norm h"
4.1395 +    using nle \<open>e > 0\<close>
4.1396 +    unfolding eventually_sequentially
4.1397 +    by (metis less_divide_eq_numeral1(1) mult_zero_left)
4.1398    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)"
4.1399      apply (rule_tac x=N in exI)
4.1400 -    apply (rule has_derivative_sequence_lipschitz_lemma[where e="1/2 *e", unfolded *])
4.1401 +    apply (rule has_derivative_sequence_lipschitz_lemma[where e="e/2", unfolded *])
4.1402      using assms \<open>e > 0\<close>
4.1403      apply auto
4.1404      done
4.1405 @@ -1843,60 +1653,51 @@
4.1406  lemma has_derivative_sequence:
4.1407    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
4.1408    assumes "convex S"
4.1409 -    and "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
4.1410 -    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"
4.1411 +    and derf: "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
4.1412 +    and nle: "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
4.1413      and "x0 \<in> S"
4.1414 -    and "((\<lambda>n. f n x0) \<longlongrightarrow> l) sequentially"
4.1415 -  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)"
4.1416 +    and lim: "((\<lambda>n. f n x0) \<longlongrightarrow> l) sequentially"
4.1417 +  shows "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) \<longlonglongrightarrow> g x \<and> (g has_derivative g'(x)) (at x within S)"
4.1418  proof -
4.1419    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.
4.1420        norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)"
4.1421      using assms(1,2,3) by (rule has_derivative_sequence_Lipschitz)
4.1422    have "\<exists>g. \<forall>x\<in>S. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
4.1423 -    apply (rule bchoice)
4.1424 -    unfolding convergent_eq_Cauchy
4.1425 -  proof
4.1426 +  proof (intro ballI bchoice)
4.1427      fix x
4.1428      assume "x \<in> S"
4.1429 -    show "Cauchy (\<lambda>n. f n x)"
4.1430 +    show "\<exists>y. (\<lambda>n. f n x) \<longlonglongrightarrow> y"
4.1431 +    unfolding convergent_eq_Cauchy
4.1432      proof (cases "x = x0")
4.1433        case True
4.1434 -      then show ?thesis
4.1435 -        using LIMSEQ_imp_Cauchy[OF assms(5)] by auto
4.1436 +      then show "Cauchy (\<lambda>n. f n x)"
4.1437 +        using LIMSEQ_imp_Cauchy[OF lim] by auto
4.1438      next
4.1439        case False
4.1440 -      show ?thesis
4.1441 +      show "Cauchy (\<lambda>n. f n x)"
4.1442          unfolding Cauchy_def
4.1443        proof (intro allI impI)
4.1444          fix e :: real
4.1445          assume "e > 0"
4.1446          hence *: "e / 2 > 0" "e / 2 / norm (x - x0) > 0" using False by auto
4.1447          obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x0) (f n x0) < e / 2"
4.1448 -          using LIMSEQ_imp_Cauchy[OF assms(5)]
4.1449 -          unfolding Cauchy_def
4.1450 -          using *(1) by blast
4.1451 +          using LIMSEQ_imp_Cauchy[OF lim] * unfolding Cauchy_def by blast
4.1452          obtain N where N:
4.1453            "\<forall>m\<ge>N. \<forall>n\<ge>N.
4.1454 -            \<forall>xa\<in>S. \<forall>y\<in>S. norm (f m xa - f n xa - (f m y - f n y)) \<le>
4.1455 -              e / 2 / norm (x - x0) * norm (xa - y)"
4.1456 +            \<forall>u\<in>S. \<forall>y\<in>S. norm (f m u - f n u - (f m y - f n y)) \<le>
4.1457 +              e / 2 / norm (x - x0) * norm (u - y)"
4.1458          using lem1 *(2) by blast
4.1459          show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e"
4.1460          proof (intro exI allI impI)
4.1461            fix m n
4.1462            assume as: "max M N \<le>m" "max M N\<le>n"
4.1463 -          have "dist (f m x) (f n x) \<le>
4.1464 -              norm (f m x0 - f n x0) + norm (f m x - f n x - (f m x0 - f n x0))"
4.1465 +          have "dist (f m x) (f n x) \<le> norm (f m x0 - f n x0) + norm (f m x - f n x - (f m x0 - f n x0))"
4.1466              unfolding dist_norm
4.1467              by (rule norm_triangle_sub)
4.1468            also have "\<dots> \<le> norm (f m x0 - f n x0) + e / 2"
4.1469 -            using N[rule_format,OF _ _ \<open>x\<in>S\<close> \<open>x0\<in>S\<close>, of m n] and as and False
4.1470 -            by auto
4.1471 +            using N \<open>x\<in>S\<close> \<open>x0\<in>S\<close> as False by fastforce
4.1472            also have "\<dots> < e / 2 + e / 2"
4.1474 -            using as and M[rule_format]
4.1475 -            unfolding dist_norm
4.1476 -            apply auto
4.1477 -            done
4.1478 +            by (rule add_strict_right_mono) (use as M in \<open>auto simp: dist_norm\<close>)
4.1479            finally show "dist (f m x) (f n x) < e"
4.1480              by auto
4.1481          qed
4.1482 @@ -1904,16 +1705,13 @@
4.1483      qed
4.1484    qed
4.1485    then obtain g where g: "\<forall>x\<in>S. (\<lambda>n. f n x) \<longlonglongrightarrow> g x" ..
4.1486 -  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)"
4.1487 -  proof (rule, rule)
4.1488 -    fix e :: real
4.1489 -    assume *: "e > 0"
4.1490 +  have lem2: "\<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)" if "e > 0" for e
4.1491 +  proof -
4.1492      obtain N where
4.1493        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)"
4.1494 -      using lem1 * by blast
4.1495 +      using lem1 \<open>e > 0\<close> by blast
4.1496      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)"
4.1497 -      apply (rule_tac x=N in exI)
4.1498 -    proof rule+
4.1499 +    proof (intro exI ballI allI impI)
4.1500        fix n x y
4.1501        assume as: "N \<le> n" "x \<in> S" "y \<in> S"
4.1502        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"
4.1503 @@ -1924,8 +1722,7 @@
4.1504          fix m
4.1505          assume "N \<le> m"
4.1506          then show "norm (f n x - f n y - (f m x - f m y)) \<le> e * norm (x - y)"
4.1507 -          using N[rule_format, of n m x y] and as
4.1508 -          by (auto simp add: algebra_simps)
4.1509 +          using N as by (auto simp add: algebra_simps)
4.1510        qed
4.1511        ultimately show "norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)"
4.1513 @@ -1933,31 +1730,28 @@
4.1514    qed
4.1515    have "\<forall>x\<in>S. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g' x) (at x within S)"
4.1516      unfolding has_derivative_within_alt2
4.1517 -  proof (intro ballI conjI)
4.1518 +  proof (intro ballI conjI allI impI)
4.1519      fix x
4.1520      assume "x \<in> S"
4.1521 -    then show "((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
4.1522 +    then show "(\<lambda>n. f n x) \<longlonglongrightarrow> g x"
4.1524 -    have lem3: "\<forall>u. ((\<lambda>n. f' n x u) \<longlongrightarrow> g' x u) sequentially"
4.1525 +    have tog': "(\<lambda>n. f' n x u) \<longlonglongrightarrow> g' x u" for u
4.1526        unfolding filterlim_def le_nhds_metric_le eventually_filtermap dist_norm
4.1527      proof (intro allI impI)
4.1528 -      fix u
4.1529        fix e :: real
4.1530        assume "e > 0"
4.1531        show "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e) sequentially"
4.1532        proof (cases "u = 0")
4.1533          case True
4.1534          have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e * norm u) sequentially"
4.1535 -          using assms(3)[folded eventually_sequentially] and \<open>0 < e\<close> and \<open>x \<in> S\<close>
4.1536 -          by (fast elim: eventually_mono)
4.1537 +          using nle \<open>0 < e\<close> \<open>x \<in> S\<close> by (fast elim: eventually_mono)
4.1538          then show ?thesis
4.1539 -          using \<open>u = 0\<close> and \<open>0 < e\<close> by (auto elim: eventually_mono)
4.1540 +          using \<open>u = 0\<close> \<open>0 < e\<close> by (auto elim: eventually_mono)
4.1541        next
4.1542          case False
4.1543          with \<open>0 < e\<close> have "0 < e / norm u" by simp
4.1544          then have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e / norm u * norm u) sequentially"
4.1545 -          using assms(3)[folded eventually_sequentially] and \<open>x \<in> S\<close>
4.1546 -          by (fast elim: eventually_mono)
4.1547 +          using nle \<open>x \<in> S\<close> by (fast elim: eventually_mono)
4.1548          then show ?thesis
4.1549            using \<open>u \<noteq> 0\<close> by simp
4.1550        qed
4.1551 @@ -1968,23 +1762,20 @@
4.1552        fix c :: real
4.1553        note lin = assms(2)[rule_format,OF \<open>x\<in>S\<close>,THEN has_derivative_bounded_linear]
4.1554        show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'"
4.1555 -        apply (rule tendsto_unique[OF trivial_limit_sequentially])
4.1556 -        apply (rule lem3[rule_format])
4.1557 +        apply (rule tendsto_unique[OF trivial_limit_sequentially tog'])
4.1558          unfolding lin[THEN bounded_linear.linear, THEN linear_cmul]
4.1559 -        apply (intro tendsto_intros)
4.1560 -        apply (rule lem3[rule_format])
4.1561 +        apply (intro tendsto_intros tog')
4.1562          done
4.1563        show "g' x (y + z) = g' x y + g' x z"
4.1564 -        apply (rule tendsto_unique[OF trivial_limit_sequentially])
4.1565 -        apply (rule lem3[rule_format])
4.1566 +        apply (rule tendsto_unique[OF trivial_limit_sequentially tog'])
4.1567          unfolding lin[THEN bounded_linear.linear, THEN linear_add]
4.1569 -        apply (rule lem3[rule_format])+
4.1570 +        apply (rule tog')+
4.1571          done
4.1572        obtain N where N: "\<forall>h. norm (f' N x h - g' x h) \<le> 1 * norm h"
4.1573 -        using assms(3) \<open>x \<in> S\<close> by (fast intro: zero_less_one)
4.1574 +        using nle \<open>x \<in> S\<close> unfolding eventually_sequentially by (fast intro: zero_less_one)
4.1575        have "bounded_linear (f' N x)"
4.1576 -        using assms(2) \<open>x \<in> S\<close> by fast
4.1577 +        using derf \<open>x \<in> S\<close> by fast
4.1578        from bounded_linear.bounded [OF this]
4.1579        obtain K where K: "\<forall>h. norm (f' N x h) \<le> norm h * K" ..
4.1580        {
4.1581 @@ -2000,20 +1791,19 @@
4.1582        }
4.1583        then show "\<exists>K. \<forall>h. norm (g' x h) \<le> norm h * K" by fast
4.1584      qed
4.1585 -    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)"
4.1586 -    proof (rule, rule)
4.1587 -      fix e :: real
4.1588 -      assume "e > 0"
4.1589 -      then have *: "e / 3 > 0"
4.1590 -        by auto
4.1591 +    show "eventually (\<lambda>y. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)) (at x within S)"
4.1592 +      if "e > 0" for e
4.1593 +    proof -
4.1594 +      have *: "e / 3 > 0"
4.1595 +        using that by auto
4.1596        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"
4.1597 -        using assms(3) * by blast
4.1598 +        using nle * unfolding eventually_sequentially by blast
4.1599        obtain N2 where
4.1600 -          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)"
4.1601 +          N2[rule_format]: "\<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)"
4.1602          using lem2 * by blast
4.1603        let ?N = "max N1 N2"
4.1604        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)"
4.1605 -        using assms(2)[unfolded has_derivative_within_alt2] and \<open>x \<in> S\<close> and * by fast
4.1606 +        using derf[unfolded has_derivative_within_alt2] and \<open>x \<in> S\<close> and * by fast
4.1607        moreover have "eventually (\<lambda>y. y \<in> S) (at x within S)"
4.1608          unfolding eventually_at by (fast intro: zero_less_one)
4.1609        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)"
4.1610 @@ -2022,7 +1812,7 @@
4.1611          assume "y \<in> S"
4.1612          assume "norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)"
4.1613          moreover have "norm (g y - g x - (f ?N y - f ?N x)) \<le> e / 3 * norm (y - x)"
4.1614 -          using N2[rule_format, OF _ \<open>y \<in> S\<close> \<open>x \<in> S\<close>]
4.1615 +          using N2[OF _ \<open>y \<in> S\<close> \<open>x \<in> S\<close>]
4.1617          ultimately have "norm (g y - g x - f' ?N x (y - x)) \<le> 2 * e / 3 * norm (y - x)"
4.1618            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)"]
4.1619 @@ -2045,7 +1835,8 @@
4.1620    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
4.1621    assumes "convex S"
4.1622      and der: "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
4.1623 -    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"
4.1624 +    and no: "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially.
4.1625 +       \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
4.1626    shows "\<exists>g. \<forall>x\<in>S. (g has_derivative g' x) (at x within S)"
4.1627  proof (cases "S = {}")
4.1628    case False
4.1629 @@ -2058,7 +1849,7 @@
4.1630      apply (rule has_derivative_sequence [OF \<open>convex S\<close> _ no, of "\<lambda>n x. f n x + (f 0 a - f n a)"])
4.1632      using \<open>a \<in> S\<close>
4.1633 -    apply auto
4.1634 +      apply auto
4.1635      done
4.1636  qed auto
4.1637
4.1638 @@ -2087,14 +1878,14 @@
4.1639      assume "e > 0"
4.1640      obtain N where N: "inverse (real (Suc N)) < e"
4.1641        using reals_Archimedean[OF \<open>e>0\<close>] ..
4.1642 -    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"
4.1643 +    show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>S.  \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
4.1644 +        unfolding eventually_sequentially
4.1645      proof (intro exI allI ballI impI)
4.1646        fix n x h
4.1647        assume n: "N \<le> n" and x: "x \<in> S"
4.1648        have *: "inverse (real (Suc n)) \<le> e"
4.1649          apply (rule order_trans[OF _ N[THEN less_imp_le]])
4.1650 -        using n
4.1651 -        apply (auto simp add: field_simps)
4.1652 +        using n apply (auto simp add: field_simps)
4.1653          done
4.1654        show "norm (f' n x h - g' x h) \<le> e * norm h"
4.1655          by (meson "*" mult_right_mono norm_ge_zero order.trans x f')
4.1656 @@ -2109,7 +1900,7 @@
4.1657    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
4.1658    assumes "convex S"
4.1659      and "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
4.1660 -    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"
4.1661 +    and "\<And>e. e>0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. \<forall>h. norm (sum (\<lambda>i. f' i x h) {..<n} - g' x h) \<le> e * norm h"
4.1662      and "x \<in> S"
4.1663      and "(\<lambda>n. f n x) sums l"
4.1664    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)"
4.1665 @@ -2130,7 +1921,9 @@
4.1666    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)"
4.1667  unfolding has_field_derivative_def
4.1668  proof (rule has_derivative_series)
4.1669 -  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
4.1670 +  show "\<forall>\<^sub>F n in sequentially.
4.1671 +       \<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
4.1672 +    unfolding eventually_sequentially
4.1673    proof -
4.1674      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"
4.1675        unfolding uniform_limit_iff eventually_at_top_linorder dist_norm by blast
4.1676 @@ -2217,17 +2010,17 @@
4.1677    shows "f' = f''"
4.1678  proof -
4.1679    have "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
4.1680 -  proof (rule frechet_derivative_unique_within)
4.1681 -    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"
4.1682 -    proof clarsimp
4.1683 -      fix e :: real assume "0 < e"
4.1684 -      with islimpt_approachable_real[of x S] not_bot
4.1685 +  proof (rule frechet_derivative_unique_within, simp_all)
4.1686 +    show "\<exists>d. d \<noteq> 0 \<and> \<bar>d\<bar> < e \<and> x + d \<in> S" if "0 < e"  for e
4.1687 +    proof -
4.1688 +      from that
4.1689        obtain x' where "x' \<in> S" "x' \<noteq> x" "\<bar>x' - x\<bar> < e"
4.1690 +        using islimpt_approachable_real[of x S] not_bot
4.1691          by (auto simp add: trivial_limit_within)
4.1692 -      then show "\<exists>d. d \<noteq> 0 \<and> \<bar>d\<bar> < e \<and> x + d \<in> S"
4.1693 -        by (intro exI[of _ "x' - x"]) auto
4.1694 +      then show ?thesis
4.1695 +        using eq_iff_diff_eq_0 by fastforce
4.1696      qed
4.1697 -  qed (insert f' f'', auto simp: has_vector_derivative_def)
4.1698 +  qed (use f' f'' in \<open>auto simp: has_vector_derivative_def\<close>)
4.1699    then show ?thesis
4.1700      unfolding fun_eq_iff by (metis scaleR_one)
4.1701  qed
4.1702 @@ -2416,59 +2209,59 @@
4.1703
4.1704  lemma vector_derivative_within_closed_interval:
4.1705    fixes f::"real \<Rightarrow> 'a::euclidean_space"
4.1706 -  assumes "a < b" and "x \<in> {a .. b}"
4.1707 -  assumes "(f has_vector_derivative f') (at x within {a .. b})"
4.1708 -  shows "vector_derivative f (at x within {a .. b}) = f'"
4.1709 +  assumes "a < b" and "x \<in> {a..b}"
4.1710 +  assumes "(f has_vector_derivative f') (at x within {a..b})"
4.1711 +  shows "vector_derivative f (at x within {a..b}) = f'"
4.1712    using assms vector_derivative_within_cbox
4.1713    by fastforce
4.1714
4.1715  lemma has_vector_derivative_within_subset:
4.1716 -  "(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
4.1717 +  "(f has_vector_derivative f') (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f has_vector_derivative f') (at x within T)"
4.1718    by (auto simp: has_vector_derivative_def intro: has_derivative_within_subset)
4.1719
4.1720  lemma has_vector_derivative_at_within:
4.1721 -  "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)"
4.1722 +  "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within S)"
4.1723    unfolding has_vector_derivative_def
4.1724    by (rule has_derivative_at_withinI)
4.1725
4.1726  lemma has_vector_derivative_weaken:
4.1727 -  fixes x D and f g s t
4.1728 -  assumes f: "(f has_vector_derivative D) (at x within t)"
4.1729 -    and "x \<in> s" "s \<subseteq> t"
4.1730 -    and "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
4.1731 -  shows "(g has_vector_derivative D) (at x within s)"
4.1732 +  fixes x D and f g S T
4.1733 +  assumes f: "(f has_vector_derivative D) (at x within T)"
4.1734 +    and "x \<in> S" "S \<subseteq> T"
4.1735 +    and "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
4.1736 +  shows "(g has_vector_derivative D) (at x within S)"
4.1737  proof -
4.1738 -  have "(f has_vector_derivative D) (at x within s) \<longleftrightarrow> (g has_vector_derivative D) (at x within s)"
4.1739 +  have "(f has_vector_derivative D) (at x within S) \<longleftrightarrow> (g has_vector_derivative D) (at x within S)"
4.1740      unfolding has_vector_derivative_def has_derivative_iff_norm
4.1741      using assms by (intro conj_cong Lim_cong_within refl) auto
4.1742    then show ?thesis
4.1743 -    using has_vector_derivative_within_subset[OF f \<open>s \<subseteq> t\<close>] by simp
4.1744 +    using has_vector_derivative_within_subset[OF f \<open>S \<subseteq> T\<close>] by simp
4.1745  qed
4.1746
4.1747  lemma has_vector_derivative_transform_within:
4.1748 -  assumes "(f has_vector_derivative f') (at x within s)"
4.1749 +  assumes "(f has_vector_derivative f') (at x within S)"
4.1750      and "0 < d"
4.1751 -    and "x \<in> s"
4.1752 -    and "\<And>x'. \<lbrakk>x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
4.1753 -    shows "(g has_vector_derivative f') (at x within s)"
4.1754 +    and "x \<in> S"
4.1755 +    and "\<And>x'. \<lbrakk>x'\<in>S; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
4.1756 +    shows "(g has_vector_derivative f') (at x within S)"
4.1757    using assms
4.1758    unfolding has_vector_derivative_def
4.1759    by (rule has_derivative_transform_within)
4.1760
4.1761  lemma has_vector_derivative_transform_within_open:
4.1762    assumes "(f has_vector_derivative f') (at x)"
4.1763 -    and "open s"
4.1764 -    and "x \<in> s"
4.1765 -    and "\<And>y. y\<in>s \<Longrightarrow> f y = g y"
4.1766 +    and "open S"
4.1767 +    and "x \<in> S"
4.1768 +    and "\<And>y. y\<in>S \<Longrightarrow> f y = g y"
4.1769    shows "(g has_vector_derivative f') (at x)"
4.1770    using assms
4.1771    unfolding has_vector_derivative_def
4.1772    by (rule has_derivative_transform_within_open)
4.1773
4.1774  lemma has_vector_derivative_transform:
4.1775 -  assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
4.1776 -  assumes f': "(f has_vector_derivative f') (at x within s)"
4.1777 -  shows "(g has_vector_derivative f') (at x within s)"
4.1778 +  assumes "x \<in> S" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
4.1779 +  assumes f': "(f has_vector_derivative f') (at x within S)"
4.1780 +  shows "(g has_vector_derivative f') (at x within S)"
4.1781    using assms
4.1782    unfolding has_vector_derivative_def
4.1783    by (rule has_derivative_transform)
4.1784 @@ -2477,23 +2270,13 @@
4.1785    assumes "(f has_vector_derivative f') (at x)"
4.1786      and "(g has_vector_derivative g') (at (f x))"
4.1787    shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x)"
4.1788 -  using assms(2)
4.1789 -  unfolding has_vector_derivative_def
4.1790 -  apply -
4.1791 -  apply (drule diff_chain_at[OF assms(1)[unfolded has_vector_derivative_def]])
4.1792 -  apply (simp only: o_def real_scaleR_def scaleR_scaleR)
4.1793 -  done
4.1794 +  using assms has_vector_derivative_at_within has_vector_derivative_def vector_derivative_diff_chain_within by blast
4.1795
4.1796  lemma vector_diff_chain_within:
4.1797    assumes "(f has_vector_derivative f') (at x within s)"
4.1798      and "(g has_vector_derivative g') (at (f x) within f ` s)"
4.1799    shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x within s)"
4.1800 -  using assms(2)
4.1801 -  unfolding has_vector_derivative_def
4.1802 -  apply -
4.1803 -  apply (drule diff_chain_within[OF assms(1)[unfolded has_vector_derivative_def]])
4.1804 -  apply (simp only: o_def real_scaleR_def scaleR_scaleR)
4.1805 -  done
4.1806 +  using assms has_vector_derivative_def vector_derivative_diff_chain_within by blast
4.1807
4.1808  lemma vector_derivative_const_at [simp]: "vector_derivative (\<lambda>x. c) (at a) = 0"
4.1810 @@ -2518,11 +2301,11 @@
4.1811   by (auto simp: o_def mult.commute has_vector_derivative_def)
4.1812
4.1813  lemma vector_derivative_chain_within:
4.1814 -  assumes "at x within s \<noteq> bot" "f differentiable (at x within s)"
4.1815 -    "(g has_derivative g') (at (f x) within f ` s)"
4.1816 -  shows "vector_derivative (g \<circ> f) (at x within s) =
4.1817 -        g' (vector_derivative f (at x within s)) "
4.1818 -  apply (rule vector_derivative_within [OF \<open>at x within s \<noteq> bot\<close>])
4.1819 +  assumes "at x within S \<noteq> bot" "f differentiable (at x within S)"
4.1820 +    "(g has_derivative g') (at (f x) within f ` S)"
4.1821 +  shows "vector_derivative (g \<circ> f) (at x within S) =
4.1822 +        g' (vector_derivative f (at x within S)) "
4.1823 +  apply (rule vector_derivative_within [OF \<open>at x within S \<noteq> bot\<close>])
4.1824    apply (rule vector_derivative_diff_chain_within)
4.1825    using assms(2-3) vector_derivative_works
4.1826    by auto
4.1827 @@ -2543,26 +2326,22 @@
4.1828  by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative)
4.1829
4.1830  lemma field_differentiable_imp_continuous_at:
4.1831 -    "f field_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
4.1832 +    "f field_differentiable (at x within S) \<Longrightarrow> continuous (at x within S) f"
4.1833    by (metis DERIV_continuous field_differentiable_def)
4.1834
4.1835  lemma field_differentiable_within_subset:
4.1836 -    "\<lbrakk>f field_differentiable (at x within s); t \<subseteq> s\<rbrakk>
4.1837 -     \<Longrightarrow> f field_differentiable (at x within t)"
4.1838 +    "\<lbrakk>f field_differentiable (at x within S); T \<subseteq> S\<rbrakk> \<Longrightarrow> f field_differentiable (at x within T)"
4.1839    by (metis DERIV_subset field_differentiable_def)
4.1840
4.1841  lemma field_differentiable_at_within:
4.1842      "\<lbrakk>f field_differentiable (at x)\<rbrakk>
4.1843 -     \<Longrightarrow> f field_differentiable (at x within s)"
4.1844 +     \<Longrightarrow> f field_differentiable (at x within S)"
4.1845    unfolding field_differentiable_def
4.1846    by (metis DERIV_subset top_greatest)
4.1847
4.1848  lemma field_differentiable_linear [simp,derivative_intros]: "(( * ) c) field_differentiable F"
4.1849 -proof -
4.1850 -  show ?thesis
4.1851 -    unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
4.1852 -    by (force intro: has_derivative_mult_right)
4.1853 -qed
4.1854 +  unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
4.1855 +  by (force intro: has_derivative_mult_right)
4.1856
4.1857  lemma field_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) field_differentiable F"
4.1858    unfolding field_differentiable_def has_field_derivative_def
4.1859 @@ -2602,45 +2381,45 @@
4.1860    by (metis field_differentiable_diff)
4.1861
4.1862  lemma field_differentiable_inverse [derivative_intros]:
4.1863 -  assumes "f field_differentiable (at a within s)" "f a \<noteq> 0"
4.1864 -  shows "(\<lambda>z. inverse (f z)) field_differentiable (at a within s)"
4.1865 +  assumes "f field_differentiable (at a within S)" "f a \<noteq> 0"
4.1866 +  shows "(\<lambda>z. inverse (f z)) field_differentiable (at a within S)"
4.1867    using assms unfolding field_differentiable_def
4.1868    by (metis DERIV_inverse_fun)
4.1869
4.1870  lemma field_differentiable_mult [derivative_intros]:
4.1871 -  assumes "f field_differentiable (at a within s)"
4.1872 -          "g field_differentiable (at a within s)"
4.1873 -    shows "(\<lambda>z. f z * g z) field_differentiable (at a within s)"
4.1874 +  assumes "f field_differentiable (at a within S)"
4.1875 +          "g field_differentiable (at a within S)"
4.1876 +    shows "(\<lambda>z. f z * g z) field_differentiable (at a within S)"
4.1877    using assms unfolding field_differentiable_def
4.1878 -  by (metis DERIV_mult [of f _ a s g])
4.1879 +  by (metis DERIV_mult [of f _ a S g])
4.1880
4.1881  lemma field_differentiable_divide [derivative_intros]:
4.1882 -  assumes "f field_differentiable (at a within s)"
4.1883 -          "g field_differentiable (at a within s)"
4.1884 +  assumes "f field_differentiable (at a within S)"
4.1885 +          "g field_differentiable (at a within S)"
4.1886            "g a \<noteq> 0"
4.1887 -    shows "(\<lambda>z. f z / g z) field_differentiable (at a within s)"
4.1888 +    shows "(\<lambda>z. f z / g z) field_differentiable (at a within S)"
4.1889    using assms unfolding field_differentiable_def
4.1890 -  by (metis DERIV_divide [of f _ a s g])
4.1891 +  by (metis DERIV_divide [of f _ a S g])
4.1892
4.1893  lemma field_differentiable_power [derivative_intros]:
4.1894 -  assumes "f field_differentiable (at a within s)"
4.1895 -    shows "(\<lambda>z. f z ^ n) field_differentiable (at a within s)"
4.1896 +  assumes "f field_differentiable (at a within S)"
4.1897 +    shows "(\<lambda>z. f z ^ n) field_differentiable (at a within S)"
4.1898    using assms unfolding field_differentiable_def
4.1899    by (metis DERIV_power)
4.1900
4.1901  lemma field_differentiable_transform_within:
4.1902    "0 < d \<Longrightarrow>
4.1903 -        x \<in> s \<Longrightarrow>
4.1904 -        (\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') \<Longrightarrow>
4.1905 -        f field_differentiable (at x within s)
4.1906 -        \<Longrightarrow> g field_differentiable (at x within s)"
4.1907 +        x \<in> S \<Longrightarrow>
4.1908 +        (\<And>x'. x' \<in> S \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') \<Longrightarrow>
4.1909 +        f field_differentiable (at x within S)
4.1910 +        \<Longrightarrow> g field_differentiable (at x within S)"
4.1911    unfolding field_differentiable_def has_field_derivative_def
4.1912    by (blast intro: has_derivative_transform_within)
4.1913
4.1914  lemma field_differentiable_compose_within:
4.1915 -  assumes "f field_differentiable (at a within s)"
4.1916 -          "g field_differentiable (at (f a) within f`s)"
4.1917 -    shows "(g o f) field_differentiable (at a within s)"
4.1918 +  assumes "f field_differentiable (at a within S)"
4.1919 +          "g field_differentiable (at (f a) within f`S)"
4.1920 +    shows "(g o f) field_differentiable (at a within S)"
4.1921    using assms unfolding field_differentiable_def
4.1922    by (metis DERIV_image_chain)
4.1923
4.1924 @@ -2650,7 +2429,7 @@
4.1925  by (metis field_differentiable_at_within field_differentiable_compose_within)
4.1926
4.1927  lemma field_differentiable_within_open:
4.1928 -     "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f field_differentiable at a within s \<longleftrightarrow>
4.1929 +     "\<lbrakk>a \<in> S; open S\<rbrakk> \<Longrightarrow> f field_differentiable at a within S \<longleftrightarrow>
4.1930                            f field_differentiable at a"
4.1931    unfolding field_differentiable_def
4.1932    by (metis at_within_open)
4.1933 @@ -2692,9 +2471,7 @@
4.1934      unfolding *
4.1935      by (rule tendsto_norm_zero_cancel) (auto intro!: tendsto_eq_intros)
4.1936
4.1937 -  moreover
4.1938 -
4.1939 -  have "\<forall>\<^sub>F x in at t within T. x \<noteq> t"
4.1940 +  moreover have "\<forall>\<^sub>F x in at t within T. x \<noteq> t"
4.1942    then have "\<forall>\<^sub>F x in at t within T. ((x - t) / \<bar>x - t\<bar>) *\<^sub>R ((\<Sum>n. ?e n x) - A) =
4.1943      (exp ((x - t) *\<^sub>R A) - 1 - (x - t) *\<^sub>R A) /\<^sub>R norm (x - t)"
4.1944 @@ -2721,9 +2498,7 @@
4.1946    qed
4.1947
4.1948 -  ultimately
4.1949 -
4.1950 -  have "((\<lambda>y. (exp ((y - t) *\<^sub>R A) - 1 - (y - t) *\<^sub>R A) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0) (at t within T)"
4.1951 +  ultimately have "((\<lambda>y. (exp ((y - t) *\<^sub>R A) - 1 - (y - t) *\<^sub>R A) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0) (at t within T)"
4.1952      by (rule Lim_transform_eventually[rotated])
4.1953    from tendsto_mult_right_zero[OF this, where c="exp (t *\<^sub>R A)"]
4.1954    show "((\<lambda>y. (exp (y *\<^sub>R A) - exp (t *\<^sub>R A) - (y - t) *\<^sub>R (exp (t *\<^sub>R A) * A)) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0)
4.1955 @@ -2756,7 +2531,7 @@
4.1956    also have "\<dots> \<subseteq> closure (interior A \<inter> {c<..})" by (intro open_Int_closure_subset) auto
4.1957    finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
4.1958    moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) \<longlongrightarrow> f') (at c within ?A')"
4.1959 -    unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
4.1960 +    unfolding has_field_derivative_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
4.1961    moreover from eventually_at_right_real[OF xc]
4.1962      have "eventually (\<lambda>y. (f y - f c) / (y - c) \<le> (f x - f c) / (x - c)) (at_right c)"
4.1963    proof eventually_elim
4.1964 @@ -2778,7 +2553,7 @@
4.1965    also have "\<dots> \<subseteq> closure (interior A \<inter> {..<c})" by (intro open_Int_closure_subset) auto
4.1966    finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
4.1967    moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) \<longlongrightarrow> f') (at c within ?A')"
4.1968 -    unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
4.1969 +    unfolding has_field_derivative_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
4.1970    moreover from eventually_at_left_real[OF xc]
4.1971      have "eventually (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at_left c)"
4.1972    proof eventually_elim
4.1973 @@ -2816,8 +2591,7 @@
4.1974
4.1975  lemma eventually_at_Pair_within_TimesI2:
4.1976    fixes x::"'a::metric_space"
4.1977 -  assumes "\<forall>\<^sub>F y' in at y within Y. P y'"
4.1978 -  assumes "P y"
4.1979 +  assumes "\<forall>\<^sub>F y' in at y within Y. P y'" "P y"
4.1980    shows "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'"
4.1981  proof -
4.1982    from assms[unfolded eventually_at_topological]
4.1983 @@ -2907,12 +2681,12 @@
4.1984        have "\<dots> \<subseteq> ball y d \<inter> Y"
4.1985          using \<open>y \<in> Y\<close> \<open>0 < d\<close> dy y'
4.1986          by (intro \<open>convex ?S\<close>[unfolded convex_contains_segment, rule_format, of y y'])
4.1987 -          (auto simp: dist_commute mem_ball)
4.1988 +          (auto simp: dist_commute)
4.1989        finally have "y + t *\<^sub>R (y' - y) \<in> ?S" .
4.1990      } note seg = this
4.1991
4.1992 -    have "\<forall>x\<in>ball y d \<inter> Y. onorm (blinfun_apply (fy x' x) - blinfun_apply (fy x' y)) \<le> e + e"
4.1993 -      by (safe intro!: onorm less_imp_le \<open>x' \<in> X\<close> dx) (auto simp: mem_ball dist_commute \<open>0 < d\<close> \<open>y \<in> Y\<close>)
4.1994 +    have "\<And>x. x \<in> ball y d \<inter> Y \<Longrightarrow> onorm (blinfun_apply (fy x' x) - blinfun_apply (fy x' y)) \<le> e + e"
4.1995 +      by (safe intro!: onorm less_imp_le \<open>x' \<in> X\<close> dx) (auto simp: dist_commute \<open>0 < d\<close> \<open>y \<in> Y\<close>)
4.1996      with seg has_derivative_within_subset[OF assms(2)[OF \<open>x' \<in> X\<close>]]
4.1997      show "norm (f x' y' - f x' y - (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
4.1998        by (rule differentiable_bound_linearization[where S="?S"])
4.1999 @@ -2923,10 +2697,10 @@
4.2000    from fx[unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
4.2001    have "\<forall>\<^sub>F x' in at x within X. ?le x'"
4.2002      by eventually_elim
4.2003 -       (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps fx.zero split: if_split_asm)
4.2004 +       (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps split: if_split_asm)
4.2005    then have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. ?le x'"
4.2006      by (rule eventually_at_Pair_within_TimesI1)
4.2007 -       (simp add: blinfun.bilinear_simps fx.zero)
4.2009    moreover have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. norm ((x', y') - (x, y)) \<noteq> 0"
4.2010      unfolding norm_eq_zero right_minus_eq
4.2011      by (auto simp: eventually_at intro!: zero_less_one)
4.2012 @@ -2996,11 +2770,11 @@
4.2013  subsection \<open>Differentiable case distinction\<close>
4.2014
4.2015  lemma has_derivative_within_If_eq:
4.2016 -  "((\<lambda>x. if P x then f x else g x) has_derivative f') (at x within s) =
4.2017 +  "((\<lambda>x. if P x then f x else g x) has_derivative f') (at x within S) =
4.2018      (bounded_linear f' \<and>
4.2019       ((\<lambda>y.(if P y then (f y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)
4.2020             else (g y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)))
4.2021 -      \<longlongrightarrow> 0) (at x within s))"
4.2022 +      \<longlongrightarrow> 0) (at x within S))"
4.2023    (is "_ = (_ \<and> (?if \<longlongrightarrow> 0) _)")
4.2024  proof -
4.2025    have "(\<lambda>y. (1 / norm (y - x)) *\<^sub>R
4.2026 @@ -3011,45 +2785,44 @@
4.2027  qed
4.2028
4.2029  lemma has_derivative_If_within_closures:
4.2030 -  assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
4.2031 -    (f has_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
4.2032 -  assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
4.2033 -    (g has_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
4.2034 -  assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
4.2035 -  assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
4.2036 -  assumes x_in: "x \<in> s \<union> t"
4.2037 -  shows "((\<lambda>x. if x \<in> s then f x else g x) has_derivative
4.2038 -      (if x \<in> s then f' x else g' x)) (at x within (s \<union> t))"
4.2039 +  assumes f': "x \<in> S \<union> (closure S \<inter> closure T) \<Longrightarrow>
4.2040 +    (f has_derivative f' x) (at x within S \<union> (closure S \<inter> closure T))"
4.2041 +  assumes g': "x \<in> T \<union> (closure S \<inter> closure T) \<Longrightarrow>
4.2042 +    (g has_derivative g' x) (at x within T \<union> (closure S \<inter> closure T))"
4.2043 +  assumes connect: "x \<in> closure S \<Longrightarrow> x \<in> closure T \<Longrightarrow> f x = g x"
4.2044 +  assumes connect': "x \<in> closure S \<Longrightarrow> x \<in> closure T \<Longrightarrow> f' x = g' x"
4.2045 +  assumes x_in: "x \<in> S \<union> T"
4.2046 +  shows "((\<lambda>x. if x \<in> S then f x else g x) has_derivative
4.2047 +      (if x \<in> S then f' x else g' x)) (at x within (S \<union> T))"
4.2048  proof -
4.2049 -  from f' x_in interpret f': bounded_linear "if x \<in> s then f' x else (\<lambda>x. 0)"
4.2050 +  from f' x_in interpret f': bounded_linear "if x \<in> S then f' x else (\<lambda>x. 0)"
4.2051      by (auto simp add: has_derivative_within)
4.2052 -  from g' interpret g': bounded_linear "if x \<in> t then g' x else (\<lambda>x. 0)"
4.2053 +  from g' interpret g': bounded_linear "if x \<in> T then g' x else (\<lambda>x. 0)"
4.2054      by (auto simp add: has_derivative_within)
4.2055 -  have bl: "bounded_linear (if x \<in> s then f' x else g' x)"
4.2056 +  have bl: "bounded_linear (if x \<in> S then f' x else g' x)"
4.2058      by (unfold_locales; force)
4.2059    show ?thesis
4.2060 -    using f' g' closure_subset[of t] closure_subset[of s]
4.2061 +    using f' g' closure_subset[of T] closure_subset[of S]
4.2062      unfolding has_derivative_within_If_eq
4.2063      by (intro conjI bl tendsto_If_within_closures x_in)
4.2064        (auto simp: has_derivative_within inverse_eq_divide connect connect' set_mp)
4.2065  qed
4.2066
4.2067  lemma has_vector_derivative_If_within_closures:
4.2068 -  assumes x_in: "x \<in> s \<union> t"
4.2069 -  assumes "u = s \<union> t"
4.2070 -  assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
4.2071 -    (f has_vector_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
4.2072 -  assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
4.2073 -    (g has_vector_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
4.2074 -  assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
4.2075 -  assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
4.2076 -  shows "((\<lambda>x. if x \<in> s then f x else g x) has_vector_derivative
4.2077 -    (if x \<in> s then f' x else g' x)) (at x within u)"
4.2078 +  assumes x_in: "x \<in> S \<union> T"
4.2079 +  assumes "u = S \<union> T"
4.2080 +  assumes f': "x \<in> S \<union> (closure S \<inter> closure T) \<Longrightarrow>
4.2081 +    (f has_vector_derivative f' x) (at x within S \<union> (closure S \<inter> closure T))"
4.2082 +  assumes g': "x \<in> T \<union> (closure S \<inter> closure T) \<Longrightarrow>
4.2083 +    (g has_vector_derivative g' x) (at x within T \<union> (closure S \<inter> closure T))"
4.2084 +  assumes connect: "x \<in> closure S \<Longrightarrow> x \<in> closure T \<Longrightarrow> f x = g x"
4.2085 +  assumes connect': "x \<in> closure S \<Longrightarrow> x \<in> closure T \<Longrightarrow> f' x = g' x"
4.2086 +  shows "((\<lambda>x. if x \<in> S then f x else g x) has_vector_derivative
4.2087 +    (if x \<in> S then f' x else g' x)) (at x within u)"
4.2088    unfolding has_vector_derivative_def assms
4.2089    using x_in
4.2090 -  apply (intro has_derivative_If_within_closures[where
4.2091 -        ?f' = "\<lambda>x a. a *\<^sub>R f' x" and ?g' = "\<lambda>x a. a *\<^sub>R g' x",
4.2092 +  apply (intro has_derivative_If_within_closures[where ?f' = "\<lambda>x a. a *\<^sub>R f' x" and ?g' = "\<lambda>x a. a *\<^sub>R g' x",
4.2093          THEN has_derivative_eq_rhs])
4.2094    subgoal by (rule f'[unfolded has_vector_derivative_def]; assumption)
4.2095    subgoal by (rule g'[unfolded has_vector_derivative_def]; assumption)
```
```     5.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun May 20 22:04:46 2018 +0200
5.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun May 20 22:10:30 2018 +0100
5.3 @@ -5089,9 +5089,9 @@
5.4              using B' [of a b] B' [of c d] norm_triangle_half_r by blast
5.5          qed
5.6        qed (use \<open>B > 0\<close> in auto)}
5.7 -  then show ?thesis
5.8 -    by force
5.9 -qed
5.10 +    then show ?thesis
5.11 +      by force
5.12 +  qed
5.13    finally show ?thesis .
5.14  qed
5.15
5.16 @@ -6496,7 +6496,7 @@
5.17            unfolding has_vector_derivative_def[symmetric]
5.18            using that \<open>x \<in> X0\<close>
5.19            by (intro has_derivative_within_subset[OF fx]) auto
5.20 -        have "\<forall>x \<in> X0 \<inter> U. onorm (blinfun_apply (fx x t) - (fx x0 t)) \<le> e"
5.21 +        have "\<And>x. x \<in> X0 \<inter> U \<Longrightarrow> onorm (blinfun_apply (fx x t) - (fx x0 t)) \<le> e"
5.22            using fx_bound t
5.23            by (auto simp add: norm_blinfun_def fun_diff_def blinfun.bilinear_simps[symmetric])
5.24          from differentiable_bound_linearization[OF seg deriv this] X0
```
```     6.1 --- a/src/HOL/Analysis/Lipschitz.thy	Sun May 20 22:04:46 2018 +0200
6.2 +++ b/src/HOL/Analysis/Lipschitz.thy	Sun May 20 22:10:30 2018 +0100
6.3 @@ -814,7 +814,7 @@
6.4      note s
6.5      also note \<open>cball t v \<subseteq> T\<close>
6.6      finally
6.7 -    have deriv: "\<forall>y\<in>cball x u. (f s has_derivative blinfun_apply (f' (s, y))) (at y within cball x u)"
6.8 +    have deriv: "\<And>y. y \<in> cball x u \<Longrightarrow> (f s has_derivative blinfun_apply (f' (s, y))) (at y within cball x u)"
6.9        using \<open>_ \<subseteq> X\<close>
6.10        by (auto intro!: has_derivative_at_withinI[OF f'])
6.11      have "norm (f s y - f s z) \<le> B * norm (y - z)"
```
```     7.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Sun May 20 22:04:46 2018 +0200
7.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Sun May 20 22:10:30 2018 +0100
7.3 @@ -250,8 +250,8 @@
7.4  lemma homeomorphic_closed_intervals_real:
7.5    fixes a::real and b and c::real and d
7.6    assumes "a<b" and "c<d"
7.7 -    shows "{a..b} homeomorphic {c..d}"
7.8 -by (metis assms compact_interval continuous_on_id convex_real_interval(5) emptyE homeomorphic_convex_compact interior_atLeastAtMost_real mvt)
7.9 +  shows "{a..b} homeomorphic {c..d}"
7.10 +  using assms by (auto intro: homeomorphic_convex_compact)
7.11
7.12  no_notation
7.13    eucl_less (infix "<e" 50)
```