author paulson Mon, 26 Oct 2015 23:41:27 +0000 changeset 61518 ff12606337e9 parent 61515 c64628dbac00 child 61519 df57e4e3c0b7
new lemmas about topology, etc., for Cauchy integral formula
```--- a/src/HOL/Finite_Set.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -1545,6 +1545,10 @@
done

+lemma card_1_singletonE:
+    assumes "card A = 1" obtains x where "A = {x}"
+  using assms by (auto simp: card_Suc_eq)
+
lemma card_le_Suc_iff: "finite A \<Longrightarrow>
Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff```
```--- a/src/HOL/Library/Convex.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Library/Convex.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -96,7 +96,7 @@
lemma convex_halfspace_gt: "convex {x. inner a x > b}"
using convex_halfspace_lt[of "-a" "-b"] by auto

-lemma convex_real_interval:
+lemma convex_real_interval [iff]:
fixes a b :: "real"
shows "convex {a..}" and "convex {..b}"
and "convex {a<..}" and "convex {..<b}"```
```--- a/src/HOL/Library/Inner_Product.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Library/Inner_Product.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -81,6 +81,20 @@
lemma power2_norm_eq_inner: "(norm x)\<^sup>2 = inner x x"

+text \<open>Identities involving real multiplication and division.\<close>
+
+lemma inner_mult_left: "inner (of_real m * a) b = m * (inner a b)"
+  by (metis real_inner_class.inner_scaleR_left scaleR_conv_of_real)
+
+lemma inner_mult_right: "inner a (of_real m * b) = m * (inner a b)"
+  by (metis real_inner_class.inner_scaleR_right scaleR_conv_of_real)
+
+lemma inner_mult_left': "inner (a * of_real m) b = m * (inner a b)"
+
+lemma inner_mult_right': "inner a (b * of_real m) = (inner a b) * m"
+  by (simp add: of_real_def real_inner_class.inner_scaleR_right)
+
lemma Cauchy_Schwarz_ineq:
"(inner x y)\<^sup>2 \<le> inner x x * inner y y"
proof (cases)
@@ -141,6 +155,16 @@

end

+lemma inner_divide_left:
+  fixes a :: "'a :: {real_inner,real_div_algebra}"
+  shows "inner (a / of_real m) b = (inner a b) / m"
+  by (metis (no_types) divide_inverse inner_commute inner_scaleR_right mult.left_neutral mult.right_neutral mult_scaleR_right of_real_inverse scaleR_conv_of_real times_divide_eq_left)
+
+lemma inner_divide_right:
+  fixes a :: "'a :: {real_inner,real_div_algebra}"
+  shows "inner a (b / of_real m) = (inner a b) / m"
+  by (metis inner_commute inner_divide_left)
+
text \<open>
Re-enable constraints for @{term "open"},
@{term dist}, and @{term norm}.```
```--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -2484,7 +2484,7 @@
shows "convex hull {a,b,c} \<subseteq> s"
using s
apply (clarsimp simp add: convex_hull_insert [of "{b,c}" a] segment_convex_hull)
-      apply (meson subs convexD convex_segment ends_in_segment(1) ends_in_segment(2) subsetCE)
+      apply (meson subs convexD convex_closed_segment ends_in_segment(1) ends_in_segment(2) subsetCE)
done

lemma triangle_path_integrals_starlike_primitive:
@@ -3096,7 +3096,6 @@
using path_integral_nearby [OF assms, where Ends=False]
by simp_all

-  thm has_vector_derivative_polynomial_function
corollary differentiable_polynomial_function:
fixes p :: "real \<Rightarrow> 'a::euclidean_space"
shows "polynomial_function p \<Longrightarrow> p differentiable_on s"
@@ -3112,6 +3111,11 @@
shows "polynomial_function p \<Longrightarrow> valid_path p"
by (force simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_polymonial_function C1_differentiable_polynomial_function)

+lemma valid_path_subpath_trivial [simp]:
+    fixes g :: "real \<Rightarrow> 'a::euclidean_space"
+    shows "z \<noteq> g x \<Longrightarrow> valid_path (subpath x x g)"
+  by (simp add: subpath_def valid_path_polynomial_function)
+
lemma path_integral_bound_exists:
assumes s: "open s"
and g: "valid_path g"```
```--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -1083,7 +1083,7 @@
also have "... \<le> B * cmod (z - w) ^ n / (fact n) * cmod (w - z)"
apply (rule complex_differentiable_bound
[where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)"
-         and s = "closed_segment w z", OF convex_segment])
+         and s = "closed_segment w z", OF convex_closed_segment])
apply (auto simp: ends_in_segment real_of_nat_def DERIV_subset [OF sum_deriv wzs]
norm_divide norm_mult norm_power divide_le_cancel cmod_bound)
done
@@ -1096,7 +1096,7 @@

lemma complex_mvt_line:
assumes "\<And>u. u \<in> closed_segment w z \<Longrightarrow> (f has_field_derivative f'(u)) (at u)"
-    shows "\<exists>u. u \<in> open_segment w z \<and> Re(f z) - Re(f w) = Re(f'(u) * (z - w))"
+    shows "\<exists>u. u \<in> closed_segment w z \<and> Re(f z) - Re(f w) = Re(f'(u) * (z - w))"
proof -
have twz: "\<And>t. (1 - t) *\<^sub>R w + t *\<^sub>R z = w + t *\<^sub>R (z - w)"
@@ -1107,11 +1107,10 @@
"\<lambda>u. Re o (\<lambda>h. f'((1 - u) *\<^sub>R w + u *\<^sub>R z) * h) o (\<lambda>t. t *\<^sub>R (z - w))"])
apply auto
apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI)
-    apply (auto simp add: open_segment_def twz) []
-    apply (intro derivative_eq_intros has_derivative_at_within)
-    apply simp_all
+    apply (auto simp: closed_segment_def twz) []
+    apply (intro derivative_eq_intros has_derivative_at_within, simp_all)
-    apply (force simp add: twz closed_segment_def)
+    apply (force simp: twz closed_segment_def)
done
qed
```
```--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -464,7 +464,7 @@
"norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
show "convex (closed_segment 0 z)"
-    by (rule convex_segment [of 0 z])
+    by (rule convex_closed_segment [of 0 z])
next
fix k x
assume "x \<in> closed_segment 0 z" "k \<le> n"```
```--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -17,10 +17,10 @@
(* To be moved elsewhere                                                     *)
(* ------------------------------------------------------------------------- *)

-lemma linear_scaleR: "linear (\<lambda>x. scaleR c x)"
+lemma linear_scaleR  [simp]: "linear (\<lambda>x. scaleR c x)"

-lemma linear_scaleR_left: "linear (\<lambda>r. scaleR r x)"
+lemma linear_scaleR_left [simp]: "linear (\<lambda>r. scaleR r x)"

lemma injective_scaleR: "c \<noteq> 0 \<Longrightarrow> inj (\<lambda>x::'a::real_vector. scaleR c x)"
@@ -259,33 +259,62 @@
by blast
qed

-lemma closure_bounded_linear_image:
+lemma closure_bounded_linear_image_subset:
assumes f: "bounded_linear f"
shows "f ` closure S \<subseteq> closure (f ` S)"
using linear_continuous_on [OF f] closed_closure closure_subset
by (rule image_closure_subset)

-lemma closure_linear_image:
+lemma closure_linear_image_subset:
fixes f :: "'m::euclidean_space \<Rightarrow> 'n::real_normed_vector"
assumes "linear f"
-  shows "f ` (closure S) \<le> closure (f ` S)"
+  shows "f ` (closure S) \<subseteq> closure (f ` S)"
using assms unfolding linear_conv_bounded_linear
-  by (rule closure_bounded_linear_image)
+  by (rule closure_bounded_linear_image_subset)
+
+lemma closed_injective_linear_image:
+    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+    assumes S: "closed S" and f: "linear f" "inj f"
+    shows "closed (f ` S)"
+proof -
+  obtain g where g: "linear g" "g \<circ> f = id"
+    using linear_injective_left_inverse [OF f] by blast
+  then have confg: "continuous_on (range f) g"
+    using linear_continuous_on linear_conv_bounded_linear by blast
+  have [simp]: "g ` f ` S = S"
+    using g by (simp add: image_comp)
+  have cgf: "closed (g ` f ` S)"
+    by (simp add: `g \<circ> f = id` S image_comp)
+  have [simp]: "{x \<in> range f. g x \<in> S} = f ` S"
+    using g by (simp add: o_def id_def image_def) metis
+  show ?thesis
+    apply (rule closedin_closed_trans [of "range f"])
+    apply (rule continuous_closedin_preimage [OF confg cgf, simplified])
+    apply (rule closed_injective_image_subspace)
+    using f
+    apply (auto simp: linear_linear linear_injective_0)
+    done
+qed
+
+lemma closed_injective_linear_image_eq:
+    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+    assumes f: "linear f" "inj f"
+      shows "(closed(image f s) \<longleftrightarrow> closed s)"
+  by (metis closed_injective_linear_image closure_eq closure_linear_image_subset closure_subset_eq f(1) f(2) inj_image_subset_iff)

lemma closure_injective_linear_image:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'n::euclidean_space"
-  assumes "linear f" "inj f"
-  shows "f ` (closure S) = closure (f ` S)"
-proof -
-  obtain f' where f': "linear f' \<and> f \<circ> f' = id \<and> f' \<circ> f = id"
-    using assms linear_injective_isomorphism[of f] isomorphism_expand by auto
-  then have "f' ` closure (f ` S) \<le> closure (S)"
-    using closure_linear_image[of f' "f ` S"] image_comp[of f' f] by auto
-  then have "f ` f' ` closure (f ` S) \<le> f ` closure S" by auto
-  then have "closure (f ` S) \<le> f ` closure S"
-    using image_comp[of f f' "closure (f ` S)"] f' by auto
-  then show ?thesis using closure_linear_image[of f S] assms by auto
-qed
+    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+    shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)"
+  apply (rule subset_antisym)
+  by (simp add: closure_minimal closed_injective_linear_image closure_subset image_mono)
+
+lemma closure_bounded_linear_image:
+    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+    shows "\<lbrakk>linear f; bounded S\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)"
+  apply (rule subset_antisym, simp add: closure_linear_image_subset)
+  apply (rule closure_minimal, simp add: closure_subset image_mono)
+  by (meson bounded_closure closed_closure compact_continuous_image compact_eq_bounded_closed linear_continuous_on linear_conv_bounded_linear)

lemma closure_scaleR:
fixes S :: "'a::real_normed_vector set"
@@ -293,7 +322,7 @@
proof
show "(op *\<^sub>R c) ` (closure S) \<subseteq> closure ((op *\<^sub>R c) ` S)"
using bounded_linear_scaleR_right
-    by (rule closure_bounded_linear_image)
+    by (rule closure_bounded_linear_image_subset)
show "closure ((op *\<^sub>R c) ` S) \<subseteq> (op *\<^sub>R c) ` (closure S)"
by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure)
qed
@@ -1422,12 +1451,12 @@
then show ?thesis by (auto simp add: convex_def Ball_def)
qed

-lemma connected_ball:
+lemma connected_ball [iff]:
fixes x :: "'a::real_normed_vector"
shows "connected (ball x e)"
using convex_connected convex_ball by auto

-lemma connected_cball:
+lemma connected_cball [iff]:
fixes x :: "'a::real_normed_vector"
shows "connected (cball x e)"
using convex_connected convex_cball by auto
@@ -2212,140 +2241,6 @@
qed

-subsection \<open>Caratheodory's theorem.\<close>
-
-lemma convex_hull_caratheodory:
-  fixes p :: "('a::euclidean_space) set"
-  shows "convex hull p =
-    {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and>
-      (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
-  unfolding convex_hull_explicit set_eq_iff mem_Collect_eq
-proof (rule, rule)
-  fix y
-  let ?P = "\<lambda>n. \<exists>s u. finite s \<and> card s = n \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and>
-    setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
-  assume "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
-  then obtain N where "?P N" by auto
-  then have "\<exists>n\<le>N. (\<forall>k<n. \<not> ?P k) \<and> ?P n"
-    apply (rule_tac ex_least_nat_le)
-    apply auto
-    done
-  then obtain n where "?P n" and smallest: "\<forall>k<n. \<not> ?P k"
-    by blast
-  then obtain s u where obt: "finite s" "card s = n" "s\<subseteq>p" "\<forall>x\<in>s. 0 \<le> u x"
-    "setsum u s = 1"  "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto
-
-  have "card s \<le> DIM('a) + 1"
-  proof (rule ccontr, simp only: not_le)
-    assume "DIM('a) + 1 < card s"
-    then have "affine_dependent s"
-      using affine_dependent_biggerset[OF obt(1)] by auto
-    then obtain w v where wv: "setsum w s = 0" "v\<in>s" "w v \<noteq> 0" "(\<Sum>v\<in>s. w v *\<^sub>R v) = 0"
-      using affine_dependent_explicit_finite[OF obt(1)] by auto
-    def i \<equiv> "(\<lambda>v. (u v) / (- w v)) ` {v\<in>s. w v < 0}"
-    def t \<equiv> "Min i"
-    have "\<exists>x\<in>s. w x < 0"
-    proof (rule ccontr, simp add: not_less)
-      assume as:"\<forall>x\<in>s. 0 \<le> w x"
-      then have "setsum w (s - {v}) \<ge> 0"
-        apply (rule_tac setsum_nonneg)
-        apply auto
-        done
-      then have "setsum w s > 0"
-        unfolding setsum.remove[OF obt(1) \<open>v\<in>s\<close>]
-        using as[THEN bspec[where x=v]] and \<open>v\<in>s\<close>
-        using \<open>w v \<noteq> 0\<close>
-        by auto
-      then show False using wv(1) by auto
-    qed
-    then have "i \<noteq> {}" unfolding i_def by auto
-
-    then have "t \<ge> 0"
-      using Min_ge_iff[of i 0 ] and obt(1)
-      unfolding t_def i_def
-      using obt(4)[unfolded le_less]
-      by (auto simp: divide_le_0_iff)
-    have t: "\<forall>v\<in>s. u v + t * w v \<ge> 0"
-    proof
-      fix v
-      assume "v \<in> s"
-      then have v: "0 \<le> u v"
-        using obt(4)[THEN bspec[where x=v]] by auto
-      show "0 \<le> u v + t * w v"
-      proof (cases "w v < 0")
-        case False
-        thus ?thesis using v \<open>t\<ge>0\<close> by auto
-      next
-        case True
-        then have "t \<le> u v / (- w v)"
-          using \<open>v\<in>s\<close>
-          unfolding t_def i_def
-          apply (rule_tac Min_le)
-          using obt(1)
-          apply auto
-          done
-        then show ?thesis
-          using pos_le_divide_eq[OF True[unfolded neg_0_less_iff_less[symmetric]]]
-          by auto
-      qed
-    qed
-
-    obtain a where "a \<in> s" and "t = (\<lambda>v. (u v) / (- w v)) a" and "w a < 0"
-      using Min_in[OF _ \<open>i\<noteq>{}\<close>] and obt(1) unfolding i_def t_def by auto
-    then have a: "a \<in> s" "u a + t * w a = 0" by auto
-    have *: "\<And>f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)"
-      unfolding setsum.remove[OF obt(1) \<open>a\<in>s\<close>] by auto
-    have "(\<Sum>v\<in>s. u v + t * w v) = 1"
-      unfolding setsum.distrib wv(1) setsum_right_distrib[symmetric] obt(5) by auto
-    moreover have "(\<Sum>v\<in>s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y"
-      unfolding setsum.distrib obt(6) scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] wv(4)
-      using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]] by simp
-    ultimately have "?P (n - 1)"
-      apply (rule_tac x="(s - {a})" in exI)
-      apply (rule_tac x="\<lambda>v. u v + t * w v" in exI)
-      using obt(1-3) and t and a
-      apply (auto simp add: * scaleR_left_distrib)
-      done
-    then show False
-      using smallest[THEN spec[where x="n - 1"]] by auto
-  qed
-  then show "\<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and>
-      (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
-    using obt by auto
-qed auto
-
-lemma caratheodory:
-  "convex hull p =
-    {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
-      card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
-  unfolding set_eq_iff
-  apply rule
-  apply rule
-  unfolding mem_Collect_eq
-proof -
-  fix x
-  assume "x \<in> convex hull p"
-  then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
-    "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"
-    unfolding convex_hull_caratheodory by auto
-  then show "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s"
-    apply (rule_tac x=s in exI)
-    using hull_subset[of s convex]
-    using convex_convex_hull[unfolded convex_explicit, of s,
-      THEN spec[where x=s], THEN spec[where x=u]]
-    apply auto
-    done
-next
-  fix x
-  assume "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s"
-  then obtain s where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1" "x \<in> convex hull s"
-    by auto
-  then show "x \<in> convex hull p"
-    using hull_mono[OF \<open>s\<subseteq>p\<close>] by auto
-qed
-
-
subsection \<open>Some Properties of Affine Dependent Sets\<close>

lemma affine_independent_empty: "\<not> affine_dependent {}"
@@ -2572,7 +2467,8 @@

subsection \<open>Affine Dimension of a Set\<close>

-definition "aff_dim V =
+definition aff_dim :: "('a::euclidean_space) set \<Rightarrow> int"
+  where "aff_dim V =
(SOME d :: int.
\<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = d + 1)"

@@ -2782,6 +2678,9 @@
using aff_independent_finite[of B] card_gt_0_iff[of B] by auto
qed

+lemma aff_dim_empty_eq [simp]: "aff_dim ({}::'a::euclidean_space set) = -1"
+  by (simp add: aff_dim_empty [symmetric])
+
lemma aff_dim_affine_hull: "aff_dim (affine hull S) = aff_dim S"
unfolding aff_dim_def using hull_hull[of _ S] by auto

@@ -2829,6 +2728,13 @@
shows "of_nat (card B) = aff_dim B + 1"
using aff_dim_unique[of B B] assms by auto

+lemma affine_independent_iff_card:
+    fixes s :: "'a::euclidean_space set"
+    shows "~ affine_dependent s \<longleftrightarrow> finite s \<and> aff_dim s = int(card s) - 1"
+  apply (rule iffI)
+  apply (simp add: aff_dim_affine_independent aff_independent_finite)
+  by (metis affine_basis_exists [of s] aff_dim_unique card_subset_eq diff_add_cancel of_nat_eq_iff)
+
lemma aff_dim_sing:
fixes a :: "'n::euclidean_space"
shows "aff_dim {a} = 0"
@@ -3136,6 +3042,165 @@
shows "dim S < DIM ('n) \<Longrightarrow> interior S = {}"
by (metis low_dim_interior affine_hull_univ dim_affine_hull less_not_refl dim_UNIV)

+subsection \<open>Caratheodory's theorem.\<close>
+
+lemma convex_hull_caratheodory_aff_dim:
+  fixes p :: "('a::euclidean_space) set"
+  shows "convex hull p =
+    {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> aff_dim p + 1 \<and>
+      (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
+  unfolding convex_hull_explicit set_eq_iff mem_Collect_eq
+proof (intro allI iffI)
+  fix y
+  let ?P = "\<lambda>n. \<exists>s u. finite s \<and> card s = n \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and>
+    setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
+  assume "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
+  then obtain N where "?P N" by auto
+  then have "\<exists>n\<le>N. (\<forall>k<n. \<not> ?P k) \<and> ?P n"
+    apply (rule_tac ex_least_nat_le)
+    apply auto
+    done
+  then obtain n where "?P n" and smallest: "\<forall>k<n. \<not> ?P k"
+    by blast
+  then obtain s u where obt: "finite s" "card s = n" "s\<subseteq>p" "\<forall>x\<in>s. 0 \<le> u x"
+    "setsum u s = 1"  "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto
+
+  have "card s \<le> aff_dim p + 1"
+  proof (rule ccontr, simp only: not_le)
+    assume "aff_dim p + 1 < card s"
+    then have "affine_dependent s"
+      using affine_dependent_biggerset[OF obt(1)] independent_card_le_aff_dim not_less obt(3)
+      by blast
+    then obtain w v where wv: "setsum w s = 0" "v\<in>s" "w v \<noteq> 0" "(\<Sum>v\<in>s. w v *\<^sub>R v) = 0"
+      using affine_dependent_explicit_finite[OF obt(1)] by auto
+    def i \<equiv> "(\<lambda>v. (u v) / (- w v)) ` {v\<in>s. w v < 0}"
+    def t \<equiv> "Min i"
+    have "\<exists>x\<in>s. w x < 0"
+    proof (rule ccontr, simp add: not_less)
+      assume as:"\<forall>x\<in>s. 0 \<le> w x"
+      then have "setsum w (s - {v}) \<ge> 0"
+        apply (rule_tac setsum_nonneg)
+        apply auto
+        done
+      then have "setsum w s > 0"
+        unfolding setsum.remove[OF obt(1) \<open>v\<in>s\<close>]
+        using as[THEN bspec[where x=v]]  \<open>v\<in>s\<close>  \<open>w v \<noteq> 0\<close> by auto
+      then show False using wv(1) by auto
+    qed
+    then have "i \<noteq> {}" unfolding i_def by auto
+    then have "t \<ge> 0"
+      using Min_ge_iff[of i 0 ] and obt(1)
+      unfolding t_def i_def
+      using obt(4)[unfolded le_less]
+      by (auto simp: divide_le_0_iff)
+    have t: "\<forall>v\<in>s. u v + t * w v \<ge> 0"
+    proof
+      fix v
+      assume "v \<in> s"
+      then have v: "0 \<le> u v"
+        using obt(4)[THEN bspec[where x=v]] by auto
+      show "0 \<le> u v + t * w v"
+      proof (cases "w v < 0")
+        case False
+        thus ?thesis using v \<open>t\<ge>0\<close> by auto
+      next
+        case True
+        then have "t \<le> u v / (- w v)"
+          using \<open>v\<in>s\<close> unfolding t_def i_def
+          apply (rule_tac Min_le)
+          using obt(1) apply auto
+          done
+        then show ?thesis
+          using pos_le_divide_eq[OF True[unfolded neg_0_less_iff_less[symmetric]]]
+          by auto
+      qed
+    qed
+    obtain a where "a \<in> s" and "t = (\<lambda>v. (u v) / (- w v)) a" and "w a < 0"
+      using Min_in[OF _ \<open>i\<noteq>{}\<close>] and obt(1) unfolding i_def t_def by auto
+    then have a: "a \<in> s" "u a + t * w a = 0" by auto
+    have *: "\<And>f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)"
+      unfolding setsum.remove[OF obt(1) \<open>a\<in>s\<close>] by auto
+    have "(\<Sum>v\<in>s. u v + t * w v) = 1"
+      unfolding setsum.distrib wv(1) setsum_right_distrib[symmetric] obt(5) by auto
+    moreover have "(\<Sum>v\<in>s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y"
+      unfolding setsum.distrib obt(6) scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] wv(4)
+      using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]] by simp
+    ultimately have "?P (n - 1)"
+      apply (rule_tac x="(s - {a})" in exI)
+      apply (rule_tac x="\<lambda>v. u v + t * w v" in exI)
+      using obt(1-3) and t and a
+      apply (auto simp add: * scaleR_left_distrib)
+      done
+    then show False
+      using smallest[THEN spec[where x="n - 1"]] by auto
+  qed
+  then show "\<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> aff_dim p + 1 \<and>
+      (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
+    using obt by auto
+qed auto
+
+lemma caratheodory_aff_dim:
+  fixes p :: "('a::euclidean_space) set"
+  shows "convex hull p = {x. \<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> aff_dim p + 1 \<and> x \<in> convex hull s}"
+        (is "?lhs = ?rhs")
+proof
+  show "?lhs \<subseteq> ?rhs"
+    apply (subst convex_hull_caratheodory_aff_dim)
+    apply clarify
+    apply (rule_tac x="s" in exI)
+    apply (simp add: hull_subset convex_explicit [THEN iffD1, OF convex_convex_hull])
+    done
+next
+  show "?rhs \<subseteq> ?lhs"
+    using hull_mono by blast
+qed
+
+lemma convex_hull_caratheodory:
+  fixes p :: "('a::euclidean_space) set"
+  shows "convex hull p =
+            {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and>
+              (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
+        (is "?lhs = ?rhs")
+proof (intro set_eqI iffI)
+  fix x
+  assume "x \<in> ?lhs" then show "x \<in> ?rhs"
+    apply (simp only: convex_hull_caratheodory_aff_dim Set.mem_Collect_eq)
+    apply (erule ex_forward)+
+    using aff_dim_subset_univ [of p]
+    apply simp
+    done
+next
+  fix x
+  assume "x \<in> ?rhs" then show "x \<in> ?lhs"
+    by (auto simp add: convex_hull_explicit)
+qed
+
+theorem caratheodory:
+  "convex hull p =
+    {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
+      card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
+proof safe
+  fix x
+  assume "x \<in> convex hull p"
+  then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
+    "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"
+    unfolding convex_hull_caratheodory by auto
+  then show "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s"
+    apply (rule_tac x=s in exI)
+    using hull_subset[of s convex]
+    using convex_convex_hull[unfolded convex_explicit, of s,
+      THEN spec[where x=s], THEN spec[where x=u]]
+    apply auto
+    done
+next
+  fix x s
+  assume  "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1" "x \<in> convex hull s"
+  then show "x \<in> convex hull p"
+    using hull_mono[OF \<open>s\<subseteq>p\<close>] by auto
+qed
+
+
subsection \<open>Relative interior of a set\<close>

definition "rel_interior S =
@@ -5708,20 +5773,33 @@
shows "is_interval s \<longleftrightarrow> convex s"
by (metis is_interval_convex convex_connected is_interval_connected_1)

-lemma convex_connected_1:
+lemma connected_convex_1:
fixes s :: "real set"
shows "connected s \<longleftrightarrow> convex s"
by (metis is_interval_convex convex_connected is_interval_connected_1)

+lemma connected_convex_1_gen:
+  fixes s :: "'a :: euclidean_space set"
+  assumes "DIM('a) = 1"
+  shows "connected s \<longleftrightarrow> convex s"
+proof -
+  obtain f:: "'a \<Rightarrow> real" where linf: "linear f" and "inj f"
+    using subspace_isomorphism [where 'a = 'a and 'b = real]
+    by (metis DIM_real dim_UNIV subspace_UNIV assms)
+  then have "f -` (f ` s) = s"
+  then show ?thesis
+    by (metis connected_convex_1 convex_linear_vimage linf convex_connected connected_linear_image)
+qed

subsection \<open>Another intermediate value theorem formulation\<close>

lemma ivt_increasing_component_on_1:
-  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
assumes "a \<le> b"
-    and "continuous_on (cbox a b) f"
+    and "continuous_on {a..b} f"
and "(f a)\<bullet>k \<le> y" "y \<le> (f b)\<bullet>k"
-  shows "\<exists>x\<in>cbox a b. (f x)\<bullet>k = y"
+  shows "\<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
proof -
have "f a \<in> f ` cbox a b" "f b \<in> f ` cbox a b"
apply (rule_tac[!] imageI)
@@ -5730,24 +5808,22 @@
done
then show ?thesis
using connected_ivt_component[of "f ` cbox a b" "f a" "f b" k y]
-    using connected_continuous_image[OF assms(2) convex_connected[OF convex_box(1)]]
-    using assms
-    by auto
+    by (simp add: Topology_Euclidean_Space.connected_continuous_image assms)
qed

lemma ivt_increasing_component_1:
fixes f :: "real \<Rightarrow> 'a::euclidean_space"
-  shows "a \<le> b \<Longrightarrow> \<forall>x\<in>cbox a b. continuous (at x) f \<Longrightarrow>
-    f a\<bullet>k \<le> y \<Longrightarrow> y \<le> f b\<bullet>k \<Longrightarrow> \<exists>x\<in>cbox a b. (f x)\<bullet>k = y"
+  shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a..b}. continuous (at x) f \<Longrightarrow>
+    f a\<bullet>k \<le> y \<Longrightarrow> y \<le> f b\<bullet>k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
by (rule ivt_increasing_component_on_1) (auto simp add: continuous_at_imp_continuous_on)

lemma ivt_decreasing_component_on_1:
fixes f :: "real \<Rightarrow> 'a::euclidean_space"
assumes "a \<le> b"
-    and "continuous_on (cbox a b) f"
+    and "continuous_on {a..b} f"
and "(f b)\<bullet>k \<le> y"
and "y \<le> (f a)\<bullet>k"
-  shows "\<exists>x\<in>cbox a b. (f x)\<bullet>k = y"
+  shows "\<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
apply (subst neg_equal_iff_equal[symmetric])
using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"]
using assms using continuous_on_minus
@@ -5756,8 +5832,8 @@

lemma ivt_decreasing_component_1:
fixes f :: "real \<Rightarrow> 'a::euclidean_space"
-  shows "a \<le> b \<Longrightarrow> \<forall>x\<in>cbox a b. continuous (at x) f \<Longrightarrow>
-    f b\<bullet>k \<le> y \<Longrightarrow> y \<le> f a\<bullet>k \<Longrightarrow> \<exists>x\<in>cbox a b. (f x)\<bullet>k = y"
+  shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a..b}. continuous (at x) f \<Longrightarrow>
+    f b\<bullet>k \<le> y \<Longrightarrow> y \<le> f a\<bullet>k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
by (rule ivt_decreasing_component_on_1) (auto simp: continuous_at_imp_continuous_on)

@@ -6234,12 +6310,12 @@
definition midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"

-definition open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
-  where "open_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real.  0 < u \<and> u < 1}"
-
definition closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"

+definition open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
+  "open_segment a b \<equiv> closed_segment a b - {a,b}"
+
definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"

lemmas segment = open_segment_def closed_segment_def
@@ -6291,7 +6367,7 @@
done
show ?t3
-    unfolding midpoint_def dist_norm
+    unfolding midpoint_def dist_norm
apply (rule *)
@@ -6325,37 +6401,28 @@
"closed_segment a b = convex hull {a,b}"
proof -
have *: "\<And>x. {x} \<noteq> {}" by auto
-  have **: "\<And>u v. u + v = 1 \<longleftrightarrow> u = 1 - (v::real)" by auto
show ?thesis
unfolding segment convex_hull_insert[OF *] convex_hull_singleton
-    apply (rule set_eqI)
-    unfolding mem_Collect_eq
-    apply (rule, erule exE)
-    apply (rule_tac x="1 - u" in exI)
-    apply rule
-    defer
-    apply (rule_tac x=u in exI)
-    defer
-    apply (elim exE conjE)
-    apply (rule_tac x="1 - u" in exI)
-    unfolding **
-    apply auto
-    done
-qed
-
-lemma convex_segment [iff]: "convex (closed_segment a b)"
-  unfolding segment_convex_hull by(rule convex_convex_hull)
-
-lemma connected_segment [iff]:
-  fixes x :: "'a :: real_normed_vector"
-  shows "connected (closed_segment x y)"
+    by (safe; rule_tac x="1 - u" in exI; force)
+qed
+
+lemma segment_open_subset_closed:
+   "open_segment a b \<subseteq> closed_segment a b"
+  by (auto simp: closed_segment_def open_segment_def)
+
+lemma bounded_closed_segment:
+    fixes a :: "'a::euclidean_space" shows "bounded (closed_segment a b)"
+  by (simp add: segment_convex_hull compact_convex_hull compact_imp_bounded)
+
+lemma bounded_open_segment:
+    fixes a :: "'a::euclidean_space" shows "bounded (open_segment a b)"
+  by (rule bounded_subset [OF bounded_closed_segment segment_open_subset_closed])
+
+lemmas bounded_segment = bounded_closed_segment open_closed_segment

lemma ends_in_segment [iff]: "a \<in> closed_segment a b" "b \<in> closed_segment a b"
unfolding segment_convex_hull
-  apply (rule_tac[!] hull_subset[unfolded subset_eq, rule_format])
-  apply auto
-  done
+  by (auto intro!: hull_subset[unfolded subset_eq, rule_format])

lemma segment_furthest_le:
fixes a b x y :: "'a::euclidean_space"
@@ -6403,6 +6470,106 @@
fixes u::real shows "closed_segment u v = (\<lambda>x. (v - u) * x + u) ` {0..1}"

+subsubsection\<open>More lemmas, especially for working with the underlying formula\<close>
+
+lemma segment_eq_compose:
+  fixes a :: "'a :: real_vector"
+  shows "(\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) = (\<lambda>x. a + x) o (\<lambda>u. u *\<^sub>R (b - a))"
+    by (simp add: o_def algebra_simps)
+
+lemma segment_degen_1:
+  fixes a :: "'a :: real_vector"
+  shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = b \<longleftrightarrow> a=b \<or> u=1"
+proof -
+  { assume "(1 - u) *\<^sub>R a + u *\<^sub>R b = b"
+    then have "(1 - u) *\<^sub>R a = (1 - u) *\<^sub>R b"
+    then have "a=b \<or> u=1"
+      by simp
+  } then show ?thesis
+      by (auto simp: algebra_simps)
+qed
+
+lemma segment_degen_0:
+    fixes a :: "'a :: real_vector"
+    shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = a \<longleftrightarrow> a=b \<or> u=0"
+  using segment_degen_1 [of "1-u" b a]
+  by (auto simp: algebra_simps)
+
+lemma closed_segment_image_interval:
+     "closed_segment a b = (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}"
+  by (auto simp: set_eq_iff image_iff closed_segment_def)
+
+lemma open_segment_image_interval:
+     "open_segment a b = (if a=b then {} else (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1})"
+  by (auto simp:  open_segment_def closed_segment_def segment_degen_0 segment_degen_1)
+
+lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval
+
+lemma closure_closed_segment [simp]:
+    fixes a :: "'a::euclidean_space"
+    shows "closure(closed_segment a b) = closed_segment a b"
+  by (simp add: closure_eq compact_imp_closed segment_convex_hull compact_convex_hull)
+
+lemma closure_open_segment [simp]:
+    fixes a :: "'a::euclidean_space"
+    shows "closure(open_segment a b) = (if a = b then {} else closed_segment a b)"
+proof -
+  have "closure ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1}) = (\<lambda>u. u *\<^sub>R (b - a)) ` closure {0<..<1}" if "a \<noteq> b"
+    apply (rule closure_injective_linear_image [symmetric])
+    using that by (simp add: inj_on_def)
+  then show ?thesis
+    by (simp add: segment_image_interval segment_eq_compose closure_greaterThanLessThan [symmetric]
+         closure_translation image_comp [symmetric] del: closure_greaterThanLessThan)
+qed
+
+lemma closed_segment [simp]:
+    fixes a :: "'a::euclidean_space"  shows "closed (closed_segment a b)"
+  using closure_subset_eq by fastforce
+
+lemma closed_open_segment_iff [simp]:
+    fixes a :: "'a::euclidean_space"  shows "closed(open_segment a b) \<longleftrightarrow> a = b"
+  by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2))
+
+lemma compact_segment [simp]:
+    fixes a :: "'a::euclidean_space"  shows "compact (closed_segment a b)"
+  by (simp add: compact_convex_hull segment_convex_hull)
+
+lemma compact_open_segment_iff [simp]:
+    fixes a :: "'a::euclidean_space"  shows "compact(open_segment a b) \<longleftrightarrow> a = b"
+  by (simp add: bounded_open_segment compact_eq_bounded_closed)
+
+lemma convex_closed_segment [iff]: "convex (closed_segment a b)"
+  unfolding segment_convex_hull by(rule convex_convex_hull)
+
+lemma convex_open_segment [iff]: "convex(open_segment a b)"
+proof -
+  have "convex ((\<lambda>u. u *\<^sub>R (b-a)) ` {0<..<1})"
+    by (rule convex_linear_image) auto
+  then show ?thesis
+    apply (simp add: open_segment_image_interval segment_eq_compose)
+    by (metis image_comp convex_translation)
+qed
+
+lemmas convex_segment = convex_closed_segment convex_open_segment
+
+lemma connected_segment [iff]:
+  fixes x :: "'a :: real_normed_vector"
+  shows "connected (closed_segment x y)"
+
+lemma affine_hull_closed_segment [simp]:
+     "affine hull (closed_segment a b) = affine hull {a,b}"
+
+lemma affine_hull_open_segment [simp]:
+    fixes a :: "'a::euclidean_space"
+    shows "affine hull (open_segment a b) = (if a = b then {} else affine hull {a,b})"
+by (metis affine_hull_convex_hull affine_hull_empty closure_open_segment closure_same_affine_hull segment_convex_hull)
+
+subsubsection\<open>Betweenness\<close>
+
lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
unfolding between_def by auto

@@ -6411,7 +6578,7 @@
case True
then show ?thesis
unfolding between_def split_conv
-    by (auto simp add:segment_refl dist_commute)
+    by (auto simp add: dist_commute)
next
case False
then have Fal: "norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0"
@@ -7958,7 +8125,7 @@
also have "\<dots> = f ` (closure (rel_interior S))"
using convex_closure_rel_interior assms by auto
also have "\<dots> \<subseteq> closure (f ` (rel_interior S))"
-    using closure_linear_image assms by auto
+    using closure_linear_image_subset assms by auto
finally have "closure (f ` S) = closure (f ` rel_interior S)"
using closure_mono[of "f ` S" "closure (f ` rel_interior S)"] closure_closure
closure_mono[of "f ` rel_interior S" "f ` S"] *
@@ -8556,7 +8723,7 @@
fixes S T :: "'a::real_normed_vector set"
shows "closure S + closure T \<subseteq> closure (S + T)"
unfolding set_plus_image closure_Times [symmetric] split_def
bounded_linear_fst bounded_linear_snd)

lemma rel_interior_sum:
@@ -8929,11 +9096,11 @@

lemma interior_atLeastLessThan [simp]:
fixes a::real shows "interior {a..<b} = {a<..<b}"
-  by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost interior_inter interior_interior interior_real_semiline)
+  by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost interior_Int interior_interior interior_real_semiline)

lemma interior_lessThanAtMost [simp]:
fixes a::real shows "interior {a<..b} = {a<..<b}"
-  by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost interior_inter
+  by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost interior_Int
interior_interior interior_real_semiline)

lemma at_within_closed_interval:```
```--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -24,9 +24,6 @@
by (rule netlimit_within [of a UNIV])
qed simp

-(* Because I do not want to type this all the time *)
-lemmas linear_linear = linear_conv_bounded_linear[symmetric]
-
declare has_derivative_bounded_linear[dest]

subsection \<open>Derivatives\<close>```
```--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -1211,7 +1211,7 @@
apply (rule arg_cong[of _ _ interior])
using p(8) uv by auto
also have "\<dots> = {}"
-      unfolding interior_inter
+      unfolding interior_Int
apply (rule inter_interior_unions_intervals)
using p(6) p(7)[OF p(2)] p(3)
apply auto
@@ -4872,7 +4872,7 @@
"cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
have "(cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<inter> (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<subseteq> cbox m n \<inter> cbox u v"
by blast
-          note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "cbox m n"]]
+          note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_Int[of "cbox m n"]]
then have "interior (cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = {}"
unfolding as Int_absorb by auto
then show "content (cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0"
@@ -7341,7 +7341,7 @@
guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = "min v v'"
have "box a ?v \<subseteq> k \<inter> k'"
unfolding v v' by (auto simp add: mem_box)
-              note interior_mono[OF this,unfolded interior_inter]
+              note interior_mono[OF this,unfolded interior_Int]
moreover have "(a + ?v)/2 \<in> box a ?v"
using k(3-)
unfolding v v' content_eq_0 not_le
@@ -7372,7 +7372,7 @@
let ?v = "max v v'"
have "box ?v b \<subseteq> k \<inter> k'"
unfolding v v' by (auto simp: mem_box)
-                note interior_mono[OF this,unfolded interior_inter]
+                note interior_mono[OF this,unfolded interior_Int]
moreover have " ((b + ?v)/2) \<in> box ?v b"
using k(3-) unfolding v v' content_eq_0 not_le by (auto simp: mem_box)
ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'"
@@ -8014,7 +8014,7 @@
apply (rule assms(1)[unfolded connected_clopen,rule_format])
apply rule
defer
-    apply (rule continuous_closed_in_preimage[OF assms(4) closed_singleton])
+    apply (rule continuous_closedin_preimage[OF assms(4) closed_singleton])
apply (rule open_openin_trans[OF assms(2)])
unfolding open_contains_ball
proof safe
@@ -9427,7 +9427,7 @@
note kl = tagged_division_ofD(3,4)[OF qq[THEN conjunct1]]
from this(2)[OF as(4,1)] guess u v by (elim exE) note uv=this
have *: "interior (k \<inter> l) = {}"
-      unfolding interior_inter
+      unfolding interior_Int
apply (rule q')
using as
unfolding r_def
@@ -10771,7 +10771,7 @@
proof goal_cases
case prems: (1 l y)
have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
-              apply (subst(2) interior_inter)
+              apply (subst(2) interior_Int)
apply (rule Int_greatest)
defer
apply (subst prems(4))
@@ -10960,7 +10960,7 @@
from d'(4)[OF this(1)] d'(4)[OF this(2)]
guess u1 v1 u2 v2 by (elim exE) note uv=this
have "{} = interior ((k \<inter> y) \<inter> cbox u v)"
-              apply (subst interior_inter)
+              apply (subst interior_Int)
using d'(5)[OF prems(1-3)]
apply auto
done```
```--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -1507,6 +1507,8 @@
show "linear f" ..
qed

+lemmas linear_linear = linear_conv_bounded_linear[symmetric]
+
lemma linear_bounded_pos:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes lf: "linear f"```
```--- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -7,6 +7,7 @@
Complex_Analysis_Basics
Bounded_Continuous_Function
Weierstrass
+  Cauchy_Integral_Thm
begin

end```
```--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -576,7 +576,7 @@
by (rule ext) (auto simp: mult.commute)

-subsection\<open>Choosing a subpath of an existing path\<close>
+section\<open>Choosing a subpath of an existing path\<close>

definition subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector"
where "subpath a b g \<equiv> \<lambda>x. g((b - a) * x + a)"
@@ -747,6 +747,121 @@
lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p"
by (rule ext) (simp add: joinpaths_def subpath_def divide_simps)

+subsection\<open>There is a subpath to the frontier\<close>
+
+lemma subpath_to_frontier_explicit:
+    fixes S :: "'a::metric_space set"
+    assumes g: "path g" and "pathfinish g \<notin> S"
+    obtains u where "0 \<le> u" "u \<le> 1"
+                "\<And>x. 0 \<le> x \<and> x < u \<Longrightarrow> g x \<in> interior S"
+                "(g u \<notin> interior S)" "(u = 0 \<or> g u \<in> closure S)"
+proof -
+  have gcon: "continuous_on {0..1} g"     using g by (simp add: path_def)
+  then have com: "compact ({0..1} \<inter> {u. g u \<in> closure (- S)})"
+    apply (simp add: Int_commute [of "{0..1}"] compact_eq_bounded_closed closed_vimage_Int [unfolded vimage_def])
+    using compact_eq_bounded_closed apply fastforce
+    done
+  have "1 \<in> {u. g u \<in> closure (- S)}"
+    using assms by (simp add: pathfinish_def closure_def)
+  then have dis: "{0..1} \<inter> {u. g u \<in> closure (- S)} \<noteq> {}"
+    using atLeastAtMost_iff zero_le_one by blast
+  then obtain u where "0 \<le> u" "u \<le> 1" and gu: "g u \<in> closure (- S)"
+                  and umin: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1; g t \<in> closure (- S)\<rbrakk> \<Longrightarrow> u \<le> t"
+    using compact_attains_inf [OF com dis] by fastforce
+  then have umin': "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1; t < u\<rbrakk> \<Longrightarrow>  g t \<in> S"
+    using closure_def by fastforce
+  { assume "u \<noteq> 0"
+    then have "u > 0" using `0 \<le> u` by auto
+    { fix e::real assume "e > 0"
+      obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {0..1}; dist x' u < d\<rbrakk> \<Longrightarrow> dist (g x') (g u) < e"
+        using continuous_onD [OF gcon _ `e > 0`] `0 \<le> _` `_ \<le> 1` atLeastAtMost_iff by auto
+      have *: "dist (max 0 (u - d / 2)) u < d"
+        using `0 \<le> u` `u \<le> 1` `d > 0` by (simp add: dist_real_def)
+      have "\<exists>y\<in>S. dist y (g u) < e"
+        using `0 < u` `u \<le> 1` `d > 0`
+        by (force intro: d [OF _ *] umin')
+    }
+    then have "g u \<in> closure S"
+      by (simp add: frontier_def closure_approachable)
+  }
+  then show ?thesis
+    apply (rule_tac u=u in that)
+    apply (auto simp: `0 \<le> u` `u \<le> 1` gu interior_closure umin)
+    using `_ \<le> 1` interior_closure umin apply fastforce
+    done
+qed
+
+lemma subpath_to_frontier_strong:
+    assumes g: "path g" and "pathfinish g \<notin> S"
+    obtains u where "0 \<le> u" "u \<le> 1" "g u \<notin> interior S"
+                    "u = 0 \<or> (\<forall>x. 0 \<le> x \<and> x < 1 \<longrightarrow> subpath 0 u g x \<in> interior S)  \<and>  g u \<in> closure S"
+proof -
+  obtain u where "0 \<le> u" "u \<le> 1"
+             and gxin: "\<And>x. 0 \<le> x \<and> x < u \<Longrightarrow> g x \<in> interior S"
+             and gunot: "(g u \<notin> interior S)" and u0: "(u = 0 \<or> g u \<in> closure S)"
+    using subpath_to_frontier_explicit [OF assms] by blast
+  show ?thesis
+    apply (rule that [OF `0 \<le> u` `u \<le> 1`])
+    using `0 \<le> u` u0 by (force simp: subpath_def gxin)
+qed
+
+lemma subpath_to_frontier:
+    assumes g: "path g" and g0: "pathstart g \<in> closure S" and g1: "pathfinish g \<notin> S"
+    obtains u where "0 \<le> u" "u \<le> 1" "g u \<in> frontier S" "(path_image(subpath 0 u g) - {g u}) \<subseteq> interior S"
+proof -
+  obtain u where "0 \<le> u" "u \<le> 1"
+             and notin: "g u \<notin> interior S"
+             and disj: "u = 0 \<or>
+                        (\<forall>x. 0 \<le> x \<and> x < 1 \<longrightarrow> subpath 0 u g x \<in> interior S) \<and> g u \<in> closure S"
+    using subpath_to_frontier_strong [OF g g1] by blast
+  show ?thesis
+    apply (rule that [OF `0 \<le> u` `u \<le> 1`])
+    apply (metis DiffI disj frontier_def g0 notin pathstart_def)
+    using `0 \<le> u` g0 disj
+    apply (auto simp: closed_segment_eq_real_ivl pathstart_def pathfinish_def subpath_def)
+    apply (rename_tac y)
+    apply (drule_tac x="y/u" in spec)
+    apply (auto split: split_if_asm)
+    done
+qed
+
+lemma exists_path_subpath_to_frontier:
+    fixes S :: "'a::real_normed_vector set"
+    assumes "path g" "pathstart g \<in> closure S" "pathfinish g \<notin> S"
+    obtains h where "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g"
+                    "path_image h - {pathfinish h} \<subseteq> interior S"
+                    "pathfinish h \<in> frontier S"
+proof -
+  obtain u where u: "0 \<le> u" "u \<le> 1" "g u \<in> frontier S" "(path_image(subpath 0 u g) - {g u}) \<subseteq> interior S"
+    using subpath_to_frontier [OF assms] by blast
+  show ?thesis
+    apply (rule that [of "subpath 0 u g"])
+    using assms u
+    apply simp_all
+    apply (force simp: closed_segment_eq_real_ivl path_image_def)
+    done
+qed
+
+lemma exists_path_subpath_to_frontier_closed:
+    fixes S :: "'a::real_normed_vector set"
+    assumes S: "closed S" and g: "path g" and g0: "pathstart g \<in> S" and g1: "pathfinish g \<notin> S"
+    obtains h where "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g \<inter> S"
+                    "pathfinish h \<in> frontier S"
+proof -
+  obtain h where h: "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g"
+                    "path_image h - {pathfinish h} \<subseteq> interior S"
+                    "pathfinish h \<in> frontier S"
+    using exists_path_subpath_to_frontier [OF g _ g1] closure_closed [OF S] g0 by auto
+  show ?thesis
+    apply (rule that [OF `path h`])
+    using assms h
+    apply auto
+    apply (metis diff_single_insert frontier_subset_eq insert_iff interior_subset subset_iff)
+    done
+qed

subsection \<open>Reparametrizing a closed curve to start at some chosen point\<close>

@@ -937,7 +1052,7 @@
qed

-subsection \<open>Path component, considered as a "joinability" relation (from Tom Hales)\<close>
+section \<open>Path component, considered as a "joinability" relation (from Tom Hales)\<close>

definition "path_component s x y \<longleftrightarrow>
(\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"
@@ -1079,8 +1194,8 @@
ultimately show False
using *[unfolded connected_local not_ex, rule_format,
of "{x\<in>{0..1}. g x \<in> e1}" "{x\<in>{0..1}. g x \<in> e2}"]
-    using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(1)]
-    using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(2)]
+    using continuous_openin_preimage[OF g(1)[unfolded path_def] as(1)]
+    using continuous_openin_preimage[OF g(1)[unfolded path_def] as(2)]
by auto
qed

@@ -1199,6 +1314,16 @@
done
qed

+lemma path_connected_segment:
+    fixes a :: "'a::real_normed_vector"
+    shows "path_connected (closed_segment a b)"
+
+lemma path_connected_open_segment:
+    fixes a :: "'a::real_normed_vector"
+    shows "path_connected (open_segment a b)"
+
lemma homeomorphic_path_connectedness:
"s homeomorphic t \<Longrightarrow> path_connected s \<longleftrightarrow> path_connected t"
unfolding homeomorphic_def homeomorphism_def
@@ -1667,7 +1792,7 @@
by (meson cobounded_unique_unbounded_components connected_eq_connected_components_eq)

-subsection\<open>The "inside" and "outside" of a set\<close>
+section\<open>The "inside" and "outside" of a set\<close>

text\<open>The inside comprises the points in a bounded connected component of the set's complement.
The outside comprises the points in unbounded connected component of the complement.\<close>
@@ -1994,6 +2119,14 @@
by (metis Diff_subset assms convex_closure frontier_def outside_frontier_misses_closure
outside_subset_convex subset_antisym)

+lemma inside_frontier_eq_interior:
+     fixes s :: "'a :: {real_normed_vector, perfect_space} set"
+     shows "\<lbrakk>bounded s; convex s\<rbrakk> \<Longrightarrow> inside(frontier s) = interior s"
+  apply (simp add: inside_outside outside_frontier_eq_complement_closure)
+  using closure_subset interior_subset
+  apply (auto simp add: frontier_def)
+  done
+
lemma open_inside:
fixes s :: "'a::real_normed_vector set"
assumes "closed s"
@@ -2055,4 +2188,271 @@
by (simp add: frontier_def open_inside interior_open)
qed

+lemma closure_outside_subset:
+    fixes s :: "'a::real_normed_vector set"
+    assumes "closed s"
+      shows "closure(outside s) \<subseteq> s \<union> outside s"
+  apply (rule closure_minimal, simp)
+  by (metis assms closed_open inside_outside open_inside)
+
+lemma frontier_outside_subset:
+    fixes s :: "'a::real_normed_vector set"
+    assumes "closed s"
+      shows "frontier(outside s) \<subseteq> s"
+  apply (simp add: frontier_def open_outside interior_open)
+  by (metis Diff_subset_conv assms closure_outside_subset interior_eq open_outside sup.commute)
+
+lemma inside_complement_unbounded_connected_empty:
+     "\<lbrakk>connected (- s); \<not> bounded (- s)\<rbrakk> \<Longrightarrow> inside s = {}"
+  by (meson Compl_iff bounded_subset connected_component_maximal order_refl)
+
+lemma inside_bounded_complement_connected_empty:
+    fixes s :: "'a::{real_normed_vector, perfect_space} set"
+    shows "\<lbrakk>connected (- s); bounded s\<rbrakk> \<Longrightarrow> inside s = {}"
+  by (metis inside_complement_unbounded_connected_empty cobounded_imp_unbounded)
+
+lemma inside_inside:
+    assumes "s \<subseteq> inside t"
+    shows "inside s - t \<subseteq> inside t"
+unfolding inside_def
+proof clarify
+  fix x
+  assume x: "x \<notin> t" "x \<notin> s" and bo: "bounded (connected_component_set (- s) x)"
+  show "bounded (connected_component_set (- t) x)"
+  proof (cases "s \<inter> connected_component_set (- t) x = {}")
+    case True show ?thesis
+      apply (rule bounded_subset [OF bo])
+      apply (rule connected_component_maximal)
+      using x True apply auto
+      done
+  next
+    case False then show ?thesis
+      using assms [unfolded inside_def] x
+      apply (simp add: disjoint_iff_not_equal, clarify)
+      apply (drule subsetD, assumption, auto)
+      by (metis (no_types, hide_lams) ComplI connected_component_eq_eq)
+  qed
+qed
+
+lemma inside_inside_subset: "inside(inside s) \<subseteq> s"
+  using inside_inside union_with_outside by fastforce
+
+lemma inside_outside_intersect_connected:
+      "\<lbrakk>connected t; inside s \<inter> t \<noteq> {}; outside s \<inter> t \<noteq> {}\<rbrakk> \<Longrightarrow> s \<inter> t \<noteq> {}"
+  apply (simp add: inside_def outside_def ex_in_conv [symmetric] disjoint_eq_subset_Compl, clarify)
+  by (metis (no_types, hide_lams) Compl_anti_mono connected_component_eq connected_component_maximal contra_subsetD double_compl)
+
+lemma outside_bounded_nonempty:
+  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
+    assumes "bounded s" shows "outside s \<noteq> {}"
+  by (metis (no_types, lifting) Collect_empty_eq Collect_mem_eq Compl_eq_Diff_UNIV Diff_cancel
+                   Diff_disjoint UNIV_I assms ball_eq_empty bounded_diff cobounded_outside convex_ball
+                   double_complement order_refl outside_convex outside_def)
+
+lemma outside_compact_in_open:
+    fixes s :: "'a :: {real_normed_vector,perfect_space} set"
+    assumes s: "compact s" and t: "open t" and "s \<subseteq> t" "t \<noteq> {}"
+      shows "outside s \<inter> t \<noteq> {}"
+proof -
+  have "outside s \<noteq> {}"
+    by (simp add: compact_imp_bounded outside_bounded_nonempty s)
+  with assms obtain a b where a: "a \<in> outside s" and b: "b \<in> t" by auto
+  show ?thesis
+  proof (cases "a \<in> t")
+    case True with a show ?thesis by blast
+  next
+    case False
+      have front: "frontier t \<subseteq> - s"
+        using `s \<subseteq> t` frontier_disjoint_eq t by auto
+      { fix \<gamma>
+        assume "path \<gamma>" and pimg_sbs: "path_image \<gamma> - {pathfinish \<gamma>} \<subseteq> interior (- t)"
+           and pf: "pathfinish \<gamma> \<in> frontier t" and ps: "pathstart \<gamma> = a"
+        def c \<equiv> "pathfinish \<gamma>"
+        have "c \<in> -s" unfolding c_def using front pf by blast
+        moreover have "open (-s)" using s compact_imp_closed by blast
+        ultimately obtain \<epsilon>::real where "\<epsilon> > 0" and \<epsilon>: "cball c \<epsilon> \<subseteq> -s"
+          using open_contains_cball[of "-s"] s by blast
+        then obtain d where "d \<in> t" and d: "dist d c < \<epsilon>"
+          using closure_approachable [of c t] pf unfolding c_def
+          by (metis Diff_iff frontier_def)
+        then have "d \<in> -s" using \<epsilon>
+          using dist_commute by (metis contra_subsetD mem_cball not_le not_less_iff_gr_or_eq)
+        have pimg_sbs_cos: "path_image \<gamma> \<subseteq> -s"
+          using pimg_sbs apply (auto simp: path_image_def)
+          apply (drule subsetD)
+          using `c \<in> - s` `s \<subseteq> t` interior_subset apply (auto simp: c_def)
+          done
+        have "closed_segment c d \<le> cball c \<epsilon>"
+          apply (rule hull_minimal)
+          using  `\<epsilon> > 0` d apply (auto simp: dist_commute)
+          done
+        with \<epsilon> have "closed_segment c d \<subseteq> -s" by blast
+        moreover have con_gcd: "connected (path_image \<gamma> \<union> closed_segment c d)"
+          by (rule connected_Un) (auto simp: c_def `path \<gamma>` connected_path_image)
+        ultimately have "connected_component (- s) a d"
+          unfolding connected_component_def using pimg_sbs_cos ps by blast
+        then have "outside s \<inter> t \<noteq> {}"
+          using outside_same_component [OF _ a]  by (metis IntI `d \<in> t` empty_iff)
+      } note * = this
+      have pal: "pathstart (linepath a b) \<in> closure (- t)"
+        by (auto simp: False closure_def)
+      show ?thesis
+        by (rule exists_path_subpath_to_frontier [OF path_linepath pal _ *]) (auto simp: b)
+  qed
+qed
+
+lemma inside_inside_compact_connected:
+    fixes s :: "'a :: euclidean_space set"
+    assumes s: "closed s" and t: "compact t" and "connected t" "s \<subseteq> inside t"
+      shows "inside s \<subseteq> inside t"
+proof (cases "inside t = {}")
+  case True with assms show ?thesis by auto
+next
+  case False
+  consider "DIM('a) = 1" | "DIM('a) \<ge> 2"
+    using antisym not_less_eq_eq by fastforce
+  then show ?thesis
+  proof cases
+    case 1 then show ?thesis
+             using connected_convex_1_gen assms False inside_convex by blast
+  next
+    case 2
+    have coms: "compact s"
+      using assms apply (simp add: s compact_eq_bounded_closed)
+       by (meson bounded_inside bounded_subset compact_imp_bounded)
+    then have bst: "bounded (s \<union> t)"
+      by (simp add: compact_imp_bounded t)
+    then obtain r where "0 < r" and r: "s \<union> t \<subseteq> ball 0 r"
+      using bounded_subset_ballD by blast
+    have outst: "outside s \<inter> outside t \<noteq> {}"
+    proof -
+      have "- ball 0 r \<subseteq> outside s"
+        apply (rule outside_subset_convex)
+        using r by auto
+      moreover have "- ball 0 r \<subseteq> outside t"
+        apply (rule outside_subset_convex)
+        using r by auto
+      ultimately show ?thesis
+        by (metis Compl_subset_Compl_iff Int_subset_iff bounded_ball inf.orderE outside_bounded_nonempty outside_no_overlap)
+    qed
+    have "s \<inter> t = {}" using assms
+      by (metis disjoint_iff_not_equal inside_no_overlap subsetCE)
+    moreover have "outside s \<inter> inside t \<noteq> {}"
+      by (meson False assms(4) compact_eq_bounded_closed coms open_inside outside_compact_in_open t)
+    ultimately have "inside s \<inter> t = {}"
+      using inside_outside_intersect_connected [OF `connected t`, of s]
+      by (metis "2" compact_eq_bounded_closed coms connected_outside inf.commute inside_outside_intersect_connected outst)
+    then show ?thesis
+      using inside_inside [OF `s \<subseteq> inside t`] by blast
+  qed
+qed
+
+lemma connected_with_inside:
+    fixes s :: "'a :: real_normed_vector set"
+    assumes s: "closed s" and cons: "connected s"
+      shows "connected(s \<union> inside s)"
+proof (cases "s \<union> inside s = UNIV")
+  case True with assms show ?thesis by auto
+next
+  case False
+  then obtain b where b: "b \<notin> s" "b \<notin> inside s" by blast
+  have *: "\<exists>y t. y \<in> s \<and> connected t \<and> a \<in> t \<and> y \<in> t \<and> t \<subseteq> (s \<union> inside s)" if "a \<in> (s \<union> inside s)" for a
+  using that proof
+    assume "a \<in> s" then show ?thesis
+      apply (rule_tac x=a in exI)
+      apply (rule_tac x="{a}" in exI)
+      done
+  next
+    assume a: "a \<in> inside s"
+    show ?thesis
+      apply (rule exists_path_subpath_to_frontier [OF path_linepath [of a b], of "inside s"])
+      using a apply (simp add: closure_def)
+      apply (rule_tac x="pathfinish h" in exI)
+      apply (rule_tac x="path_image h" in exI)
+      apply (simp add: pathfinish_in_path_image connected_path_image, auto)
+      using frontier_inside_subset s apply fastforce
+      by (metis (no_types, lifting) frontier_inside_subset insertE insert_Diff interior_eq open_inside pathfinish_in_path_image s subsetCE)
+  qed
+  show ?thesis
+    apply (clarify dest!: *)
+    apply (rename_tac u u' t t')
+    apply (rule_tac x="(s \<union> t \<union> t')" in exI)
+    apply (auto simp: intro!: connected_Un cons)
+    done
+qed
+
+text\<open>The proof is virtually the same as that above.\<close>
+lemma connected_with_outside:
+    fixes s :: "'a :: real_normed_vector set"
+    assumes s: "closed s" and cons: "connected s"
+      shows "connected(s \<union> outside s)"
+proof (cases "s \<union> outside s = UNIV")
+  case True with assms show ?thesis by auto
+next
+  case False
+  then obtain b where b: "b \<notin> s" "b \<notin> outside s" by blast
+  have *: "\<exists>y t. y \<in> s \<and> connected t \<and> a \<in> t \<and> y \<in> t \<and> t \<subseteq> (s \<union> outside s)" if "a \<in> (s \<union> outside s)" for a
+  using that proof
+    assume "a \<in> s" then show ?thesis
+      apply (rule_tac x=a in exI)
+      apply (rule_tac x="{a}" in exI)
+      done
+  next
+    assume a: "a \<in> outside s"
+    show ?thesis
+      apply (rule exists_path_subpath_to_frontier [OF path_linepath [of a b], of "outside s"])
+      using a apply (simp add: closure_def)
+      apply (rule_tac x="pathfinish h" in exI)
+      apply (rule_tac x="path_image h" in exI)
+      apply (simp add: pathfinish_in_path_image connected_path_image, auto)
+      using frontier_outside_subset s apply fastforce
+      by (metis (no_types, lifting) frontier_outside_subset insertE insert_Diff interior_eq open_outside pathfinish_in_path_image s subsetCE)
+  qed
+  show ?thesis
+    apply (clarify dest!: *)
+    apply (rename_tac u u' t t')
+    apply (rule_tac x="(s \<union> t \<union> t')" in exI)
+    apply (auto simp: intro!: connected_Un cons)
+    done
+qed
+
+lemma inside_inside_eq_empty [simp]:
+    fixes s :: "'a :: {real_normed_vector, perfect_space} set"
+    assumes s: "closed s" and cons: "connected s"
+      shows "inside (inside s) = {}"
+  by (metis (no_types) unbounded_outside connected_with_outside [OF assms] bounded_Un
+           inside_complement_unbounded_connected_empty unbounded_outside union_with_outside)
+
+lemma inside_in_components:
+     "inside s \<in> components (- s) \<longleftrightarrow> connected(inside s) \<and> inside s \<noteq> {}"
+  apply (auto intro: inside_same_component connected_componentI)
+  apply (metis IntI empty_iff inside_no_overlap)
+  done
+
+text\<open>The proof is virtually the same as that above.\<close>
+lemma outside_in_components:
+     "outside s \<in> components (- s) \<longleftrightarrow> connected(outside s) \<and> outside s \<noteq> {}"
+  apply (auto intro: outside_same_component connected_componentI)
+  apply (metis IntI empty_iff outside_no_overlap)
+  done
+
+lemma bounded_unique_outside:
+    fixes s :: "'a :: euclidean_space set"
+    shows "\<lbrakk>bounded s; DIM('a) \<ge> 2\<rbrakk> \<Longrightarrow> (c \<in> components (- s) \<and> ~bounded c \<longleftrightarrow> c = outside s)"
+  apply (rule iffI)
+  apply (metis cobounded_unique_unbounded_components connected_outside double_compl outside_bounded_nonempty outside_in_components unbounded_outside)
+  by (simp add: connected_outside outside_bounded_nonempty outside_in_components unbounded_outside)
+
end```
```--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -513,9 +513,6 @@
lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)"
using closedin_Inter[of "{S,T}" U] by auto

-lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B"
-  by blast
-
lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2)
apply (metis openin_subset subset_eq)
@@ -790,6 +787,13 @@
lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
by (auto simp add: closedin_closed intro: closedin_trans)

+lemma openin_subtopology_inter_subset:
+   "openin (subtopology euclidean u) (u \<inter> s) \<and> v \<subseteq> u \<Longrightarrow> openin (subtopology euclidean v) (v \<inter> s)"
+  by (auto simp: openin_subtopology)
+
+lemma openin_open_eq: "open s \<Longrightarrow> (openin (subtopology euclidean s) t \<longleftrightarrow> open t \<and> t \<subseteq> s)"
+  using open_subset openin_open_trans openin_subset by fastforce
+

subsection \<open>Open and closed balls\<close>

@@ -805,23 +809,29 @@
lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e"

-lemma mem_ball_0:
+lemma ball_trivial [simp]: "ball x 0 = {}"
+
+lemma cball_trivial [simp]: "cball x 0 = {x}"
+
+lemma mem_ball_0 [simp]:
fixes x :: "'a::real_normed_vector"
shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e"

-lemma mem_cball_0:
+lemma mem_cball_0 [simp]:
fixes x :: "'a::real_normed_vector"
shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"

-lemma centre_in_ball: "x \<in> ball x e \<longleftrightarrow> 0 < e"
+lemma centre_in_ball [simp]: "x \<in> ball x e \<longleftrightarrow> 0 < e"
by simp

-lemma centre_in_cball: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e"
+lemma centre_in_cball [simp]: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e"
by simp

-lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e"
+lemma ball_subset_cball [simp,intro]: "ball x e \<subseteq> cball x e"

lemma subset_ball[intro]: "d \<le> e \<Longrightarrow> ball x d \<subseteq> ball x e"
@@ -1547,7 +1557,12 @@
shows "interior S = T"
by (intro equalityI assms interior_subset open_interior interior_maximal)

-lemma interior_inter [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
+lemma interior_singleton [simp]:
+      fixes a :: "'a::perfect_space" shows "interior {a} = {}"
+  apply (rule interior_unique, simp_all)
+  using not_open_singleton subset_singletonD by fastforce
+
+lemma interior_Int [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1
Int_lower2 interior_maximal interior_subset open_Int open_interior)

@@ -1801,6 +1816,10 @@
apply (force simp: closure_def)
done

+lemma closedin_closed_eq:
+    "closed s \<Longrightarrow> (closedin (subtopology euclidean s) t \<longleftrightarrow> closed t \<and> t \<subseteq> s)"
+  by (meson closed_in_limpt closed_subset closedin_closed_trans)
+
subsection\<open>Connected components, considered as a connectedness relation or a set\<close>

definition
@@ -2171,7 +2190,7 @@
then show ?thesis using frontier_subset_closed[of S] ..
qed

-lemma frontier_complement: "frontier (- S) = frontier S"
+lemma frontier_complement  [simp]: "frontier (- S) = frontier S"
by (auto simp add: frontier_def closure_complement interior_complement)

lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
@@ -5128,6 +5147,11 @@

text\<open>Some simple consequential lemmas.\<close>

+lemma continuous_onD:
+    assumes "continuous_on s f" "x\<in>s" "e>0"
+    obtains d where "d>0"  "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
+  using assms [unfolded continuous_on_iff] by blast
+
lemma uniformly_continuous_onE:
assumes "uniformly_continuous_on s f" "0 < e"
obtains d where "d>0" "\<And>x x'. \<lbrakk>x\<in>s; x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
@@ -5514,7 +5538,7 @@

text \<open>Half-global and completely global cases.\<close>

-lemma continuous_open_in_preimage:
+lemma continuous_openin_preimage:
assumes "continuous_on s f"  "open t"
shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
proof -
@@ -5527,7 +5551,7 @@
using * by auto
qed

-lemma continuous_closed_in_preimage:
+lemma continuous_closedin_preimage:
assumes "continuous_on s f" and "closed t"
shows "closedin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
proof -
@@ -5548,7 +5572,7 @@
shows "open {x \<in> s. f x \<in> t}"
proof-
obtain T where T: "open T" "{x \<in> s. f x \<in> t} = s \<inter> T"
-    using continuous_open_in_preimage[OF assms(1,3)] unfolding openin_open by auto
+    using continuous_openin_preimage[OF assms(1,3)] unfolding openin_open by auto
then show ?thesis
using open_Int[of s T, OF assms(2)] by auto
qed
@@ -5560,7 +5584,7 @@
shows "closed {x \<in> s. f x \<in> t}"
proof-
obtain T where "closed T" "{x \<in> s. f x \<in> t} = s \<inter> T"
-    using continuous_closed_in_preimage[OF assms(1,3)]
+    using continuous_closedin_preimage[OF assms(1,3)]
unfolding closedin_closed by auto
then show ?thesis using closed_Int[of s T, OF assms(2)] by auto
qed
@@ -5603,7 +5627,7 @@
lemma continuous_closed_in_preimage_constant:
fixes f :: "_ \<Rightarrow> 'b::t1_space"
shows "continuous_on s f \<Longrightarrow> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
-  using continuous_closed_in_preimage[of s f "{a}"] by auto
+  using continuous_closedin_preimage[of s f "{a}"] by auto

lemma continuous_closed_preimage_constant:
fixes f :: "_ \<Rightarrow> 'b::t1_space"
@@ -5969,6 +5993,12 @@
then show ?thesis
unfolding connected_clopen by auto
qed
+
+lemma connected_linear_image:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+  assumes "linear f" and "connected s"
+  shows "connected (f ` s)"
+using connected_continuous_image assms linear_continuous_on linear_conv_bounded_linear by blast

text \<open>Continuity implies uniform continuity on a compact domain.\<close>

@@ -5986,7 +6016,7 @@
proof safe
fix y
assume "y \<in> s"
-    from continuous_open_in_preimage[OF f open_ball]
+    from continuous_openin_preimage[OF f open_ball]
obtain T where "open T" and T: "{x \<in> s. f x \<in> ball (f y) (e/2)} = T \<inter> s"
unfolding openin_subtopology open_openin by metis
then obtain d where "ball y d \<subseteq> T" "0 < d"```
```--- a/src/HOL/Set.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Set.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -1552,6 +1552,9 @@
lemma Diff_Int: "A - (B \<inter> C) = (A - B) \<union> (A - C)"
by blast

+lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B"
+  by blast
+
lemma Un_Diff: "(A \<union> B) - C = (A - C) \<union> (B - C)"
by blast
```
```--- a/src/HOL/Transcendental.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Transcendental.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -1145,7 +1145,8 @@
done

-declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
+declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
+        DERIV_exp[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]

lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
proof -
@@ -1589,6 +1590,8 @@
by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)

declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
+        DERIV_ln_divide[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
+

lemma ln_series:
assumes "0 < x" and "x < 2"
@@ -2173,6 +2176,7 @@
qed

lemmas DERIV_log[THEN DERIV_chain2, derivative_intros]
+       DERIV_log[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]

lemma powr_log_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powr (log a x) = x"
@@ -2720,6 +2724,7 @@
done

declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
+        DERIV_sin[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]

lemma DERIV_cos [simp]:
fixes x :: "'a::{real_normed_field,banach}"
@@ -2735,6 +2740,7 @@
done

declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
+        DERIV_cos[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]

lemma isCont_sin:
fixes x :: "'a::{real_normed_field,banach}"
@@ -4528,8 +4534,11 @@

declare
DERIV_arcsin[THEN DERIV_chain2, derivative_intros]
+  DERIV_arcsin[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
DERIV_arccos[THEN DERIV_chain2, derivative_intros]
+  DERIV_arccos[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
DERIV_arctan[THEN DERIV_chain2, derivative_intros]
+  DERIV_arctan[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]

lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
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])```