new material about vec, real^1, etc.
authorpaulson <lp15@cam.ac.uk>
Sat Apr 14 09:23:00 2018 +0100 (13 months ago)
changeset 6797953323937ee25
parent 67978 06bce659d41b
child 67980 a8177d098b74
new material about vec, real^1, etc.
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Lipschitz.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Apr 13 17:00:57 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sat Apr 14 09:23:00 2018 +0100
     1.3 @@ -139,6 +139,9 @@
     1.4  lemma vec_cmul: "vec(c * x) = c *s vec x " by vector
     1.5  lemma vec_neg: "vec(- x) = - vec x " by vector
     1.6  
     1.7 +lemma vec_scaleR: "vec(c * x) = c *\<^sub>R vec x"
     1.8 +  by vector
     1.9 +
    1.10  lemma vec_sum:
    1.11    assumes "finite S"
    1.12    shows "vec(sum f S) = sum (vec \<circ> f) S"
    1.13 @@ -263,6 +266,26 @@
    1.14  lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)"
    1.15    by (simp add: vec_eq_iff)
    1.16  
    1.17 +lemma linear_vec [simp]: "linear vec"
    1.18 +  by (simp add: linearI vec_add vec_eq_iff)
    1.19 +
    1.20 +lemma differentiable_vec:
    1.21 +  fixes S :: "'a::euclidean_space set"
    1.22 +  shows "vec differentiable_on S"
    1.23 +  by (simp add: linear_linear bounded_linear_imp_differentiable_on)
    1.24 +
    1.25 +lemma continuous_vec [continuous_intros]:
    1.26 +  fixes x :: "'a::euclidean_space"
    1.27 +  shows "isCont vec x"
    1.28 +  apply (clarsimp simp add: continuous_def LIM_def dist_vec_def L2_set_def)
    1.29 +  apply (rule_tac x="r / sqrt (real CARD('b))" in exI)
    1.30 +  by (simp add: mult.commute pos_less_divide_eq real_sqrt_mult)
    1.31 +
    1.32 +lemma box_vec_eq_empty [simp]:
    1.33 +  shows "cbox (vec a) (vec b) = {} \<longleftrightarrow> cbox a b = {}"
    1.34 +        "box (vec a) (vec b) = {} \<longleftrightarrow> box a b = {}"
    1.35 +  by (auto simp: Basis_vec_def mem_box box_eq_empty inner_axis)
    1.36 +
    1.37  lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
    1.38  
    1.39  lemma norm_axis_1 [simp]: "norm (axis m (1::real)) = 1"
    1.40 @@ -283,18 +306,18 @@
    1.41  lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"
    1.42    by (metis vector_mul_rcancel)
    1.43  
    1.44 -lemma component_le_norm_cart: "\<bar>x$i\<bar> <= norm x"
    1.45 +lemma component_le_norm_cart: "\<bar>x$i\<bar> \<le> norm x"
    1.46    apply (simp add: norm_vec_def)
    1.47    apply (rule member_le_L2_set, simp_all)
    1.48    done
    1.49  
    1.50 -lemma norm_bound_component_le_cart: "norm x <= e ==> \<bar>x$i\<bar> <= e"
    1.51 +lemma norm_bound_component_le_cart: "norm x \<le> e ==> \<bar>x$i\<bar> \<le> e"
    1.52    by (metis component_le_norm_cart order_trans)
    1.53  
    1.54  lemma norm_bound_component_lt_cart: "norm x < e ==> \<bar>x$i\<bar> < e"
    1.55    by (metis component_le_norm_cart le_less_trans)
    1.56  
    1.57 -lemma norm_le_l1_cart: "norm x <= sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
    1.58 +lemma norm_le_l1_cart: "norm x \<le> sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
    1.59    by (simp add: norm_vec_def L2_set_le_sum)
    1.60  
    1.61  lemma scalar_mult_eq_scaleR [simp]: "c *s x = c *\<^sub>R x"
    1.62 @@ -1440,7 +1463,7 @@
    1.63    shows "x = 1 \<or> x = 2"
    1.64  proof (induct x)
    1.65    case (of_int z)
    1.66 -  then have "0 <= z" and "z < 2" by simp_all
    1.67 +  then have "0 \<le> z" and "z < 2" by simp_all
    1.68    then have "z = 0 | z = 1" by arith
    1.69    then show ?case by auto
    1.70  qed
    1.71 @@ -1453,7 +1476,7 @@
    1.72    shows "x = 1 \<or> x = 2 \<or> x = 3"
    1.73  proof (induct x)
    1.74    case (of_int z)
    1.75 -  then have "0 <= z" and "z < 3" by simp_all
    1.76 +  then have "0 \<le> z" and "z < 3" by simp_all
    1.77    then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
    1.78    then show ?case by auto
    1.79  qed
    1.80 @@ -1479,6 +1502,14 @@
    1.81  lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3"
    1.82    unfolding UNIV_3 by (simp add: ac_simps)
    1.83  
    1.84 +lemma num1_eqI:
    1.85 +  fixes a::num1 shows "a = b"
    1.86 +  by (metis (full_types) UNIV_1 UNIV_I empty_iff insert_iff)
    1.87 +
    1.88 +lemma num1_eq1 [simp]:
    1.89 +  fixes a::num1 shows "a = 1"
    1.90 +  by (rule num1_eqI)
    1.91 +
    1.92  instantiation num1 :: cart_one
    1.93  begin
    1.94  
    1.95 @@ -1489,6 +1520,16 @@
    1.96  
    1.97  end
    1.98  
    1.99 +instantiation num1 :: linorder begin
   1.100 +definition "a < b \<longleftrightarrow> Rep_num1 a < Rep_num1 b"
   1.101 +definition "a \<le> b \<longleftrightarrow> Rep_num1 a \<le> Rep_num1 b"
   1.102 +instance
   1.103 +  by intro_classes (auto simp: less_eq_num1_def less_num1_def intro: num1_eqI)
   1.104 +end
   1.105 +
   1.106 +instance num1 :: wellorder
   1.107 +  by intro_classes (auto simp: less_eq_num1_def less_num1_def)
   1.108 +
   1.109  subsection\<open>The collapse of the general concepts to dimension one\<close>
   1.110  
   1.111  lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
   1.112 @@ -1503,6 +1544,11 @@
   1.113  lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
   1.114    by (simp add: norm_vec_def)
   1.115  
   1.116 +lemma dist_vector_1:
   1.117 +  fixes x :: "'a::real_normed_vector^1"
   1.118 +  shows "dist x y = dist (x$1) (y$1)"
   1.119 +  by (simp add: dist_norm norm_vector_1)
   1.120 +
   1.121  lemma norm_real: "norm(x::real ^ 1) = \<bar>x$1\<bar>"
   1.122    by (simp add: norm_vector_1)
   1.123  
   1.124 @@ -1510,6 +1556,33 @@
   1.125    by (auto simp add: norm_real dist_norm)
   1.126  
   1.127  
   1.128 +lemma tendsto_at_within_vector_1:
   1.129 +  fixes S :: "'a :: metric_space set"
   1.130 +  assumes "(f \<longlongrightarrow> fx) (at x within S)"
   1.131 +  shows "((\<lambda>y::'a^1. \<chi> i. f (y $ 1)) \<longlongrightarrow> (vec fx::'a^1)) (at (vec x) within vec ` S)"
   1.132 +proof (rule topological_tendstoI)
   1.133 +  fix T :: "('a^1) set"
   1.134 +  assume "open T" "vec fx \<in> T"
   1.135 +  have "\<forall>\<^sub>F x in at x within S. f x \<in> (\<lambda>x. x $ 1) ` T"
   1.136 +    using \<open>open T\<close> \<open>vec fx \<in> T\<close> assms open_image_vec_nth tendsto_def by fastforce
   1.137 +  then show "\<forall>\<^sub>F x::'a^1 in at (vec x) within vec ` S. (\<chi> i. f (x $ 1)) \<in> T"
   1.138 +    unfolding eventually_at dist_norm [symmetric]
   1.139 +    by (rule ex_forward)
   1.140 +       (use \<open>open T\<close> in 
   1.141 +         \<open>fastforce simp: dist_norm dist_vec_def L2_set_def image_iff vector_one open_vec_def\<close>)
   1.142 +qed
   1.143 +
   1.144 +lemma has_derivative_vector_1:
   1.145 +  assumes der_g: "(g has_derivative (\<lambda>x. x * g' a)) (at a within S)"
   1.146 +  shows "((\<lambda>x. vec (g (x $ 1))) has_derivative ( *\<^sub>R) (g' a))
   1.147 +         (at ((vec a)::real^1) within vec ` S)"
   1.148 +    using der_g
   1.149 +    apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
   1.150 +    apply (drule tendsto_at_within_vector_1, vector)
   1.151 +    apply (auto simp: algebra_simps eventually_at tendsto_def)
   1.152 +    done
   1.153 +
   1.154 +
   1.155  subsection\<open>Explicit vector construction from lists\<close>
   1.156  
   1.157  definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"
     2.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Apr 13 17:00:57 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat Apr 14 09:23:00 2018 +0100
     2.3 @@ -378,7 +378,7 @@
     2.4      "f piecewise_C1_differentiable_on i \<Longrightarrow> f piecewise_differentiable_on i"
     2.5    by (auto simp: piecewise_C1_differentiable_on_def piecewise_differentiable_on_def
     2.6             C1_differentiable_on_def differentiable_def has_vector_derivative_def
     2.7 -           intro: has_derivative_at_within)
     2.8 +           intro: has_derivative_at_withinI)
     2.9  
    2.10  lemma piecewise_C1_differentiable_compose:
    2.11      "\<lbrakk>f piecewise_C1_differentiable_on s; g piecewise_C1_differentiable_on (f ` s);
    2.12 @@ -3807,7 +3807,7 @@
    2.13            (at x within {a..b})"
    2.14          using x gdx t
    2.15          apply (clarsimp simp add: differentiable_iff_scaleR)
    2.16 -        apply (rule exp_fg [unfolded has_vector_derivative_def, simplified], blast intro: has_derivative_at_within)
    2.17 +        apply (rule exp_fg [unfolded has_vector_derivative_def, simplified], blast intro: has_derivative_at_withinI)
    2.18          apply (simp_all add: has_vector_derivative_def [symmetric])
    2.19          done
    2.20        } note * = this
     3.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Apr 13 17:00:57 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat Apr 14 09:23:00 2018 +0100
     3.3 @@ -1113,7 +1113,7 @@
     3.4      apply auto
     3.5      apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI)
     3.6      apply (auto simp: closed_segment_def twz) []
     3.7 -    apply (intro derivative_eq_intros has_derivative_at_within, simp_all)
     3.8 +    apply (intro derivative_eq_intros has_derivative_at_withinI, simp_all)
     3.9      apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib)
    3.10      apply (force simp: twz closed_segment_def)
    3.11      done
     4.1 --- a/src/HOL/Analysis/Derivative.thy	Fri Apr 13 17:00:57 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Derivative.thy	Sat Apr 14 09:23:00 2018 +0100
     4.3 @@ -66,7 +66,7 @@
     4.4    using has_derivative_within' [of f f' x UNIV]
     4.5    by simp
     4.6  
     4.7 -lemma has_derivative_at_within:
     4.8 +lemma has_derivative_at_withinI:
     4.9    "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
    4.10    unfolding has_derivative_within' has_derivative_at'
    4.11    by blast
    4.12 @@ -135,7 +135,7 @@
    4.13  
    4.14  lemma differentiable_at_withinI: "f differentiable (at x) \<Longrightarrow> f differentiable (at x within s)"
    4.15    unfolding differentiable_def
    4.16 -  using has_derivative_at_within
    4.17 +  using has_derivative_at_withinI
    4.18    by blast
    4.19  
    4.20  lemma differentiable_at_imp_differentiable_on:
    4.21 @@ -1819,7 +1819,7 @@
    4.22            apply (rule derivative_intros)
    4.23            defer
    4.24            apply (rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
    4.25 -          apply (rule has_derivative_at_within)
    4.26 +          apply (rule has_derivative_at_withinI)
    4.27            using assms(5) and \<open>u \<in> s\<close> \<open>a \<in> s\<close>
    4.28            apply (auto intro!: derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] has_derivative_bounded_linear)
    4.29            done
    4.30 @@ -2526,7 +2526,7 @@
    4.31  lemma has_vector_derivative_at_within:
    4.32    "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)"
    4.33    unfolding has_vector_derivative_def
    4.34 -  by (rule has_derivative_at_within)
    4.35 +  by (rule has_derivative_at_withinI)
    4.36  
    4.37  lemma has_vector_derivative_weaken:
    4.38    fixes x D and f g s t
     5.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Apr 13 17:00:57 2018 +0100
     5.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Apr 14 09:23:00 2018 +0100
     5.3 @@ -917,6 +917,9 @@
     5.4    where "f absolutely_integrable_on s \<equiv> set_integrable lebesgue s f"
     5.5  
     5.6  
     5.7 +lemma absolutely_integrable_zero [simp]: "(\<lambda>x. 0) absolutely_integrable_on S"
     5.8 +    by (simp add: set_integrable_def)
     5.9 +
    5.10  lemma absolutely_integrable_on_def:
    5.11    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
    5.12    shows "f absolutely_integrable_on S \<longleftrightarrow> f integrable_on S \<and> (\<lambda>x. norm (f x)) integrable_on S"
    5.13 @@ -987,6 +990,18 @@
    5.14      unfolding absolutely_integrable_on_def by auto
    5.15  qed
    5.16  
    5.17 +lemma absolutely_integrable_on_scaleR_iff:
    5.18 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
    5.19 +  shows
    5.20 +   "(\<lambda>x. c *\<^sub>R f x) absolutely_integrable_on S \<longleftrightarrow>
    5.21 +      c = 0 \<or> f absolutely_integrable_on S"
    5.22 +proof (cases "c=0")
    5.23 +  case False
    5.24 +  then show ?thesis
    5.25 +  unfolding absolutely_integrable_on_def 
    5.26 +  by (simp add: norm_mult)
    5.27 +qed auto
    5.28 +
    5.29  lemma lmeasurable_iff_integrable_on: "S \<in> lmeasurable \<longleftrightarrow> (\<lambda>x. 1::real) integrable_on S"
    5.30    by (subst absolutely_integrable_on_iff_nonneg[symmetric])
    5.31       (simp_all add: lmeasurable_iff_integrable set_integrable_def)
    5.32 @@ -2128,9 +2143,6 @@
    5.33    using integrable_bounded_linear[of h lebesgue "\<lambda>x. indicator s x *\<^sub>R f x"]
    5.34    by (simp add: linear_simps[of h] set_integrable_def)
    5.35  
    5.36 -lemma absolutely_integrable_zero [simp]: "(\<lambda>x. 0) absolutely_integrable_on S"
    5.37 -    by (simp add: set_integrable_def)
    5.38 -
    5.39  lemma absolutely_integrable_sum:
    5.40    fixes f :: "'a \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
    5.41    assumes "finite T" and "\<And>a. a \<in> T \<Longrightarrow> (f a) absolutely_integrable_on S"
    5.42 @@ -2477,6 +2489,75 @@
    5.43      by simp
    5.44  qed
    5.45  
    5.46 +lemma dominated_convergence_integrable_1:
    5.47 +  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
    5.48 +  assumes f: "\<And>k. f k absolutely_integrable_on S"
    5.49 +    and h: "h integrable_on S"
    5.50 +    and normg: "\<And>x. x \<in> S \<Longrightarrow> norm(g x) \<le> (h x)"
    5.51 +    and lim: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
    5.52 + shows "g integrable_on S"
    5.53 +proof -
    5.54 +  have habs: "h absolutely_integrable_on S"
    5.55 +    using h normg nonnegative_absolutely_integrable_1 norm_ge_zero order_trans by blast
    5.56 +  let ?f = "\<lambda>n x. (min (max (- h x) (f n x)) (h x))"
    5.57 +  have h0: "h x \<ge> 0" if "x \<in> S" for x
    5.58 +    using normg that by force
    5.59 +  have leh: "norm (?f k x) \<le> h x" if "x \<in> S" for k x
    5.60 +    using h0 that by force
    5.61 +  have limf: "(\<lambda>k. ?f k x) \<longlonglongrightarrow> g x" if "x \<in> S" for x
    5.62 +  proof -
    5.63 +    have "\<And>e y. \<bar>f y x - g x\<bar> < e \<Longrightarrow> \<bar>min (max (- h x) (f y x)) (h x) - g x\<bar> < e"
    5.64 +      using h0 [OF that] normg [OF that] by simp
    5.65 +    then show ?thesis
    5.66 +      using lim [OF that] by (auto simp add: tendsto_iff dist_norm elim!: eventually_mono)
    5.67 +  qed
    5.68 +  show ?thesis
    5.69 +  proof (rule dominated_convergence [of ?f S h g])
    5.70 +    have "(\<lambda>x. - h x) absolutely_integrable_on S"
    5.71 +      using habs unfolding set_integrable_def by auto
    5.72 +    then show "?f k integrable_on S" for k
    5.73 +      by (intro set_lebesgue_integral_eq_integral absolutely_integrable_min_1 absolutely_integrable_max_1 f habs)
    5.74 +  qed (use assms leh limf in auto)
    5.75 +qed
    5.76 +
    5.77 +lemma dominated_convergence_integrable:
    5.78 +  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
    5.79 +  assumes f: "\<And>k. f k absolutely_integrable_on S"
    5.80 +    and h: "h integrable_on S"
    5.81 +    and normg: "\<And>x. x \<in> S \<Longrightarrow> norm(g x) \<le> (h x)"
    5.82 +    and lim: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
    5.83 +  shows "g integrable_on S"
    5.84 +  using f
    5.85 +  unfolding integrable_componentwise_iff [of g] absolutely_integrable_componentwise_iff [where f = "f k" for k]
    5.86 +proof clarify
    5.87 +  fix b :: "'m"
    5.88 +  assume fb [rule_format]: "\<And>k. \<forall>b\<in>Basis. (\<lambda>x. f k x \<bullet> b) absolutely_integrable_on S" and b: "b \<in> Basis"
    5.89 +  show "(\<lambda>x. g x \<bullet> b) integrable_on S"
    5.90 +  proof (rule dominated_convergence_integrable_1 [OF fb h])
    5.91 +    fix x 
    5.92 +    assume "x \<in> S"
    5.93 +    show "norm (g x \<bullet> b) \<le> h x"
    5.94 +      using norm_nth_le \<open>x \<in> S\<close> b normg order.trans by blast
    5.95 +    show "(\<lambda>k. f k x \<bullet> b) \<longlonglongrightarrow> g x \<bullet> b"
    5.96 +      using \<open>x \<in> S\<close> b lim tendsto_componentwise_iff by fastforce
    5.97 +  qed (use b in auto)
    5.98 +qed
    5.99 +
   5.100 +
   5.101 +lemma dominated_convergence_absolutely_integrable:
   5.102 +  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   5.103 +  assumes f: "\<And>k. f k absolutely_integrable_on S"
   5.104 +    and h: "h integrable_on S"
   5.105 +    and normg: "\<And>x. x \<in> S \<Longrightarrow> norm(g x) \<le> (h x)"
   5.106 +    and lim: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
   5.107 +  shows "g absolutely_integrable_on S"
   5.108 +proof -
   5.109 +  have "g integrable_on S"
   5.110 +    by (rule dominated_convergence_integrable [OF assms])
   5.111 +  with assms show ?thesis
   5.112 +    by (blast intro:  absolutely_integrable_integrable_bound [where g=h])
   5.113 +qed
   5.114 +
   5.115  subsection \<open>Fundamental Theorem of Calculus for the Lebesgue integral\<close>
   5.116  
   5.117  text \<open>
     6.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Apr 13 17:00:57 2018 +0100
     6.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Apr 14 09:23:00 2018 +0100
     6.3 @@ -5258,7 +5258,7 @@
     6.4    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
     6.5    assumes "f integrable_on S" "f integrable_on T" "negligible (S \<inter> T)"
     6.6    shows "integral (S \<union> T) f = integral S f + integral T f"
     6.7 -  using has_integral_Un by (simp add: has_integral_Un assms integrable_integral integral_unique)
     6.8 +  by (simp add: has_integral_Un assms integrable_integral integral_unique)
     6.9  
    6.10  lemma integrable_Un:
    6.11    fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: banach"
     7.1 --- a/src/HOL/Analysis/Lipschitz.thy	Fri Apr 13 17:00:57 2018 +0100
     7.2 +++ b/src/HOL/Analysis/Lipschitz.thy	Sat Apr 14 09:23:00 2018 +0100
     7.3 @@ -816,7 +816,7 @@
     7.4      finally
     7.5      have deriv: "\<forall>y\<in>cball x u. (f s has_derivative blinfun_apply (f' (s, y))) (at y within cball x u)"
     7.6        using \<open>_ \<subseteq> X\<close>
     7.7 -      by (auto intro!: has_derivative_at_within[OF f'])
     7.8 +      by (auto intro!: has_derivative_at_withinI[OF f'])
     7.9      have "norm (f s y - f s z) \<le> B * norm (y - z)"
    7.10        if "y \<in> cball x u" "z \<in> cball x u"
    7.11        for y z
     8.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Apr 13 17:00:57 2018 +0100
     8.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sat Apr 14 09:23:00 2018 +0100
     8.3 @@ -3219,7 +3219,7 @@
     8.4  lemma netlimit_within: "\<not> trivial_limit (at a within S) \<Longrightarrow> netlimit (at a within S) = a"
     8.5    by (rule tendsto_Lim) (auto intro: tendsto_intros)
     8.6  
     8.7 -lemma netlimit_at:
     8.8 +lemma netlimit_at [simp]:
     8.9    fixes a :: "'a::{perfect_space,t2_space}"
    8.10    shows "netlimit (at a) = a"
    8.11    using netlimit_within [of a UNIV] by simp