moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
authorimmler
Thu Feb 22 15:17:25 2018 +0100 (15 months ago)
changeset 67685bdff8bf0a75b
parent 67682 00c436488398
child 67686 2c58505bf151
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
src/HOL/Analysis/Borel_Space.thy
src/HOL/Analysis/Bounded_Linear_Function.thy
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Connected.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Euclidean_Space.thy
src/HOL/Analysis/Finite_Cartesian_Product.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/L2_Norm.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Operator_Norm.thy
src/HOL/Analysis/Ordered_Euclidean_Space.thy
src/HOL/Analysis/Product_Vector.thy
src/HOL/Analysis/Riemann_Mapping.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Analysis/Uniform_Limit.thy
src/HOL/Deriv.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Limits.thy
src/HOL/NthRoot.thy
src/HOL/Set_Interval.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Analysis/Borel_Space.thy	Tue Feb 20 22:25:23 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Thu Feb 22 15:17:25 2018 +0100
     1.3 @@ -242,6 +242,11 @@
     1.4    shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S"
     1.5    by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup)
     1.6  
     1.7 +lemma closed_subset_contains_Sup:
     1.8 +  fixes A C :: "real set"
     1.9 +  shows "closed C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> Sup A \<in> C"
    1.10 +  by (metis closure_contains_Sup closure_minimal subset_eq)
    1.11 +
    1.12  lemma deriv_nonneg_imp_mono:
    1.13    assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
    1.14    assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
     2.1 --- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Tue Feb 20 22:25:23 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Feb 22 15:17:25 2018 +0100
     2.3 @@ -8,8 +8,35 @@
     2.4  imports
     2.5    Topology_Euclidean_Space
     2.6    Operator_Norm
     2.7 +  Uniform_Limit
     2.8  begin
     2.9  
    2.10 +lemma onorm_componentwise:
    2.11 +  assumes "bounded_linear f"
    2.12 +  shows "onorm f \<le> (\<Sum>i\<in>Basis. norm (f i))"
    2.13 +proof -
    2.14 +  {
    2.15 +    fix i::'a
    2.16 +    assume "i \<in> Basis"
    2.17 +    hence "onorm (\<lambda>x. (x \<bullet> i) *\<^sub>R f i) \<le> onorm (\<lambda>x. (x \<bullet> i)) * norm (f i)"
    2.18 +      by (auto intro!: onorm_scaleR_left_lemma bounded_linear_inner_left)
    2.19 +    also have "\<dots> \<le>  norm i * norm (f i)"
    2.20 +      by (rule mult_right_mono)
    2.21 +        (auto simp: ac_simps Cauchy_Schwarz_ineq2 intro!: onorm_le)
    2.22 +    finally have "onorm (\<lambda>x. (x \<bullet> i) *\<^sub>R f i) \<le> norm (f i)" using \<open>i \<in> Basis\<close>
    2.23 +      by simp
    2.24 +  } hence "onorm (\<lambda>x. \<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<le> (\<Sum>i\<in>Basis. norm (f i))"
    2.25 +    by (auto intro!: order_trans[OF onorm_sum_le] bounded_linear_scaleR_const
    2.26 +      sum_mono bounded_linear_inner_left)
    2.27 +  also have "(\<lambda>x. \<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) = (\<lambda>x. f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i))"
    2.28 +    by (simp add: linear_sum bounded_linear.linear assms linear_simps)
    2.29 +  also have "\<dots> = f"
    2.30 +    by (simp add: euclidean_representation)
    2.31 +  finally show ?thesis .
    2.32 +qed
    2.33 +
    2.34 +lemmas onorm_componentwise_le = order_trans[OF onorm_componentwise]
    2.35 +
    2.36  subsection \<open>Intro rules for @{term bounded_linear}\<close>
    2.37  
    2.38  named_theorems bounded_linear_intros
    2.39 @@ -447,6 +474,15 @@
    2.40    shows "continuous F f"
    2.41    using assms by (auto simp: continuous_def intro!: tendsto_componentwise1)
    2.42  
    2.43 +lemma
    2.44 +  continuous_on_blinfun_componentwise:
    2.45 +  fixes f:: "'d::t2_space \<Rightarrow> 'e::euclidean_space \<Rightarrow>\<^sub>L 'f::real_normed_vector"
    2.46 +  assumes "\<And>i. i \<in> Basis \<Longrightarrow> continuous_on s (\<lambda>x. f x i)"
    2.47 +  shows "continuous_on s f"
    2.48 +  using assms
    2.49 +  by (auto intro!: continuous_at_imp_continuous_on intro!: tendsto_componentwise1
    2.50 +    simp: continuous_on_eq_continuous_within continuous_def)
    2.51 +
    2.52  lemma bounded_linear_blinfun_matrix: "bounded_linear (\<lambda>x. (x::_\<Rightarrow>\<^sub>L _) j \<bullet> i)"
    2.53    by (auto intro!: bounded_linearI' bounded_linear_intros)
    2.54  
    2.55 @@ -692,4 +728,9 @@
    2.56  lemma bounded_linear_blinfun_mult_left[bounded_linear]: "bounded_linear blinfun_mult_left"
    2.57    by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_mult])
    2.58  
    2.59 +lemmas bounded_linear_function_uniform_limit_intros[uniform_limit_intros] =
    2.60 +  bounded_linear.uniform_limit[OF bounded_linear_apply_blinfun]
    2.61 +  bounded_linear.uniform_limit[OF bounded_linear_blinfun_apply]
    2.62 +  bounded_linear.uniform_limit[OF bounded_linear_blinfun_matrix]
    2.63 +
    2.64  end
     3.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Tue Feb 20 22:25:23 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Feb 22 15:17:25 2018 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space.\<close>
     3.5  
     3.6  theory Cartesian_Euclidean_Space
     3.7 -imports Finite_Cartesian_Product Derivative 
     3.8 +imports Finite_Cartesian_Product Derivative
     3.9  begin
    3.10  
    3.11  lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}"
    3.12 @@ -1455,4 +1455,9 @@
    3.13    unfolding vec_lambda_beta
    3.14    by auto
    3.15  
    3.16 +lemmas cartesian_euclidean_space_uniform_limit_intros[uniform_limit_intros] =
    3.17 +  bounded_linear.uniform_limit[OF blinfun.bounded_linear_right]
    3.18 +  bounded_linear.uniform_limit[OF bounded_linear_vec_nth]
    3.19 +  bounded_linear.uniform_limit[OF bounded_linear_component_cart]
    3.20 +
    3.21  end
     4.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Feb 20 22:25:23 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Feb 22 15:17:25 2018 +0100
     4.3 @@ -1199,7 +1199,7 @@
     4.4  
     4.5  lemma vector_derivative_linepath_within:
     4.6      "x \<in> {0..1} \<Longrightarrow> vector_derivative (linepath a b) (at x within {0..1}) = b - a"
     4.7 -  apply (rule vector_derivative_within_closed_interval [of 0 "1::real", simplified])
     4.8 +  apply (rule vector_derivative_within_cbox [of 0 "1::real", simplified])
     4.9    apply (auto simp: has_vector_derivative_linepath_within)
    4.10    done
    4.11  
    4.12 @@ -2695,7 +2695,7 @@
    4.13    then have *: "(\<lambda>y. (?pathint x y - f x * (y - x)) /\<^sub>R cmod (y - x)) \<midarrow>x\<rightarrow> 0"
    4.14      by (simp add: Lim_at dist_norm inverse_eq_divide)
    4.15    show ?thesis
    4.16 -    apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right)
    4.17 +    apply (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right)
    4.18      apply (rule Lim_transform [OF * Lim_eventually])
    4.19      apply (simp add: inverse_eq_divide [symmetric] eventually_at)
    4.20      using \<open>open s\<close> x
    4.21 @@ -3573,7 +3573,7 @@
    4.22        if "x \<in> {0..1} - S" for x
    4.23      proof -
    4.24        have "vector_derivative (uminus \<circ> \<gamma>) (at x within cbox 0 1) = - vector_derivative \<gamma> (at x within cbox 0 1)"
    4.25 -        apply (rule vector_derivative_within_closed_interval)
    4.26 +        apply (rule vector_derivative_within_cbox)
    4.27          using that
    4.28            apply (auto simp: o_def)
    4.29          apply (rule has_vector_derivative_minus)
     5.1 --- a/src/HOL/Analysis/Connected.thy	Tue Feb 20 22:25:23 2018 +0100
     5.2 +++ b/src/HOL/Analysis/Connected.thy	Thu Feb 22 15:17:25 2018 +0100
     5.3 @@ -1095,6 +1095,43 @@
     5.4    qed
     5.5  qed
     5.6  
     5.7 +text \<open>Hence some handy theorems on distance, diameter etc. of/from a set.\<close>
     5.8 +
     5.9 +lemma distance_attains_sup:
    5.10 +  assumes "compact s" "s \<noteq> {}"
    5.11 +  shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a y \<le> dist a x"
    5.12 +proof (rule continuous_attains_sup [OF assms])
    5.13 +  {
    5.14 +    fix x
    5.15 +    assume "x\<in>s"
    5.16 +    have "(dist a \<longlongrightarrow> dist a x) (at x within s)"
    5.17 +      by (intro tendsto_dist tendsto_const tendsto_ident_at)
    5.18 +  }
    5.19 +  then show "continuous_on s (dist a)"
    5.20 +    unfolding continuous_on ..
    5.21 +qed
    5.22 +
    5.23 +text \<open>For \emph{minimal} distance, we only need closure, not compactness.\<close>
    5.24 +
    5.25 +lemma distance_attains_inf:
    5.26 +  fixes a :: "'a::heine_borel"
    5.27 +  assumes "closed s" and "s \<noteq> {}"
    5.28 +  obtains x where "x\<in>s" "\<And>y. y \<in> s \<Longrightarrow> dist a x \<le> dist a y"
    5.29 +proof -
    5.30 +  from assms obtain b where "b \<in> s" by auto
    5.31 +  let ?B = "s \<inter> cball a (dist b a)"
    5.32 +  have "?B \<noteq> {}" using \<open>b \<in> s\<close>
    5.33 +    by (auto simp: dist_commute)
    5.34 +  moreover have "continuous_on ?B (dist a)"
    5.35 +    by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
    5.36 +  moreover have "compact ?B"
    5.37 +    by (intro closed_Int_compact \<open>closed s\<close> compact_cball)
    5.38 +  ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
    5.39 +    by (metis continuous_attains_inf)
    5.40 +  with that show ?thesis by fastforce
    5.41 +qed
    5.42 +
    5.43 +
    5.44  subsection\<open>Relations among convergence and absolute convergence for power series.\<close>
    5.45  
    5.46  lemma summable_imp_bounded:
    5.47 @@ -1353,6 +1390,24 @@
    5.48    shows "infdist x S > 0"
    5.49  using in_closed_iff_infdist_zero[OF assms(1) assms(2), of x] assms(3) infdist_nonneg le_less by fastforce
    5.50  
    5.51 +lemma
    5.52 +  infdist_attains_inf:
    5.53 +  fixes X::"'a::heine_borel set"
    5.54 +  assumes "closed X"
    5.55 +  assumes "X \<noteq> {}"
    5.56 +  obtains x where "x \<in> X" "infdist y X = dist y x"
    5.57 +proof -
    5.58 +  have "bdd_below (dist y ` X)"
    5.59 +    by auto
    5.60 +  from distance_attains_inf[OF assms, of y]
    5.61 +  obtain x where INF: "x \<in> X" "\<And>z. z \<in> X \<Longrightarrow> dist y x \<le> dist y z" by auto
    5.62 +  have "infdist y X = dist y x"
    5.63 +    by (auto simp: infdist_def assms
    5.64 +      intro!: antisym cINF_lower[OF _ \<open>x \<in> X\<close>] cINF_greatest[OF assms(2) INF(2)])
    5.65 +  with \<open>x \<in> X\<close> show ?thesis ..
    5.66 +qed
    5.67 +
    5.68 +
    5.69  text \<open>Every metric space is a T4 space:\<close>
    5.70  
    5.71  instance metric_space \<subseteq> t4_space
    5.72 @@ -1423,6 +1478,36 @@
    5.73    shows "continuous F (\<lambda>x. infdist (f x) A)"
    5.74    using assms unfolding continuous_def by (rule tendsto_infdist)
    5.75  
    5.76 +lemma compact_infdist_le:
    5.77 +  fixes A::"'a::heine_borel set"
    5.78 +  assumes "A \<noteq> {}"
    5.79 +  assumes "compact A"
    5.80 +  assumes "e > 0"
    5.81 +  shows "compact {x. infdist x A \<le> e}"
    5.82 +proof -
    5.83 +  from continuous_closed_vimage[of "{0..e}" "\<lambda>x. infdist x A"]
    5.84 +    continuous_infdist[OF continuous_ident, of _ UNIV A]
    5.85 +  have "closed {x. infdist x A \<le> e}" by (auto simp: vimage_def infdist_nonneg)
    5.86 +  moreover
    5.87 +  from assms obtain x0 b where b: "\<And>x. x \<in> A \<Longrightarrow> dist x0 x \<le> b" "closed A"
    5.88 +    by (auto simp: compact_eq_bounded_closed bounded_def)
    5.89 +  {
    5.90 +    fix y
    5.91 +    assume le: "infdist y A \<le> e"
    5.92 +    from infdist_attains_inf[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>, of y]
    5.93 +    obtain z where z: "z \<in> A" "infdist y A = dist y z" by blast
    5.94 +    have "dist x0 y \<le> dist y z + dist x0 z"
    5.95 +      by (metis dist_commute dist_triangle)
    5.96 +    also have "dist y z \<le> e" using le z by simp
    5.97 +    also have "dist x0 z \<le> b" using b z by simp
    5.98 +    finally have "dist x0 y \<le> b + e" by arith
    5.99 +  } then
   5.100 +  have "bounded {x. infdist x A \<le> e}"
   5.101 +    by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"])
   5.102 +  ultimately show "compact {x. infdist x A \<le> e}"
   5.103 +    by (simp add: compact_eq_bounded_closed)
   5.104 +qed
   5.105 +
   5.106  subsection \<open>Equality of continuous functions on closure and related results.\<close>
   5.107  
   5.108  lemma continuous_closedin_preimage_constant:
   5.109 @@ -2209,6 +2294,13 @@
   5.110      by (metis assms continuous_open_vimage vimage_def)
   5.111  qed
   5.112  
   5.113 +lemma open_neg_translation:
   5.114 +  fixes s :: "'a::real_normed_vector set"
   5.115 +  assumes "open s"
   5.116 +  shows "open((\<lambda>x. a - x) ` s)"
   5.117 +  using open_translation[OF open_negations[OF assms], of a]
   5.118 +  by (auto simp: image_image)
   5.119 +
   5.120  lemma open_affinity:
   5.121    fixes S :: "'a::real_normed_vector set"
   5.122    assumes "open S"  "c \<noteq> 0"
   5.123 @@ -2392,42 +2484,6 @@
   5.124      (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d \<longrightarrow> \<bar>f x' - f x\<bar> < e))"
   5.125    unfolding continuous_on_iff dist_norm by simp
   5.126  
   5.127 -text \<open>Hence some handy theorems on distance, diameter etc. of/from a set.\<close>
   5.128 -
   5.129 -lemma distance_attains_sup:
   5.130 -  assumes "compact s" "s \<noteq> {}"
   5.131 -  shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a y \<le> dist a x"
   5.132 -proof (rule continuous_attains_sup [OF assms])
   5.133 -  {
   5.134 -    fix x
   5.135 -    assume "x\<in>s"
   5.136 -    have "(dist a \<longlongrightarrow> dist a x) (at x within s)"
   5.137 -      by (intro tendsto_dist tendsto_const tendsto_ident_at)
   5.138 -  }
   5.139 -  then show "continuous_on s (dist a)"
   5.140 -    unfolding continuous_on ..
   5.141 -qed
   5.142 -
   5.143 -text \<open>For \emph{minimal} distance, we only need closure, not compactness.\<close>
   5.144 -
   5.145 -lemma distance_attains_inf:
   5.146 -  fixes a :: "'a::heine_borel"
   5.147 -  assumes "closed s" and "s \<noteq> {}"
   5.148 -  obtains x where "x\<in>s" "\<And>y. y \<in> s \<Longrightarrow> dist a x \<le> dist a y"
   5.149 -proof -
   5.150 -  from assms obtain b where "b \<in> s" by auto
   5.151 -  let ?B = "s \<inter> cball a (dist b a)"
   5.152 -  have "?B \<noteq> {}" using \<open>b \<in> s\<close>
   5.153 -    by (auto simp: dist_commute)
   5.154 -  moreover have "continuous_on ?B (dist a)"
   5.155 -    by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
   5.156 -  moreover have "compact ?B"
   5.157 -    by (intro closed_Int_compact \<open>closed s\<close> compact_cball)
   5.158 -  ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
   5.159 -    by (metis continuous_attains_inf)
   5.160 -  with that show ?thesis by fastforce
   5.161 -qed
   5.162 -
   5.163  
   5.164  subsection \<open>Cartesian products\<close>
   5.165  
   5.166 @@ -2911,6 +2967,38 @@
   5.167      using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute)
   5.168  qed
   5.169  
   5.170 +lemma compact_in_open_separated:
   5.171 +  fixes A::"'a::heine_borel set"
   5.172 +  assumes "A \<noteq> {}"
   5.173 +  assumes "compact A"
   5.174 +  assumes "open B"
   5.175 +  assumes "A \<subseteq> B"
   5.176 +  obtains e where "e > 0" "{x. infdist x A \<le> e} \<subseteq> B"
   5.177 +proof atomize_elim
   5.178 +  have "closed (- B)" "compact A" "- B \<inter> A = {}"
   5.179 +    using assms by (auto simp: open_Diff compact_eq_bounded_closed)
   5.180 +  from separate_closed_compact[OF this]
   5.181 +  obtain d'::real where d': "d'>0" "\<And>x y. x \<notin> B \<Longrightarrow> y \<in> A \<Longrightarrow> d' \<le> dist x y"
   5.182 +    by auto
   5.183 +  define d where "d = d' / 2"
   5.184 +  hence "d>0" "d < d'" using d' by auto
   5.185 +  with d' have d: "\<And>x y. x \<notin> B \<Longrightarrow> y \<in> A \<Longrightarrow> d < dist x y"
   5.186 +    by force
   5.187 +  show "\<exists>e>0. {x. infdist x A \<le> e} \<subseteq> B"
   5.188 +  proof (rule ccontr)
   5.189 +    assume "\<nexists>e. 0 < e \<and> {x. infdist x A \<le> e} \<subseteq> B"
   5.190 +    with \<open>d > 0\<close> obtain x where x: "infdist x A \<le> d" "x \<notin> B"
   5.191 +      by auto
   5.192 +    from assms have "closed A" "A \<noteq> {}" by (auto simp: compact_eq_bounded_closed)
   5.193 +    from infdist_attains_inf[OF this]
   5.194 +    obtain y where y: "y \<in> A" "infdist x A = dist x y"
   5.195 +      by auto
   5.196 +    have "dist x y \<le> d" using x y by simp
   5.197 +    also have "\<dots> < dist x y" using y d x by auto
   5.198 +    finally show False by simp
   5.199 +  qed
   5.200 +qed
   5.201 +
   5.202  
   5.203  subsection \<open>Compact sets and the closure operation.\<close>
   5.204  
   5.205 @@ -4221,6 +4309,14 @@
   5.206      using \<open>x\<in>s\<close> by blast
   5.207  qed
   5.208  
   5.209 +lemma banach_fix_type:
   5.210 +  fixes f::"'a::complete_space\<Rightarrow>'a"
   5.211 +  assumes c:"0 \<le> c" "c < 1"
   5.212 +      and lipschitz:"\<forall>x. \<forall>y. dist (f x) (f y) \<le> c * dist x y"
   5.213 +  shows "\<exists>!x. (f x = x)"
   5.214 +  using assms banach_fix[OF complete_UNIV UNIV_not_empty assms(1,2) subset_UNIV, of f]
   5.215 +  by auto
   5.216 +
   5.217  
   5.218  subsection \<open>Edelstein fixed point theorem\<close>
   5.219  
     6.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Feb 20 22:25:23 2018 +0100
     6.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Feb 22 15:17:25 2018 +0100
     6.3 @@ -6659,9 +6659,13 @@
     6.4  
     6.5  subsection \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
     6.6  
     6.7 -lemma is_interval_1:
     6.8 -  "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
     6.9 -  unfolding is_interval_def by auto
    6.10 +lemma mem_is_interval_1_I:
    6.11 +  fixes a b c::real
    6.12 +  assumes "is_interval S"
    6.13 +  assumes "a \<in> S" "c \<in> S"
    6.14 +  assumes "a \<le> b" "b \<le> c"
    6.15 +  shows "b \<in> S"
    6.16 +  using assms is_interval_1 by blast
    6.17  
    6.18  lemma is_interval_connected_1:
    6.19    fixes s :: "real set"
    6.20 @@ -6708,6 +6712,9 @@
    6.21    shows "is_interval s \<longleftrightarrow> convex s"
    6.22    by (metis is_interval_convex convex_connected is_interval_connected_1)
    6.23  
    6.24 +lemma is_interval_ball_real: "is_interval (ball a b)" for a b::real
    6.25 +  by (metis connected_ball is_interval_connected_1)
    6.26 +
    6.27  lemma connected_compact_interval_1:
    6.28       "connected S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = {a..b::real})"
    6.29    by (auto simp: is_interval_connected_1 [symmetric] is_interval_compact)
    6.30 @@ -6731,6 +6738,10 @@
    6.31      by (metis connected_convex_1 convex_linear_vimage linf convex_connected connected_linear_image)
    6.32  qed
    6.33  
    6.34 +lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real
    6.35 +  by (auto simp: is_interval_convex_1 convex_cball)
    6.36 +
    6.37 +
    6.38  subsection \<open>Another intermediate value theorem formulation\<close>
    6.39  
    6.40  lemma ivt_increasing_component_on_1:
     7.1 --- a/src/HOL/Analysis/Derivative.thy	Tue Feb 20 22:25:23 2018 +0100
     7.2 +++ b/src/HOL/Analysis/Derivative.thy	Thu Feb 22 15:17:25 2018 +0100
     7.3 @@ -48,18 +48,6 @@
     7.4    shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
     7.5    using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
     7.6  
     7.7 -text \<open>These are the only cases we'll care about, probably.\<close>
     7.8 -
     7.9 -lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
    7.10 -    bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x within s)"
    7.11 -  unfolding has_derivative_def Lim
    7.12 -  by (auto simp add: netlimit_within field_simps)
    7.13 -
    7.14 -lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
    7.15 -    bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x)"
    7.16 -  using has_derivative_within [of f f' x UNIV]
    7.17 -  by simp
    7.18 -
    7.19  text \<open>More explicit epsilon-delta forms.\<close>
    7.20  
    7.21  lemma has_derivative_within':
    7.22 @@ -131,27 +119,6 @@
    7.23      by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
    7.24  qed
    7.25  
    7.26 -subsubsection \<open>Limit transformation for derivatives\<close>
    7.27 -
    7.28 -lemma has_derivative_transform_within:
    7.29 -  assumes "(f has_derivative f') (at x within s)"
    7.30 -    and "0 < d"
    7.31 -    and "x \<in> s"
    7.32 -    and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
    7.33 -  shows "(g has_derivative f') (at x within s)"
    7.34 -  using assms
    7.35 -  unfolding has_derivative_within
    7.36 -  by (force simp add: intro: Lim_transform_within)
    7.37 -
    7.38 -lemma has_derivative_transform_within_open:
    7.39 -  assumes "(f has_derivative f') (at x)"
    7.40 -    and "open s"
    7.41 -    and "x \<in> s"
    7.42 -    and "\<And>x. x\<in>s \<Longrightarrow> f x = g x"
    7.43 -  shows "(g has_derivative f') (at x)"
    7.44 -  using assms  unfolding has_derivative_at
    7.45 -  by (force simp add: intro: Lim_transform_within_open)
    7.46 -
    7.47  subsection \<open>Differentiability\<close>
    7.48  
    7.49  definition
    7.50 @@ -304,6 +271,10 @@
    7.51    unfolding differentiable_on_def
    7.52    by auto
    7.53  
    7.54 +lemma has_derivative_continuous_on:
    7.55 +  "(\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x within s)) \<Longrightarrow> continuous_on s f"
    7.56 +  by (auto intro!: differentiable_imp_continuous_on differentiableI simp: differentiable_on_def)
    7.57 +
    7.58  text \<open>Results about neighborhoods filter.\<close>
    7.59  
    7.60  lemma eventually_nhds_metric_le:
    7.61 @@ -1143,6 +1114,20 @@
    7.62      by (simp add: g_def field_simps linear_diff[OF has_derivative_linear[OF f']])
    7.63  qed
    7.64  
    7.65 +lemma vector_differentiable_bound_linearization:
    7.66 +  fixes f::"real \<Rightarrow> 'b::real_normed_vector"
    7.67 +  assumes f': "\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)"
    7.68 +  assumes "closed_segment a b \<subseteq> S"
    7.69 +  assumes B: "\<forall>x\<in>S. norm (f' x - f' x0) \<le> B"
    7.70 +  assumes "x0 \<in> S"
    7.71 +  shows "norm (f b - f a - (b - a) *\<^sub>R f' x0) \<le> norm (b - a) * B"
    7.72 +  using assms
    7.73 +  by (intro differentiable_bound_linearization[of a b S f "\<lambda>x h. h *\<^sub>R f' x" x0 B])
    7.74 +    (force simp: closed_segment_real_eq has_vector_derivative_def
    7.75 +      scaleR_diff_right[symmetric] mult.commute[of B]
    7.76 +      intro!: onorm_le mult_left_mono)+
    7.77 +
    7.78 +
    7.79  text \<open>In particular.\<close>
    7.80  
    7.81  lemma has_derivative_zero_constant:
    7.82 @@ -1169,6 +1154,14 @@
    7.83      using assms(2)[of x] by (simp add: has_field_derivative_def A)
    7.84  qed fact
    7.85  
    7.86 +lemma
    7.87 +  has_vector_derivative_zero_constant:
    7.88 +  assumes "convex s"
    7.89 +  assumes "\<And>x. x \<in> s \<Longrightarrow> (f has_vector_derivative 0) (at x within s)"
    7.90 +  obtains c where "\<And>x. x \<in> s \<Longrightarrow> f x = c"
    7.91 +  using has_derivative_zero_constant[of s f] assms
    7.92 +  by (auto simp: has_vector_derivative_def)
    7.93 +
    7.94  lemma has_derivative_zero_unique:
    7.95    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
    7.96    assumes "convex s"
    7.97 @@ -2510,7 +2503,7 @@
    7.98  apply (auto simp: vector_derivative_works has_vector_derivative_def has_field_derivative_def mult_commute_abs)
    7.99  done
   7.100  
   7.101 -lemma vector_derivative_within_closed_interval:
   7.102 +lemma vector_derivative_within_cbox:
   7.103    assumes ab: "a < b" "x \<in> cbox a b"
   7.104    assumes f: "(f has_vector_derivative f') (at x within cbox a b)"
   7.105    shows "vector_derivative f (at x within cbox a b) = f'"
   7.106 @@ -2518,6 +2511,14 @@
   7.107              vector_derivative_works[THEN iffD1] differentiableI_vector)
   7.108       fact
   7.109  
   7.110 +lemma vector_derivative_within_closed_interval:
   7.111 +  fixes f::"real \<Rightarrow> 'a::euclidean_space"
   7.112 +  assumes "a < b" and "x \<in> {a .. b}"
   7.113 +  assumes "(f has_vector_derivative f') (at x within {a .. b})"
   7.114 +  shows "vector_derivative f (at x within {a .. b}) = f'"
   7.115 +  using assms vector_derivative_within_cbox
   7.116 +  by fastforce
   7.117 +
   7.118  lemma has_vector_derivative_within_subset:
   7.119    "(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
   7.120    by (auto simp: has_vector_derivative_def intro: has_derivative_within_subset)
   7.121 @@ -2561,6 +2562,14 @@
   7.122    unfolding has_vector_derivative_def
   7.123    by (rule has_derivative_transform_within_open)
   7.124  
   7.125 +lemma has_vector_derivative_transform:
   7.126 +  assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
   7.127 +  assumes f': "(f has_vector_derivative f') (at x within s)"
   7.128 +  shows "(g has_vector_derivative f') (at x within s)"
   7.129 +  using assms
   7.130 +  unfolding has_vector_derivative_def
   7.131 +  by (rule has_derivative_transform)
   7.132 +
   7.133  lemma vector_diff_chain_at:
   7.134    assumes "(f has_vector_derivative f') (at x)"
   7.135      and "(g has_vector_derivative g') (at (f x))"
   7.136 @@ -2589,7 +2598,7 @@
   7.137  lemma vector_derivative_at_within_ivl:
   7.138    "(f has_vector_derivative f') (at x) \<Longrightarrow>
   7.139      a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> a<b \<Longrightarrow> vector_derivative f (at x within {a..b}) = f'"
   7.140 -using has_vector_derivative_at_within vector_derivative_within_closed_interval by fastforce
   7.141 +  using has_vector_derivative_at_within vector_derivative_within_cbox by fastforce
   7.142  
   7.143  lemma vector_derivative_chain_at:
   7.144    assumes "f differentiable at x" "(g differentiable at (f x))"
   7.145 @@ -2917,21 +2926,19 @@
   7.146  qed
   7.147  
   7.148  lemma has_derivative_partialsI:
   7.149 -  assumes fx: "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> ((\<lambda>x. f x y) has_derivative blinfun_apply (fx x y)) (at x within X)"
   7.150 +  fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector \<Rightarrow> 'c::real_normed_vector"
   7.151 +  assumes fx: "((\<lambda>x. f x y) has_derivative fx) (at x within X)"
   7.152    assumes fy: "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> ((\<lambda>y. f x y) has_derivative blinfun_apply (fy x y)) (at y within Y)"
   7.153 -  assumes fx_cont: "continuous_on (X \<times> Y) (\<lambda>(x, y). fx x y)"
   7.154 -  assumes fy_cont: "continuous_on (X \<times> Y) (\<lambda>(x, y). fy x y)"
   7.155 -  assumes "x \<in> X" "y \<in> Y"
   7.156 -  assumes "convex X" "convex Y"
   7.157 -  shows "((\<lambda>(x, y). f x y) has_derivative (\<lambda>(tx, ty). fx x y tx + fy x y ty)) (at (x, y) within X \<times> Y)"
   7.158 +  assumes fy_cont[unfolded continuous_within]: "continuous (at (x, y) within X \<times> Y) (\<lambda>(x, y). fy x y)"
   7.159 +  assumes "y \<in> Y" "convex Y"
   7.160 +  shows "((\<lambda>(x, y). f x y) has_derivative (\<lambda>(tx, ty). fx tx + fy x y ty)) (at (x, y) within X \<times> Y)"
   7.161  proof (safe intro!: has_derivativeI tendstoI, goal_cases)
   7.162    case (2 e')
   7.163 +  interpret fx: bounded_linear "fx" using fx by (rule has_derivative_bounded_linear)
   7.164    define e where "e = e' / 9"
   7.165    have "e > 0" using \<open>e' > 0\<close> by (simp add: e_def)
   7.166  
   7.167 -  have "(x, y) \<in> X \<times> Y" using assms by auto
   7.168 -  from fy_cont[unfolded continuous_on_eq_continuous_within, rule_format, OF this,
   7.169 -    unfolded continuous_within, THEN tendstoD, OF \<open>e > 0\<close>]
   7.170 +  from fy_cont[THEN tendstoD, OF \<open>e > 0\<close>]
   7.171    have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. dist (fy x' y') (fy x y) < e"
   7.172      by (auto simp: split_beta')
   7.173    from this[unfolded eventually_at] obtain d' where
   7.174 @@ -2971,12 +2978,12 @@
   7.175    } note onorm = this
   7.176  
   7.177    have ev_mem: "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. (x', y') \<in> X \<times> Y"
   7.178 -    using \<open>x \<in> X\<close> \<open>y \<in> Y\<close>
   7.179 +    using \<open>y \<in> Y\<close>
   7.180      by (auto simp: eventually_at intro!: zero_less_one)
   7.181    moreover
   7.182    have ev_dist: "\<forall>\<^sub>F xy in at (x, y) within X \<times> Y. dist xy (x, y) < d" if "d > 0" for d
   7.183      using eventually_at_ball[OF that]
   7.184 -    by (rule eventually_elim2) (auto simp: dist_commute intro!: eventually_True)
   7.185 +    by (rule eventually_elim2) (auto simp: dist_commute mem_ball intro!: eventually_True)
   7.186    note ev_dist[OF \<open>0 < d\<close>]
   7.187    ultimately
   7.188    have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y.
   7.189 @@ -2997,32 +3004,31 @@
   7.190        have "\<dots> \<subseteq> ball y d \<inter> Y"
   7.191          using \<open>y \<in> Y\<close> \<open>0 < d\<close> dy y'
   7.192          by (intro \<open>convex ?S\<close>[unfolded convex_contains_segment, rule_format, of y y'])
   7.193 -          (auto simp: dist_commute)
   7.194 +          (auto simp: dist_commute mem_ball)
   7.195        finally have "y + t *\<^sub>R (y' - y) \<in> ?S" .
   7.196      } note seg = this
   7.197  
   7.198      have "\<forall>x\<in>ball y d \<inter> Y. onorm (blinfun_apply (fy x' x) - blinfun_apply (fy x' y)) \<le> e + e"
   7.199 -      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>)
   7.200 +      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>)
   7.201      with seg has_derivative_within_subset[OF assms(2)[OF \<open>x' \<in> X\<close>]]
   7.202      show "norm (f x' y' - f x' y - (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
   7.203        by (rule differentiable_bound_linearization[where S="?S"])
   7.204          (auto intro!: \<open>0 < d\<close> \<open>y \<in> Y\<close>)
   7.205    qed
   7.206    moreover
   7.207 -  let ?le = "\<lambda>x'. norm (f x' y - f x y - (fx x y) (x' - x)) \<le> norm (x' - x) * e"
   7.208 -  from fx[OF \<open>x \<in> X\<close> \<open>y \<in> Y\<close>, unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
   7.209 +  let ?le = "\<lambda>x'. norm (f x' y - f x y - (fx) (x' - x)) \<le> norm (x' - x) * e"
   7.210 +  from fx[unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
   7.211    have "\<forall>\<^sub>F x' in at x within X. ?le x'"
   7.212      by eventually_elim
   7.213 -       (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps split: if_split_asm)
   7.214 +       (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps fx.zero split: if_split_asm)
   7.215    then have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. ?le x'"
   7.216      by (rule eventually_at_Pair_within_TimesI1)
   7.217 -       (simp add: blinfun.bilinear_simps)
   7.218 +       (simp add: blinfun.bilinear_simps fx.zero)
   7.219    moreover have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. norm ((x', y') - (x, y)) \<noteq> 0"
   7.220      unfolding norm_eq_zero right_minus_eq
   7.221      by (auto simp: eventually_at intro!: zero_less_one)
   7.222    moreover
   7.223 -  from fy_cont[unfolded continuous_on_eq_continuous_within, rule_format, OF SigmaI[OF \<open>x \<in> X\<close> \<open>y \<in> Y\<close>],
   7.224 -      unfolded continuous_within, THEN tendstoD, OF \<open>0 < e\<close>]
   7.225 +  from fy_cont[THEN tendstoD, OF \<open>0 < e\<close>]
   7.226    have "\<forall>\<^sub>F x' in at x within X. norm (fy x' y - fy x y) < e"
   7.227      unfolding eventually_at
   7.228      using \<open>y \<in> Y\<close>
   7.229 @@ -3032,22 +3038,22 @@
   7.230         (simp add: blinfun.bilinear_simps \<open>0 < e\<close>)
   7.231    ultimately
   7.232    have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y.
   7.233 -            norm ((f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) /\<^sub>R
   7.234 +            norm ((f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) /\<^sub>R
   7.235                norm ((x', y') - (x, y)))
   7.236              < e'"
   7.237      apply eventually_elim
   7.238    proof safe
   7.239      fix x' y'
   7.240 -    have "norm (f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) \<le>
   7.241 +    have "norm (f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) \<le>
   7.242          norm (f x' y' - f x' y - fy x' y (y' - y)) +
   7.243          norm (fy x y (y' - y) - fy x' y (y' - y)) +
   7.244 -        norm (f x' y - f x y - fx x y (x' - x))"
   7.245 +        norm (f x' y - f x y - fx (x' - x))"
   7.246        by norm
   7.247      also
   7.248      assume nz: "norm ((x', y') - (x, y)) \<noteq> 0"
   7.249        and nfy: "norm (fy x' y - fy x y) < e"
   7.250      assume "norm (f x' y' - f x' y - blinfun_apply (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
   7.251 -    also assume "norm (f x' y - f x y - blinfun_apply (fx x y) (x' - x)) \<le> norm (x' - x) * e"
   7.252 +    also assume "norm (f x' y - f x y - (fx) (x' - x)) \<le> norm (x' - x) * e"
   7.253      also
   7.254      have "norm ((fy x y) (y' - y) - (fy x' y) (y' - y)) \<le> norm ((fy x y) - (fy x' y)) * norm (y' - y)"
   7.255        by (auto simp: blinfun.bilinear_simps[symmetric] intro!: norm_blinfun)
   7.256 @@ -3070,11 +3076,80 @@
   7.257      also have "\<dots> < norm ((x', y') - (x, y)) * e'"
   7.258        using \<open>0 < e'\<close> nz
   7.259        by (auto simp: e_def)
   7.260 -    finally show "norm ((f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) /\<^sub>R norm ((x', y') - (x, y))) < e'"
   7.261 +    finally show "norm ((f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) /\<^sub>R norm ((x', y') - (x, y))) < e'"
   7.262        by (auto simp: divide_simps dist_norm mult.commute)
   7.263    qed
   7.264    then show ?case
   7.265      by eventually_elim (auto simp: dist_norm field_simps)
   7.266 -qed (auto intro!: bounded_linear_intros simp: split_beta')
   7.267 +next
   7.268 +  from has_derivative_bounded_linear[OF fx]
   7.269 +  obtain fxb where "fx = blinfun_apply fxb"
   7.270 +    by (metis bounded_linear_Blinfun_apply)
   7.271 +  then show "bounded_linear (\<lambda>(tx, ty). fx tx + blinfun_apply (fy x y) ty)"
   7.272 +    by (auto intro!: bounded_linear_intros simp: split_beta')
   7.273 +qed
   7.274 +
   7.275 +
   7.276 +subsection \<open>Differentiable case distinction\<close>
   7.277 +
   7.278 +lemma has_derivative_within_If_eq:
   7.279 +  "((\<lambda>x. if P x then f x else g x) has_derivative f') (at x within s) =
   7.280 +    (bounded_linear f' \<and>
   7.281 +     ((\<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)
   7.282 +           else (g y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)))
   7.283 +      \<longlongrightarrow> 0) (at x within s))"
   7.284 +  (is "_ = (_ \<and> (?if \<longlongrightarrow> 0) _)")
   7.285 +proof -
   7.286 +  have "(\<lambda>y. (1 / norm (y - x)) *\<^sub>R
   7.287 +           ((if P y then f y else g y) -
   7.288 +            ((if P x then f x else g x) + f' (y - x)))) = ?if"
   7.289 +    by (auto simp: inverse_eq_divide)
   7.290 +  thus ?thesis by (auto simp: has_derivative_within)
   7.291 +qed
   7.292 +
   7.293 +lemma has_derivative_If_within_closures:
   7.294 +  assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
   7.295 +    (f has_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
   7.296 +  assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
   7.297 +    (g has_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
   7.298 +  assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
   7.299 +  assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
   7.300 +  assumes x_in: "x \<in> s \<union> t"
   7.301 +  shows "((\<lambda>x. if x \<in> s then f x else g x) has_derivative
   7.302 +      (if x \<in> s then f' x else g' x)) (at x within (s \<union> t))"
   7.303 +proof -
   7.304 +  from f' x_in interpret f': bounded_linear "if x \<in> s then f' x else (\<lambda>x. 0)"
   7.305 +    by (auto simp add: has_derivative_within)
   7.306 +  from g' interpret g': bounded_linear "if x \<in> t then g' x else (\<lambda>x. 0)"
   7.307 +    by (auto simp add: has_derivative_within)
   7.308 +  have bl: "bounded_linear (if x \<in> s then f' x else g' x)"
   7.309 +    using f'.scaleR f'.bounded f'.add g'.scaleR g'.bounded g'.add x_in
   7.310 +    by (unfold_locales; force)
   7.311 +  show ?thesis
   7.312 +    using f' g' closure_subset[of t] closure_subset[of s]
   7.313 +    unfolding has_derivative_within_If_eq
   7.314 +    by (intro conjI bl tendsto_If_within_closures x_in)
   7.315 +      (auto simp: has_derivative_within inverse_eq_divide connect connect' set_mp)
   7.316 +qed
   7.317 +
   7.318 +lemma has_vector_derivative_If_within_closures:
   7.319 +  assumes x_in: "x \<in> s \<union> t"
   7.320 +  assumes "u = s \<union> t"
   7.321 +  assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
   7.322 +    (f has_vector_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
   7.323 +  assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
   7.324 +    (g has_vector_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
   7.325 +  assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
   7.326 +  assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
   7.327 +  shows "((\<lambda>x. if x \<in> s then f x else g x) has_vector_derivative
   7.328 +    (if x \<in> s then f' x else g' x)) (at x within u)"
   7.329 +  unfolding has_vector_derivative_def assms
   7.330 +  using x_in
   7.331 +  apply (intro has_derivative_If_within_closures[where
   7.332 +        ?f' = "\<lambda>x a. a *\<^sub>R f' x" and ?g' = "\<lambda>x a. a *\<^sub>R g' x",
   7.333 +        THEN has_derivative_eq_rhs])
   7.334 +  subgoal by (rule f'[unfolded has_vector_derivative_def]; assumption)
   7.335 +  subgoal by (rule g'[unfolded has_vector_derivative_def]; assumption)
   7.336 +  by (auto simp: assms)
   7.337  
   7.338  end
     8.1 --- a/src/HOL/Analysis/Euclidean_Space.thy	Tue Feb 20 22:25:23 2018 +0100
     8.2 +++ b/src/HOL/Analysis/Euclidean_Space.thy	Thu Feb 22 15:17:25 2018 +0100
     8.3 @@ -84,6 +84,10 @@
     8.4  lemma (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x"
     8.5    unfolding euclidean_representation_sum by simp
     8.6  
     8.7 +lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (inner x b) * (inner y b))"
     8.8 +  by (subst (1 2) euclidean_representation [symmetric])
     8.9 +    (simp add: inner_sum_right inner_Basis ac_simps)
    8.10 +
    8.11  lemma (in euclidean_space) choice_Basis_iff:
    8.12    fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool"
    8.13    shows "(\<forall>i\<in>Basis. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. P i (inner x i))"
     9.1 --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Tue Feb 20 22:25:23 2018 +0100
     9.2 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Feb 22 15:17:25 2018 +0100
     9.3 @@ -20,9 +20,19 @@
     9.4  
     9.5  declare vec_lambda_inject [simplified, simp]
     9.6  
     9.7 +bundle vec_syntax begin
     9.8  notation
     9.9    vec_nth (infixl "$" 90) and
    9.10    vec_lambda (binder "\<chi>" 10)
    9.11 +end
    9.12 +
    9.13 +bundle no_vec_syntax begin
    9.14 +no_notation
    9.15 +  vec_nth (infixl "$" 90) and
    9.16 +  vec_lambda (binder "\<chi>" 10)
    9.17 +end
    9.18 +
    9.19 +unbundle vec_syntax
    9.20  
    9.21  (*
    9.22    Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than
    10.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Feb 20 22:25:23 2018 +0100
    10.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Feb 22 15:17:25 2018 +0100
    10.3 @@ -621,6 +621,11 @@
    10.4    with False show ?thesis by (simp add: not_integrable_integral)
    10.5  qed
    10.6  
    10.7 +lemma integral_mult:
    10.8 +  fixes K::real
    10.9 +  shows "f integrable_on X \<Longrightarrow> K * integral X f = integral X (\<lambda>x. K * f x)"
   10.10 +  unfolding real_scaleR_def[symmetric] integral_cmul ..
   10.11 +
   10.12  lemma integral_neg [simp]: "integral S (\<lambda>x. - f x) = - integral S f"
   10.13  proof (cases "f integrable_on S")
   10.14    case True then show ?thesis
   10.15 @@ -2549,6 +2554,13 @@
   10.16  
   10.17  lemmas integrable_continuous_real = integrable_continuous_interval[where 'b=real]
   10.18  
   10.19 +lemma integrable_continuous_closed_segment:
   10.20 +  fixes f :: "real \<Rightarrow> 'a::banach"
   10.21 +  assumes "continuous_on (closed_segment a b) f"
   10.22 +  shows "f integrable_on (closed_segment a b)"
   10.23 +  using assms
   10.24 +  by (auto intro!: integrable_continuous_interval simp: closed_segment_eq_real_ivl)
   10.25 +
   10.26  
   10.27  subsection \<open>Specialization of additivity to one dimension.\<close>
   10.28  
   10.29 @@ -2722,6 +2734,32 @@
   10.30  
   10.31  subsection \<open>Taylor series expansion\<close>
   10.32  
   10.33 +lemma mvt_integral:
   10.34 +  fixes f::"'a::real_normed_vector\<Rightarrow>'b::banach"
   10.35 +  assumes f'[derivative_intros]:
   10.36 +    "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
   10.37 +  assumes line_in: "\<And>t. t \<in> {0..1} \<Longrightarrow> x + t *\<^sub>R y \<in> S"
   10.38 +  shows "f (x + y) - f x = integral {0..1} (\<lambda>t. f' (x + t *\<^sub>R y) y)" (is ?th1)
   10.39 +proof -
   10.40 +  from assms have subset: "(\<lambda>xa. x + xa *\<^sub>R y) ` {0..1} \<subseteq> S" by auto
   10.41 +  note [derivative_intros] =
   10.42 +    has_derivative_subset[OF _ subset]
   10.43 +    has_derivative_in_compose[where f="(\<lambda>xa. x + xa *\<^sub>R y)" and g = f]
   10.44 +  note [continuous_intros] =
   10.45 +    continuous_on_compose2[where f="(\<lambda>xa. x + xa *\<^sub>R y)"]
   10.46 +    continuous_on_subset[OF _ subset]
   10.47 +  have "\<And>t. t \<in> {0..1} \<Longrightarrow>
   10.48 +    ((\<lambda>t. f (x + t *\<^sub>R y)) has_vector_derivative f' (x + t *\<^sub>R y) y)
   10.49 +    (at t within {0..1})"
   10.50 +    using assms
   10.51 +    by (auto simp: has_vector_derivative_def
   10.52 +        linear_cmul[OF has_derivative_linear[OF f'], symmetric]
   10.53 +      intro!: derivative_eq_intros)
   10.54 +  from fundamental_theorem_of_calculus[rule_format, OF _ this]
   10.55 +  show ?th1
   10.56 +    by (auto intro!: integral_unique[symmetric])
   10.57 +qed
   10.58 +
   10.59  lemma (in bounded_bilinear) sum_prod_derivatives_has_vector_derivative:
   10.60    assumes "p>0"
   10.61    and f0: "Df 0 = f"
   10.62 @@ -2835,7 +2873,6 @@
   10.63  qed
   10.64  
   10.65  
   10.66 -
   10.67  subsection \<open>Only need trivial subintervals if the interval itself is trivial.\<close>
   10.68  
   10.69  proposition division_of_nontrivial:
   10.70 @@ -3024,6 +3061,21 @@
   10.71    unfolding integrable_on_def
   10.72    by (auto intro!: has_integral_combine)
   10.73  
   10.74 +lemma integral_minus_sets:
   10.75 +  fixes f::"real \<Rightarrow> 'a::banach"
   10.76 +  shows "c \<le> a \<Longrightarrow> c \<le> b \<Longrightarrow> f integrable_on {c .. max a b} \<Longrightarrow>
   10.77 +    integral {c .. a} f - integral {c .. b} f =
   10.78 +    (if a \<le> b then - integral {a .. b} f else integral {b .. a} f)"
   10.79 +  using integral_combine[of c a b f]  integral_combine[of c b a f]
   10.80 +  by (auto simp: algebra_simps max_def)
   10.81 +
   10.82 +lemma integral_minus_sets':
   10.83 +  fixes f::"real \<Rightarrow> 'a::banach"
   10.84 +  shows "c \<ge> a \<Longrightarrow> c \<ge> b \<Longrightarrow> f integrable_on {min a b .. c} \<Longrightarrow>
   10.85 +    integral {a .. c} f - integral {b .. c} f =
   10.86 +    (if a \<le> b then integral {a .. b} f else - integral {b .. a} f)"
   10.87 +  using integral_combine[of b a c f] integral_combine[of a b c f]
   10.88 +  by (auto simp: algebra_simps min_def)
   10.89  
   10.90  subsection \<open>Reduce integrability to "local" integrability.\<close>
   10.91  
   10.92 @@ -3129,13 +3181,19 @@
   10.93  using assms integral_has_vector_derivative_continuous_at [OF integrable_continuous_real]
   10.94    by (fastforce simp: continuous_on_eq_continuous_within)
   10.95  
   10.96 +lemma integral_has_real_derivative:
   10.97 +  assumes "continuous_on {a..b} g"
   10.98 +  assumes "t \<in> {a..b}"
   10.99 +  shows "((\<lambda>x. integral {a..x} g) has_real_derivative g t) (at t within {a..b})"
  10.100 +  using integral_has_vector_derivative[of a b g t] assms
  10.101 +  by (auto simp: has_field_derivative_iff_has_vector_derivative)
  10.102 +
  10.103  lemma antiderivative_continuous:
  10.104    fixes q b :: real
  10.105    assumes "continuous_on {a..b} f"
  10.106    obtains g where "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative (f x::_::banach)) (at x within {a..b})"
  10.107    using integral_has_vector_derivative[OF assms] by auto
  10.108  
  10.109 -
  10.110  subsection \<open>Combined fundamental theorem of calculus.\<close>
  10.111  
  10.112  lemma antiderivative_integral_continuous:
  10.113 @@ -3149,7 +3207,8 @@
  10.114    have "(f has_integral g v - g u) {u..v}" if "u \<in> {a..b}" "v \<in> {a..b}" "u \<le> v" for u v
  10.115    proof -
  10.116      have "\<And>x. x \<in> cbox u v \<Longrightarrow> (g has_vector_derivative f x) (at x within cbox u v)"
  10.117 -      by (meson g has_vector_derivative_within_subset interval_subset_is_interval is_interval_closed_interval subsetCE that(1) that(2))
  10.118 +      by (metis atLeastAtMost_iff atLeastatMost_subset_iff box_real(2) g
  10.119 +          has_vector_derivative_within_subset subsetCE that(1,2))
  10.120      then show ?thesis
  10.121        by (metis box_real(2) that(3) fundamental_theorem_of_calculus)
  10.122    qed
  10.123 @@ -4125,6 +4184,28 @@
  10.124      by (rule continuous_on_eq) (auto intro!: continuous_intros indefinite_integral_continuous_1 assms)
  10.125  qed
  10.126  
  10.127 +theorem integral_has_vector_derivative':
  10.128 +  fixes f :: "real \<Rightarrow> 'b::banach"
  10.129 +  assumes "continuous_on {a..b} f"
  10.130 +    and "x \<in> {a..b}"
  10.131 +  shows "((\<lambda>u. integral {u..b} f) has_vector_derivative - f x) (at x within {a..b})"
  10.132 +proof -
  10.133 +  have *: "integral {x..b} f = integral {a .. b} f - integral {a .. x} f" if "a \<le> x" "x \<le> b" for x
  10.134 +    using integral_combine[of a x b for x, OF that integrable_continuous_real[OF assms(1)]]
  10.135 +    by (simp add: algebra_simps)
  10.136 +  show ?thesis
  10.137 +    using \<open>x \<in> _\<close> *
  10.138 +    by (rule has_vector_derivative_transform)
  10.139 +      (auto intro!: derivative_eq_intros assms integral_has_vector_derivative)
  10.140 +qed
  10.141 +
  10.142 +lemma integral_has_real_derivative':
  10.143 +  assumes "continuous_on {a..b} g"
  10.144 +  assumes "t \<in> {a..b}"
  10.145 +  shows "((\<lambda>x. integral {x..b} g) has_real_derivative -g t) (at t within {a..b})"
  10.146 +  using integral_has_vector_derivative'[OF assms]
  10.147 +  by (auto simp: has_field_derivative_iff_has_vector_derivative)
  10.148 +
  10.149  
  10.150  subsection \<open>This doesn't directly involve integration, but that gives an easy proof.\<close>
  10.151  
  10.152 @@ -4661,6 +4742,10 @@
  10.153    shows "f integrable_on S \<longleftrightarrow> f integrable_on T"
  10.154    by (blast intro: integrable_spike_set assms negligible_subset)
  10.155  
  10.156 +lemma integrable_on_insert_iff: "f integrable_on (insert x X) \<longleftrightarrow> f integrable_on X"
  10.157 +  for f::"_ \<Rightarrow> 'a::banach"
  10.158 +  by (rule integrable_spike_set_eq) (auto simp: insert_Diff_if)
  10.159 +
  10.160  lemma has_integral_interior:
  10.161    fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
  10.162    shows "negligible(frontier S) \<Longrightarrow> (f has_integral y) (interior S) \<longleftrightarrow> (f has_integral y) S"
  10.163 @@ -6049,6 +6134,26 @@
  10.164    qed
  10.165  qed
  10.166  
  10.167 +lemma continuous_on_imp_absolutely_integrable_on:
  10.168 +  fixes f::"real \<Rightarrow> 'a::banach"
  10.169 +  shows "continuous_on {a..b} f \<Longrightarrow>
  10.170 +    norm (integral {a..b} f) \<le> integral {a..b} (\<lambda>x. norm (f x))"
  10.171 +  by (intro integral_norm_bound_integral integrable_continuous_real continuous_on_norm) auto
  10.172 +
  10.173 +lemma integral_bound:
  10.174 +  fixes f::"real \<Rightarrow> 'a::banach"
  10.175 +  assumes "a \<le> b"
  10.176 +  assumes "continuous_on {a .. b} f"
  10.177 +  assumes "\<And>t. t \<in> {a .. b} \<Longrightarrow> norm (f t) \<le> B"
  10.178 +  shows "norm (integral {a .. b} f) \<le> B * (b - a)"
  10.179 +proof -
  10.180 +  note continuous_on_imp_absolutely_integrable_on[OF assms(2)]
  10.181 +  also have "integral {a..b} (\<lambda>x. norm (f x)) \<le> integral {a..b} (\<lambda>_. B)"
  10.182 +    by (rule integral_le)
  10.183 +      (auto intro!: integrable_continuous_real continuous_intros assms)
  10.184 +  also have "\<dots> = B * (b - a)" using assms by simp
  10.185 +  finally show ?thesis .
  10.186 +qed
  10.187  
  10.188  lemma integral_norm_bound_integral_component:
  10.189    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
    11.1 --- a/src/HOL/Analysis/L2_Norm.thy	Tue Feb 20 22:25:23 2018 +0100
    11.2 +++ b/src/HOL/Analysis/L2_Norm.thy	Thu Feb 22 15:17:25 2018 +0100
    11.3 @@ -98,13 +98,6 @@
    11.4    qed
    11.5  qed
    11.6  
    11.7 -lemma sqrt_sum_squares_le_sum:
    11.8 -  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
    11.9 -  apply (rule power2_le_imp_le)
   11.10 -  apply (simp add: power2_sum)
   11.11 -  apply simp
   11.12 -  done
   11.13 -
   11.14  lemma L2_set_le_sum [rule_format]:
   11.15    "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> L2_set f A \<le> sum f A"
   11.16    apply (cases "finite A")
    12.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Feb 20 22:25:23 2018 +0100
    12.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Feb 22 15:17:25 2018 +0100
    12.3 @@ -2987,10 +2987,6 @@
    12.4  lemma infnorm_le_norm: "infnorm x \<le> norm x"
    12.5    by (simp add: Basis_le_norm infnorm_Max)
    12.6  
    12.7 -lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (x \<bullet> b) * (y \<bullet> b))"
    12.8 -  by (subst (1 2) euclidean_representation [symmetric])
    12.9 -    (simp add: inner_sum_right inner_Basis ac_simps)
   12.10 -
   12.11  lemma norm_le_infnorm:
   12.12    fixes x :: "'a::euclidean_space"
   12.13    shows "norm x \<le> sqrt DIM('a) * infnorm x"
    13.1 --- a/src/HOL/Analysis/Operator_Norm.thy	Tue Feb 20 22:25:23 2018 +0100
    13.2 +++ b/src/HOL/Analysis/Operator_Norm.thy	Thu Feb 22 15:17:25 2018 +0100
    13.3 @@ -235,4 +235,13 @@
    13.4    shows "onorm (\<lambda>x. f x + g x) < e"
    13.5    using assms by (rule onorm_triangle [THEN order_le_less_trans])
    13.6  
    13.7 +lemma onorm_sum:
    13.8 +  assumes "finite S"
    13.9 +  assumes "\<And>s. s \<in> S \<Longrightarrow> bounded_linear (f s)"
   13.10 +  shows "onorm (\<lambda>x. sum (\<lambda>s. f s x) S) \<le> sum (\<lambda>s. onorm (f s)) S"
   13.11 +  using assms
   13.12 +  by (induction) (auto simp: onorm_zero intro!: onorm_triangle_le bounded_linear_sum)
   13.13 +
   13.14 +lemmas onorm_sum_le = onorm_sum[THEN order_trans]
   13.15 +
   13.16  end
    14.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Tue Feb 20 22:25:23 2018 +0100
    14.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Feb 22 15:17:25 2018 +0100
    14.3 @@ -214,9 +214,20 @@
    14.4    using image_smult_cbox[of m a b]
    14.5    by (simp add: cbox_interval)
    14.6  
    14.7 -lemma is_interval_closed_interval [simp]:
    14.8 -  "is_interval {a .. (b::'a::ordered_euclidean_space)}"
    14.9 -  by (metis cbox_interval is_interval_cbox)
   14.10 +lemma [simp]:
   14.11 +  fixes a b::"'a::ordered_euclidean_space" and r s::real
   14.12 +  shows is_interval_io: "is_interval {..<r}"
   14.13 +    and is_interval_ic: "is_interval {..a}"
   14.14 +    and is_interval_oi: "is_interval {r<..}"
   14.15 +    and is_interval_ci: "is_interval {a..}"
   14.16 +    and is_interval_oo: "is_interval {r<..<s}"
   14.17 +    and is_interval_oc: "is_interval {r<..s}"
   14.18 +    and is_interval_co: "is_interval {r..<s}"
   14.19 +    and is_interval_cc: "is_interval {b..a}"
   14.20 +  by (force simp: is_interval_def eucl_le[where 'a='a])+
   14.21 +
   14.22 +lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
   14.23 +  by (auto simp: real_atLeastGreaterThan_eq)
   14.24  
   14.25  lemma compact_interval [simp]:
   14.26    fixes a b::"'a::ordered_euclidean_space"
    15.1 --- a/src/HOL/Analysis/Product_Vector.thy	Tue Feb 20 22:25:23 2018 +0100
    15.2 +++ b/src/HOL/Analysis/Product_Vector.thy	Thu Feb 22 15:17:25 2018 +0100
    15.3 @@ -306,6 +306,11 @@
    15.4      by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt])
    15.5  qed simp
    15.6  
    15.7 +lemma differentiable_Pair [simp, derivative_intros]:
    15.8 +  "f differentiable at x within s \<Longrightarrow> g differentiable at x within s \<Longrightarrow>
    15.9 +    (\<lambda>x. (f x, g x)) differentiable at x within s"
   15.10 +  unfolding differentiable_def by (blast intro: has_derivative_Pair)
   15.11 +
   15.12  lemmas has_derivative_fst [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst]
   15.13  lemmas has_derivative_snd [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd]
   15.14  
   15.15 @@ -313,6 +318,17 @@
   15.16    "((\<lambda>p. f (fst p) (snd p)) has_derivative f') F \<Longrightarrow> ((\<lambda>(a, b). f a b) has_derivative f') F"
   15.17    unfolding split_beta' .
   15.18  
   15.19 +
   15.20 +subsubsection \<open>Vector derivatives involving pairs\<close>
   15.21 +
   15.22 +lemma has_vector_derivative_Pair[derivative_intros]:
   15.23 +  assumes "(f has_vector_derivative f') (at x within s)"
   15.24 +    "(g has_vector_derivative g') (at x within s)"
   15.25 +  shows "((\<lambda>x. (f x, g x)) has_vector_derivative (f', g')) (at x within s)"
   15.26 +  using assms
   15.27 +  by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
   15.28 +
   15.29 +
   15.30  subsection \<open>Product is an inner product space\<close>
   15.31  
   15.32  instantiation prod :: (real_inner, real_inner) real_inner
   15.33 @@ -368,4 +384,9 @@
   15.34  lemma norm_snd_le: "norm y \<le> norm (x,y)"
   15.35    by (metis dist_snd_le snd_conv snd_zero norm_conv_dist)
   15.36  
   15.37 +lemma norm_Pair_le:
   15.38 +  shows "norm (x, y) \<le> norm x + norm y"
   15.39 +  unfolding norm_Pair
   15.40 +  by (metis norm_ge_zero sqrt_sum_squares_le_sum)
   15.41 +
   15.42  end
    16.1 --- a/src/HOL/Analysis/Riemann_Mapping.thy	Tue Feb 20 22:25:23 2018 +0100
    16.2 +++ b/src/HOL/Analysis/Riemann_Mapping.thy	Thu Feb 22 15:17:25 2018 +0100
    16.3 @@ -489,7 +489,7 @@
    16.4      let ?g = "\<lambda>z. (SOME g. polynomial_function g \<and> path_image g \<subseteq> S \<and> pathstart g = a \<and> pathfinish g = z)"
    16.5      show "((\<lambda>z. contour_integral (?g z) f) has_field_derivative f x)
    16.6            (at x)"
    16.7 -    proof (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right, rule Lim_transform)
    16.8 +    proof (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right, rule Lim_transform)
    16.9        show "(\<lambda>y. inverse(norm(y - x)) *\<^sub>R (contour_integral(linepath x y) f - f x * (y - x))) \<midarrow>x\<rightarrow> 0"
   16.10        proof (clarsimp simp add: Lim_at)
   16.11          fix e::real assume "e > 0"
    17.1 --- a/src/HOL/Analysis/Starlike.thy	Tue Feb 20 22:25:23 2018 +0100
    17.2 +++ b/src/HOL/Analysis/Starlike.thy	Thu Feb 22 15:17:25 2018 +0100
    17.3 @@ -13,9 +13,87 @@
    17.4  
    17.5  begin
    17.6  
    17.7 +subsection \<open>Midpoint\<close>
    17.8 +
    17.9  definition midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
   17.10    where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
   17.11  
   17.12 +lemma midpoint_idem [simp]: "midpoint x x = x"
   17.13 +  unfolding midpoint_def
   17.14 +  unfolding scaleR_right_distrib
   17.15 +  unfolding scaleR_left_distrib[symmetric]
   17.16 +  by auto
   17.17 +
   17.18 +lemma midpoint_sym: "midpoint a b = midpoint b a"
   17.19 +  unfolding midpoint_def by (auto simp add: scaleR_right_distrib)
   17.20 +
   17.21 +lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c"
   17.22 +proof -
   17.23 +  have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c"
   17.24 +    by simp
   17.25 +  then show ?thesis
   17.26 +    unfolding midpoint_def scaleR_2 [symmetric] by simp
   17.27 +qed
   17.28 +
   17.29 +lemma
   17.30 +  fixes a::real
   17.31 +  assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
   17.32 +                    and le_midpoint_1: "midpoint a b \<le> b"
   17.33 +  by (simp_all add: midpoint_def assms)
   17.34 +
   17.35 +lemma dist_midpoint:
   17.36 +  fixes a b :: "'a::real_normed_vector" shows
   17.37 +  "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
   17.38 +  "dist b (midpoint a b) = (dist a b) / 2" (is ?t2)
   17.39 +  "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
   17.40 +  "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
   17.41 +proof -
   17.42 +  have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2"
   17.43 +    unfolding equation_minus_iff by auto
   17.44 +  have **: "\<And>x y::'a. 2 *\<^sub>R x =   y \<Longrightarrow> norm x = (norm y) / 2"
   17.45 +    by auto
   17.46 +  note scaleR_right_distrib [simp]
   17.47 +  show ?t1
   17.48 +    unfolding midpoint_def dist_norm
   17.49 +    apply (rule **)
   17.50 +    apply (simp add: scaleR_right_diff_distrib)
   17.51 +    apply (simp add: scaleR_2)
   17.52 +    done
   17.53 +  show ?t2
   17.54 +    unfolding midpoint_def dist_norm
   17.55 +    apply (rule *)
   17.56 +    apply (simp add: scaleR_right_diff_distrib)
   17.57 +    apply (simp add: scaleR_2)
   17.58 +    done
   17.59 +  show ?t3
   17.60 +    unfolding midpoint_def dist_norm
   17.61 +    apply (rule *)
   17.62 +    apply (simp add: scaleR_right_diff_distrib)
   17.63 +    apply (simp add: scaleR_2)
   17.64 +    done
   17.65 +  show ?t4
   17.66 +    unfolding midpoint_def dist_norm
   17.67 +    apply (rule **)
   17.68 +    apply (simp add: scaleR_right_diff_distrib)
   17.69 +    apply (simp add: scaleR_2)
   17.70 +    done
   17.71 +qed
   17.72 +
   17.73 +lemma midpoint_eq_endpoint [simp]:
   17.74 +  "midpoint a b = a \<longleftrightarrow> a = b"
   17.75 +  "midpoint a b = b \<longleftrightarrow> a = b"
   17.76 +  unfolding midpoint_eq_iff by auto
   17.77 +
   17.78 +lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
   17.79 +  using midpoint_eq_iff by metis
   17.80 +
   17.81 +lemma midpoint_linear_image:
   17.82 +   "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
   17.83 +by (simp add: linear_iff midpoint_def)
   17.84 +
   17.85 +
   17.86 +subsection \<open>Line segments\<close>
   17.87 +
   17.88  definition closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
   17.89    where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
   17.90  
   17.91 @@ -106,86 +184,6 @@
   17.92    apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE)
   17.93    using of_real_eq_iff by fastforce
   17.94  
   17.95 -lemma midpoint_idem [simp]: "midpoint x x = x"
   17.96 -  unfolding midpoint_def
   17.97 -  unfolding scaleR_right_distrib
   17.98 -  unfolding scaleR_left_distrib[symmetric]
   17.99 -  by auto
  17.100 -
  17.101 -lemma midpoint_sym: "midpoint a b = midpoint b a"
  17.102 -  unfolding midpoint_def by (auto simp add: scaleR_right_distrib)
  17.103 -
  17.104 -lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c"
  17.105 -proof -
  17.106 -  have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c"
  17.107 -    by simp
  17.108 -  then show ?thesis
  17.109 -    unfolding midpoint_def scaleR_2 [symmetric] by simp
  17.110 -qed
  17.111 -
  17.112 -lemma
  17.113 -  fixes a::real
  17.114 -  assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
  17.115 -                    and le_midpoint_1: "midpoint a b \<le> b"
  17.116 -  by (simp_all add: midpoint_def assms)
  17.117 -
  17.118 -lemma dist_midpoint:
  17.119 -  fixes a b :: "'a::real_normed_vector" shows
  17.120 -  "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
  17.121 -  "dist b (midpoint a b) = (dist a b) / 2" (is ?t2)
  17.122 -  "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
  17.123 -  "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
  17.124 -proof -
  17.125 -  have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2"
  17.126 -    unfolding equation_minus_iff by auto
  17.127 -  have **: "\<And>x y::'a. 2 *\<^sub>R x =   y \<Longrightarrow> norm x = (norm y) / 2"
  17.128 -    by auto
  17.129 -  note scaleR_right_distrib [simp]
  17.130 -  show ?t1
  17.131 -    unfolding midpoint_def dist_norm
  17.132 -    apply (rule **)
  17.133 -    apply (simp add: scaleR_right_diff_distrib)
  17.134 -    apply (simp add: scaleR_2)
  17.135 -    done
  17.136 -  show ?t2
  17.137 -    unfolding midpoint_def dist_norm
  17.138 -    apply (rule *)
  17.139 -    apply (simp add: scaleR_right_diff_distrib)
  17.140 -    apply (simp add: scaleR_2)
  17.141 -    done
  17.142 -  show ?t3
  17.143 -    unfolding midpoint_def dist_norm
  17.144 -    apply (rule *)
  17.145 -    apply (simp add: scaleR_right_diff_distrib)
  17.146 -    apply (simp add: scaleR_2)
  17.147 -    done
  17.148 -  show ?t4
  17.149 -    unfolding midpoint_def dist_norm
  17.150 -    apply (rule **)
  17.151 -    apply (simp add: scaleR_right_diff_distrib)
  17.152 -    apply (simp add: scaleR_2)
  17.153 -    done
  17.154 -qed
  17.155 -
  17.156 -lemma midpoint_eq_endpoint [simp]:
  17.157 -  "midpoint a b = a \<longleftrightarrow> a = b"
  17.158 -  "midpoint a b = b \<longleftrightarrow> a = b"
  17.159 -  unfolding midpoint_eq_iff by auto
  17.160 -
  17.161 -lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
  17.162 -  using midpoint_eq_iff by metis
  17.163 -
  17.164 -lemma midpoint_linear_image:
  17.165 -   "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
  17.166 -by (simp add: linear_iff midpoint_def)
  17.167 -
  17.168 -subsection\<open>Starlike sets\<close>
  17.169 -
  17.170 -definition "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
  17.171 -
  17.172 -lemma starlike_UNIV [simp]: "starlike UNIV"
  17.173 -  by (simp add: starlike_def)
  17.174 -
  17.175  lemma convex_contains_segment:
  17.176    "convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)"
  17.177    unfolding convex_alt closed_segment_def by auto
  17.178 @@ -197,10 +195,6 @@
  17.179      "\<lbrakk>x \<in> convex hull S; y \<in> convex hull S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull S"
  17.180    using convex_contains_segment by blast
  17.181  
  17.182 -lemma convex_imp_starlike:
  17.183 -  "convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S"
  17.184 -  unfolding convex_contains_segment starlike_def by auto
  17.185 -
  17.186  lemma segment_convex_hull:
  17.187    "closed_segment a b = convex hull {a,b}"
  17.188  proof -
  17.189 @@ -349,7 +343,7 @@
  17.190    proof -
  17.191      have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
  17.192        using \<open>u \<le> 1\<close> by force
  17.193 -    then show ?thesis                     
  17.194 +    then show ?thesis
  17.195        by (simp add: dist_norm real_vector.scale_right_diff_distrib)
  17.196    qed
  17.197    also have "... \<le> dist a b"
  17.198 @@ -581,7 +575,6 @@
  17.199      by (metis image_comp convex_translation)
  17.200  qed
  17.201  
  17.202 -
  17.203  lemmas convex_segment = convex_closed_segment convex_open_segment
  17.204  
  17.205  lemma connected_segment [iff]:
  17.206 @@ -589,6 +582,33 @@
  17.207    shows "connected (closed_segment x y)"
  17.208    by (simp add: convex_connected)
  17.209  
  17.210 +lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real
  17.211 +  by (auto simp: is_interval_convex_1)
  17.212 +
  17.213 +lemma IVT'_closed_segment_real:
  17.214 +  fixes f :: "real \<Rightarrow> real"
  17.215 +  assumes "y \<in> closed_segment (f a) (f b)"
  17.216 +  assumes "continuous_on (closed_segment a b) f"
  17.217 +  shows "\<exists>x \<in> closed_segment a b. f x = y"
  17.218 +  using IVT'[of f a y b]
  17.219 +    IVT'[of "-f" a "-y" b]
  17.220 +    IVT'[of f b y a]
  17.221 +    IVT'[of "-f" b "-y" a] assms
  17.222 +  by (cases "a \<le> b"; cases "f b \<ge> f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus)
  17.223 +
  17.224 +
  17.225 +subsection\<open>Starlike sets\<close>
  17.226 +
  17.227 +definition "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
  17.228 +
  17.229 +lemma starlike_UNIV [simp]: "starlike UNIV"
  17.230 +  by (simp add: starlike_def)
  17.231 +
  17.232 +lemma convex_imp_starlike:
  17.233 +  "convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S"
  17.234 +  unfolding convex_contains_segment starlike_def by auto
  17.235 +
  17.236 +
  17.237  lemma affine_hull_closed_segment [simp]:
  17.238       "affine hull (closed_segment a b) = affine hull {a,b}"
  17.239    by (simp add: segment_convex_hull)
    18.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Feb 20 22:25:23 2018 +0100
    18.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Feb 22 15:17:25 2018 +0100
    18.3 @@ -7,7 +7,7 @@
    18.4  section \<open>Elementary topology in Euclidean space.\<close>
    18.5  
    18.6  theory Topology_Euclidean_Space
    18.7 -imports                                                         
    18.8 +imports
    18.9    "HOL-Library.Indicator_Function"
   18.10    "HOL-Library.Countable_Set"
   18.11    "HOL-Library.FuncSet"
   18.12 @@ -1112,6 +1112,9 @@
   18.13  lemma ball_subset_cball [simp, intro]: "ball x e \<subseteq> cball x e"
   18.14    by (simp add: subset_eq)
   18.15  
   18.16 +lemma mem_ball_imp_mem_cball: "x \<in> ball y e \<Longrightarrow> x \<in> cball y e"
   18.17 +  by (auto simp: mem_ball mem_cball)
   18.18 +
   18.19  lemma sphere_cball [simp,intro]: "sphere z r \<subseteq> cball z r"
   18.20    by force
   18.21  
   18.22 @@ -1124,6 +1127,22 @@
   18.23  lemma subset_cball[intro]: "d \<le> e \<Longrightarrow> cball x d \<subseteq> cball x e"
   18.24    by (simp add: subset_eq)
   18.25  
   18.26 +lemma mem_ball_leI: "x \<in> ball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> ball y f"
   18.27 +  by (auto simp: mem_ball mem_cball)
   18.28 +
   18.29 +lemma mem_cball_leI: "x \<in> cball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> cball y f"
   18.30 +  by (auto simp: mem_ball mem_cball)
   18.31 +
   18.32 +lemma cball_trans: "y \<in> cball z b \<Longrightarrow> x \<in> cball y a \<Longrightarrow> x \<in> cball z (b + a)"
   18.33 +  unfolding mem_cball
   18.34 +proof -
   18.35 +  have "dist z x \<le> dist z y + dist y x"
   18.36 +    by (rule dist_triangle)
   18.37 +  also assume "dist z y \<le> b"
   18.38 +  also assume "dist y x \<le> a"
   18.39 +  finally show "dist z x \<le> b + a" by arith
   18.40 +qed
   18.41 +
   18.42  lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s"
   18.43    by (simp add: set_eq_iff) arith
   18.44  
   18.45 @@ -1253,6 +1272,17 @@
   18.46    unfolding dist_norm norm_eq_sqrt_inner L2_set_def
   18.47    by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
   18.48  
   18.49 +lemma norm_nth_le: "norm (x \<bullet> i) \<le> norm x" if "i \<in> Basis"
   18.50 +proof -
   18.51 +  have "(x \<bullet> i)\<^sup>2 = (\<Sum>i\<in>{i}. (x \<bullet> i)\<^sup>2)"
   18.52 +    by simp
   18.53 +  also have "\<dots> \<le> (\<Sum>i\<in>Basis. (x \<bullet> i)\<^sup>2)"
   18.54 +    by (intro sum_mono2) (auto simp: that)
   18.55 +  finally show ?thesis
   18.56 +    unfolding norm_conv_dist euclidean_dist_l2[of x] L2_set_def
   18.57 +    by (auto intro!: real_le_rsqrt)
   18.58 +qed
   18.59 +
   18.60  lemma eventually_nhds_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>x. x \<in> ball z d) (nhds z)"
   18.61    by (rule eventually_nhds_in_open) simp_all
   18.62  
   18.63 @@ -1262,6 +1292,20 @@
   18.64  lemma eventually_at_ball': "d > 0 \<Longrightarrow> eventually (\<lambda>t. t \<in> ball z d \<and> t \<noteq> z \<and> t \<in> A) (at z within A)"
   18.65    unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
   18.66  
   18.67 +lemma at_within_ball: "e > 0 \<Longrightarrow> dist x y < e \<Longrightarrow> at y within ball x e = at y"
   18.68 +  by (subst at_within_open) auto
   18.69 +
   18.70 +lemma atLeastAtMost_eq_cball:
   18.71 +  fixes a b::real
   18.72 +  shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"
   18.73 +  by (auto simp: dist_real_def field_simps mem_cball)
   18.74 +
   18.75 +lemma greaterThanLessThan_eq_ball:
   18.76 +  fixes a b::real
   18.77 +  shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"
   18.78 +  by (auto simp: dist_real_def field_simps mem_ball)
   18.79 +
   18.80 +
   18.81  subsection \<open>Boxes\<close>
   18.82  
   18.83  abbreviation One :: "'a::euclidean_space"
   18.84 @@ -1834,6 +1878,14 @@
   18.85  definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
   18.86    (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
   18.87  
   18.88 +lemma is_interval_1:
   18.89 +  "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
   18.90 +  unfolding is_interval_def by auto
   18.91 +
   18.92 +lemma is_interval_inter: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)"
   18.93 +  unfolding is_interval_def
   18.94 +  by blast
   18.95 +
   18.96  lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
   18.97    and is_interval_box [simp]: "is_interval (box a b)" (is ?th2)
   18.98    unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
   18.99 @@ -1916,6 +1968,88 @@
  18.100      by blast
  18.101  qed
  18.102  
  18.103 +lemma is_real_interval_union:
  18.104 +  "is_interval (X \<union> Y)"
  18.105 +  if X: "is_interval X" and Y: "is_interval Y" and I: "(X \<noteq> {} \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> X \<inter> Y \<noteq> {})"
  18.106 +  for X Y::"real set"
  18.107 +proof -
  18.108 +  consider "X \<noteq> {}" "Y \<noteq> {}" | "X = {}" | "Y = {}" by blast
  18.109 +  then show ?thesis
  18.110 +  proof cases
  18.111 +    case 1
  18.112 +    then obtain r where "r \<in> X \<or> X \<inter> Y = {}" "r \<in> Y \<or> X \<inter> Y = {}"
  18.113 +      by blast
  18.114 +    then show ?thesis
  18.115 +      using I 1 X Y unfolding is_interval_1
  18.116 +      by (metis (full_types) Un_iff le_cases)
  18.117 +  qed (use that in auto)
  18.118 +qed
  18.119 +
  18.120 +lemma is_interval_translationI:
  18.121 +  assumes "is_interval X"
  18.122 +  shows "is_interval ((+) x ` X)"
  18.123 +  unfolding is_interval_def
  18.124 +proof safe
  18.125 +  fix b d e
  18.126 +  assume "b \<in> X" "d \<in> X"
  18.127 +    "\<forall>i\<in>Basis. (x + b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + d) \<bullet> i \<or>
  18.128 +       (x + d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + b) \<bullet> i"
  18.129 +  hence "e - x \<in> X"
  18.130 +    by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "e - x"])
  18.131 +      (auto simp: algebra_simps)
  18.132 +  thus "e \<in> (+) x ` X" by force
  18.133 +qed
  18.134 +
  18.135 +lemma is_interval_uminusI:
  18.136 +  assumes "is_interval X"
  18.137 +  shows "is_interval (uminus ` X)"
  18.138 +  unfolding is_interval_def
  18.139 +proof safe
  18.140 +  fix b d e
  18.141 +  assume "b \<in> X" "d \<in> X"
  18.142 +    "\<forall>i\<in>Basis. (- b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- d) \<bullet> i \<or>
  18.143 +       (- d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- b) \<bullet> i"
  18.144 +  hence "- e \<in> X"
  18.145 +    by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "- e"])
  18.146 +      (auto simp: algebra_simps)
  18.147 +  thus "e \<in> uminus ` X" by force
  18.148 +qed
  18.149 +
  18.150 +lemma is_interval_uminus[simp]: "is_interval (uminus ` x) = is_interval x"
  18.151 +  using is_interval_uminusI[of x] is_interval_uminusI[of "uminus ` x"]
  18.152 +  by (auto simp: image_image)
  18.153 +
  18.154 +lemma is_interval_neg_translationI:
  18.155 +  assumes "is_interval X"
  18.156 +  shows "is_interval ((-) x ` X)"
  18.157 +proof -
  18.158 +  have "(-) x ` X = (+) x ` uminus ` X"
  18.159 +    by (force simp: algebra_simps)
  18.160 +  also have "is_interval \<dots>"
  18.161 +    by (metis is_interval_uminusI is_interval_translationI assms)
  18.162 +  finally show ?thesis .
  18.163 +qed
  18.164 +
  18.165 +lemma is_interval_translation[simp]:
  18.166 +  "is_interval ((+) x ` X) = is_interval X"
  18.167 +  using is_interval_neg_translationI[of "(+) x ` X" x]
  18.168 +  by (auto intro!: is_interval_translationI simp: image_image)
  18.169 +
  18.170 +lemma is_interval_minus_translation[simp]:
  18.171 +  shows "is_interval ((-) x ` X) = is_interval X"
  18.172 +proof -
  18.173 +  have "(-) x ` X = (+) x ` uminus ` X"
  18.174 +    by (force simp: algebra_simps)
  18.175 +  also have "is_interval \<dots> = is_interval X"
  18.176 +    by simp
  18.177 +  finally show ?thesis .
  18.178 +qed
  18.179 +
  18.180 +lemma is_interval_minus_translation'[simp]:
  18.181 +  shows "is_interval ((\<lambda>x. x - c) ` X) = is_interval X"
  18.182 +  using is_interval_translation[of "-c" X]
  18.183 +  by (metis image_cong uminus_add_conv_diff)
  18.184 +
  18.185  
  18.186  subsection \<open>Limit points\<close>
  18.187  
  18.188 @@ -2629,6 +2763,15 @@
  18.189  lemma not_trivial_limit_within: "\<not> trivial_limit (at x within S) = (x \<in> closure (S - {x}))"
  18.190    using islimpt_in_closure by (metis trivial_limit_within)
  18.191  
  18.192 +lemma not_in_closure_trivial_limitI:
  18.193 +  "x \<notin> closure s \<Longrightarrow> trivial_limit (at x within s)"
  18.194 +  using not_trivial_limit_within[of x s]
  18.195 +  by safe (metis Diff_empty Diff_insert0 closure_subset contra_subsetD)
  18.196 +
  18.197 +lemma filterlim_at_within_closure_implies_filterlim: "filterlim f l (at x within s)"
  18.198 +  if "x \<in> closure s \<Longrightarrow> filterlim f l (at x within s)"
  18.199 +  by (metis bot.extremum filterlim_filtercomap filterlim_mono not_in_closure_trivial_limitI that)
  18.200 +
  18.201  lemma at_within_eq_bot_iff: "at c within A = bot \<longleftrightarrow> c \<notin> closure (A - {c})"
  18.202    using not_trivial_limit_within[of c A] by blast
  18.203  
  18.204 @@ -3229,6 +3372,28 @@
  18.205    qed
  18.206  qed
  18.207  
  18.208 +lemma tendsto_If_within_closures:
  18.209 +  assumes f: "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
  18.210 +      (f \<longlongrightarrow> l x) (at x within s \<union> (closure s \<inter> closure t))"
  18.211 +  assumes g: "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
  18.212 +      (g \<longlongrightarrow> l x) (at x within t \<union> (closure s \<inter> closure t))"
  18.213 +  assumes "x \<in> s \<union> t"
  18.214 +  shows "((\<lambda>x. if x \<in> s then f x else g x) \<longlongrightarrow> l x) (at x within s \<union> t)"
  18.215 +proof -
  18.216 +  have *: "(s \<union> t) \<inter> {x. x \<in> s} = s" "(s \<union> t) \<inter> {x. x \<notin> s} = t - s"
  18.217 +    by auto
  18.218 +  have "(f \<longlongrightarrow> l x) (at x within s)"
  18.219 +    by (rule filterlim_at_within_closure_implies_filterlim)
  18.220 +       (use \<open>x \<in> _\<close> in \<open>auto simp: inf_commute closure_def intro: tendsto_within_subset[OF f]\<close>)
  18.221 +  moreover
  18.222 +  have "(g \<longlongrightarrow> l x) (at x within t - s)"
  18.223 +    by (rule filterlim_at_within_closure_implies_filterlim)
  18.224 +      (use \<open>x \<in> _\<close> in
  18.225 +        \<open>auto intro!: tendsto_within_subset[OF g] simp: closure_def intro: islimpt_subset\<close>)
  18.226 +  ultimately show ?thesis
  18.227 +    by (intro filterlim_at_within_If) (simp_all only: *)
  18.228 +qed
  18.229 +
  18.230  
  18.231  subsection \<open>Boundedness\<close>
  18.232  
    19.1 --- a/src/HOL/Analysis/Uniform_Limit.thy	Tue Feb 20 22:25:23 2018 +0100
    19.2 +++ b/src/HOL/Analysis/Uniform_Limit.thy	Thu Feb 22 15:17:25 2018 +0100
    19.3 @@ -438,6 +438,7 @@
    19.4    bounded_linear.uniform_limit[OF bounded_linear_mult_right]
    19.5    bounded_linear.uniform_limit[OF bounded_linear_scaleR_left]
    19.6  
    19.7 +
    19.8  lemmas uniform_limit_uminus[uniform_limit_intros] =
    19.9    bounded_linear.uniform_limit[OF bounded_linear_minus[OF bounded_linear_ident]]
   19.10  
   19.11 @@ -728,5 +729,7 @@
   19.12  apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
   19.13  using sm sums_unique by fastforce
   19.14  
   19.15 +lemmas uniform_limit_subset_union = uniform_limit_on_subset[OF uniform_limit_on_Union]
   19.16 +
   19.17  end
   19.18  
    20.1 --- a/src/HOL/Deriv.thy	Tue Feb 20 22:25:23 2018 +0100
    20.2 +++ b/src/HOL/Deriv.thy	Thu Feb 22 15:17:25 2018 +0100
    20.3 @@ -26,6 +26,13 @@
    20.4    most cases @{term s} is either a variable or @{term UNIV}.
    20.5  \<close>
    20.6  
    20.7 +text \<open>These are the only cases we'll care about, probably.\<close>
    20.8 +
    20.9 +lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
   20.10 +    bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x within s)"
   20.11 +  unfolding has_derivative_def tendsto_iff
   20.12 +  by (subst eventually_Lim_ident_at) (auto simp add: field_simps)
   20.13 +
   20.14  lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
   20.15    by simp
   20.16  
   20.17 @@ -189,6 +196,52 @@
   20.18  
   20.19  lemmas has_derivative_within_subset = has_derivative_subset
   20.20  
   20.21 +lemma has_derivative_within_singleton_iff:
   20.22 +  "(f has_derivative g) (at x within {x}) \<longleftrightarrow> bounded_linear g"
   20.23 +  by (auto intro!: has_derivativeI_sandwich[where e=1] has_derivative_bounded_linear)
   20.24 +
   20.25 +
   20.26 +subsubsection \<open>Limit transformation for derivatives\<close>
   20.27 +
   20.28 +lemma has_derivative_transform_within:
   20.29 +  assumes "(f has_derivative f') (at x within s)"
   20.30 +    and "0 < d"
   20.31 +    and "x \<in> s"
   20.32 +    and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
   20.33 +  shows "(g has_derivative f') (at x within s)"
   20.34 +  using assms
   20.35 +  unfolding has_derivative_within
   20.36 +  by (force simp add: intro: Lim_transform_within)
   20.37 +
   20.38 +lemma has_derivative_transform_within_open:
   20.39 +  assumes "(f has_derivative f') (at x within t)"
   20.40 +    and "open s"
   20.41 +    and "x \<in> s"
   20.42 +    and "\<And>x. x\<in>s \<Longrightarrow> f x = g x"
   20.43 +  shows "(g has_derivative f') (at x within t)"
   20.44 +  using assms unfolding has_derivative_within
   20.45 +  by (force simp add: intro: Lim_transform_within_open)
   20.46 +
   20.47 +lemma has_derivative_transform:
   20.48 +  assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
   20.49 +  assumes "(f has_derivative f') (at x within s)"
   20.50 +  shows "(g has_derivative f') (at x within s)"
   20.51 +  using assms
   20.52 +  by (intro has_derivative_transform_within[OF _ zero_less_one, where g=g]) auto
   20.53 +
   20.54 +lemma has_derivative_transform_eventually:
   20.55 +  assumes "(f has_derivative f') (at x within s)"
   20.56 +    "(\<forall>\<^sub>F x' in at x within s. f x' = g x')"
   20.57 +  assumes "f x = g x" "x \<in> s"
   20.58 +  shows "(g has_derivative f') (at x within s)"
   20.59 +  using assms
   20.60 +proof -
   20.61 +  from assms(2,3) obtain d where "d > 0" "\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x'"
   20.62 +    by (force simp: eventually_at)
   20.63 +  from has_derivative_transform_within[OF assms(1) this(1) assms(4) this(2)]
   20.64 +  show ?thesis .
   20.65 +qed
   20.66 +
   20.67  
   20.68  subsection \<open>Continuity\<close>
   20.69  
   20.70 @@ -295,6 +348,14 @@
   20.71    ((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)"
   20.72    by (blast intro: has_derivative_in_compose has_derivative_subset)
   20.73  
   20.74 +lemma has_derivative_in_compose2:
   20.75 +  assumes "\<And>x. x \<in> t \<Longrightarrow> (g has_derivative g' x) (at x within t)"
   20.76 +  assumes "f ` s \<subseteq> t" "x \<in> s"
   20.77 +  assumes "(f has_derivative f') (at x within s)"
   20.78 +  shows "((\<lambda>x. g (f x)) has_derivative (\<lambda>y. g' (f x) (f' y))) (at x within s)"
   20.79 +  using assms
   20.80 +  by (auto intro: has_derivative_within_subset intro!: has_derivative_in_compose[of f f' x s g])
   20.81 +
   20.82  lemma (in bounded_bilinear) FDERIV:
   20.83    assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
   20.84    shows "((\<lambda>x. f x ** g x) has_derivative (\<lambda>h. f x ** g' h + f' h ** g x)) (at x within s)"
   20.85 @@ -467,6 +528,10 @@
   20.86  all directions. There is a proof in \<open>Analysis\<close> for \<open>euclidean_space\<close>.
   20.87  \<close>
   20.88  
   20.89 +lemma has_derivative_at2: "(f has_derivative f') (at x) \<longleftrightarrow>
   20.90 +    bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x)"
   20.91 +  using has_derivative_within [of f f' x UNIV]
   20.92 +  by simp
   20.93  lemma has_derivative_zero_unique:
   20.94    assumes "((\<lambda>x. 0) has_derivative F) (at x)"
   20.95    shows "F = (\<lambda>h. 0)"
   20.96 @@ -542,10 +607,19 @@
   20.97      (\<lambda>x. f (g x)) differentiable (at x within s)"
   20.98    by (blast intro: differentiable_in_compose differentiable_subset)
   20.99  
  20.100 -lemma differentiable_sum [simp, derivative_intros]:
  20.101 +lemma differentiable_add [simp, derivative_intros]:
  20.102    "f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x + g x) differentiable F"
  20.103    unfolding differentiable_def by (blast intro: has_derivative_add)
  20.104  
  20.105 +lemma differentiable_sum[simp, derivative_intros]:
  20.106 +  assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net"
  20.107 +  shows "(\<lambda>x. sum (\<lambda>a. f a x) s) differentiable net"
  20.108 +proof -
  20.109 +  from bchoice[OF assms(2)[unfolded differentiable_def]]
  20.110 +  show ?thesis
  20.111 +    by (auto intro!: has_derivative_sum simp: differentiable_def)
  20.112 +qed
  20.113 +
  20.114  lemma differentiable_minus [simp, derivative_intros]:
  20.115    "f differentiable F \<Longrightarrow> (\<lambda>x. - f x) differentiable F"
  20.116    unfolding differentiable_def by (blast intro: has_derivative_minus)
  20.117 @@ -651,6 +725,14 @@
  20.118    for c :: "'a::ab_semigroup_mult"
  20.119    by (simp add: fun_eq_iff mult.commute)
  20.120  
  20.121 +lemma DERIV_compose_FDERIV:
  20.122 +  fixes f::"real\<Rightarrow>real"
  20.123 +  assumes "DERIV f (g x) :> f'"
  20.124 +  assumes "(g has_derivative g') (at x within s)"
  20.125 +  shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>x. g' x * f')) (at x within s)"
  20.126 +  using assms has_derivative_compose[of g g' x s f "( * ) f'"]
  20.127 +  by (auto simp: has_field_derivative_def ac_simps)
  20.128 +
  20.129  
  20.130  subsection \<open>Vector derivative\<close>
  20.131  
  20.132 @@ -998,6 +1080,8 @@
  20.133      by eventually_elim auto
  20.134  qed
  20.135  
  20.136 +lemmas has_derivative_floor[derivative_intros] =
  20.137 +  floor_has_real_derivative[THEN DERIV_compose_FDERIV]
  20.138  
  20.139  text \<open>Caratheodory formulation of derivative at a point\<close>
  20.140  
    21.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Feb 20 22:25:23 2018 +0100
    21.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Feb 22 15:17:25 2018 +0100
    21.3 @@ -1800,8 +1800,176 @@
    21.4  lemma max_MInf2 [simp]: "max x (-\<infinity>::ereal) = x"
    21.5  by (metis max_bot2 bot_ereal_def)
    21.6  
    21.7 -
    21.8 -subsubsection "Topological space"
    21.9 +subsection \<open>Extended real intervals\<close>
   21.10 +
   21.11 +lemma real_greaterThanLessThan_infinity_eq:
   21.12 +  "real_of_ereal ` {N::ereal<..<\<infinity>} =
   21.13 +    (if N = \<infinity> then {} else if N = -\<infinity> then UNIV else {real_of_ereal N<..})"
   21.14 +proof -
   21.15 +  {
   21.16 +    fix x::real
   21.17 +    have "x \<in> real_of_ereal ` {- \<infinity><..<\<infinity>::ereal}"
   21.18 +      by (auto intro!: image_eqI[where x="ereal x"])
   21.19 +  } moreover {
   21.20 +    fix x::ereal
   21.21 +    assume "N \<noteq> - \<infinity>" "N < x" "x \<noteq> \<infinity>"
   21.22 +    then have "real_of_ereal N < real_of_ereal x"
   21.23 +      by (cases N; cases x; simp)
   21.24 +  } moreover {
   21.25 +    fix x::real
   21.26 +    assume "N \<noteq> \<infinity>" "real_of_ereal N < x"
   21.27 +    then have "x \<in> real_of_ereal ` {N<..<\<infinity>}"
   21.28 +      by (cases N) (auto intro!: image_eqI[where x="ereal x"])
   21.29 +  } ultimately show ?thesis by auto
   21.30 +qed
   21.31 +
   21.32 +lemma real_greaterThanLessThan_minus_infinity_eq:
   21.33 +  "real_of_ereal ` {-\<infinity><..<N::ereal} =
   21.34 +    (if N = \<infinity> then UNIV else if N = -\<infinity> then {} else {..<real_of_ereal N})"
   21.35 +proof -
   21.36 +  have "real_of_ereal ` {-\<infinity><..<N::ereal} = uminus ` real_of_ereal ` {-N<..<\<infinity>}"
   21.37 +    by (auto simp: ereal_uminus_less_reorder intro!: image_eqI[where x="-x" for x])
   21.38 +  also note real_greaterThanLessThan_infinity_eq
   21.39 +  finally show ?thesis by (auto intro!: image_eqI[where x="-x" for x])
   21.40 +qed
   21.41 +
   21.42 +lemma real_greaterThanLessThan_inter:
   21.43 +  "real_of_ereal ` {N<..<M::ereal} = real_of_ereal ` {-\<infinity><..<M} \<inter> real_of_ereal ` {N<..<\<infinity>}"
   21.44 +  apply safe
   21.45 +  subgoal by force
   21.46 +  subgoal by force
   21.47 +  subgoal for x y z
   21.48 +    by (cases y; cases z) (auto intro!: image_eqI[where x=z] simp: )
   21.49 +  done
   21.50 +
   21.51 +lemma real_atLeastGreaterThan_eq: "real_of_ereal ` {N<..<M::ereal} =
   21.52 +   (if N = \<infinity> then {} else
   21.53 +   if N = -\<infinity> then
   21.54 +    (if M = \<infinity> then UNIV
   21.55 +    else if M = -\<infinity> then {}
   21.56 +    else {..< real_of_ereal M})
   21.57 +  else if M = - \<infinity> then {}
   21.58 +  else if M = \<infinity> then {real_of_ereal N<..}
   21.59 +  else {real_of_ereal N <..< real_of_ereal M})"
   21.60 +  apply (subst real_greaterThanLessThan_inter)
   21.61 +  apply (subst real_greaterThanLessThan_minus_infinity_eq)
   21.62 +  apply (subst real_greaterThanLessThan_infinity_eq)
   21.63 +  apply auto
   21.64 +  done
   21.65 +
   21.66 +lemma real_image_ereal_ivl:
   21.67 +  fixes a b::ereal
   21.68 +  shows
   21.69 +  "real_of_ereal ` {a<..<b} =
   21.70 +  (if a < b then (if a = - \<infinity> then if b = \<infinity> then UNIV else {..<real_of_ereal b}
   21.71 +  else if b = \<infinity> then {real_of_ereal a<..} else {real_of_ereal a <..< real_of_ereal b}) else {})"
   21.72 +  by (cases a; cases b; simp add: real_atLeastGreaterThan_eq not_less)
   21.73 +
   21.74 +lemma fixes a b c::ereal
   21.75 +  shows not_inftyI: "a < b \<Longrightarrow> b < c \<Longrightarrow> abs b \<noteq> \<infinity>"
   21.76 +  by force
   21.77 +
   21.78 +lemma
   21.79 +  interval_neqs:
   21.80 +  fixes r s t::real
   21.81 +  shows "{r<..<s} \<noteq> {t<..}"
   21.82 +    and "{r<..<s} \<noteq> {..<t}"
   21.83 +    and "{r<..<ra} \<noteq> UNIV"
   21.84 +    and "{r<..} \<noteq> {..<s}"
   21.85 +    and "{r<..} \<noteq> UNIV"
   21.86 +    and "{..<r} \<noteq> UNIV"
   21.87 +    and "{} \<noteq> {r<..}"
   21.88 +    and "{} \<noteq> {..<r}"
   21.89 +  subgoal
   21.90 +    by (metis dual_order.strict_trans greaterThanLessThan_iff greaterThan_iff gt_ex not_le order_refl)
   21.91 +  subgoal
   21.92 +    by (metis (no_types, hide_lams) greaterThanLessThan_empty_iff greaterThanLessThan_iff gt_ex
   21.93 +        lessThan_iff minus_minus neg_less_iff_less not_less order_less_irrefl)
   21.94 +  subgoal by force
   21.95 +  subgoal
   21.96 +    by (metis greaterThanLessThan_empty_iff greaterThanLessThan_eq greaterThan_iff inf.idem
   21.97 +        lessThan_iff lessThan_non_empty less_irrefl not_le)
   21.98 +  subgoal by force
   21.99 +  subgoal by force
  21.100 +  subgoal using greaterThan_non_empty by blast
  21.101 +  subgoal using lessThan_non_empty by blast
  21.102 +  done
  21.103 +
  21.104 +lemma greaterThanLessThan_eq_iff:
  21.105 +  fixes r s t u::real
  21.106 +  shows "({r<..<s} = {t<..<u}) = (r \<ge> s \<and> u \<le> t \<or> r = t \<and> s = u)"
  21.107 +  by (metis cInf_greaterThanLessThan cSup_greaterThanLessThan greaterThanLessThan_empty_iff not_le)
  21.108 +
  21.109 +lemma real_of_ereal_image_greaterThanLessThan_iff:
  21.110 +  "real_of_ereal ` {a <..< b} = real_of_ereal ` {c <..< d} \<longleftrightarrow> (a \<ge> b \<and> c \<ge> d \<or> a = c \<and> b = d)"
  21.111 +  unfolding real_atLeastGreaterThan_eq
  21.112 +  by (cases a; cases b; cases c; cases d;
  21.113 +    simp add: greaterThanLessThan_eq_iff interval_neqs interval_neqs[symmetric])
  21.114 +
  21.115 +lemma uminus_image_real_of_ereal_image_greaterThanLessThan:
  21.116 +  "uminus ` real_of_ereal ` {l <..< u} = real_of_ereal ` {-u <..< -l}"
  21.117 +  by (force simp: algebra_simps ereal_less_uminus_reorder
  21.118 +    ereal_uminus_less_reorder intro: image_eqI[where x="-x" for x])
  21.119 +
  21.120 +lemma add_image_real_of_ereal_image_greaterThanLessThan:
  21.121 +  "(+) c ` real_of_ereal ` {l <..< u} = real_of_ereal ` {c + l <..< c + u}"
  21.122 +  apply safe
  21.123 +  subgoal for x
  21.124 +    using ereal_less_add[of c]
  21.125 +    by (force simp: real_of_ereal_add add.commute)
  21.126 +  subgoal for _ x
  21.127 +    by (force simp: add.commute real_of_ereal_minus ereal_minus_less ereal_less_minus
  21.128 +      intro: image_eqI[where x="x - c"])
  21.129 +  done
  21.130 +
  21.131 +lemma add2_image_real_of_ereal_image_greaterThanLessThan:
  21.132 +  "(\<lambda>x. x + c) ` real_of_ereal ` {l <..< u} = real_of_ereal ` {l + c <..< u + c}"
  21.133 +  using add_image_real_of_ereal_image_greaterThanLessThan[of c l u]
  21.134 +  by (metis add.commute image_cong)
  21.135 +
  21.136 +lemma minus_image_real_of_ereal_image_greaterThanLessThan:
  21.137 +  "(-) c ` real_of_ereal ` {l <..< u} = real_of_ereal ` {c - u <..< c - l}"
  21.138 +  (is "?l = ?r")
  21.139 +proof -
  21.140 +  have "?l = (+) c ` uminus ` real_of_ereal ` {l <..< u}" by auto
  21.141 +  also note uminus_image_real_of_ereal_image_greaterThanLessThan
  21.142 +  also note add_image_real_of_ereal_image_greaterThanLessThan
  21.143 +  finally show ?thesis by (simp add: minus_ereal_def)
  21.144 +qed
  21.145 +
  21.146 +lemma real_ereal_bound_lemma_up:
  21.147 +  assumes "s \<in> real_of_ereal ` {a<..<b}"
  21.148 +  assumes "t \<notin> real_of_ereal ` {a<..<b}"
  21.149 +  assumes "s \<le> t"
  21.150 +  shows "b \<noteq> \<infinity>"
  21.151 +  using assms
  21.152 +  apply (cases b)
  21.153 +  subgoal by force
  21.154 +  subgoal by (metis PInfty_neq_ereal(2) assms dual_order.strict_trans1 ereal_infty_less(1)
  21.155 +    ereal_less_ereal_Ex greaterThanLessThan_empty_iff greaterThanLessThan_iff greaterThan_iff
  21.156 +    image_eqI less_imp_le linordered_field_no_ub not_less order_trans
  21.157 +    real_greaterThanLessThan_infinity_eq real_image_ereal_ivl real_of_ereal.simps(1))
  21.158 +  subgoal by force
  21.159 +  done
  21.160 +
  21.161 +lemma real_ereal_bound_lemma_down:
  21.162 +  assumes "s \<in> real_of_ereal ` {a<..<b}"
  21.163 +  assumes "t \<notin> real_of_ereal ` {a<..<b}"
  21.164 +  assumes "t \<le> s"
  21.165 +  shows "a \<noteq> - \<infinity>"
  21.166 +  using assms
  21.167 +  apply (cases b)
  21.168 +  subgoal
  21.169 +    apply safe
  21.170 +    using assms(1)
  21.171 +    apply (auto simp: real_greaterThanLessThan_minus_infinity_eq)
  21.172 +    done
  21.173 +  subgoal by (auto simp: real_greaterThanLessThan_minus_infinity_eq)
  21.174 +  subgoal by auto
  21.175 +  done
  21.176 +
  21.177 +
  21.178 +subsection "Topological space"
  21.179  
  21.180  instantiation ereal :: linear_continuum_topology
  21.181  begin
  21.182 @@ -2469,6 +2637,21 @@
  21.183       by auto
  21.184  qed (auto simp add: image_Union image_Int)
  21.185  
  21.186 +lemma open_image_real_of_ereal:
  21.187 +  fixes X::"ereal set"
  21.188 +  assumes "open X"
  21.189 +  assumes "\<infinity> \<notin> X"
  21.190 +  assumes "-\<infinity> \<notin> X"
  21.191 +  shows "open (real_of_ereal ` X)"
  21.192 +proof -
  21.193 +  have "real_of_ereal ` X = ereal -` X"
  21.194 +    apply safe
  21.195 +    subgoal by (metis assms(2) assms(3) real_of_ereal.elims vimageI)
  21.196 +    subgoal using image_iff by fastforce
  21.197 +    done
  21.198 +  thus ?thesis
  21.199 +    by (auto intro!: open_ereal_vimage assms)
  21.200 +qed
  21.201  
  21.202  lemma eventually_finite:
  21.203    fixes x :: ereal
    22.1 --- a/src/HOL/Limits.thy	Tue Feb 20 22:25:23 2018 +0100
    22.2 +++ b/src/HOL/Limits.thy	Thu Feb 22 15:17:25 2018 +0100
    22.3 @@ -52,6 +52,9 @@
    22.4    for f :: "_ \<Rightarrow> real"
    22.5    by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl])
    22.6  
    22.7 +lemma filterlim_real_at_infinity_sequentially: "filterlim real at_infinity sequentially"
    22.8 +  by (simp add: filterlim_at_top_imp_at_infinity filterlim_real_sequentially)
    22.9 +
   22.10  lemma lim_infinity_imp_sequentially: "(f \<longlongrightarrow> l) at_infinity \<Longrightarrow> ((\<lambda>n. f(n)) \<longlongrightarrow> l) sequentially"
   22.11    by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially)
   22.12  
   22.13 @@ -1256,6 +1259,20 @@
   22.14    for a :: real
   22.15    unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
   22.16  
   22.17 +lemma at_to_0: "at a = filtermap (\<lambda>x. x + a) (at 0)"
   22.18 +  for a :: "'a::real_normed_vector"
   22.19 +  using filtermap_at_shift[of "-a" 0] by simp
   22.20 +
   22.21 +lemma filterlim_at_to_0:
   22.22 +  "filterlim f F (at a) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at 0)"
   22.23 +  for a :: "'a::real_normed_vector"
   22.24 +  unfolding filterlim_def filtermap_filtermap at_to_0[of a] ..
   22.25 +
   22.26 +lemma eventually_at_to_0:
   22.27 +  "eventually P (at a) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at 0)"
   22.28 +  for a ::  "'a::real_normed_vector"
   22.29 +  unfolding at_to_0[of a] by (simp add: eventually_filtermap)
   22.30 +
   22.31  lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a)"
   22.32    for a :: "'a::real_normed_vector"
   22.33    by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
   22.34 @@ -1268,6 +1285,7 @@
   22.35    for a :: real
   22.36    by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
   22.37  
   22.38 +
   22.39  lemma filterlim_at_left_to_right:
   22.40    "filterlim f F (at_left a) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
   22.41    for a :: real
   22.42 @@ -1486,6 +1504,36 @@
   22.43    for c :: nat
   22.44    by (rule filterlim_subseq) (auto simp: strict_mono_def)
   22.45  
   22.46 +lemma filterlim_times_pos:
   22.47 +  "LIM x F1. c * f x :> at_right l"
   22.48 +  if "filterlim f (at_right p) F1" "0 < c" "l = c * p"
   22.49 +  for c::"'a::{linordered_field, linorder_topology}"
   22.50 +  unfolding filterlim_iff
   22.51 +proof safe
   22.52 +  fix P
   22.53 +  assume "\<forall>\<^sub>F x in at_right l. P x"
   22.54 +  then obtain d where "c * p < d" "\<And>y. y > c * p \<Longrightarrow> y < d \<Longrightarrow> P y"
   22.55 +    unfolding \<open>l = _ \<close> eventually_at_right_field
   22.56 +    by auto
   22.57 +  then have "\<forall>\<^sub>F a in at_right p. P (c * a)"
   22.58 +    by (auto simp: eventually_at_right_field \<open>0 < c\<close> field_simps intro!: exI[where x="d/c"])
   22.59 +  from that(1)[unfolded filterlim_iff, rule_format, OF this]
   22.60 +  show "\<forall>\<^sub>F x in F1. P (c * f x)" .
   22.61 +qed
   22.62 +
   22.63 +lemma filtermap_nhds_times: "c \<noteq> 0 \<Longrightarrow> filtermap (times c) (nhds a) = nhds (c * a)"
   22.64 +  for a c :: "'a::real_normed_field"
   22.65 +  by (rule filtermap_fun_inverse[where g="\<lambda>x. inverse c * x"])
   22.66 +    (auto intro!: tendsto_eq_intros filterlim_ident)
   22.67 +
   22.68 +lemma filtermap_times_pos_at_right:
   22.69 +  fixes c::"'a::{linordered_field, linorder_topology}"
   22.70 +  assumes "c > 0"
   22.71 +  shows "filtermap (times c) (at_right p) = at_right (c * p)"
   22.72 +  using assms
   22.73 +  by (intro filtermap_fun_inverse[where g="\<lambda>x. inverse c * x"])
   22.74 +    (auto intro!: filterlim_ident filterlim_times_pos)
   22.75 +
   22.76  lemma at_to_infinity: "(at (0::'a::{real_normed_field,field})) = filtermap inverse at_infinity"
   22.77  proof (rule antisym)
   22.78    have "(inverse \<longlongrightarrow> (0::'a)) at_infinity"
   22.79 @@ -1936,6 +1984,10 @@
   22.80  lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
   22.81    using lim_1_over_n by (simp add: inverse_eq_divide)
   22.82  
   22.83 +lemma lim_inverse_n': "((\<lambda>n. 1 / n) \<longlongrightarrow> 0) sequentially"
   22.84 +  using lim_inverse_n
   22.85 +  by (simp add: inverse_eq_divide)
   22.86 +
   22.87  lemma LIMSEQ_Suc_n_over_n: "(\<lambda>n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) \<longlonglongrightarrow> 1"
   22.88  proof (rule Lim_transform_eventually)
   22.89    show "eventually (\<lambda>n. 1 + inverse (of_nat n :: 'a) = of_nat (Suc n) / of_nat n) sequentially"
    23.1 --- a/src/HOL/NthRoot.thy	Tue Feb 20 22:25:23 2018 +0100
    23.2 +++ b/src/HOL/NthRoot.thy	Thu Feb 22 15:17:25 2018 +0100
    23.3 @@ -480,6 +480,9 @@
    23.4  lemma sqrt_le_D: "sqrt x \<le> y \<Longrightarrow> x \<le> y\<^sup>2"
    23.5    by (meson not_le real_less_rsqrt)
    23.6  
    23.7 +lemma sqrt_ge_absD: "\<bar>x\<bar> \<le> sqrt y \<Longrightarrow> x\<^sup>2 \<le> y"
    23.8 +  using real_sqrt_le_iff[of "x\<^sup>2"] by simp
    23.9 +
   23.10  lemma sqrt_even_pow2:
   23.11    assumes n: "even n"
   23.12    shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
   23.13 @@ -538,6 +541,8 @@
   23.14    DERIV_real_sqrt_generic[THEN DERIV_chain2, derivative_intros]
   23.15    DERIV_real_root_generic[THEN DERIV_chain2, derivative_intros]
   23.16  
   23.17 +lemmas has_derivative_real_sqrt[derivative_intros] = DERIV_real_sqrt[THEN DERIV_compose_FDERIV]
   23.18 +
   23.19  lemma not_real_square_gt_zero [simp]: "\<not> 0 < x * x \<longleftrightarrow> x = 0"
   23.20    for x :: real
   23.21    apply auto
   23.22 @@ -658,6 +663,13 @@
   23.23  lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
   23.24    by (simp add: power2_eq_square [symmetric])
   23.25  
   23.26 +lemma sqrt_sum_squares_le_sum:
   23.27 +  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
   23.28 +  apply (rule power2_le_imp_le)
   23.29 +  apply (simp add: power2_sum)
   23.30 +  apply simp
   23.31 +  done
   23.32 +
   23.33  lemma real_sqrt_sum_squares_triangle_ineq:
   23.34    "sqrt ((a + c)\<^sup>2 + (b + d)\<^sup>2) \<le> sqrt (a\<^sup>2 + b\<^sup>2) + sqrt (c\<^sup>2 + d\<^sup>2)"
   23.35    apply (rule power2_le_imp_le)
    24.1 --- a/src/HOL/Set_Interval.thy	Tue Feb 20 22:25:23 2018 +0100
    24.2 +++ b/src/HOL/Set_Interval.thy	Thu Feb 22 15:17:25 2018 +0100
    24.3 @@ -222,6 +222,10 @@
    24.4    "{a..<b} = {a..b} - {b}"
    24.5    by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
    24.6  
    24.7 +lemma (in order) greaterThanAtMost_eq_atLeastAtMost_diff:
    24.8 +  "{a<..b} = {a..b} - {a}"
    24.9 +  by (auto simp add: greaterThanAtMost_def atLeastAtMost_def)
   24.10 +
   24.11  end
   24.12  
   24.13  subsubsection\<open>Emptyness, singletons, subset\<close>
   24.14 @@ -869,6 +873,19 @@
   24.15  context linordered_semidom
   24.16  begin
   24.17  
   24.18 +lemma image_add_atLeast[simp]: "plus k ` {i..} = {k + i..}"
   24.19 +proof -
   24.20 +  have "n = k + (n - k)" if "i + k \<le> n" for n
   24.21 +  proof -
   24.22 +    have "n = (n - (k + i)) + (k + i)" using that
   24.23 +      by (metis add_commute le_add_diff_inverse)
   24.24 +    then show "n = k + (n - k)"
   24.25 +      by (metis local.add_diff_cancel_left' add_assoc add_commute)
   24.26 +  qed
   24.27 +  then show ?thesis
   24.28 +    by (fastforce simp: add_le_imp_le_diff add.commute)
   24.29 +qed
   24.30 +
   24.31  lemma image_add_atLeastAtMost [simp]:
   24.32    "plus k ` {i..j} = {i + k..j + k}" (is "?A = ?B")
   24.33  proof
   24.34 @@ -911,112 +928,11 @@
   24.35    "(\<lambda>n. n + k) ` {i..<j} = {i + k..<j + k}"
   24.36    by (simp add: add.commute [of _ k])
   24.37  
   24.38 +lemma image_add_greaterThanAtMost[simp]: "(+) c ` {a<..b} = {c + a<..c + b}"
   24.39 +  by (simp add: image_set_diff greaterThanAtMost_eq_atLeastAtMost_diff ac_simps)
   24.40 +
   24.41  end
   24.42  
   24.43 -lemma image_Suc_atLeastAtMost [simp]:
   24.44 -  "Suc ` {i..j} = {Suc i..Suc j}"
   24.45 -  using image_add_atLeastAtMost [of 1 i j]
   24.46 -    by (simp only: plus_1_eq_Suc) simp
   24.47 -
   24.48 -lemma image_Suc_atLeastLessThan [simp]:
   24.49 -  "Suc ` {i..<j} = {Suc i..<Suc j}"
   24.50 -  using image_add_atLeastLessThan [of 1 i j]
   24.51 -    by (simp only: plus_1_eq_Suc) simp
   24.52 -
   24.53 -corollary image_Suc_atMost:
   24.54 -  "Suc ` {..n} = {1..Suc n}"
   24.55 -  by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost)
   24.56 -
   24.57 -corollary image_Suc_lessThan:
   24.58 -  "Suc ` {..<n} = {1..n}"
   24.59 -  by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost)
   24.60 -  
   24.61 -lemma image_diff_atLeastAtMost [simp]:
   24.62 -  fixes d::"'a::linordered_idom" shows "((-) d ` {a..b}) = {d-b..d-a}"
   24.63 -  apply auto
   24.64 -  apply (rule_tac x="d-x" in rev_image_eqI, auto)
   24.65 -  done
   24.66 -
   24.67 -lemma image_mult_atLeastAtMost [simp]:
   24.68 -  fixes d::"'a::linordered_field"
   24.69 -  assumes "d>0" shows "(( * ) d ` {a..b}) = {d*a..d*b}"
   24.70 -  using assms
   24.71 -  by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
   24.72 -
   24.73 -lemma image_affinity_atLeastAtMost:
   24.74 -  fixes c :: "'a::linordered_field"
   24.75 -  shows "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {}
   24.76 -            else if 0 \<le> m then {m*a + c .. m *b + c}
   24.77 -            else {m*b + c .. m*a + c})"
   24.78 -  apply (case_tac "m=0", auto simp: mult_le_cancel_left)
   24.79 -  apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)
   24.80 -  apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)
   24.81 -  done
   24.82 -
   24.83 -lemma image_affinity_atLeastAtMost_diff:
   24.84 -  fixes c :: "'a::linordered_field"
   24.85 -  shows "((\<lambda>x. m*x - c) ` {a..b}) = (if {a..b}={} then {}
   24.86 -            else if 0 \<le> m then {m*a - c .. m*b - c}
   24.87 -            else {m*b - c .. m*a - c})"
   24.88 -  using image_affinity_atLeastAtMost [of m "-c" a b]
   24.89 -  by simp
   24.90 -
   24.91 -lemma image_affinity_atLeastAtMost_div:
   24.92 -  fixes c :: "'a::linordered_field"
   24.93 -  shows "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
   24.94 -            else if 0 \<le> m then {a/m + c .. b/m + c}
   24.95 -            else {b/m + c .. a/m + c})"
   24.96 -  using image_affinity_atLeastAtMost [of "inverse m" c a b]
   24.97 -  by (simp add: field_class.field_divide_inverse algebra_simps)
   24.98 -
   24.99 -lemma image_affinity_atLeastAtMost_div_diff:
  24.100 -  fixes c :: "'a::linordered_field"
  24.101 -  shows "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
  24.102 -            else if 0 \<le> m then {a/m - c .. b/m - c}
  24.103 -            else {b/m - c .. a/m - c})"
  24.104 -  using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]
  24.105 -  by (simp add: field_class.field_divide_inverse algebra_simps)
  24.106 -
  24.107 -lemma atLeast1_lessThan_eq_remove0:
  24.108 -  "{Suc 0..<n} = {..<n} - {0}"
  24.109 -  by auto
  24.110 -
  24.111 -lemma atLeast1_atMost_eq_remove0:
  24.112 -  "{Suc 0..n} = {..n} - {0}"
  24.113 -  by auto
  24.114 -
  24.115 -lemma image_add_int_atLeastLessThan:
  24.116 -    "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
  24.117 -  apply (auto simp add: image_def)
  24.118 -  apply (rule_tac x = "x - l" in bexI)
  24.119 -  apply auto
  24.120 -  done
  24.121 -
  24.122 -lemma image_minus_const_atLeastLessThan_nat:
  24.123 -  fixes c :: nat
  24.124 -  shows "(\<lambda>i. i - c) ` {x ..< y} =
  24.125 -      (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
  24.126 -    (is "_ = ?right")
  24.127 -proof safe
  24.128 -  fix a assume a: "a \<in> ?right"
  24.129 -  show "a \<in> (\<lambda>i. i - c) ` {x ..< y}"
  24.130 -  proof cases
  24.131 -    assume "c < y" with a show ?thesis
  24.132 -      by (auto intro!: image_eqI[of _ _ "a + c"])
  24.133 -  next
  24.134 -    assume "\<not> c < y" with a show ?thesis
  24.135 -      by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)
  24.136 -  qed
  24.137 -qed auto
  24.138 -
  24.139 -lemma image_int_atLeastLessThan:
  24.140 -  "int ` {a..<b} = {int a..<int b}"
  24.141 -  by (auto intro!: image_eqI [where x = "nat x" for x])
  24.142 -
  24.143 -lemma image_int_atLeastAtMost:
  24.144 -  "int ` {a..b} = {int a..int b}"
  24.145 -  by (auto intro!: image_eqI [where x = "nat x" for x])
  24.146 -
  24.147  context ordered_ab_group_add
  24.148  begin
  24.149  
  24.150 @@ -1057,8 +973,184 @@
  24.151    and image_uminus_greaterThanLessThan[simp]: "uminus ` {x<..<y} = {-y<..<-x}"
  24.152    by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def
  24.153        greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute)
  24.154 +
  24.155 +lemma image_add_atMost[simp]: "(+) c ` {..a} = {..c + a}"
  24.156 +  by (auto intro!: image_eqI[where x="x - c" for x] simp: algebra_simps)
  24.157 +
  24.158  end
  24.159  
  24.160 +lemma image_Suc_atLeastAtMost [simp]:
  24.161 +  "Suc ` {i..j} = {Suc i..Suc j}"
  24.162 +  using image_add_atLeastAtMost [of 1 i j]
  24.163 +    by (simp only: plus_1_eq_Suc) simp
  24.164 +
  24.165 +lemma image_Suc_atLeastLessThan [simp]:
  24.166 +  "Suc ` {i..<j} = {Suc i..<Suc j}"
  24.167 +  using image_add_atLeastLessThan [of 1 i j]
  24.168 +    by (simp only: plus_1_eq_Suc) simp
  24.169 +
  24.170 +corollary image_Suc_atMost:
  24.171 +  "Suc ` {..n} = {1..Suc n}"
  24.172 +  by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost)
  24.173 +
  24.174 +corollary image_Suc_lessThan:
  24.175 +  "Suc ` {..<n} = {1..n}"
  24.176 +  by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost)
  24.177 +
  24.178 +lemma image_diff_atLeastAtMost [simp]:
  24.179 +  fixes d::"'a::linordered_idom" shows "((-) d ` {a..b}) = {d-b..d-a}"
  24.180 +  apply auto
  24.181 +  apply (rule_tac x="d-x" in rev_image_eqI, auto)
  24.182 +  done
  24.183 +
  24.184 +lemma image_diff_atLeastLessThan [simp]:
  24.185 +  fixes a b c::"'a::linordered_idom"
  24.186 +  shows "(-) c ` {a..<b} = {c - b<..c - a}"
  24.187 +proof -
  24.188 +  have "(-) c ` {a..<b} = (+) c ` uminus ` {a ..<b}"
  24.189 +    unfolding image_image by simp
  24.190 +  also have "\<dots> = {c - b<..c - a}" by simp
  24.191 +  finally show ?thesis by simp
  24.192 +qed
  24.193 +
  24.194 +lemma image_minus_const_greaterThanAtMost_real[simp]:
  24.195 +  fixes a b c::"'a::linordered_idom"
  24.196 +  shows "(-) c ` {a<..b} = {c - b..<c - a}"
  24.197 +proof -
  24.198 +  have "(-) c ` {a<..b} = (+) c ` uminus ` {a<..b}"
  24.199 +    unfolding image_image by simp
  24.200 +  also have "\<dots> = {c - b..<c - a}" by simp
  24.201 +  finally show ?thesis by simp
  24.202 +qed
  24.203 +
  24.204 +lemma image_minus_const_atLeast_real[simp]:
  24.205 +  fixes a c::"'a::linordered_idom"
  24.206 +  shows "(-) c ` {a..} = {..c - a}"
  24.207 +proof -
  24.208 +  have "(-) c ` {a..} = (+) c ` uminus ` {a ..}"
  24.209 +    unfolding image_image by simp
  24.210 +  also have "\<dots> = {..c - a}" by simp
  24.211 +  finally show ?thesis by simp
  24.212 +qed
  24.213 +
  24.214 +lemma image_minus_const_AtMost_real[simp]:
  24.215 +  fixes b c::"'a::linordered_idom"
  24.216 +  shows "(-) c ` {..b} = {c - b..}"
  24.217 +proof -
  24.218 +  have "(-) c ` {..b} = (+) c ` uminus ` {..b}"
  24.219 +    unfolding image_image by simp
  24.220 +  also have "\<dots> = {c - b..}" by simp
  24.221 +  finally show ?thesis by simp
  24.222 +qed
  24.223 +
  24.224 +context linordered_field begin
  24.225 +
  24.226 +lemma image_mult_atLeastAtMost [simp]:
  24.227 +  "(( * ) d ` {a..b}) = {d*a..d*b}" if "d>0"
  24.228 +  using that
  24.229 +  by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
  24.230 +
  24.231 +lemma image_mult_atLeastAtMost_if:
  24.232 +  "( * ) c ` {x .. y} =
  24.233 +    (if c > 0 then {c * x .. c * y} else if x \<le> y then {c * y .. c * x} else {})"
  24.234 +proof -
  24.235 +  consider "c < 0" "x \<le> y" | "c = 0" "x \<le> y" | "c > 0" "x \<le> y" | "x > y"
  24.236 +    using local.antisym_conv3 local.leI by blast
  24.237 +  then show ?thesis
  24.238 +  proof cases
  24.239 +    case 1
  24.240 +    have "( * ) c ` {x .. y} = uminus ` ( * ) (- c) ` {x .. y}"
  24.241 +      by (simp add: image_image)
  24.242 +    also have "\<dots> = {c * y .. c * x}"
  24.243 +      using \<open>c < 0\<close>
  24.244 +      by simp
  24.245 +    finally show ?thesis
  24.246 +      using \<open>c < 0\<close> by auto
  24.247 +  qed (auto simp: not_le local.mult_less_cancel_left_pos)
  24.248 +qed
  24.249 +
  24.250 +lemma image_mult_atLeastAtMost_if':
  24.251 +  "(\<lambda>x. x * c) ` {x..y} =
  24.252 +    (if x \<le> y then if c > 0 then {x * c .. y * c} else {y * c .. x * c} else {})"
  24.253 +  by (subst mult.commute)
  24.254 +    (simp add: image_mult_atLeastAtMost_if mult.commute mult_le_cancel_left_pos)
  24.255 +
  24.256 +lemma image_affinity_atLeastAtMost:
  24.257 +  "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {}
  24.258 +            else if 0 \<le> m then {m*a + c .. m *b + c}
  24.259 +            else {m*b + c .. m*a + c})"
  24.260 +proof -
  24.261 +  have "(\<lambda>x. m*x + c) = ((\<lambda>x. x + c) o ( * ) m)"
  24.262 +    unfolding image_comp[symmetric]
  24.263 +    by (simp add: o_def)
  24.264 +  then show ?thesis
  24.265 +    by (auto simp add: image_comp[symmetric] image_mult_atLeastAtMost_if mult_le_cancel_left)
  24.266 +qed
  24.267 +
  24.268 +lemma image_affinity_atLeastAtMost_diff:
  24.269 +  "((\<lambda>x. m*x - c) ` {a..b}) = (if {a..b}={} then {}
  24.270 +            else if 0 \<le> m then {m*a - c .. m*b - c}
  24.271 +            else {m*b - c .. m*a - c})"
  24.272 +  using image_affinity_atLeastAtMost [of m "-c" a b]
  24.273 +  by simp
  24.274 +
  24.275 +lemma image_affinity_atLeastAtMost_div:
  24.276 +  "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
  24.277 +            else if 0 \<le> m then {a/m + c .. b/m + c}
  24.278 +            else {b/m + c .. a/m + c})"
  24.279 +  using image_affinity_atLeastAtMost [of "inverse m" c a b]
  24.280 +  by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide)
  24.281 +
  24.282 +lemma image_affinity_atLeastAtMost_div_diff:
  24.283 +  "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
  24.284 +            else if 0 \<le> m then {a/m - c .. b/m - c}
  24.285 +            else {b/m - c .. a/m - c})"
  24.286 +  using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]
  24.287 +  by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide)
  24.288 +
  24.289 +end
  24.290 +
  24.291 +lemma atLeast1_lessThan_eq_remove0:
  24.292 +  "{Suc 0..<n} = {..<n} - {0}"
  24.293 +  by auto
  24.294 +
  24.295 +lemma atLeast1_atMost_eq_remove0:
  24.296 +  "{Suc 0..n} = {..n} - {0}"
  24.297 +  by auto
  24.298 +
  24.299 +lemma image_add_int_atLeastLessThan:
  24.300 +    "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
  24.301 +  apply (auto simp add: image_def)
  24.302 +  apply (rule_tac x = "x - l" in bexI)
  24.303 +  apply auto
  24.304 +  done
  24.305 +
  24.306 +lemma image_minus_const_atLeastLessThan_nat:
  24.307 +  fixes c :: nat
  24.308 +  shows "(\<lambda>i. i - c) ` {x ..< y} =
  24.309 +      (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
  24.310 +    (is "_ = ?right")
  24.311 +proof safe
  24.312 +  fix a assume a: "a \<in> ?right"
  24.313 +  show "a \<in> (\<lambda>i. i - c) ` {x ..< y}"
  24.314 +  proof cases
  24.315 +    assume "c < y" with a show ?thesis
  24.316 +      by (auto intro!: image_eqI[of _ _ "a + c"])
  24.317 +  next
  24.318 +    assume "\<not> c < y" with a show ?thesis
  24.319 +      by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)
  24.320 +  qed
  24.321 +qed auto
  24.322 +
  24.323 +lemma image_int_atLeastLessThan:
  24.324 +  "int ` {a..<b} = {int a..<int b}"
  24.325 +  by (auto intro!: image_eqI [where x = "nat x" for x])
  24.326 +
  24.327 +lemma image_int_atLeastAtMost:
  24.328 +  "int ` {a..b} = {int a..int b}"
  24.329 +  by (auto intro!: image_eqI [where x = "nat x" for x])
  24.330 +
  24.331 +
  24.332  subsubsection \<open>Finiteness\<close>
  24.333  
  24.334  lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
    25.1 --- a/src/HOL/Topological_Spaces.thy	Tue Feb 20 22:25:23 2018 +0100
    25.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Feb 22 15:17:25 2018 +0100
    25.3 @@ -609,7 +609,6 @@
    25.4      and "filterlim g G (at x within {x. \<not>P x})"
    25.5    shows "filterlim (\<lambda>x. if P x then f x else g x) G (at x)"
    25.6    using assms by (intro filterlim_at_within_If) simp_all
    25.7 -
    25.8  lemma (in linorder_topology) at_within_order:
    25.9    assumes "UNIV \<noteq> {x}"
   25.10    shows "at x within s =
   25.11 @@ -692,7 +691,18 @@
   25.12       (\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<inter> B - {A} \<longrightarrow> P x))" (is "?lhs = ?rhs")
   25.13    unfolding at_within_def filtercomap_inf eventually_inf_principal filtercomap_principal 
   25.14            eventually_filtercomap_nhds eventually_principal by blast
   25.15 -    
   25.16 +
   25.17 +lemma eventually_at_right_field:
   25.18 +  "eventually P (at_right x) \<longleftrightarrow> (\<exists>b>x. \<forall>y>x. y < b \<longrightarrow> P y)"
   25.19 +  for x :: "'a::{linordered_field, linorder_topology}"
   25.20 +  using linordered_field_no_ub[rule_format, of x]
   25.21 +  by (auto simp: eventually_at_right)
   25.22 +
   25.23 +lemma eventually_at_left_field:
   25.24 +  "eventually P (at_left x) \<longleftrightarrow> (\<exists>b<x. \<forall>y>b. y < x \<longrightarrow> P y)"
   25.25 +  for x :: "'a::{linordered_field, linorder_topology}"
   25.26 +  using linordered_field_no_lb[rule_format, of x]
   25.27 +  by (auto simp: eventually_at_left)
   25.28  
   25.29  
   25.30  subsubsection \<open>Tendsto\<close>
   25.31 @@ -762,9 +772,11 @@
   25.32  
   25.33  end
   25.34  
   25.35 -lemma tendsto_within_subset:
   25.36 -  "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T)"
   25.37 -  by (blast intro: tendsto_mono at_le)
   25.38 +lemma (in topological_space) filterlim_within_subset:
   25.39 +  "filterlim f l (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> filterlim f l (at x within T)"
   25.40 +  by (blast intro: filterlim_mono at_le)
   25.41 +
   25.42 +lemmas tendsto_within_subset = filterlim_within_subset
   25.43  
   25.44  lemma (in order_topology) order_tendsto_iff:
   25.45    "(f \<longlongrightarrow> x) F \<longleftrightarrow> (\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
   25.46 @@ -963,6 +975,11 @@
   25.47  lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
   25.48    by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
   25.49  
   25.50 +lemma eventually_Lim_ident_at:
   25.51 +  "(\<forall>\<^sub>F y in at x within X. P (Lim (at x within X) (\<lambda>x. x)) y) \<longleftrightarrow>
   25.52 +    (\<forall>\<^sub>F y in at x within X. P x y)" for x::"'a::t2_space"
   25.53 +  by (cases "at x within X = bot") (auto simp: Lim_ident_at)
   25.54 +
   25.55  lemma filterlim_at_bot_at_right:
   25.56    fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
   25.57    assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   25.58 @@ -2612,6 +2629,37 @@
   25.59      by (metis less_le)
   25.60  qed
   25.61  
   25.62 +lemma (in linorder_topology) not_in_connected_cases:
   25.63 +  assumes conn: "connected S"
   25.64 +  assumes nbdd: "x \<notin> S"
   25.65 +  assumes ne: "S \<noteq> {}"
   25.66 +  obtains "bdd_above S" "\<And>y. y \<in> S \<Longrightarrow> x \<ge> y" | "bdd_below S" "\<And>y. y \<in> S \<Longrightarrow> x \<le> y"
   25.67 +proof -
   25.68 +  obtain s where "s \<in> S" using ne by blast
   25.69 +  {
   25.70 +    assume "s \<le> x"
   25.71 +    have "False" if "x \<le> y" "y \<in> S" for y
   25.72 +      using connectedD_interval[OF conn \<open>s \<in> S\<close> \<open>y \<in> S\<close> \<open>s \<le> x\<close> \<open>x \<le> y\<close>] \<open>x \<notin> S\<close>
   25.73 +      by simp
   25.74 +    then have wit: "y \<in> S \<Longrightarrow> x \<ge> y" for y
   25.75 +      using le_cases by blast
   25.76 +    then have "bdd_above S"
   25.77 +      by (rule local.bdd_aboveI)
   25.78 +    note this wit
   25.79 +  } moreover {
   25.80 +    assume "x \<le> s"
   25.81 +    have "False" if "x \<ge> y" "y \<in> S" for y
   25.82 +      using connectedD_interval[OF conn \<open>y \<in> S\<close> \<open>s \<in> S\<close> \<open>x \<ge> y\<close> \<open>s \<ge> x\<close> ] \<open>x \<notin> S\<close>
   25.83 +      by simp
   25.84 +    then have wit: "y \<in> S \<Longrightarrow> x \<le> y" for y
   25.85 +      using le_cases by blast
   25.86 +    then have "bdd_below S"
   25.87 +      by (rule bdd_belowI)
   25.88 +    note this wit
   25.89 +  } ultimately show ?thesis
   25.90 +    by (meson le_cases that)
   25.91 +qed
   25.92 +
   25.93  lemma connected_continuous_image:
   25.94    assumes *: "continuous_on s f"
   25.95      and "connected s"
   25.96 @@ -3454,6 +3502,15 @@
   25.97  lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
   25.98    by (fact continuous_Pair)
   25.99  
  25.100 +lemma continuous_on_compose_Pair:
  25.101 +  assumes f: "continuous_on (Sigma A B) (\<lambda>(a, b). f a b)"
  25.102 +  assumes g: "continuous_on C g"
  25.103 +  assumes h: "continuous_on C h"
  25.104 +  assumes subset: "\<And>c. c \<in> C \<Longrightarrow> g c \<in> A" "\<And>c. c \<in> C \<Longrightarrow> h c \<in> B (g c)"
  25.105 +  shows "continuous_on C (\<lambda>c. f (g c) (h c))"
  25.106 +  using continuous_on_compose2[OF f continuous_on_Pair[OF g h]] subset
  25.107 +  by auto
  25.108 +
  25.109  
  25.110  subsubsection \<open>Connectedness of products\<close>
  25.111  
    26.1 --- a/src/HOL/Transcendental.thy	Tue Feb 20 22:25:23 2018 +0100
    26.2 +++ b/src/HOL/Transcendental.thy	Thu Feb 22 15:17:25 2018 +0100
    26.3 @@ -1389,6 +1389,8 @@
    26.4  declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
    26.5    and DERIV_exp[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
    26.6  
    26.7 +lemmas has_derivative_exp[derivative_intros] = DERIV_exp[THEN DERIV_compose_FDERIV]
    26.8 +
    26.9  lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
   26.10  proof -
   26.11    from summable_norm[OF summable_norm_exp, of x]
   26.12 @@ -1883,6 +1885,8 @@
   26.13  declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
   26.14    and DERIV_ln_divide[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
   26.15  
   26.16 +lemmas has_derivative_ln[derivative_intros] = DERIV_ln[THEN DERIV_compose_FDERIV]
   26.17 +
   26.18  lemma ln_series:
   26.19    assumes "0 < x" and "x < 2"
   26.20    shows "ln x = (\<Sum> n. (-1)^n * (1 / real (n + 1)) * (x - 1)^(Suc n))"
   26.21 @@ -3094,24 +3098,33 @@
   26.22    shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> a powr b) F"
   26.23    using tendsto_powr'[of f a F g b] assms by auto
   26.24  
   26.25 +lemma has_derivative_powr[derivative_intros]:
   26.26 +  assumes g[derivative_intros]: "(g has_derivative g') (at x within X)"
   26.27 +    and f[derivative_intros]:"(f has_derivative f') (at x within X)"
   26.28 +  assumes pos: "0 < g x" and "x \<in> X"
   26.29 +  shows "((\<lambda>x. g x powr f x::real) has_derivative (\<lambda>h. (g x powr f x) * (f' h * ln (g x) + g' h * f x / g x))) (at x within X)"
   26.30 +proof -
   26.31 +  have "\<forall>\<^sub>F x in at x within X. g x > 0"
   26.32 +    by (rule order_tendstoD[OF _ pos])
   26.33 +      (rule has_derivative_continuous[OF g, unfolded continuous_within])
   26.34 +  then obtain d where "d > 0" and pos': "\<And>x'. x' \<in> X \<Longrightarrow> dist x' x < d \<Longrightarrow> 0 < g x'"
   26.35 +    using pos unfolding eventually_at by force
   26.36 +  have "((\<lambda>x. exp (f x * ln (g x))) has_derivative
   26.37 +    (\<lambda>h. (g x powr f x) * (f' h * ln (g x) + g' h * f x / g x))) (at x within X)"
   26.38 +    using pos
   26.39 +    by (auto intro!: derivative_eq_intros simp: divide_simps powr_def)
   26.40 +  then show ?thesis
   26.41 +    by (rule has_derivative_transform_within[OF _ \<open>d > 0\<close> \<open>x \<in> X\<close>]) (auto simp: powr_def dest: pos')
   26.42 +qed
   26.43 +
   26.44  lemma DERIV_powr:
   26.45    fixes r :: real
   26.46    assumes g: "DERIV g x :> m"
   26.47      and pos: "g x > 0"
   26.48      and f: "DERIV f x :> r"
   26.49    shows "DERIV (\<lambda>x. g x powr f x) x :> (g x powr f x) * (r * ln (g x) + m * f x / g x)"
   26.50 -proof -
   26.51 -  have "DERIV (\<lambda>x. exp (f x * ln (g x))) x :> (g x powr f x) * (r * ln (g x) + m * f x / g x)"
   26.52 -    using pos
   26.53 -    by (auto intro!: derivative_eq_intros g pos f simp: powr_def field_simps exp_diff)
   26.54 -  then show ?thesis
   26.55 -  proof (rule DERIV_cong_ev[OF refl _ refl, THEN iffD1, rotated])
   26.56 -    from DERIV_isCont[OF g] pos have "\<forall>\<^sub>F x in at x. 0 < g x"
   26.57 -      unfolding isCont_def by (rule order_tendstoD(1))
   26.58 -    with pos show "\<forall>\<^sub>F x in nhds x. exp (f x * ln (g x)) = g x powr f x"
   26.59 -      by (auto simp: eventually_at_filter powr_def elim: eventually_mono)
   26.60 -  qed
   26.61 -qed
   26.62 +  using assms
   26.63 +  by (auto intro!: derivative_eq_intros ext simp: has_field_derivative_def algebra_simps)
   26.64  
   26.65  lemma DERIV_fun_powr:
   26.66    fixes r :: real
   26.67 @@ -3344,6 +3357,8 @@
   26.68  declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
   26.69    and DERIV_sin[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
   26.70  
   26.71 +lemmas has_derivative_sin[derivative_intros] = DERIV_sin[THEN DERIV_compose_FDERIV]
   26.72 +
   26.73  lemma DERIV_cos [simp]: "DERIV cos x :> - sin x"
   26.74    for x :: "'a::{real_normed_field,banach}"
   26.75    unfolding sin_def cos_def scaleR_conv_of_real
   26.76 @@ -3359,6 +3374,8 @@
   26.77  declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
   26.78    and DERIV_cos[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
   26.79  
   26.80 +lemmas has_derivative_cos[derivative_intros] = DERIV_cos[THEN DERIV_compose_FDERIV]
   26.81 +
   26.82  lemma isCont_sin: "isCont sin x"
   26.83    for x :: "'a::{real_normed_field,banach}"
   26.84    by (rule DERIV_sin [THEN DERIV_isCont])
   26.85 @@ -4598,6 +4615,8 @@
   26.86    unfolding tan_def
   26.87    by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
   26.88  
   26.89 +lemmas has_derivative_tan[derivative_intros] = DERIV_tan[THEN DERIV_compose_FDERIV]
   26.90 +
   26.91  lemma isCont_tan: "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
   26.92    for x :: "'a::{real_normed_field,banach}"
   26.93    by (rule DERIV_tan [THEN DERIV_isCont])
   26.94 @@ -5265,6 +5284,10 @@
   26.95    DERIV_arctan[THEN DERIV_chain2, derivative_intros]
   26.96    DERIV_arctan[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
   26.97  
   26.98 +lemmas has_derivative_arctan[derivative_intros] = DERIV_arctan[THEN DERIV_compose_FDERIV]
   26.99 +  and has_derivative_arccos[derivative_intros] = DERIV_arccos[THEN DERIV_compose_FDERIV]
  26.100 +  and has_derivative_arcsin[derivative_intros] = DERIV_arcsin[THEN DERIV_compose_FDERIV]
  26.101 +
  26.102  lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- (pi/2)))"
  26.103    by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
  26.104       (auto simp: arctan le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1