Merge
authorpaulson <lp15@cam.ac.uk>
Tue, 24 May 2016 15:08:07 +0100
changeset 63129 e5cb3440af74
parent 63128 24708cf4ba61 (diff)
parent 63121 284e1802bc5c (current diff)
child 63130 4ae5da02d627
Merge
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy
--- a/src/HOL/Library/Countable_Set.thy	Tue May 24 11:39:26 2016 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Tue May 24 15:08:07 2016 +0100
@@ -105,6 +105,11 @@
   using to_nat_on_infinite[of S, unfolded bij_betw_def]
   by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite)
 
+lemma countable_as_injective_image:
+  assumes "countable A" "infinite A"
+  obtains f :: "nat \<Rightarrow> 'a" where "A = range f" "inj f"
+by (metis bij_betw_def bij_betw_from_nat_into [OF assms])
+
 lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A"
   using to_nat_on_infinite[of A] to_nat_on_finite[of A]
   by (cases "finite A") (auto simp: bij_betw_def)
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue May 24 11:39:26 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue May 24 15:08:07 2016 +0100
@@ -19,7 +19,7 @@
 section \<open>Results connected with topological dimension.\<close>
 
 theory Brouwer_Fixpoint
-imports Path_Connected
+imports Path_Connected Homeomorphism
 begin
 
 lemma bij_betw_singleton_eq:
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue May 24 11:39:26 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue May 24 15:08:07 2016 +0100
@@ -11,30 +11,6 @@
   "~~/src/HOL/Library/Set_Algebras"
 begin
 
-lemma independent_injective_on_span_image:
-  assumes iS: "independent S"
-    and lf: "linear f"
-    and fi: "inj_on f (span S)"
-  shows "independent (f ` S)"
-proof -
-  {
-    fix a
-    assume a: "a \<in> S" "f a \<in> span (f ` S - {f a})"
-    have eq: "f ` S - {f a} = f ` (S - {a})"
-      using fi a span_inc by (auto simp add: inj_on_def)
-    from a have "f a \<in> f ` span (S -{a})"
-      unfolding eq span_linear_image [OF lf, of "S - {a}"] by blast
-    moreover have "span (S - {a}) \<subseteq> span S"
-      using span_mono[of "S - {a}" S] by auto
-    ultimately have "a \<in> span (S - {a})"
-      using fi a span_inc by (auto simp add: inj_on_def)
-    with a(1) iS have False
-      by (simp add: dependent_def)
-  }
-  then show ?thesis
-    unfolding dependent_def by blast
-qed
-
 lemma dim_image_eq:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   assumes lf: "linear f"
@@ -46,7 +22,7 @@
   then have "span S = span B"
     using span_mono[of B S] span_mono[of S "span B"] span_span[of B] by auto
   then have "independent (f ` B)"
-    using independent_injective_on_span_image[of B f] B assms by auto
+    using independent_inj_on_image[of B f] B assms by auto
   moreover have "card (f ` B) = card B"
     using assms card_image[of f B] subset_inj_on[of f "span S" B] B span_inc by auto
   moreover have "(f ` B) \<subseteq> (f ` S)"
@@ -5321,500 +5297,6 @@
   done
 
 
-subsection \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
-
-lemma compact_frontier_line_lemma:
-  fixes s :: "'a::euclidean_space set"
-  assumes "compact s"
-    and "0 \<in> s"
-    and "x \<noteq> 0"
-  obtains u where "0 \<le> u" and "(u *\<^sub>R x) \<in> frontier s" "\<forall>v>u. (v *\<^sub>R x) \<notin> s"
-proof -
-  obtain b where b: "b > 0" "\<forall>x\<in>s. norm x \<le> b"
-    using compact_imp_bounded[OF assms(1), unfolded bounded_pos] by auto
-  let ?A = "{y. \<exists>u. 0 \<le> u \<and> u \<le> b / norm(x) \<and> (y = u *\<^sub>R x)}"
-  have A: "?A = (\<lambda>u. u *\<^sub>R x) ` {0 .. b / norm x}"
-    by auto
-  have *: "\<And>x A B. x\<in>A \<Longrightarrow> x\<in>B \<Longrightarrow> A\<inter>B \<noteq> {}" by blast
-  have "compact ?A"
-    unfolding A
-    apply (rule compact_continuous_image)
-    apply (rule continuous_at_imp_continuous_on)
-    apply rule
-    apply (intro continuous_intros)
-    apply (rule compact_Icc)
-    done
-  moreover have "{y. \<exists>u\<ge>0. u \<le> b / norm x \<and> y = u *\<^sub>R x} \<inter> s \<noteq> {}"
-    apply(rule *[OF _ assms(2)])
-    unfolding mem_Collect_eq
-    using \<open>b > 0\<close> assms(3)
-    apply auto
-    done
-  ultimately obtain u y where obt: "u\<ge>0" "u \<le> b / norm x" "y = u *\<^sub>R x"
-    "y \<in> ?A" "y \<in> s" "\<forall>z\<in>?A \<inter> s. dist 0 z \<le> dist 0 y"
-    using distance_attains_sup[OF compact_Int[OF _ assms(1), of ?A], of 0] by blast
-  have "norm x > 0"
-    using assms(3)[unfolded zero_less_norm_iff[symmetric]] by auto
-  {
-    fix v
-    assume as: "v > u" "v *\<^sub>R x \<in> s"
-    then have "v \<le> b / norm x"
-      using b(2)[rule_format, OF as(2)]
-      using \<open>u\<ge>0\<close>
-      unfolding pos_le_divide_eq[OF \<open>norm x > 0\<close>]
-      by auto
-    then have "norm (v *\<^sub>R x) \<le> norm y"
-      apply (rule_tac obt(6)[rule_format, unfolded dist_0_norm])
-      apply (rule IntI)
-      defer
-      apply (rule as(2))
-      unfolding mem_Collect_eq
-      apply (rule_tac x=v in exI)
-      using as(1) \<open>u\<ge>0\<close>
-      apply (auto simp add: field_simps)
-      done
-    then have False
-      unfolding obt(3) using \<open>u\<ge>0\<close> \<open>norm x > 0\<close> \<open>v > u\<close>
-      by (auto simp add:field_simps)
-  } note u_max = this
-
-  have "u *\<^sub>R x \<in> frontier s"
-    unfolding frontier_straddle
-    apply (rule,rule,rule)
-    apply (rule_tac x="u *\<^sub>R x" in bexI)
-    unfolding obt(3)[symmetric]
-    prefer 3
-    apply (rule_tac x="(u + (e / 2) / norm x) *\<^sub>R x" in exI)
-    apply (rule, rule)
-  proof -
-    fix e
-    assume "e > 0" and as: "(u + e / 2 / norm x) *\<^sub>R x \<in> s"
-    then have "u + e / 2 / norm x > u"
-      using \<open>norm x > 0\<close> by (auto simp del:zero_less_norm_iff)
-    then show False using u_max[OF _ as] by auto
-  qed (insert \<open>y\<in>s\<close>, auto simp add: dist_norm scaleR_left_distrib obt(3))
-  then show ?thesis by(metis that[of u] u_max obt(1))
-qed
-
-lemma starlike_compact_projective:
-  assumes "compact s"
-    and "cball (0::'a::euclidean_space) 1 \<subseteq> s "
-    and "\<forall>x\<in>s. \<forall>u. 0 \<le> u \<and> u < 1 \<longrightarrow> u *\<^sub>R x \<in> s - frontier s"
-  shows "s homeomorphic (cball (0::'a::euclidean_space) 1)"
-proof -
-  have fs: "frontier s \<subseteq> s"
-    apply (rule frontier_subset_closed)
-    using compact_imp_closed[OF assms(1)]
-    apply simp
-    done
-  define pi where [abs_def]: "pi x = inverse (norm x) *\<^sub>R x" for x :: 'a
-  have "0 \<notin> frontier s"
-    unfolding frontier_straddle
-    apply (rule notI)
-    apply (erule_tac x=1 in allE)
-    using assms(2)[unfolded subset_eq Ball_def mem_cball]
-    apply auto
-    done
-  have injpi: "\<And>x y. pi x = pi y \<and> norm x = norm y \<longleftrightarrow> x = y"
-    unfolding pi_def by auto
-
-  have contpi: "continuous_on (UNIV - {0}) pi"
-    apply (rule continuous_at_imp_continuous_on)
-    apply rule unfolding pi_def
-    apply (intro continuous_intros)
-    apply simp
-    done
-  define sphere :: "'a set" where "sphere = {x. norm x = 1}"
-  have pi: "\<And>x. x \<noteq> 0 \<Longrightarrow> pi x \<in> sphere" "\<And>x u. u>0 \<Longrightarrow> pi (u *\<^sub>R x) = pi x"
-    unfolding pi_def sphere_def by auto
-
-  have "0 \<in> s"
-    using assms(2) and centre_in_cball[of 0 1] by auto
-  have front_smul: "\<forall>x\<in>frontier s. \<forall>u\<ge>0. u *\<^sub>R x \<in> s \<longleftrightarrow> u \<le> 1"
-  proof (rule,rule,rule)
-    fix x and u :: real
-    assume x: "x \<in> frontier s" and "0 \<le> u"
-    then have "x \<noteq> 0"
-      using \<open>0 \<notin> frontier s\<close> by auto
-    obtain v where v: "0 \<le> v" "v *\<^sub>R x \<in> frontier s" "\<forall>w>v. w *\<^sub>R x \<notin> s"
-      using compact_frontier_line_lemma[OF assms(1) \<open>0\<in>s\<close> \<open>x\<noteq>0\<close>] by auto
-    have "v = 1"
-      apply (rule ccontr)
-      unfolding neq_iff
-      apply (erule disjE)
-    proof -
-      assume "v < 1"
-      then show False
-        using v(3)[THEN spec[where x=1]] using x fs by (simp add: pth_1 subset_iff)
-    next
-      assume "v > 1"
-      then show False
-        using assms(3)[THEN bspec[where x="v *\<^sub>R x"], THEN spec[where x="inverse v"]]
-        using v and x and fs
-        unfolding inverse_less_1_iff by auto
-    qed
-    show "u *\<^sub>R x \<in> s \<longleftrightarrow> u \<le> 1"
-      apply rule
-      using v(3)[unfolded \<open>v=1\<close>, THEN spec[where x=u]]
-    proof -
-      assume "u \<le> 1"
-      then show "u *\<^sub>R x \<in> s"
-      apply (cases "u = 1")
-        using assms(3)[THEN bspec[where x=x], THEN spec[where x=u]]
-        using \<open>0\<le>u\<close> and x and fs
-        by auto
-    qed auto
-  qed
-
-  have "\<exists>surf. homeomorphism (frontier s) sphere pi surf"
-    apply (rule homeomorphism_compact)
-    apply (rule compact_frontier[OF assms(1)])
-    apply (rule continuous_on_subset[OF contpi])
-    defer
-    apply (rule set_eqI)
-    apply rule
-    unfolding inj_on_def
-    prefer 3
-    apply(rule,rule,rule)
-  proof -
-    fix x
-    assume "x \<in> pi ` frontier s"
-    then obtain y where "y \<in> frontier s" "x = pi y" by auto
-    then show "x \<in> sphere"
-      using pi(1)[of y] and \<open>0 \<notin> frontier s\<close> by auto
-  next
-    fix x
-    assume "x \<in> sphere"
-    then have "norm x = 1" "x \<noteq> 0"
-      unfolding sphere_def by auto
-    then obtain u where "0 \<le> u" "u *\<^sub>R x \<in> frontier s" "\<forall>v>u. v *\<^sub>R x \<notin> s"
-      using compact_frontier_line_lemma[OF assms(1) \<open>0\<in>s\<close>, of x] by auto
-    then show "x \<in> pi ` frontier s"
-      unfolding image_iff le_less pi_def
-      apply (rule_tac x="u *\<^sub>R x" in bexI)
-      using \<open>norm x = 1\<close> \<open>0 \<notin> frontier s\<close>
-      apply auto
-      done
-  next
-    fix x y
-    assume as: "x \<in> frontier s" "y \<in> frontier s" "pi x = pi y"
-    then have xys: "x \<in> s" "y \<in> s"
-      using fs by auto
-    from as(1,2) have nor: "norm x \<noteq> 0" "norm y \<noteq> 0"
-      using \<open>0\<notin>frontier s\<close> by auto
-    from nor have x: "x = norm x *\<^sub>R ((inverse (norm y)) *\<^sub>R y)"
-      unfolding as(3)[unfolded pi_def, symmetric] by auto
-    from nor have y: "y = norm y *\<^sub>R ((inverse (norm x)) *\<^sub>R x)"
-      unfolding as(3)[unfolded pi_def] by auto
-    have "0 \<le> norm y * inverse (norm x)" and "0 \<le> norm x * inverse (norm y)"
-      using nor
-      apply auto
-      done
-    then have "norm x = norm y"
-      apply -
-      apply (rule ccontr)
-      unfolding neq_iff
-      using x y and front_smul[THEN bspec, OF as(1), THEN spec[where x="norm y * (inverse (norm x))"]]
-      using front_smul[THEN bspec, OF as(2), THEN spec[where x="norm x * (inverse (norm y))"]]
-      using xys nor
-      apply (auto simp add: field_simps)
-      done
-    then show "x = y"
-      apply (subst injpi[symmetric])
-      using as(3)
-      apply auto
-      done
-  qed (insert \<open>0 \<notin> frontier s\<close>, auto)
-  then obtain surf where
-    surf: "\<forall>x\<in>frontier s. surf (pi x) = x"  "pi ` frontier s = sphere" "continuous_on (frontier s) pi"
-    "\<forall>y\<in>sphere. pi (surf y) = y" "surf ` sphere = frontier s" "continuous_on sphere surf"
-    unfolding homeomorphism_def by auto
-
-  have cont_surfpi: "continuous_on (UNIV -  {0}) (surf \<circ> pi)"
-    apply (rule continuous_on_compose)
-    apply (rule contpi)
-    apply (rule continuous_on_subset[of sphere])
-    apply (rule surf(6))
-    using pi(1)
-    apply auto
-    done
-
-  {
-    fix x
-    assume as: "x \<in> cball (0::'a) 1"
-    have "norm x *\<^sub>R surf (pi x) \<in> s"
-    proof (cases "x=0 \<or> norm x = 1")
-      case False
-      then have "pi x \<in> sphere" "norm x < 1"
-        using pi(1)[of x] as by(auto simp add: dist_norm)
-      then show ?thesis
-        apply (rule_tac assms(3)[rule_format, THEN DiffD1])
-        apply (rule_tac fs[unfolded subset_eq, rule_format])
-        unfolding surf(5)[symmetric]
-        apply auto
-        done
-    next
-      case True
-      then show ?thesis
-        apply rule
-        defer
-        unfolding pi_def
-        apply (rule fs[unfolded subset_eq, rule_format])
-        unfolding surf(5)[unfolded sphere_def, symmetric]
-        using \<open>0\<in>s\<close>
-        apply auto
-        done
-    qed
-  } note hom = this
-
-  {
-    fix x
-    assume "x \<in> s"
-    then have "x \<in> (\<lambda>x. norm x *\<^sub>R surf (pi x)) ` cball 0 1"
-    proof (cases "x = 0")
-      case True
-      show ?thesis
-        unfolding image_iff True
-        apply (rule_tac x=0 in bexI)
-        apply auto
-        done
-    next
-      let ?a = "inverse (norm (surf (pi x)))"
-      case False
-      then have invn: "inverse (norm x) \<noteq> 0" by auto
-      from False have pix: "pi x\<in>sphere" using pi(1) by auto
-      then have "pi (surf (pi x)) = pi x"
-        apply (rule_tac surf(4)[rule_format])
-        apply assumption
-        done
-      then have **: "norm x *\<^sub>R (?a *\<^sub>R surf (pi x)) = x"
-        apply (rule_tac scaleR_left_imp_eq[OF invn])
-        unfolding pi_def
-        using invn
-        apply auto
-        done
-      then have *: "?a * norm x > 0" and "?a > 0" "?a \<noteq> 0"
-        using surf(5) \<open>0\<notin>frontier s\<close>
-        apply -
-        apply (rule mult_pos_pos)
-        using False[unfolded zero_less_norm_iff[symmetric]]
-        apply auto
-        done
-      have "norm (surf (pi x)) \<noteq> 0"
-        using ** False by auto
-      then have "norm x = norm ((?a * norm x) *\<^sub>R surf (pi x))"
-        unfolding norm_scaleR abs_mult abs_norm_cancel abs_of_pos[OF \<open>?a > 0\<close>] by auto
-      moreover have "pi x = pi ((inverse (norm (surf (pi x))) * norm x) *\<^sub>R surf (pi x))"
-        unfolding pi(2)[OF *] surf(4)[rule_format, OF pix] ..
-      moreover have "surf (pi x) \<in> frontier s"
-        using surf(5) pix by auto
-      then have "dist 0 (inverse (norm (surf (pi x))) *\<^sub>R x) \<le> 1"
-        unfolding dist_norm
-        using ** and *
-        using front_smul[THEN bspec[where x="surf (pi x)"], THEN spec[where x="norm x * ?a"]]
-        using False \<open>x\<in>s\<close>
-        by (auto simp add: field_simps)
-      ultimately show ?thesis
-        unfolding image_iff
-        apply (rule_tac x="inverse (norm (surf(pi x))) *\<^sub>R x" in bexI)
-        apply (subst injpi[symmetric])
-        unfolding abs_mult abs_norm_cancel abs_of_pos[OF \<open>?a > 0\<close>]
-        unfolding pi(2)[OF \<open>?a > 0\<close>]
-        apply auto
-        done
-    qed
-  } note hom2 = this
-
-  show ?thesis
-    apply (subst homeomorphic_sym)
-    apply (rule homeomorphic_compact[where f="\<lambda>x. norm x *\<^sub>R surf (pi x)"])
-    apply (rule compact_cball)
-    defer
-    apply (rule set_eqI)
-    apply rule
-    apply (erule imageE)
-    apply (drule hom)
-    prefer 4
-    apply (rule continuous_at_imp_continuous_on)
-    apply rule
-    apply (rule_tac [3] hom2)
-  proof -
-    fix x :: 'a
-    assume as: "x \<in> cball 0 1"
-    then show "continuous (at x) (\<lambda>x. norm x *\<^sub>R surf (pi x))"
-    proof (cases "x = 0")
-      case False
-      then show ?thesis
-        apply (intro continuous_intros)
-        using cont_surfpi
-        unfolding continuous_on_eq_continuous_at[OF open_delete[OF open_UNIV]] o_def
-        apply auto
-        done
-    next
-      case True
-      obtain B where B: "\<forall>x\<in>s. norm x \<le> B"
-        using compact_imp_bounded[OF assms(1)] unfolding bounded_iff by auto
-      then have "B > 0"
-        using assms(2)
-        unfolding subset_eq
-        apply (erule_tac x="SOME i. i\<in>Basis" in ballE)
-        defer
-        apply (erule_tac x="SOME i. i\<in>Basis" in ballE)
-        unfolding Ball_def mem_cball dist_norm
-        using DIM_positive[where 'a='a]
-        apply (auto simp: SOME_Basis)
-        done
-      show ?thesis
-        unfolding True continuous_at Lim_at
-        apply(rule,rule)
-        apply(rule_tac x="e / B" in exI)
-        apply rule
-        apply (rule divide_pos_pos)
-        prefer 3
-        apply(rule,rule,erule conjE)
-        unfolding norm_zero scaleR_zero_left dist_norm diff_0_right norm_scaleR abs_norm_cancel
-      proof -
-        fix e and x :: 'a
-        assume as: "norm x < e / B" "0 < norm x" "e > 0"
-        then have "surf (pi x) \<in> frontier s"
-          using pi(1)[of x] unfolding surf(5)[symmetric] by auto
-        then have "norm (surf (pi x)) \<le> B"
-          using B fs by auto
-        then have "norm x * norm (surf (pi x)) \<le> norm x * B"
-          using as(2) by auto
-        also have "\<dots> < e / B * B"
-          apply (rule mult_strict_right_mono)
-          using as(1) \<open>B>0\<close>
-          apply auto
-          done
-        also have "\<dots> = e" using \<open>B > 0\<close> by auto
-        finally show "norm x * norm (surf (pi x)) < e" .
-      qed (insert \<open>B>0\<close>, auto)
-    qed
-  next
-    {
-      fix x
-      assume as: "surf (pi x) = 0"
-      have "x = 0"
-      proof (rule ccontr)
-        assume "x \<noteq> 0"
-        then have "pi x \<in> sphere"
-          using pi(1) by auto
-        then have "surf (pi x) \<in> frontier s"
-          using surf(5) by auto
-        then show False
-          using \<open>0\<notin>frontier s\<close> unfolding as by simp
-      qed
-    } note surf_0 = this
-    show "inj_on (\<lambda>x. norm x *\<^sub>R surf (pi x)) (cball 0 1)"
-      unfolding inj_on_def
-    proof (rule,rule,rule)
-      fix x y
-      assume as: "x \<in> cball 0 1" "y \<in> cball 0 1" "norm x *\<^sub>R surf (pi x) = norm y *\<^sub>R surf (pi y)"
-      then show "x = y"
-      proof (cases "x=0 \<or> y=0")
-        case True
-        then show ?thesis
-          using as by (auto elim: surf_0)
-      next
-        case False
-        then have "pi (surf (pi x)) = pi (surf (pi y))"
-          using as(3)
-          using pi(2)[of "norm x" "surf (pi x)"] pi(2)[of "norm y" "surf (pi y)"]
-          by auto
-        moreover have "pi x \<in> sphere" "pi y \<in> sphere"
-          using pi(1) False by auto
-        ultimately have *: "pi x = pi y"
-          using surf(4)[THEN bspec[where x="pi x"]] surf(4)[THEN bspec[where x="pi y"]]
-          by auto
-        moreover have "norm x = norm y"
-          using as(3)[unfolded *] using False
-          by (auto dest:surf_0)
-        ultimately show ?thesis
-          using injpi by auto
-      qed
-    qed
-  qed auto
-qed
-
-lemma homeomorphic_convex_compact_lemma:
-  fixes s :: "'a::euclidean_space set"
-  assumes "convex s"
-    and "compact s"
-    and "cball 0 1 \<subseteq> s"
-  shows "s homeomorphic (cball (0::'a) 1)"
-proof (rule starlike_compact_projective[OF assms(2-3)], clarify)
-  fix x u
-  assume "x \<in> s" and "0 \<le> u" and "u < (1::real)"
-  have "open (ball (u *\<^sub>R x) (1 - u))"
-    by (rule open_ball)
-  moreover have "u *\<^sub>R x \<in> ball (u *\<^sub>R x) (1 - u)"
-    unfolding centre_in_ball using \<open>u < 1\<close> by simp
-  moreover have "ball (u *\<^sub>R x) (1 - u) \<subseteq> s"
-  proof
-    fix y
-    assume "y \<in> ball (u *\<^sub>R x) (1 - u)"
-    then have "dist (u *\<^sub>R x) y < 1 - u"
-      unfolding mem_ball .
-    with \<open>u < 1\<close> have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> cball 0 1"
-      by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
-    with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s" ..
-    with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> s"
-      using \<open>x \<in> s\<close> \<open>0 \<le> u\<close> \<open>u < 1\<close> [THEN less_imp_le] by (rule convexD_alt)
-    then show "y \<in> s" using \<open>u < 1\<close>
-      by simp
-  qed
-  ultimately have "u *\<^sub>R x \<in> interior s" ..
-  then show "u *\<^sub>R x \<in> s - frontier s"
-    using frontier_def and interior_subset by auto
-qed
-
-lemma homeomorphic_convex_compact_cball:
-  fixes e :: real
-    and s :: "'a::euclidean_space set"
-  assumes "convex s"
-    and "compact s"
-    and "interior s \<noteq> {}"
-    and "e > 0"
-  shows "s homeomorphic (cball (b::'a) e)"
-proof -
-  obtain a where "a \<in> interior s"
-    using assms(3) by auto
-  then obtain d where "d > 0" and d: "cball a d \<subseteq> s"
-    unfolding mem_interior_cball by auto
-  let ?d = "inverse d" and ?n = "0::'a"
-  have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *\<^sub>R (x - a)) ` s"
-    apply rule
-    apply (rule_tac x="d *\<^sub>R x + a" in image_eqI)
-    defer
-    apply (rule d[unfolded subset_eq, rule_format])
-    using \<open>d > 0\<close>
-    unfolding mem_cball dist_norm
-    apply (auto simp add: mult_right_le_one_le)
-    done
-  then have "(\<lambda>x. inverse d *\<^sub>R (x - a)) ` s homeomorphic cball ?n 1"
-    using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` s",
-      OF convex_affinity compact_affinity]
-    using assms(1,2)
-    by (auto simp add: scaleR_right_diff_distrib)
-  then show ?thesis
-    apply (rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]])
-    apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" s "?d *\<^sub>R -a"]])
-    using \<open>d>0\<close> \<open>e>0\<close>
-    apply (auto simp add: scaleR_right_diff_distrib)
-    done
-qed
-
-lemma homeomorphic_convex_compact:
-  fixes s :: "'a::euclidean_space set"
-    and t :: "'a set"
-  assumes "convex s" "compact s" "interior s \<noteq> {}"
-    and "convex t" "compact t" "interior t \<noteq> {}"
-  shows "s homeomorphic t"
-  using assms
-  by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
-
-
 subsection \<open>Epigraphs of convex functions\<close>
 
 definition "epigraph s (f :: _ \<Rightarrow> real) = {xy. fst xy \<in> s \<and> f (fst xy) \<le> snd xy}"
@@ -7503,6 +6985,20 @@
     done
 qed
 
+lemma in_interior_closure_convex_segment:
+  fixes S :: "'a::euclidean_space set"
+  assumes "convex S" and a: "a \<in> interior S" and b: "b \<in> closure S"
+    shows "open_segment a b \<subseteq> interior S"
+proof (clarsimp simp: in_segment)
+  fix u::real
+  assume u: "0 < u" "u < 1"
+  have "(1 - u) *\<^sub>R a + u *\<^sub>R b = b - (1 - u) *\<^sub>R (b - a)"
+    by (simp add: algebra_simps)
+  also have "... \<in> interior S" using mem_interior_closure_convex_shrink [OF assms] u
+    by simp
+  finally show "(1 - u) *\<^sub>R a + u *\<^sub>R b \<in> interior S" .
+qed
+
 
 subsection \<open>Some obvious but surprisingly hard simplex lemmas\<close>
 
@@ -7516,7 +7012,7 @@
   unfolding mem_Collect_eq
   apply (erule_tac[!] exE)
   apply (erule_tac[!] conjE)+
-  unfolding setsum_clauses(2)[OF assms(1)]
+  unfolding setsum_clauses(2)[OF \<open>finite s\<close>]
   apply (rule_tac x=u in exI)
   defer
   apply (rule_tac x="\<lambda>x. if x = 0 then 1 - setsum u s else u x" in exI)
@@ -8705,7 +8201,7 @@
   then show ?thesis by auto
 qed
 
-lemma closure_inter: "closure (\<Inter>I) \<le> \<Inter>{closure S |S. S \<in> I}"
+lemma closure_Int: "closure (\<Inter>I) \<le> \<Inter>{closure S |S. S \<in> I}"
 proof -
   {
     fix y
@@ -8793,7 +8289,7 @@
     using rel_interior_inter_aux closure_mono[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"]
     by auto
   ultimately show ?thesis
-    using closure_inter[of I] by auto
+    using closure_Int[of I] by auto
 qed
 
 lemma convex_inter_rel_interior_same_closure:
@@ -8808,7 +8304,7 @@
     using rel_interior_inter_aux closure_mono[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"]
     by auto
   ultimately show ?thesis
-    using closure_inter[of I] by auto
+    using closure_Int[of I] by auto
 qed
 
 lemma convex_rel_interior_inter:
@@ -8898,7 +8394,7 @@
   shows "rel_interior (S \<inter> T) = rel_interior S \<inter> rel_interior T"
   using convex_rel_interior_finite_inter[of "{S,T}"] assms by auto
 
-lemma convex_affine_closure_inter:
+lemma convex_affine_closure_Int:
   fixes S T :: "'n::euclidean_space set"
   assumes "convex S"
     and "affine T"
@@ -8928,7 +8424,7 @@
   shows "connected_component S a b \<longleftrightarrow> closed_segment a b \<subseteq> S"
 by (simp add: connected_component_1_gen)
 
-lemma convex_affine_rel_interior_inter:
+lemma convex_affine_rel_interior_Int:
   fixes S T :: "'n::euclidean_space set"
   assumes "convex S"
     and "affine T"
@@ -8945,6 +8441,16 @@
     using convex_rel_interior_inter_two[of S T] assms affine_imp_convex by auto
 qed
 
+lemma convex_affine_rel_frontier_Int:
+   fixes S T :: "'n::euclidean_space set"
+  assumes "convex S"
+    and "affine T"
+    and "interior S \<inter> T \<noteq> {}"
+  shows "rel_frontier(S \<inter> T) = frontier S \<inter> T"
+using assms
+apply (simp add: rel_frontier_def convex_affine_closure_Int frontier_def)
+by (metis Diff_Int_distrib2 Int_emptyI convex_affine_closure_Int convex_affine_rel_interior_Int empty_iff interior_rel_interior_gen)
+
 lemma subset_rel_interior_convex:
   fixes S T :: "'n::euclidean_space set"
   assumes "convex S"
@@ -9087,7 +8593,7 @@
     moreover have "affine (range f)"
       by (metis assms(1) subspace_UNIV subspace_imp_affine subspace_linear_image)
     ultimately have "f z \<in> rel_interior S"
-      using convex_affine_rel_interior_inter[of S "range f"] assms by auto
+      using convex_affine_rel_interior_Int[of S "range f"] assms by auto
     then have "z \<in> f -` (rel_interior S)"
       by auto
   }
@@ -9250,7 +8756,7 @@
     moreover have aff: "affine (fst -` {y})"
       unfolding affine_alt by (simp add: algebra_simps)
     ultimately have **: "rel_interior (S \<inter> fst -` {y}) = rel_interior S \<inter> fst -` {y}"
-      using convex_affine_rel_interior_inter[of S "fst -` {y}"] assms by auto
+      using convex_affine_rel_interior_Int[of S "fst -` {y}"] assms by auto
     have conv: "convex (S \<inter> fst -` {y})"
       using convex_Int assms aff affine_imp_convex by auto
     {
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue May 24 11:39:26 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue May 24 15:08:07 2016 +0100
@@ -2606,7 +2606,7 @@
   assume xc: "x > c"
   let ?A' = "interior A \<inter> {c<..}"
   from c have "c \<in> interior A \<inter> closure {c<..}" by auto
-  also have "\<dots> \<subseteq> closure (interior A \<inter> {c<..})" by (intro open_inter_closure_subset) auto
+  also have "\<dots> \<subseteq> closure (interior A \<inter> {c<..})" by (intro open_Int_closure_subset) auto
   finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
   moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) \<longlongrightarrow> f') (at c within ?A')"
     unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
@@ -2628,7 +2628,7 @@
   assume xc: "x < c"
   let ?A' = "interior A \<inter> {..<c}"
   from c have "c \<in> interior A \<inter> closure {..<c}" by auto
-  also have "\<dots> \<subseteq> closure (interior A \<inter> {..<c})" by (intro open_inter_closure_subset) auto
+  also have "\<dots> \<subseteq> closure (interior A \<inter> {..<c})" by (intro open_Int_closure_subset) auto
   finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
   moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) \<longlongrightarrow> f') (at c within ?A')"
     unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
--- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Tue May 24 11:39:26 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Tue May 24 15:08:07 2016 +0100
@@ -3,6 +3,7 @@
   Fashoda
   Extended_Real_Limits
   Determinants
+  Homeomorphism
   Ordered_Euclidean_Space
   Bounded_Continuous_Function
   Weierstrass
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Tue May 24 11:39:26 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Tue May 24 15:08:07 2016 +0100
@@ -5252,7 +5252,6 @@
 
 subsection\<open>Existence of isometry between subspaces of same dimension\<close>
 
-thm subspace_isomorphism
 lemma isometry_subset_subspace:
   fixes S :: "'a::euclidean_space set"
     and T :: "'b::euclidean_space set"
@@ -5412,7 +5411,6 @@
     done
 qed
 
-(*REPLACE*)
 lemma isometry_subspaces:
   fixes S :: "'a::euclidean_space set"
     and T :: "'b::euclidean_space set"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue May 24 11:39:26 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue May 24 15:08:07 2016 +0100
@@ -1853,7 +1853,7 @@
   unfolding closure_interior
   by auto
 
-lemma open_inter_closure_subset:
+lemma open_Int_closure_subset:
   "open S \<Longrightarrow> (S \<inter> (closure T)) \<subseteq> closure(S \<inter> T)"
 proof
   fix x
@@ -2643,6 +2643,29 @@
     by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult)
 qed
 
+lemma lim_null_scaleR_bounded:
+  assumes f: "(f \<longlongrightarrow> 0) net" and gB: "eventually (\<lambda>a. f a = 0 \<or> norm(g a) \<le> B) net"
+    shows "((\<lambda>n. f n *\<^sub>R g n) \<longlongrightarrow> 0) net"
+proof
+  fix \<epsilon>::real
+  assume "0 < \<epsilon>"
+  then have B: "0 < \<epsilon> / (abs B + 1)" by simp
+  have *: "\<bar>f x\<bar> * norm (g x) < \<epsilon>" if f: "\<bar>f x\<bar> * (\<bar>B\<bar> + 1) < \<epsilon>" and g: "norm (g x) \<le> B" for x
+  proof -
+    have "\<bar>f x\<bar> * norm (g x) \<le> \<bar>f x\<bar> * B"
+      by (simp add: mult_left_mono g)
+    also have "... \<le> \<bar>f x\<bar> * (\<bar>B\<bar> + 1)"
+      by (simp add: mult_left_mono)
+    also have "... < \<epsilon>"
+      by (rule f)
+    finally show ?thesis .
+  qed
+  show "\<forall>\<^sub>F x in net. dist (f x *\<^sub>R g x) 0 < \<epsilon>"
+    apply (rule eventually_mono [OF eventually_conj [OF tendstoD [OF f B] gB] ])
+    apply (auto simp: \<open>0 < \<epsilon>\<close> divide_simps * split: if_split_asm)
+    done
+qed
+
 text\<open>Deducing things about the limit from the elements.\<close>
 
 lemma Lim_in_closed_set:
@@ -3986,7 +4009,7 @@
   with x have "x \<in> closure X - closure (-S)"
     by auto
   also have "\<dots> \<subseteq> closure (X \<inter> S)"
-    using \<open>open S\<close> open_inter_closure_subset[of S X] by (simp add: closed_Compl ac_simps)
+    using \<open>open S\<close> open_Int_closure_subset[of S X] by (simp add: closed_Compl ac_simps)
   finally have "X \<inter> S \<noteq> {}" by auto
   then show False using \<open>X \<inter> A = {}\<close> \<open>S \<subseteq> A\<close> by auto
 next
--- a/src/HOL/Real_Vector_Spaces.thy	Tue May 24 11:39:26 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue May 24 15:08:07 2016 +0100
@@ -1754,7 +1754,7 @@
   "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
   unfolding nhds_metric filterlim_INF filterlim_principal by auto
 
-lemma (in metric_space) tendstoI: "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F) \<Longrightarrow> (f \<longlongrightarrow> l) F"
+lemma (in metric_space) tendstoI [intro?]: "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F) \<Longrightarrow> (f \<longlongrightarrow> l) F"
   by (auto simp: tendsto_iff)
 
 lemma (in metric_space) tendstoD: "(f \<longlongrightarrow> l) F \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F"