Lots of new material for multivariate analysis
authorpaulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 6311427afe7af7379
parent 63107 932cf444f2fe
child 63115 39dca4891601
Lots of new material for multivariate analysis
src/HOL/Complex.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Set.thy
src/HOL/Set_Interval.thy
     1.1 --- a/src/HOL/Complex.thy	Sat May 21 07:08:59 2016 +0200
     1.2 +++ b/src/HOL/Complex.thy	Mon May 23 15:33:24 2016 +0100
     1.3 @@ -799,9 +799,15 @@
     1.4  lemma exp_pi_i [simp]: "exp(of_real pi * ii) = -1"
     1.5    by (metis cis_conv_exp cis_pi mult.commute)
     1.6  
     1.7 +lemma exp_pi_i' [simp]: "exp(ii * of_real pi) = -1"
     1.8 +  using cis_conv_exp cis_pi by auto
     1.9 +
    1.10  lemma exp_two_pi_i [simp]: "exp(2 * of_real pi * ii) = 1"
    1.11    by (simp add: exp_eq_polar complex_eq_iff)
    1.12  
    1.13 +lemma exp_two_pi_i' [simp]: "exp (\<i> * (of_real pi * 2)) = 1"
    1.14 +  by (metis exp_two_pi_i mult.commute)
    1.15 +
    1.16  subsubsection \<open>Complex argument\<close>
    1.17  
    1.18  definition arg :: "complex \<Rightarrow> real" where
     2.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat May 21 07:08:59 2016 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon May 23 15:33:24 2016 +0100
     2.3 @@ -1,9 +1,8 @@
     2.4  (*  Title:      HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
     2.5 -    Author:     Robert Himmelmann, TU Muenchen
     2.6 -    Author:     Bogdan Grechuk, University of Edinburgh
     2.7 +    Authors: Robert Himmelmann, TU Muenchen; Bogdan Grechuk, University of Edinburgh; LCP
     2.8  *)
     2.9  
    2.10 -section \<open>Convex sets, functions and related things.\<close>
    2.11 +section \<open>Convex sets, functions and related things\<close>
    2.12  
    2.13  theory Convex_Euclidean_Space
    2.14  imports
    2.15 @@ -70,7 +69,7 @@
    2.16    also have "\<dots> \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. f (x - y) = 0 \<longrightarrow> x - y = 0)"
    2.17      by (simp add: linear_sub[OF lf])
    2.18    also have "\<dots> \<longleftrightarrow> (\<forall>x \<in> S. f x = 0 \<longrightarrow> x = 0)"
    2.19 -    using \<open>subspace S\<close> subspace_def[of S] subspace_sub[of S] by auto
    2.20 +    using \<open>subspace S\<close> subspace_def[of S] subspace_diff[of S] by auto
    2.21    finally show ?thesis .
    2.22  qed
    2.23  
    2.24 @@ -426,6 +425,12 @@
    2.25  lemma affine_Int[intro]: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)"
    2.26    unfolding affine_def by auto
    2.27  
    2.28 +lemma affine_scaling: "affine s \<Longrightarrow> affine (image (\<lambda>x. c *\<^sub>R x) s)"
    2.29 +  apply (clarsimp simp add: affine_def)
    2.30 +  apply (rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in image_eqI)
    2.31 +  apply (auto simp: algebra_simps)
    2.32 +  done
    2.33 +
    2.34  lemma affine_affine_hull [simp]: "affine(affine hull s)"
    2.35    unfolding hull_def
    2.36    using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"] by auto
    2.37 @@ -2915,11 +2920,16 @@
    2.38  
    2.39  lemma aff_dim_subspace:
    2.40    fixes S :: "'n::euclidean_space set"
    2.41 -  assumes "S \<noteq> {}"
    2.42 -    and "subspace S"
    2.43 +  assumes "subspace S"
    2.44    shows "aff_dim S = int (dim S)"
    2.45 -  using aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S]
    2.46 -  by auto
    2.47 +proof (cases "S={}")
    2.48 +  case True with assms show ?thesis
    2.49 +    by (simp add: subspace_affine)
    2.50 +next
    2.51 +  case False
    2.52 +  with aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S] subspace_affine
    2.53 +  show ?thesis by auto
    2.54 +qed
    2.55  
    2.56  lemma aff_dim_zero:
    2.57    fixes S :: "'n::euclidean_space set"
    2.58 @@ -2964,6 +2974,41 @@
    2.59    then show ?thesis by auto
    2.60  qed
    2.61  
    2.62 +lemma affine_independent_card_dim_diffs:
    2.63 +  fixes S :: "'a :: euclidean_space set"
    2.64 +  assumes "~ affine_dependent S" "a \<in> S"
    2.65 +    shows "card S = dim {x - a|x. x \<in> S} + 1"
    2.66 +proof -
    2.67 +  have 1: "{b - a|b. b \<in> (S - {a})} \<subseteq> {x - a|x. x \<in> S}" by auto
    2.68 +  have 2: "x - a \<in> span {b - a |b. b \<in> S - {a}}" if "x \<in> S" for x
    2.69 +  proof (cases "x = a")
    2.70 +    case True then show ?thesis by simp
    2.71 +  next
    2.72 +    case False then show ?thesis
    2.73 +      using assms by (blast intro: span_superset that)
    2.74 +  qed
    2.75 +  have "\<not> affine_dependent (insert a S)"
    2.76 +    by (simp add: assms insert_absorb)
    2.77 +  then have 3: "independent {b - a |b. b \<in> S - {a}}"
    2.78 +      using dependent_imp_affine_dependent by fastforce
    2.79 +  have "{b - a |b. b \<in> S - {a}} = (\<lambda>b. b-a) ` (S - {a})"
    2.80 +    by blast
    2.81 +  then have "card {b - a |b. b \<in> S - {a}} = card ((\<lambda>b. b-a) ` (S - {a}))"
    2.82 +    by simp
    2.83 +  also have "... = card (S - {a})"
    2.84 +    by (metis (no_types, lifting) card_image diff_add_cancel inj_onI)
    2.85 +  also have "... = card S - 1"
    2.86 +    by (simp add: aff_independent_finite assms)
    2.87 +  finally have 4: "card {b - a |b. b \<in> S - {a}} = card S - 1" .
    2.88 +  have "finite S"
    2.89 +    by (meson assms aff_independent_finite)
    2.90 +  with \<open>a \<in> S\<close> have "card S \<noteq> 0" by auto
    2.91 +  moreover have "dim {x - a |x. x \<in> S} = card S - 1"
    2.92 +    using 2 by (blast intro: dim_unique [OF 1 _ 3 4])
    2.93 +  ultimately show ?thesis
    2.94 +    by auto
    2.95 +qed
    2.96 +
    2.97  lemma independent_card_le_aff_dim:
    2.98    fixes B :: "'n::euclidean_space set"
    2.99    assumes "B \<subseteq> V"
   2.100 @@ -3361,11 +3406,11 @@
   2.101  lemma affine_hull_sing [simp]: "affine hull {a :: 'n::euclidean_space} = {a}"
   2.102    by (metis affine_hull_eq affine_sing)
   2.103  
   2.104 -lemma rel_interior_sing [simp]: "rel_interior {a :: 'n::euclidean_space} = {a}"
   2.105 -  unfolding rel_interior_ball affine_hull_sing
   2.106 -  apply auto
   2.107 -  apply (rule_tac x = "1 :: real" in exI)
   2.108 -  apply simp
   2.109 +lemma rel_interior_sing [simp]:
   2.110 +    fixes a :: "'n::euclidean_space"  shows "rel_interior {a} = {a}"
   2.111 +  apply (auto simp: rel_interior_ball)
   2.112 +  apply (rule_tac x=1 in exI)
   2.113 +  apply force
   2.114    done
   2.115  
   2.116  lemma subset_rel_interior:
   2.117 @@ -3671,7 +3716,7 @@
   2.118    ultimately show ?thesis by auto
   2.119  qed
   2.120  
   2.121 -lemma closure_aff_dim:
   2.122 +lemma closure_aff_dim [simp]:
   2.123    fixes S :: "'n::euclidean_space set"
   2.124    shows "aff_dim (closure S) = aff_dim S"
   2.125  proof -
   2.126 @@ -3911,7 +3956,7 @@
   2.127        moreover have "f x - f xy = f (x - xy)"
   2.128          using assms linear_sub[of f x xy] linear_conv_bounded_linear[of f] by auto
   2.129        moreover have *: "x - xy \<in> span S"
   2.130 -        using subspace_sub[of "span S" x xy] subspace_span \<open>x \<in> S\<close> xy
   2.131 +        using subspace_diff[of "span S" x xy] subspace_span \<open>x \<in> S\<close> xy
   2.132            affine_hull_subset_span[of S] span_inc
   2.133          by auto
   2.134        moreover from * have "e1 * norm (x - xy) \<le> norm (f (x - xy))"
   2.135 @@ -6570,6 +6615,17 @@
   2.136      "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> open_segment (f a) (f b) = f ` (open_segment a b)"
   2.137    by (force simp: open_segment_def closed_segment_linear_image inj_on_def)
   2.138  
   2.139 +lemma closed_segment_translation:
   2.140 +    "closed_segment (c + a) (c + b) = image (\<lambda>x. c + x) (closed_segment a b)"
   2.141 +apply safe
   2.142 +apply (rule_tac x="x-c" in image_eqI)
   2.143 +apply (auto simp: in_segment algebra_simps)
   2.144 +done
   2.145 +
   2.146 +lemma open_segment_translation:
   2.147 +    "open_segment (c + a) (c + b) = image (\<lambda>x. c + x) (open_segment a b)"
   2.148 +by (simp add: open_segment_def closed_segment_translation translation_diff)
   2.149 +
   2.150  lemma open_segment_PairD:
   2.151      "(x, x') \<in> open_segment (a, a') (b, b')
   2.152       \<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')"
   2.153 @@ -6782,6 +6838,118 @@
   2.154    fixes u::real shows "closed_segment u v = (\<lambda>x. (v - u) * x + u) ` {0..1}"
   2.155    by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl)
   2.156  
   2.157 +lemma dist_in_closed_segment:
   2.158 +  fixes a :: "'a :: euclidean_space"
   2.159 +  assumes "x \<in> closed_segment a b"
   2.160 +    shows "dist x a \<le> dist a b \<and> dist x b \<le> dist a b"
   2.161 +proof (intro conjI)
   2.162 +  obtain u where u: "0 \<le> u" "u \<le> 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
   2.163 +    using assms by (force simp: in_segment algebra_simps)
   2.164 +  have "dist x a = u * dist a b"
   2.165 +    apply (simp add: dist_norm algebra_simps x)
   2.166 +    by (metis \<open>0 \<le> u\<close> abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib)
   2.167 +  also have "...  \<le> dist a b"
   2.168 +    by (simp add: mult_left_le_one_le u)
   2.169 +  finally show "dist x a \<le> dist a b" .
   2.170 +  have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)"
   2.171 +    by (simp add: dist_norm algebra_simps x)
   2.172 +  also have "... = (1-u) * dist a b"
   2.173 +  proof -
   2.174 +    have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
   2.175 +      using \<open>u \<le> 1\<close> by force
   2.176 +    then show ?thesis
   2.177 +      by (simp add: dist_norm real_vector.scale_right_diff_distrib)
   2.178 +  qed
   2.179 +  also have "... \<le> dist a b"
   2.180 +    by (simp add: mult_left_le_one_le u)
   2.181 +  finally show "dist x b \<le> dist a b" .
   2.182 +qed
   2.183 +
   2.184 +lemma dist_in_open_segment:
   2.185 +  fixes a :: "'a :: euclidean_space"
   2.186 +  assumes "x \<in> open_segment a b"
   2.187 +    shows "dist x a < dist a b \<and> dist x b < dist a b"
   2.188 +proof (intro conjI)
   2.189 +  obtain u where u: "0 < u" "u < 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
   2.190 +    using assms by (force simp: in_segment algebra_simps)
   2.191 +  have "dist x a = u * dist a b"
   2.192 +    apply (simp add: dist_norm algebra_simps x)
   2.193 +    by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib \<open>0 < u\<close>)
   2.194 +  also have *: "...  < dist a b"
   2.195 +    by (metis (no_types) assms dist_eq_0_iff dist_not_less_zero in_segment(2) linorder_neqE_linordered_idom mult.left_neutral real_mult_less_iff1 \<open>u < 1\<close>)
   2.196 +  finally show "dist x a < dist a b" .
   2.197 +  have ab_ne0: "dist a b \<noteq> 0"
   2.198 +    using * by fastforce
   2.199 +  have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)"
   2.200 +    by (simp add: dist_norm algebra_simps x)
   2.201 +  also have "... = (1-u) * dist a b"
   2.202 +  proof -
   2.203 +    have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
   2.204 +      using \<open>u < 1\<close> by force
   2.205 +    then show ?thesis
   2.206 +      by (simp add: dist_norm real_vector.scale_right_diff_distrib)
   2.207 +  qed
   2.208 +  also have "... < dist a b"
   2.209 +    using ab_ne0 \<open>0 < u\<close> by simp
   2.210 +  finally show "dist x b < dist a b" .
   2.211 +qed
   2.212 +
   2.213 +lemma dist_decreases_open_segment_0:
   2.214 +  fixes x :: "'a :: euclidean_space"
   2.215 +  assumes "x \<in> open_segment 0 b"
   2.216 +    shows "dist c x < dist c 0 \<or> dist c x < dist c b"
   2.217 +proof (rule ccontr, clarsimp simp: not_less)
   2.218 +  obtain u where u: "0 \<noteq> b" "0 < u" "u < 1" and x: "x = u *\<^sub>R b"
   2.219 +    using assms by (auto simp: in_segment)
   2.220 +  have xb: "x \<bullet> b < b \<bullet> b"
   2.221 +    using u x by auto
   2.222 +  assume "norm c \<le> dist c x"
   2.223 +  then have "c \<bullet> c \<le> (c - x) \<bullet> (c - x)"
   2.224 +    by (simp add: dist_norm norm_le)
   2.225 +  moreover have "0 < x \<bullet> b"
   2.226 +    using u x by auto
   2.227 +  ultimately have less: "c \<bullet> b < x \<bullet> b"
   2.228 +    by (simp add: x algebra_simps inner_commute u)
   2.229 +  assume "dist c b \<le> dist c x"
   2.230 +  then have "(c - b) \<bullet> (c - b) \<le> (c - x) \<bullet> (c - x)"
   2.231 +    by (simp add: dist_norm norm_le)
   2.232 +  then have "(b \<bullet> b) * (1 - u*u) \<le> 2 * (b \<bullet> c) * (1-u)"
   2.233 +    by (simp add: x algebra_simps inner_commute)
   2.234 +  then have "(1+u) * (b \<bullet> b) * (1-u) \<le> 2 * (b \<bullet> c) * (1-u)"
   2.235 +    by (simp add: algebra_simps)
   2.236 +  then have "(1+u) * (b \<bullet> b) \<le> 2 * (b \<bullet> c)"
   2.237 +    using \<open>u < 1\<close> by auto
   2.238 +  with xb have "c \<bullet> b \<ge> x \<bullet> b"
   2.239 +    by (auto simp: x algebra_simps inner_commute)
   2.240 +  with less show False by auto
   2.241 +qed
   2.242 +
   2.243 +proposition dist_decreases_open_segment:
   2.244 +  fixes a :: "'a :: euclidean_space"
   2.245 +  assumes "x \<in> open_segment a b"
   2.246 +    shows "dist c x < dist c a \<or> dist c x < dist c b"
   2.247 +proof -
   2.248 +  have *: "x - a \<in> open_segment 0 (b - a)" using assms
   2.249 +    by (metis diff_self open_segment_translation_eq uminus_add_conv_diff)
   2.250 +  show ?thesis
   2.251 +    using dist_decreases_open_segment_0 [OF *, of "c-a"] assms
   2.252 +    by (simp add: dist_norm)
   2.253 +qed
   2.254 +
   2.255 +lemma dist_decreases_closed_segment:
   2.256 +  fixes a :: "'a :: euclidean_space"
   2.257 +  assumes "x \<in> closed_segment a b"
   2.258 +    shows "dist c x \<le> dist c a \<or> dist c x \<le> dist c b"
   2.259 +apply (cases "x \<in> open_segment a b")
   2.260 + using dist_decreases_open_segment less_eq_real_def apply blast
   2.261 +by (metis DiffI assms empty_iff insertE open_segment_def order_refl)
   2.262 +
   2.263 +lemma convex_intermediate_ball:
   2.264 +  fixes a :: "'a :: euclidean_space"
   2.265 +  shows "\<lbrakk>ball a r \<subseteq> T; T \<subseteq> cball a r\<rbrakk> \<Longrightarrow> convex T"
   2.266 +apply (simp add: convex_contains_open_segment, clarify)
   2.267 +by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment)
   2.268 +
   2.269  subsubsection\<open>More lemmas, especially for working with the underlying formula\<close>
   2.270  
   2.271  lemma segment_eq_compose:
   2.272 @@ -8157,6 +8325,28 @@
   2.273  
   2.274  definition "rel_frontier S = closure S - rel_interior S"
   2.275  
   2.276 +lemma rel_frontier_empty [simp]: "rel_frontier {} = {}"
   2.277 +  by (simp add: rel_frontier_def)
   2.278 +
   2.279 +lemma rel_frontier_sing [simp]:
   2.280 +    fixes a :: "'n::euclidean_space"
   2.281 +    shows "rel_frontier {a} = {}"
   2.282 +  by (simp add: rel_frontier_def)
   2.283 +
   2.284 +lemma rel_frontier_cball [simp]:
   2.285 +    fixes a :: "'n::euclidean_space"
   2.286 +    shows "rel_frontier(cball a r) = (if r = 0 then {} else sphere a r)"
   2.287 +proof (cases rule: linorder_cases [of r 0])
   2.288 +  case less then show ?thesis
   2.289 +    by (force simp: sphere_def)
   2.290 +next
   2.291 +  case equal then show ?thesis by simp
   2.292 +next
   2.293 +  case greater then show ?thesis
   2.294 +    apply simp
   2.295 +    by (metis centre_in_ball empty_iff frontier_cball frontier_def interior_cball interior_rel_interior_gen rel_frontier_def)
   2.296 +qed
   2.297 +
   2.298  lemma closed_affine_hull:
   2.299    fixes S :: "'n::euclidean_space set"
   2.300    shows "closed (affine hull S)"
   2.301 @@ -8190,6 +8380,43 @@
   2.302      done
   2.303  qed
   2.304  
   2.305 +lemma closed_rel_boundary:
   2.306 +  fixes S :: "'n::euclidean_space set"
   2.307 +  shows "closed S \<Longrightarrow> closed(S - rel_interior S)"
   2.308 +by (metis closed_rel_frontier closure_closed rel_frontier_def)
   2.309 +
   2.310 +lemma compact_rel_boundary:
   2.311 +  fixes S :: "'n::euclidean_space set"
   2.312 +  shows "compact S \<Longrightarrow> compact(S - rel_interior S)"
   2.313 +by (metis bounded_diff closed_rel_boundary closure_eq compact_closure compact_imp_closed)
   2.314 +
   2.315 +lemma bounded_rel_frontier:
   2.316 +  fixes S :: "'n::euclidean_space set"
   2.317 +  shows "bounded S \<Longrightarrow> bounded(rel_frontier S)"
   2.318 +by (simp add: bounded_closure bounded_diff rel_frontier_def)
   2.319 +
   2.320 +lemma compact_rel_frontier_bounded:
   2.321 +  fixes S :: "'n::euclidean_space set"
   2.322 +  shows "bounded S \<Longrightarrow> compact(rel_frontier S)"
   2.323 +using bounded_rel_frontier closed_rel_frontier compact_eq_bounded_closed by blast
   2.324 +
   2.325 +lemma compact_rel_frontier:
   2.326 +  fixes S :: "'n::euclidean_space set"
   2.327 +  shows "compact S \<Longrightarrow> compact(rel_frontier S)"
   2.328 +by (meson compact_eq_bounded_closed compact_rel_frontier_bounded)
   2.329 +
   2.330 +lemma convex_same_rel_interior_closure:
   2.331 +  fixes S :: "'n::euclidean_space set"
   2.332 +  shows "\<lbrakk>convex S; convex T\<rbrakk>
   2.333 +         \<Longrightarrow> rel_interior S = rel_interior T \<longleftrightarrow> closure S = closure T"
   2.334 +by (simp add: closure_eq_rel_interior_eq)
   2.335 +
   2.336 +lemma convex_same_rel_interior_closure_straddle:
   2.337 +  fixes S :: "'n::euclidean_space set"
   2.338 +  shows "\<lbrakk>convex S; convex T\<rbrakk>
   2.339 +         \<Longrightarrow> rel_interior S = rel_interior T \<longleftrightarrow>
   2.340 +             rel_interior S \<subseteq> T \<and> T \<subseteq> closure S"
   2.341 +by (simp add: closure_eq_between convex_same_rel_interior_closure)
   2.342  
   2.343  lemma convex_rel_frontier_aff_dim:
   2.344    fixes S1 S2 :: "'n::euclidean_space set"
   2.345 @@ -10701,6 +10928,16 @@
   2.346    shows "setdist s {x} = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
   2.347  by (auto simp: setdist_eq_0_bounded)
   2.348  
   2.349 +lemma setdist_neq_0_sing_1:
   2.350 +    fixes s :: "'a::euclidean_space set"
   2.351 +    shows "\<lbrakk>setdist {x} s = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> s \<noteq> {} \<and> x \<notin> closure s"
   2.352 +by auto
   2.353 +
   2.354 +lemma setdist_neq_0_sing_2:
   2.355 +  fixes s :: "'a::euclidean_space set"
   2.356 +    shows "\<lbrakk>setdist s {x} = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> s \<noteq> {} \<and> x \<notin> closure s"
   2.357 +by auto
   2.358 +
   2.359  lemma setdist_sing_in_set:
   2.360    fixes s :: "'a::euclidean_space set"
   2.361    shows "x \<in> s \<Longrightarrow> setdist {x} s = 0"
   2.362 @@ -12046,6 +12283,42 @@
   2.363      done
   2.364  qed
   2.365  
   2.366 +proposition orthonormal_basis_subspace:
   2.367 +  fixes S :: "'a :: euclidean_space set"
   2.368 +  assumes "subspace S"
   2.369 +  obtains B where "B \<subseteq> S" "pairwise orthogonal B"
   2.370 +              and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
   2.371 +              and "independent B" "card B = dim S" "span B = S"
   2.372 +proof -
   2.373 +  obtain B where "0 \<notin> B" "B \<subseteq> S"
   2.374 +             and orth: "pairwise orthogonal B"
   2.375 +             and "independent B" "card B = dim S" "span B = S"
   2.376 +    by (blast intro: orthogonal_basis_subspace [OF assms])
   2.377 +  have 1: "(\<lambda>x. x /\<^sub>R norm x) ` B \<subseteq> S"
   2.378 +    using \<open>span B = S\<close> span_clauses(1) span_mul by fastforce
   2.379 +  have 2: "pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` B)"
   2.380 +    using orth by (force simp: pairwise_def orthogonal_clauses)
   2.381 +  have 3: "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` B \<Longrightarrow> norm x = 1"
   2.382 +    by (metis (no_types, lifting) \<open>0 \<notin> B\<close> image_iff norm_sgn sgn_div_norm)
   2.383 +  have 4: "independent ((\<lambda>x. x /\<^sub>R norm x) ` B)"
   2.384 +    by (metis "2" "3" norm_zero pairwise_orthogonal_independent zero_neq_one)
   2.385 +  have "inj_on (\<lambda>x. x /\<^sub>R norm x) B"
   2.386 +  proof
   2.387 +    fix x y
   2.388 +    assume "x \<in> B" "y \<in> B" "x /\<^sub>R norm x = y /\<^sub>R norm y"
   2.389 +    moreover have "\<And>i. i \<in> B \<Longrightarrow> norm (i /\<^sub>R norm i) = 1"
   2.390 +      using 3 by blast
   2.391 +    ultimately show "x = y"
   2.392 +      by (metis norm_eq_1 orth orthogonal_clauses(7) orthogonal_commute orthogonal_def pairwise_def zero_neq_one)
   2.393 +  qed
   2.394 +  then have 5: "card ((\<lambda>x. x /\<^sub>R norm x) ` B) = dim S"
   2.395 +    by (metis \<open>card B = dim S\<close> card_image)
   2.396 +  have 6: "span ((\<lambda>x. x /\<^sub>R norm x) ` B) = S"
   2.397 +    by (metis "1" "4" "5" assms card_eq_dim independent_finite span_subspace)
   2.398 +  show ?thesis
   2.399 +    by (rule that [OF 1 2 3 4 5 6])
   2.400 +qed
   2.401 +
   2.402  proposition orthogonal_subspace_decomp_exists:
   2.403    fixes S :: "'a :: euclidean_space set"
   2.404    obtains y z where "y \<in> span S" "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" "x = y + z"
   2.405 @@ -12078,6 +12351,7 @@
   2.406    with assms show ?thesis by auto
   2.407  qed
   2.408  
   2.409 +subsection\<open>Parallel slices, etc.\<close>
   2.410  
   2.411  text\<open> If we take a slice out of a set, we can do it perpendicularly,
   2.412    with the normal vector to the slice parallel to the affine hull.\<close>
   2.413 @@ -12139,4 +12413,167 @@
   2.414    qed
   2.415  qed
   2.416  
   2.417 +lemma diffs_affine_hull_span:
   2.418 +  assumes "a \<in> S"
   2.419 +    shows "{x - a |x. x \<in> affine hull S} = span {x - a |x. x \<in> S}"
   2.420 +proof -
   2.421 +  have *: "((\<lambda>x. x - a) ` (S - {a})) = {x. x + a \<in> S} - {0}"
   2.422 +    by (auto simp: algebra_simps)
   2.423 +  show ?thesis
   2.424 +    apply (simp add: affine_hull_span2 [OF assms] *)
   2.425 +    apply (auto simp: algebra_simps)
   2.426 +    done
   2.427 +qed
   2.428 +
   2.429 +lemma aff_dim_dim_affine_diffs:
   2.430 +  fixes S :: "'a :: euclidean_space set"
   2.431 +  assumes "affine S" "a \<in> S"
   2.432 +    shows "aff_dim S = dim {x - a |x. x \<in> S}"
   2.433 +proof -
   2.434 +  obtain B where aff: "affine hull B = affine hull S"
   2.435 +             and ind: "\<not> affine_dependent B"
   2.436 +             and card: "of_nat (card B) = aff_dim S + 1"
   2.437 +    using aff_dim_basis_exists by blast
   2.438 +  then have "B \<noteq> {}" using assms
   2.439 +    by (metis affine_hull_eq_empty ex_in_conv)
   2.440 +  then obtain c where "c \<in> B" by auto
   2.441 +  then have "c \<in> S"
   2.442 +    by (metis aff affine_hull_eq \<open>affine S\<close> hull_inc)
   2.443 +  have xy: "x - c = y - a \<longleftrightarrow> y = x + 1 *\<^sub>R (a - c)" for x y c and a::'a
   2.444 +    by (auto simp: algebra_simps)
   2.445 +  have *: "{x - c |x. x \<in> S} = {x - a |x. x \<in> S}"
   2.446 +    apply safe
   2.447 +    apply (simp_all only: xy)
   2.448 +    using mem_affine_3_minus [OF \<open>affine S\<close>] \<open>a \<in> S\<close> \<open>c \<in> S\<close> apply blast+
   2.449 +    done
   2.450 +  have affS: "affine hull S = S"
   2.451 +    by (simp add: \<open>affine S\<close>)
   2.452 +  have "aff_dim S = of_nat (card B) - 1"
   2.453 +    using card by simp
   2.454 +  also have "... = dim {x - c |x. x \<in> B}"
   2.455 +    by (simp add: affine_independent_card_dim_diffs [OF ind \<open>c \<in> B\<close>])
   2.456 +  also have "... = dim {x - c | x. x \<in> affine hull B}"
   2.457 +     by (simp add: diffs_affine_hull_span \<open>c \<in> B\<close>)
   2.458 +  also have "... = dim {x - a |x. x \<in> S}"
   2.459 +     by (simp add: affS aff *)
   2.460 +   finally show ?thesis .
   2.461 +qed
   2.462 +
   2.463 +lemma aff_dim_linear_image_le:
   2.464 +  assumes "linear f"
   2.465 +    shows "aff_dim(f ` S) \<le> aff_dim S"
   2.466 +proof -
   2.467 +  have "aff_dim (f ` T) \<le> aff_dim T" if "affine T" for T
   2.468 +  proof (cases "T = {}")
   2.469 +    case True then show ?thesis by (simp add: aff_dim_geq)
   2.470 +  next
   2.471 +    case False
   2.472 +    then obtain a where "a \<in> T" by auto
   2.473 +    have 1: "((\<lambda>x. x - f a) ` f ` T) = {x - f a |x. x \<in> f ` T}"
   2.474 +      by auto
   2.475 +    have 2: "{x - f a| x. x \<in> f ` T} = f ` {x - a| x. x \<in> T}"
   2.476 +      by (force simp: linear_sub [OF assms])
   2.477 +    have "aff_dim (f ` T) = int (dim {x - f a |x. x \<in> f ` T})"
   2.478 +      by (simp add: \<open>a \<in> T\<close> hull_inc aff_dim_eq_dim [of "f a"] 1)
   2.479 +    also have "... = int (dim (f ` {x - a| x. x \<in> T}))"
   2.480 +      by (force simp: linear_sub [OF assms] 2)
   2.481 +    also have "... \<le> int (dim {x - a| x. x \<in> T})"
   2.482 +      by (simp add: dim_image_le [OF assms])
   2.483 +    also have "... \<le> aff_dim T"
   2.484 +      by (simp add: aff_dim_dim_affine_diffs [symmetric] \<open>a \<in> T\<close> \<open>affine T\<close>)
   2.485 +    finally show ?thesis .
   2.486 +  qed
   2.487 +  then
   2.488 +  have "aff_dim (f ` (affine hull S)) \<le> aff_dim (affine hull S)"
   2.489 +    using affine_affine_hull [of S] by blast
   2.490 +  then show ?thesis
   2.491 +    using affine_hull_linear_image assms linear_conv_bounded_linear by fastforce
   2.492 +qed
   2.493 +
   2.494 +lemma aff_dim_injective_linear_image [simp]:
   2.495 +  assumes "linear f" "inj f"
   2.496 +    shows "aff_dim (f ` S) = aff_dim S"
   2.497 +proof (rule antisym)
   2.498 +  show "aff_dim (f ` S) \<le> aff_dim S"
   2.499 +    by (simp add: aff_dim_linear_image_le assms(1))
   2.500 +next
   2.501 +  obtain g where "linear g" "g \<circ> f = id"
   2.502 +    using linear_injective_left_inverse assms by blast
   2.503 +  then have "aff_dim S \<le> aff_dim(g ` f ` S)"
   2.504 +    by (simp add: image_comp)
   2.505 +  also have "... \<le> aff_dim (f ` S)"
   2.506 +    by (simp add: \<open>linear g\<close> aff_dim_linear_image_le)
   2.507 +  finally show "aff_dim S \<le> aff_dim (f ` S)" .
   2.508 +qed
   2.509 +
   2.510 +text\<open>Choosing a subspace of a given dimension\<close>
   2.511 +proposition choose_subspace_of_subspace:
   2.512 +  fixes S :: "'n::euclidean_space set"
   2.513 +  assumes "n \<le> dim S"
   2.514 +  obtains T where "subspace T" "T \<subseteq> span S" "dim T = n"
   2.515 +proof -
   2.516 +  have "\<exists>T. subspace T \<and> T \<subseteq> span S \<and> dim T = n"
   2.517 +  using assms
   2.518 +  proof (induction n)
   2.519 +    case 0 then show ?case by force
   2.520 +  next
   2.521 +    case (Suc n)
   2.522 +    then obtain T where "subspace T" "T \<subseteq> span S" "dim T = n"
   2.523 +      by force
   2.524 +    then show ?case
   2.525 +    proof (cases "span S \<subseteq> span T")
   2.526 +      case True
   2.527 +      have "dim S = dim T"
   2.528 +        apply (rule span_eq_dim [OF subset_antisym [OF True]])
   2.529 +        by (simp add: \<open>T \<subseteq> span S\<close> span_minimal subspace_span)
   2.530 +      then show ?thesis
   2.531 +        using Suc.prems \<open>dim T = n\<close> by linarith
   2.532 +    next
   2.533 +      case False
   2.534 +      then obtain y where y: "y \<in> S" "y \<notin> T"
   2.535 +        by (meson span_mono subsetI)
   2.536 +      then have "span (insert y T) \<subseteq> span S"
   2.537 +        by (metis (no_types) \<open>T \<subseteq> span S\<close> subsetD insert_subset span_inc span_mono span_span)
   2.538 +      with \<open>dim T = n\<close>  \<open>subspace T\<close> span_induct y show ?thesis
   2.539 +        apply (rule_tac x="span(insert y T)" in exI)
   2.540 +        apply (auto simp: subspace_span dim_insert)
   2.541 +        done
   2.542 +    qed
   2.543 +  qed
   2.544 +  with that show ?thesis by blast
   2.545 +qed
   2.546 +
   2.547 +lemma choose_affine_subset:
   2.548 +  assumes "affine S" "-1 \<le> d" and dle: "d \<le> aff_dim S"
   2.549 +  obtains T where "affine T" "T \<subseteq> S" "aff_dim T = d"
   2.550 +proof (cases "d = -1 \<or> S={}")
   2.551 +  case True with assms show ?thesis
   2.552 +    by (metis aff_dim_empty affine_empty bot.extremum that eq_iff)
   2.553 +next
   2.554 +  case False
   2.555 +  with assms obtain a where "a \<in> S" "0 \<le> d" by auto
   2.556 +  with assms have ss: "subspace (op + (- a) ` S)"
   2.557 +    by (simp add: affine_diffs_subspace)
   2.558 +  have "nat d \<le> dim (op + (- a) ` S)"
   2.559 +    by (metis aff_dim_subspace aff_dim_translation_eq dle nat_int nat_mono ss)
   2.560 +  then obtain T where "subspace T" and Tsb: "T \<subseteq> span (op + (- a) ` S)"
   2.561 +                  and Tdim: "dim T = nat d"
   2.562 +    using choose_subspace_of_subspace [of "nat d" "op + (- a) ` S"] by blast
   2.563 +  then have "affine T"
   2.564 +    using subspace_affine by blast
   2.565 +  then have "affine (op + a ` T)"
   2.566 +    by (metis affine_hull_eq affine_hull_translation)
   2.567 +  moreover have "op + a ` T \<subseteq> S"
   2.568 +  proof -
   2.569 +    have "T \<subseteq> op + (- a) ` S"
   2.570 +      by (metis (no_types) span_eq Tsb ss)
   2.571 +    then show "op + a ` T \<subseteq> S"
   2.572 +      using add_ac by auto
   2.573 +  qed
   2.574 +  moreover have "aff_dim (op + a ` T) = d"
   2.575 +    by (simp add: aff_dim_subspace Tdim \<open>0 \<le> d\<close> \<open>subspace T\<close> aff_dim_translation_eq)
   2.576 +  ultimately show ?thesis
   2.577 +    by (rule that)
   2.578 +qed
   2.579 +
   2.580  end
     3.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sat May 21 07:08:59 2016 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon May 23 15:33:24 2016 +0100
     3.3 @@ -110,6 +110,18 @@
     3.4  lemma DIM_ge_Suc0 [iff]: "Suc 0 \<le> card Basis"
     3.5    by (meson DIM_positive Suc_leI)
     3.6  
     3.7 +
     3.8 +lemma setsum_inner_Basis_scaleR [simp]:
     3.9 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_vector"
    3.10 +  assumes "b \<in> Basis" shows "(\<Sum>i\<in>Basis. (inner i b) *\<^sub>R f i) = f b"
    3.11 +  by (simp add: comm_monoid_add_class.setsum.remove [OF finite_Basis assms]
    3.12 +         assms inner_not_same_Basis comm_monoid_add_class.setsum.neutral)
    3.13 +
    3.14 +lemma setsum_inner_Basis_eq [simp]:
    3.15 +  assumes "b \<in> Basis" shows "(\<Sum>i\<in>Basis. (inner i b) * f i) = f b"
    3.16 +  by (simp add: comm_monoid_add_class.setsum.remove [OF finite_Basis assms]
    3.17 +         assms inner_not_same_Basis comm_monoid_add_class.setsum.neutral)
    3.18 +
    3.19  subsection \<open>Subclass relationships\<close>
    3.20  
    3.21  instance euclidean_space \<subseteq> perfect_space
     4.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sat May 21 07:08:59 2016 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon May 23 15:33:24 2016 +0100
     4.3 @@ -223,7 +223,7 @@
     4.4  lemma subspace_neg: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> - x \<in> S"
     4.5    by (metis scaleR_minus1_left subspace_mul)
     4.6  
     4.7 -lemma subspace_sub: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
     4.8 +lemma subspace_diff: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
     4.9    using subspace_add [of S x "- y"] by (simp add: subspace_neg)
    4.10  
    4.11  lemma (in real_vector) subspace_setsum:
    4.12 @@ -434,7 +434,7 @@
    4.13    by (metis subspace_neg subspace_span)
    4.14  
    4.15  lemma span_sub: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
    4.16 -  by (metis subspace_span subspace_sub)
    4.17 +  by (metis subspace_span subspace_diff)
    4.18  
    4.19  lemma (in real_vector) span_setsum: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> span S) \<Longrightarrow> setsum f A \<in> span S"
    4.20    by (rule subspace_setsum [OF subspace_span])
    4.21 @@ -1524,6 +1524,46 @@
    4.22  lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
    4.23    by (simp add: orthogonal_def inner_commute)
    4.24  
    4.25 +lemma orthogonal_scaleR [simp]: "c \<noteq> 0 \<Longrightarrow> orthogonal (c *\<^sub>R x) = orthogonal x"
    4.26 +  by (rule ext) (simp add: orthogonal_def)
    4.27 +
    4.28 +lemma pairwise_ortho_scaleR:
    4.29 +    "pairwise (\<lambda>i j. orthogonal (f i) (g j)) B
    4.30 +    \<Longrightarrow> pairwise (\<lambda>i j. orthogonal (a i *\<^sub>R f i) (a j *\<^sub>R g j)) B"
    4.31 +  by (auto simp: pairwise_def orthogonal_clauses)
    4.32 +
    4.33 +lemma orthogonal_rvsum:
    4.34 +    "\<lbrakk>finite s; \<And>y. y \<in> s \<Longrightarrow> orthogonal x (f y)\<rbrakk> \<Longrightarrow> orthogonal x (setsum f s)"
    4.35 +  by (induction s rule: finite_induct) (auto simp: orthogonal_clauses)
    4.36 +
    4.37 +lemma orthogonal_lvsum:
    4.38 +    "\<lbrakk>finite s; \<And>x. x \<in> s \<Longrightarrow> orthogonal (f x) y\<rbrakk> \<Longrightarrow> orthogonal (setsum f s) y"
    4.39 +  by (induction s rule: finite_induct) (auto simp: orthogonal_clauses)
    4.40 +
    4.41 +lemma norm_add_Pythagorean:
    4.42 +  assumes "orthogonal a b"
    4.43 +    shows "norm(a + b) ^ 2 = norm a ^ 2 + norm b ^ 2"
    4.44 +proof -
    4.45 +  from assms have "(a - (0 - b)) \<bullet> (a - (0 - b)) = a \<bullet> a - (0 - b \<bullet> b)"
    4.46 +    by (simp add: algebra_simps orthogonal_def inner_commute)
    4.47 +  then show ?thesis
    4.48 +    by (simp add: power2_norm_eq_inner)
    4.49 +qed
    4.50 +
    4.51 +lemma norm_setsum_Pythagorean:
    4.52 +  assumes "finite I" "pairwise (\<lambda>i j. orthogonal (f i) (f j)) I"
    4.53 +    shows "(norm (setsum f I))\<^sup>2 = (\<Sum>i\<in>I. (norm (f i))\<^sup>2)"
    4.54 +using assms
    4.55 +proof (induction I rule: finite_induct)
    4.56 +  case empty then show ?case by simp
    4.57 +next
    4.58 +  case (insert x I)
    4.59 +  then have "orthogonal (f x) (setsum f I)"
    4.60 +    by (metis pairwise_insert orthogonal_rvsum)
    4.61 +  with insert show ?case
    4.62 +    by (simp add: pairwise_insert norm_add_Pythagorean)
    4.63 +qed
    4.64 +
    4.65  
    4.66  subsection \<open>Bilinear functions.\<close>
    4.67  
     5.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Sat May 21 07:08:59 2016 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon May 23 15:33:24 2016 +0100
     5.3 @@ -2109,6 +2109,79 @@
     5.4      by (auto simp: closure_def)
     5.5  qed
     5.6  
     5.7 +lemma connected_disjoint_Union_open_pick:
     5.8 +  assumes "pairwise disjnt B"
     5.9 +          "\<And>S. S \<in> A \<Longrightarrow> connected S \<and> S \<noteq> {}"
    5.10 +          "\<And>S. S \<in> B \<Longrightarrow> open S"
    5.11 +          "\<Union>A \<subseteq> \<Union>B"
    5.12 +          "S \<in> A"
    5.13 +  obtains T where "T \<in> B" "S \<subseteq> T" "S \<inter> \<Union>(B - {T}) = {}"
    5.14 +proof -
    5.15 +  have "S \<subseteq> \<Union>B" "connected S" "S \<noteq> {}"
    5.16 +    using assms \<open>S \<in> A\<close> by blast+
    5.17 +  then obtain T where "T \<in> B" "S \<inter> T \<noteq> {}"
    5.18 +    by (metis Sup_inf_eq_bot_iff inf.absorb_iff2 inf_commute)
    5.19 +  have 1: "open T" by (simp add: \<open>T \<in> B\<close> assms)
    5.20 +  have 2: "open (\<Union>(B-{T}))" using assms by blast
    5.21 +  have 3: "S \<subseteq> T \<union> \<Union>(B - {T})" using \<open>S \<subseteq> \<Union>B\<close> by blast
    5.22 +  have "T \<inter> \<Union>(B - {T}) = {}" using \<open>T \<in> B\<close> \<open>pairwise disjnt B\<close>
    5.23 +    by (auto simp: pairwise_def disjnt_def)
    5.24 +  then have 4: "T \<inter> \<Union>(B - {T}) \<inter> S = {}" by auto
    5.25 +  from connectedD [OF \<open>connected S\<close> 1 2 3 4]
    5.26 +  have "S \<inter> \<Union>(B-{T}) = {}"
    5.27 +    by (auto simp: Int_commute \<open>S \<inter> T \<noteq> {}\<close>)
    5.28 +  with \<open>T \<in> B\<close> have "S \<subseteq> T"
    5.29 +    using "3" by auto
    5.30 +  show ?thesis
    5.31 +    using \<open>S \<inter> \<Union>(B - {T}) = {}\<close> \<open>S \<subseteq> T\<close> \<open>T \<in> B\<close> that by auto
    5.32 +qed
    5.33 +
    5.34 +lemma connected_disjoint_Union_open_subset:
    5.35 +  assumes A: "pairwise disjnt A" and B: "pairwise disjnt B"
    5.36 +      and SA: "\<And>S. S \<in> A \<Longrightarrow> open S \<and> connected S \<and> S \<noteq> {}"
    5.37 +      and SB: "\<And>S. S \<in> B \<Longrightarrow> open S \<and> connected S \<and> S \<noteq> {}"
    5.38 +      and eq [simp]: "\<Union>A = \<Union>B"
    5.39 +    shows "A \<subseteq> B"
    5.40 +proof
    5.41 +  fix S
    5.42 +  assume "S \<in> A"
    5.43 +  obtain T where "T \<in> B" "S \<subseteq> T" "S \<inter> \<Union>(B - {T}) = {}"
    5.44 +      apply (rule connected_disjoint_Union_open_pick [OF B, of A])
    5.45 +      using SA SB \<open>S \<in> A\<close> by auto
    5.46 +  moreover obtain S' where "S' \<in> A" "T \<subseteq> S'" "T \<inter> \<Union>(A - {S'}) = {}"
    5.47 +      apply (rule connected_disjoint_Union_open_pick [OF A, of B])
    5.48 +      using SA SB \<open>T \<in> B\<close> by auto
    5.49 +  ultimately have "S' = S"
    5.50 +    by (metis A Int_subset_iff SA \<open>S \<in> A\<close> disjnt_def inf.orderE pairwise_def)
    5.51 +  with \<open>T \<subseteq> S'\<close> have "T \<subseteq> S" by simp
    5.52 +  with \<open>S \<subseteq> T\<close> have "S = T" by blast
    5.53 +  with \<open>T \<in> B\<close> show "S \<in> B" by simp
    5.54 +qed
    5.55 +
    5.56 +lemma connected_disjoint_Union_open_unique:
    5.57 +  assumes A: "pairwise disjnt A" and B: "pairwise disjnt B"
    5.58 +      and SA: "\<And>S. S \<in> A \<Longrightarrow> open S \<and> connected S \<and> S \<noteq> {}"
    5.59 +      and SB: "\<And>S. S \<in> B \<Longrightarrow> open S \<and> connected S \<and> S \<noteq> {}"
    5.60 +      and eq [simp]: "\<Union>A = \<Union>B"
    5.61 +    shows "A = B"
    5.62 +by (rule subset_antisym; metis connected_disjoint_Union_open_subset assms)
    5.63 +
    5.64 +proposition components_open_unique:
    5.65 + fixes S :: "'a::real_normed_vector set"
    5.66 +  assumes "pairwise disjnt A" "\<Union>A = S"
    5.67 +          "\<And>X. X \<in> A \<Longrightarrow> open X \<and> connected X \<and> X \<noteq> {}"
    5.68 +    shows "components S = A"
    5.69 +proof -
    5.70 +  have "open S" using assms by blast
    5.71 +  show ?thesis
    5.72 +    apply (rule connected_disjoint_Union_open_unique)
    5.73 +    apply (simp add: components_eq disjnt_def pairwise_def)
    5.74 +    using \<open>open S\<close>
    5.75 +    apply (simp_all add: assms open_components in_components_connected in_components_nonempty)
    5.76 +    done
    5.77 +qed
    5.78 +
    5.79 +
    5.80  subsection\<open>Existence of unbounded components\<close>
    5.81  
    5.82  lemma cobounded_unbounded_component:
    5.83 @@ -3742,14 +3815,13 @@
    5.84  lemma homotopic_paths_linear:
    5.85    fixes g h :: "real \<Rightarrow> 'a::real_normed_vector"
    5.86    assumes "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g"
    5.87 -          "\<And>t x. t \<in> {0..1} \<Longrightarrow> closed_segment (g t) (h t) \<subseteq> s"
    5.88 +          "\<And>t. t \<in> {0..1} \<Longrightarrow> closed_segment (g t) (h t) \<subseteq> s"
    5.89      shows "homotopic_paths s g h"
    5.90    using assms
    5.91    unfolding path_def
    5.92    apply (simp add: closed_segment_def pathstart_def pathfinish_def homotopic_paths_def homotopic_with_def)
    5.93 -  apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R g(snd y) + (fst y) *\<^sub>R h(snd y))" in exI)
    5.94 -  apply (intro conjI subsetI continuous_intros)
    5.95 -  apply (fastforce intro: continuous_intros continuous_on_compose2 [where g=g] continuous_on_compose2 [where g=h])+
    5.96 +  apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R (g o snd) y + (fst y) *\<^sub>R (h o snd) y)" in exI)
    5.97 +  apply (intro conjI subsetI continuous_intros; force)
    5.98    done
    5.99  
   5.100  lemma homotopic_loops_linear:
   5.101 @@ -5052,6 +5124,346 @@
   5.102  apply (force simp: convex_Int convex_imp_path_connected)
   5.103  done
   5.104  
   5.105 +subsection\<open>Components, continuity, openin, closedin\<close>
   5.106 +
   5.107 +lemma continuous_openin_preimage_eq:
   5.108 +   "continuous_on S f \<longleftrightarrow>
   5.109 +    (\<forall>t. open t \<longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
   5.110 +apply (auto simp: continuous_openin_preimage)
   5.111 +apply (fastforce simp add: continuous_on_open openin_open)
   5.112 +done
   5.113 +
   5.114 +lemma continuous_closedin_preimage_eq:
   5.115 +   "continuous_on S f \<longleftrightarrow>
   5.116 +    (\<forall>t. closed t \<longrightarrow> closedin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
   5.117 +apply safe
   5.118 +apply (simp add: continuous_closedin_preimage)
   5.119 +apply (fastforce simp add: continuous_on_closed closedin_closed)
   5.120 +done
   5.121 +
   5.122 +lemma continuous_on_components_gen:
   5.123 + fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   5.124 +  assumes "\<And>c. c \<in> components S \<Longrightarrow>
   5.125 +              openin (subtopology euclidean S) c \<and> continuous_on c f"
   5.126 +    shows "continuous_on S f"
   5.127 +proof (clarsimp simp: continuous_openin_preimage_eq)
   5.128 +  fix t :: "'b set"
   5.129 +  assume "open t"
   5.130 +  have "{x. x \<in> S \<and> f x \<in> t} = \<Union>{{x. x \<in> c \<and> f x \<in> t} |c. c \<in> components S}"
   5.131 +    apply auto
   5.132 +    apply (metis (lifting) components_iff connected_component_refl_eq mem_Collect_eq)
   5.133 +    using Union_components by blast
   5.134 +  then show "openin (subtopology euclidean S) {x \<in> S. f x \<in> t}"
   5.135 +    using \<open>open t\<close> assms
   5.136 +    by (fastforce intro: openin_trans continuous_openin_preimage)
   5.137 +qed
   5.138 +
   5.139 +lemma continuous_on_components:
   5.140 + fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   5.141 +  assumes "locally connected S "
   5.142 +          "\<And>c. c \<in> components S \<Longrightarrow> continuous_on c f"
   5.143 +    shows "continuous_on S f"
   5.144 +apply (rule continuous_on_components_gen)
   5.145 +apply (auto simp: assms intro: openin_components_locally_connected)
   5.146 +done
   5.147 +
   5.148 +lemma continuous_on_components_eq:
   5.149 +    "locally connected S
   5.150 +     \<Longrightarrow> (continuous_on S f \<longleftrightarrow> (\<forall>c \<in> components S. continuous_on c f))"
   5.151 +by (meson continuous_on_components continuous_on_subset in_components_subset)
   5.152 +
   5.153 +lemma continuous_on_components_open:
   5.154 + fixes S :: "'a::real_normed_vector set"
   5.155 +  assumes "open S "
   5.156 +          "\<And>c. c \<in> components S \<Longrightarrow> continuous_on c f"
   5.157 +    shows "continuous_on S f"
   5.158 +using continuous_on_components open_imp_locally_connected assms by blast
   5.159 +
   5.160 +lemma continuous_on_components_open_eq:
   5.161 +  fixes S :: "'a::real_normed_vector set"
   5.162 +  shows "open S \<Longrightarrow> (continuous_on S f \<longleftrightarrow> (\<forall>c \<in> components S. continuous_on c f))"
   5.163 +using continuous_on_subset in_components_subset
   5.164 +by (blast intro: continuous_on_components_open)
   5.165 +
   5.166 +lemma closedin_union_complement_components:
   5.167 +  assumes u: "locally connected u"
   5.168 +      and S: "closedin (subtopology euclidean u) S"
   5.169 +      and cuS: "c \<subseteq> components(u - S)"
   5.170 +    shows "closedin (subtopology euclidean u) (S \<union> \<Union>c)"
   5.171 +proof -
   5.172 +  have di: "(\<And>S t. S \<in> c \<and> t \<in> c' \<Longrightarrow> disjnt S t) \<Longrightarrow> disjnt (\<Union> c) (\<Union> c')" for c'
   5.173 +    by (simp add: disjnt_def) blast
   5.174 +  have "S \<subseteq> u"
   5.175 +    using S closedin_imp_subset by blast
   5.176 +  moreover have "u - S = \<Union>c \<union> \<Union>(components (u - S) - c)"
   5.177 +    by (metis Diff_partition Topology_Euclidean_Space.Union_components Union_Un_distrib assms(3))
   5.178 +  moreover have "disjnt (\<Union>c) (\<Union>(components (u - S) - c))"
   5.179 +    apply (rule di)
   5.180 +    by (metis DiffD1 DiffD2 assms(3) components_nonoverlap disjnt_def subsetCE)
   5.181 +  ultimately have eq: "S \<union> \<Union>c = u - (\<Union>(components(u - S) - c))"
   5.182 +    by (auto simp: disjnt_def)
   5.183 +  have *: "openin (subtopology euclidean u) (\<Union>(components (u - S) - c))"
   5.184 +    apply (rule openin_Union)
   5.185 +    apply (rule openin_trans [of "u - S"])
   5.186 +    apply (simp add: u S locally_diff_closed openin_components_locally_connected)
   5.187 +    apply (simp add: openin_diff S)
   5.188 +    done
   5.189 +  have "openin (subtopology euclidean u) (u - (u - \<Union>(components (u - S) - c)))"
   5.190 +    apply (rule openin_diff, simp)
   5.191 +    apply (metis closedin_diff closedin_topspace topspace_euclidean_subtopology *)
   5.192 +    done
   5.193 +  then show ?thesis
   5.194 +    by (force simp: eq closedin_def)
   5.195 +qed
   5.196 +
   5.197 +lemma closed_union_complement_components:
   5.198 +  fixes S :: "'a::real_normed_vector set"
   5.199 +  assumes S: "closed S" and c: "c \<subseteq> components(- S)"
   5.200 +    shows "closed(S \<union> \<Union> c)"
   5.201 +proof -
   5.202 +  have "closedin (subtopology euclidean UNIV) (S \<union> \<Union>c)"
   5.203 +    apply (rule closedin_union_complement_components [OF locally_connected_UNIV])
   5.204 +    using S apply (simp add: closed_closedin)
   5.205 +    using c apply (simp add: Compl_eq_Diff_UNIV)
   5.206 +    done
   5.207 +  then show ?thesis
   5.208 +    by (simp add: closed_closedin)
   5.209 +qed
   5.210 +
   5.211 +lemma closedin_Un_complement_component:
   5.212 +  fixes S :: "'a::real_normed_vector set"
   5.213 +  assumes u: "locally connected u"
   5.214 +      and S: "closedin (subtopology euclidean u) S"
   5.215 +      and c: " c \<in> components(u - S)"
   5.216 +    shows "closedin (subtopology euclidean u) (S \<union> c)"
   5.217 +proof -
   5.218 +  have "closedin (subtopology euclidean u) (S \<union> \<Union>{c})"
   5.219 +    using c by (blast intro: closedin_union_complement_components [OF u S])
   5.220 +  then show ?thesis
   5.221 +    by simp
   5.222 +qed
   5.223 +
   5.224 +lemma closed_Un_complement_component:
   5.225 +  fixes S :: "'a::real_normed_vector set"
   5.226 +  assumes S: "closed S" and c: " c \<in> components(-S)"
   5.227 +    shows "closed (S \<union> c)"
   5.228 +by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_Un_complement_component locally_connected_UNIV subtopology_UNIV)
   5.229 +
   5.230 +
   5.231 +subsection\<open>Existence of isometry between subspaces of same dimension\<close>
   5.232 +
   5.233 +thm subspace_isomorphism
   5.234 +lemma isometry_subset_subspace:
   5.235 +  fixes S :: "'a::euclidean_space set"
   5.236 +    and T :: "'b::euclidean_space set"
   5.237 +  assumes S: "subspace S"
   5.238 +      and T: "subspace T"
   5.239 +      and d: "dim S \<le> dim T"
   5.240 +  obtains f where "linear f" "f ` S \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> norm(f x) = norm x"
   5.241 +proof -
   5.242 +  obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
   5.243 +             and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
   5.244 +             and "independent B" "finite B" "card B = dim S" "span B = S"
   5.245 +    by (metis orthonormal_basis_subspace [OF S] independent_finite)
   5.246 +  obtain C where "C \<subseteq> T" and Corth: "pairwise orthogonal C"
   5.247 +             and C1:"\<And>x. x \<in> C \<Longrightarrow> norm x = 1"
   5.248 +             and "independent C" "finite C" "card C = dim T" "span C = T"
   5.249 +    by (metis orthonormal_basis_subspace [OF T] independent_finite)
   5.250 +  obtain fb where "fb ` B \<subseteq> C" "inj_on fb B"
   5.251 +    by (metis \<open>card B = dim S\<close> \<open>card C = dim T\<close> \<open>finite B\<close> \<open>finite C\<close> card_le_inj d)
   5.252 +  then have pairwise_orth_fb: "pairwise (\<lambda>v j. orthogonal (fb v) (fb j)) B"
   5.253 +    using Corth
   5.254 +    apply (auto simp: pairwise_def orthogonal_clauses)
   5.255 +    by (meson subsetD image_eqI inj_on_def)
   5.256 +  obtain f where "linear f" and ffb: "\<And>x. x \<in> B \<Longrightarrow> f x = fb x"
   5.257 +    using linear_independent_extend \<open>independent B\<close> by fastforce
   5.258 +  have "f ` S \<subseteq> T"
   5.259 +    by (metis ffb \<open>fb ` B \<subseteq> C\<close> \<open>linear f\<close> \<open>span B = S\<close> \<open>span C = T\<close> image_cong span_linear_image span_mono)
   5.260 +  have [simp]: "\<And>x. x \<in> B \<Longrightarrow> norm (fb x) = norm x"
   5.261 +    using B1 C1 \<open>fb ` B \<subseteq> C\<close> by auto
   5.262 +  have "norm (f x) = norm x" if "x \<in> S" for x
   5.263 +  proof -
   5.264 +    obtain a where x: "x = (\<Sum>v \<in> B. a v *\<^sub>R v)"
   5.265 +      using \<open>finite B\<close> \<open>span B = S\<close> \<open>x \<in> S\<close> span_finite by fastforce
   5.266 +    have "f x = (\<Sum>v \<in> B. f (a v *\<^sub>R v))"
   5.267 +      using linear_setsum [OF \<open>linear f\<close>] x by auto
   5.268 +    also have "... = (\<Sum>v \<in> B. a v *\<^sub>R f v)"
   5.269 +      using \<open>linear f\<close> by (simp add: linear_setsum linear.scaleR)
   5.270 +    also have "... = (\<Sum>v \<in> B. a v *\<^sub>R fb v)"
   5.271 +      by (simp add: ffb cong: setsum.cong)
   5.272 +    finally have "norm (f x)^2 = norm (\<Sum>v\<in>B. a v *\<^sub>R fb v)^2" by simp
   5.273 +    also have "... = (\<Sum>v\<in>B. norm ((a v *\<^sub>R fb v))^2)"
   5.274 +      apply (rule norm_setsum_Pythagorean [OF \<open>finite B\<close>])
   5.275 +      apply (rule pairwise_ortho_scaleR [OF pairwise_orth_fb])
   5.276 +      done
   5.277 +    also have "... = norm x ^2"
   5.278 +      by (simp add: x pairwise_ortho_scaleR Borth norm_setsum_Pythagorean [OF \<open>finite B\<close>])
   5.279 +    finally show ?thesis
   5.280 +      by (simp add: norm_eq_sqrt_inner)
   5.281 +  qed
   5.282 +  then show ?thesis
   5.283 +    by (rule that [OF \<open>linear f\<close> \<open>f ` S \<subseteq> T\<close>])
   5.284 +qed
   5.285 +
   5.286 +proposition isometries_subspaces:
   5.287 +  fixes S :: "'a::euclidean_space set"
   5.288 +    and T :: "'b::euclidean_space set"
   5.289 +  assumes S: "subspace S"
   5.290 +      and T: "subspace T"
   5.291 +      and d: "dim S = dim T"
   5.292 +  obtains f g where "linear f" "linear g" "f ` S = T" "g ` T = S"
   5.293 +                    "\<And>x. x \<in> S \<Longrightarrow> norm(f x) = norm x"
   5.294 +                    "\<And>x. x \<in> T \<Longrightarrow> norm(g x) = norm x"
   5.295 +                    "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
   5.296 +                    "\<And>x. x \<in> T \<Longrightarrow> f(g x) = x"
   5.297 +proof -
   5.298 +  obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
   5.299 +             and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
   5.300 +             and "independent B" "finite B" "card B = dim S" "span B = S"
   5.301 +    by (metis orthonormal_basis_subspace [OF S] independent_finite)
   5.302 +  obtain C where "C \<subseteq> T" and Corth: "pairwise orthogonal C"
   5.303 +             and C1:"\<And>x. x \<in> C \<Longrightarrow> norm x = 1"
   5.304 +             and "independent C" "finite C" "card C = dim T" "span C = T"
   5.305 +    by (metis orthonormal_basis_subspace [OF T] independent_finite)
   5.306 +  obtain fb where "bij_betw fb B C"
   5.307 +    by (metis \<open>finite B\<close> \<open>finite C\<close> bij_betw_iff_card \<open>card B = dim S\<close> \<open>card C = dim T\<close> d)
   5.308 +  then have pairwise_orth_fb: "pairwise (\<lambda>v j. orthogonal (fb v) (fb j)) B"
   5.309 +    using Corth
   5.310 +    apply (auto simp: pairwise_def orthogonal_clauses bij_betw_def)
   5.311 +    by (meson subsetD image_eqI inj_on_def)
   5.312 +  obtain f where "linear f" and ffb: "\<And>x. x \<in> B \<Longrightarrow> f x = fb x"
   5.313 +    using linear_independent_extend \<open>independent B\<close> by fastforce
   5.314 +  define gb where "gb \<equiv> inv_into B fb"
   5.315 +  then have pairwise_orth_gb: "pairwise (\<lambda>v j. orthogonal (gb v) (gb j)) C"
   5.316 +    using Borth
   5.317 +    apply (auto simp: pairwise_def orthogonal_clauses bij_betw_def)
   5.318 +    by (metis \<open>bij_betw fb B C\<close> bij_betw_imp_surj_on bij_betw_inv_into_right inv_into_into)
   5.319 +  obtain g where "linear g" and ggb: "\<And>x. x \<in> C \<Longrightarrow> g x = gb x"
   5.320 +    using linear_independent_extend \<open>independent C\<close> by fastforce
   5.321 +  have "f ` S \<subseteq> T"
   5.322 +    by (metis \<open>bij_betw fb B C\<close> bij_betw_imp_surj_on eq_iff ffb  \<open>linear f\<close> \<open>span B = S\<close> \<open>span C = T\<close> image_cong span_linear_image)
   5.323 +  have [simp]: "\<And>x. x \<in> B \<Longrightarrow> norm (fb x) = norm x"
   5.324 +    using B1 C1 \<open>bij_betw fb B C\<close> bij_betw_imp_surj_on by fastforce
   5.325 +  have f [simp]: "norm (f x) = norm x" "g (f x) = x" if "x \<in> S" for x
   5.326 +  proof -
   5.327 +    obtain a where x: "x = (\<Sum>v \<in> B. a v *\<^sub>R v)"
   5.328 +      using \<open>finite B\<close> \<open>span B = S\<close> \<open>x \<in> S\<close> span_finite by fastforce
   5.329 +    have "f x = (\<Sum>v \<in> B. f (a v *\<^sub>R v))"
   5.330 +      using linear_setsum [OF \<open>linear f\<close>] x by auto
   5.331 +    also have "... = (\<Sum>v \<in> B. a v *\<^sub>R f v)"
   5.332 +      using \<open>linear f\<close> by (simp add: linear_setsum linear.scaleR)
   5.333 +    also have "... = (\<Sum>v \<in> B. a v *\<^sub>R fb v)"
   5.334 +      by (simp add: ffb cong: setsum.cong)
   5.335 +    finally have *: "f x = (\<Sum>v\<in>B. a v *\<^sub>R fb v)" .
   5.336 +    then have "(norm (f x))\<^sup>2 = (norm (\<Sum>v\<in>B. a v *\<^sub>R fb v))\<^sup>2" by simp
   5.337 +    also have "... = (\<Sum>v\<in>B. norm ((a v *\<^sub>R fb v))^2)"
   5.338 +      apply (rule norm_setsum_Pythagorean [OF \<open>finite B\<close>])
   5.339 +      apply (rule pairwise_ortho_scaleR [OF pairwise_orth_fb])
   5.340 +      done
   5.341 +    also have "... = (norm x)\<^sup>2"
   5.342 +      by (simp add: x pairwise_ortho_scaleR Borth norm_setsum_Pythagorean [OF \<open>finite B\<close>])
   5.343 +    finally show "norm (f x) = norm x"
   5.344 +      by (simp add: norm_eq_sqrt_inner)
   5.345 +    have "g (f x) = g (\<Sum>v\<in>B. a v *\<^sub>R fb v)" by (simp add: *)
   5.346 +    also have "... = (\<Sum>v\<in>B. g (a v *\<^sub>R fb v))"
   5.347 +      using \<open>linear g\<close> by (simp add: linear_setsum linear.scaleR)
   5.348 +    also have "... = (\<Sum>v\<in>B. a v *\<^sub>R g (fb v))"
   5.349 +      by (simp add: \<open>linear g\<close> linear.scaleR)
   5.350 +    also have "... = (\<Sum>v\<in>B. a v *\<^sub>R v)"
   5.351 +      apply (rule setsum.cong [OF refl])
   5.352 +      using \<open>bij_betw fb B C\<close> gb_def bij_betwE bij_betw_inv_into_left gb_def ggb by fastforce
   5.353 +    also have "... = x"
   5.354 +      using x by blast
   5.355 +    finally show "g (f x) = x" .
   5.356 +  qed
   5.357 +  have [simp]: "\<And>x. x \<in> C \<Longrightarrow> norm (gb x) = norm x"
   5.358 +    by (metis B1 C1 \<open>bij_betw fb B C\<close> bij_betw_imp_surj_on gb_def inv_into_into)
   5.359 +  have g [simp]: "f (g x) = x" if "x \<in> T" for x
   5.360 +  proof -
   5.361 +    obtain a where x: "x = (\<Sum>v \<in> C. a v *\<^sub>R v)"
   5.362 +      using \<open>finite C\<close> \<open>span C = T\<close> \<open>x \<in> T\<close> span_finite by fastforce
   5.363 +    have "g x = (\<Sum>v \<in> C. g (a v *\<^sub>R v))"
   5.364 +      using linear_setsum [OF \<open>linear g\<close>] x by auto
   5.365 +    also have "... = (\<Sum>v \<in> C. a v *\<^sub>R g v)"
   5.366 +      using \<open>linear g\<close> by (simp add: linear_setsum linear.scaleR)
   5.367 +    also have "... = (\<Sum>v \<in> C. a v *\<^sub>R gb v)"
   5.368 +      by (simp add: ggb cong: setsum.cong)
   5.369 +    finally have "f (g x) = f (\<Sum>v\<in>C. a v *\<^sub>R gb v)" by simp
   5.370 +    also have "... = (\<Sum>v\<in>C. f (a v *\<^sub>R gb v))"
   5.371 +      using \<open>linear f\<close> by (simp add: linear_setsum linear.scaleR)
   5.372 +    also have "... = (\<Sum>v\<in>C. a v *\<^sub>R f (gb v))"
   5.373 +      by (simp add: \<open>linear f\<close> linear.scaleR)
   5.374 +    also have "... = (\<Sum>v\<in>C. a v *\<^sub>R v)"
   5.375 +      using \<open>bij_betw fb B C\<close>
   5.376 +      by (simp add: bij_betw_def gb_def bij_betw_inv_into_right ffb inv_into_into)
   5.377 +    also have "... = x"
   5.378 +      using x by blast
   5.379 +    finally show "f (g x) = x" .
   5.380 +  qed
   5.381 +  have gim: "g ` T = S"
   5.382 +    by (metis (no_types, lifting) \<open>f ` S \<subseteq> T\<close> \<open>linear g\<close> \<open>span B = S\<close> \<open>span C = T\<close> d dim_eq_span dim_image_le f(2) image_subset_iff span_linear_image span_span subsetI)
   5.383 +  have fim: "f ` S = T"
   5.384 +    using \<open>g ` T = S\<close> image_iff by fastforce
   5.385 +  have [simp]: "norm (g x) = norm x" if "x \<in> T" for x
   5.386 +    using fim that by auto
   5.387 +  show ?thesis
   5.388 +    apply (rule that [OF \<open>linear f\<close> \<open>linear g\<close>])
   5.389 +    apply (simp_all add: fim gim)
   5.390 +    done
   5.391 +qed
   5.392 +
   5.393 +(*REPLACE*)
   5.394 +lemma isometry_subspaces:
   5.395 +  fixes S :: "'a::euclidean_space set"
   5.396 +    and T :: "'b::euclidean_space set"
   5.397 +  assumes S: "subspace S"
   5.398 +      and T: "subspace T"
   5.399 +      and d: "dim S = dim T"
   5.400 +  obtains f where "linear f" "f ` S = T" "\<And>x. x \<in> S \<Longrightarrow> norm(f x) = norm x"
   5.401 +using isometries_subspaces [OF assms]
   5.402 +by metis
   5.403 +
   5.404 +lemma homeomorphic_subspaces:
   5.405 +  fixes S :: "'a::euclidean_space set"
   5.406 +    and T :: "'b::euclidean_space set"
   5.407 +  assumes S: "subspace S"
   5.408 +      and T: "subspace T"
   5.409 +      and d: "dim S = dim T"
   5.410 +    shows "S homeomorphic T"
   5.411 +proof -
   5.412 +  obtain f g where "linear f" "linear g" "f ` S = T" "g ` T = S"
   5.413 +                   "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" "\<And>x. x \<in> T \<Longrightarrow> f(g x) = x"
   5.414 +    by (blast intro: isometries_subspaces [OF assms])
   5.415 +  then show ?thesis
   5.416 +    apply (simp add: homeomorphic_def homeomorphism_def)
   5.417 +    apply (rule_tac x=f in exI)
   5.418 +    apply (rule_tac x=g in exI)
   5.419 +    apply (auto simp: linear_continuous_on linear_conv_bounded_linear)
   5.420 +    done
   5.421 +qed
   5.422 +
   5.423 +lemma homeomorphic_affine_sets:
   5.424 +  assumes "affine S" "affine T" "aff_dim S = aff_dim T"
   5.425 +    shows "S homeomorphic T"
   5.426 +proof (cases "S = {} \<or> T = {}")
   5.427 +  case True  with assms aff_dim_empty homeomorphic_empty show ?thesis
   5.428 +    by metis
   5.429 +next
   5.430 +  case False
   5.431 +  then obtain a b where ab: "a \<in> S" "b \<in> T" by auto
   5.432 +  then have ss: "subspace (op + (- a) ` S)" "subspace (op + (- b) ` T)"
   5.433 +    using affine_diffs_subspace assms by blast+
   5.434 +  have dd: "dim (op + (- a) ` S) = dim (op + (- b) ` T)"
   5.435 +    using assms ab  by (simp add: aff_dim_eq_dim  [OF hull_inc] image_def)
   5.436 +  have "S homeomorphic (op + (- a) ` S)"
   5.437 +    by (simp add: homeomorphic_translation)
   5.438 +  also have "... homeomorphic (op + (- b) ` T)"
   5.439 +    by (rule homeomorphic_subspaces [OF ss dd])
   5.440 +  also have "... homeomorphic T"
   5.441 +    using homeomorphic_sym homeomorphic_translation by auto
   5.442 +  finally show ?thesis .
   5.443 +qed
   5.444 +
   5.445  subsection\<open>Retracts, in a general sense, preserve (co)homotopic triviality)\<close>
   5.446  
   5.447  locale Retracts =
     6.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat May 21 07:08:59 2016 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon May 23 15:33:24 2016 +0100
     6.3 @@ -861,6 +861,11 @@
     6.4    shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
     6.5    by (simp add: dist_norm)
     6.6  
     6.7 +lemma mem_sphere_0 [simp]:
     6.8 +  fixes x :: "'a::real_normed_vector"
     6.9 +  shows "x \<in> sphere 0 e \<longleftrightarrow> norm x = e"
    6.10 +  by (simp add: dist_norm)
    6.11 +
    6.12  lemma centre_in_ball [simp]: "x \<in> ball x e \<longleftrightarrow> 0 < e"
    6.13    by simp
    6.14  
    6.15 @@ -986,6 +991,22 @@
    6.16  abbreviation One :: "'a::euclidean_space"
    6.17    where "One \<equiv> \<Sum>Basis"
    6.18  
    6.19 +lemma One_non_0: assumes "One = (0::'a::euclidean_space)" shows False
    6.20 +proof -
    6.21 +  have "dependent (Basis :: 'a set)"
    6.22 +    apply (simp add: dependent_finite)
    6.23 +    apply (rule_tac x="\<lambda>i. 1" in exI)
    6.24 +    using SOME_Basis apply (auto simp: assms)
    6.25 +    done
    6.26 +  with independent_Basis show False by force
    6.27 +qed
    6.28 +
    6.29 +corollary One_neq_0[iff]: "One \<noteq> 0"
    6.30 +  by (metis One_non_0)
    6.31 +
    6.32 +corollary Zero_neq_One[iff]: "0 \<noteq> One"
    6.33 +  by (metis One_non_0)
    6.34 +
    6.35  definition (in euclidean_space) eucl_less (infix "<e" 50)
    6.36    where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
    6.37  
    6.38 @@ -5788,7 +5809,7 @@
    6.39    unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute
    6.40    by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
    6.41  
    6.42 -text \<open>Half-global and completely global cases.\<close>
    6.43 +subsection \<open>Half-global and completely global cases.\<close>
    6.44  
    6.45  lemma continuous_openin_preimage:
    6.46    assumes "continuous_on s f"  "open t"
    6.47 @@ -5874,7 +5895,7 @@
    6.48    with \<open>x = f y\<close> show "x \<in> f ` interior s" ..
    6.49  qed
    6.50  
    6.51 -text \<open>Equality of continuous functions on closure and related results.\<close>
    6.52 +subsection \<open>Equality of continuous functions on closure and related results.\<close>
    6.53  
    6.54  lemma continuous_closedin_preimage_constant:
    6.55    fixes f :: "_ \<Rightarrow> 'b::t1_space"
    6.56 @@ -7238,6 +7259,11 @@
    6.57    shows "(\<lambda>x. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)"
    6.58    by auto
    6.59  
    6.60 +lemma translation_Int:
    6.61 +  fixes a :: "'a::ab_group_add"
    6.62 +  shows "(\<lambda>x. a + x) ` (s \<inter> t) = ((\<lambda>x. a + x) ` s) \<inter> ((\<lambda>x. a + x) ` t)"
    6.63 +  by auto
    6.64 +
    6.65  lemma closure_translation:
    6.66    fixes a :: "'a::real_normed_vector"
    6.67    shows "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)"
    6.68 @@ -7261,6 +7287,30 @@
    6.69    unfolding frontier_def translation_diff interior_translation closure_translation
    6.70    by auto
    6.71  
    6.72 +lemma sphere_translation:
    6.73 +  fixes a :: "'n::euclidean_space"
    6.74 +  shows "sphere (a+c) r = op+a ` sphere c r"
    6.75 +apply safe
    6.76 +apply (rule_tac x="x-a" in image_eqI)
    6.77 +apply (auto simp: dist_norm algebra_simps)
    6.78 +done
    6.79 +
    6.80 +lemma cball_translation:
    6.81 +  fixes a :: "'n::euclidean_space"
    6.82 +  shows "cball (a+c) r = op+a ` cball c r"
    6.83 +apply safe
    6.84 +apply (rule_tac x="x-a" in image_eqI)
    6.85 +apply (auto simp: dist_norm algebra_simps)
    6.86 +done
    6.87 +
    6.88 +lemma ball_translation:
    6.89 +  fixes a :: "'n::euclidean_space"
    6.90 +  shows "ball (a+c) r = op+a ` ball c r"
    6.91 +apply safe
    6.92 +apply (rule_tac x="x-a" in image_eqI)
    6.93 +apply (auto simp: dist_norm algebra_simps)
    6.94 +done
    6.95 +
    6.96  
    6.97  subsection \<open>Separation between points and sets\<close>
    6.98  
    6.99 @@ -8211,6 +8261,37 @@
   6.100    apply auto
   6.101    done
   6.102  
   6.103 +lemma homeomorphicI [intro?]:
   6.104 +   "\<lbrakk>f ` S = T; g ` T = S;
   6.105 +     continuous_on S f; continuous_on T g;
   6.106 +     \<And>x. x \<in> S \<Longrightarrow> g(f(x)) = x;
   6.107 +     \<And>y. y \<in> T \<Longrightarrow> f(g(y)) = y\<rbrakk> \<Longrightarrow> S homeomorphic T"
   6.108 +unfolding homeomorphic_def homeomorphism_def by metis
   6.109 +
   6.110 +lemma homeomorphism_of_subsets:
   6.111 +   "\<lbrakk>homeomorphism S T f g; S' \<subseteq> S; T'' \<subseteq> T; f ` S' = T'\<rbrakk>
   6.112 +    \<Longrightarrow> homeomorphism S' T' f g"
   6.113 +apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
   6.114 +by (metis contra_subsetD imageI)
   6.115 +
   6.116 +lemma homeomorphism_apply1: "\<lbrakk>homeomorphism S T f g; x \<in> S\<rbrakk> \<Longrightarrow> g(f x) = x"
   6.117 +  by (simp add: homeomorphism_def)
   6.118 +
   6.119 +lemma homeomorphism_apply2: "\<lbrakk>homeomorphism S T f g; x \<in> T\<rbrakk> \<Longrightarrow> f(g x) = x"
   6.120 +  by (simp add: homeomorphism_def)
   6.121 +
   6.122 +lemma homeomorphism_image1: "homeomorphism S T f g \<Longrightarrow> f ` S = T"
   6.123 +  by (simp add: homeomorphism_def)
   6.124 +
   6.125 +lemma homeomorphism_image2: "homeomorphism S T f g \<Longrightarrow> g ` T = S"
   6.126 +  by (simp add: homeomorphism_def)
   6.127 +
   6.128 +lemma homeomorphism_cont1: "homeomorphism S T f g \<Longrightarrow> continuous_on S f"
   6.129 +  by (simp add: homeomorphism_def)
   6.130 +
   6.131 +lemma homeomorphism_cont2: "homeomorphism S T f g \<Longrightarrow> continuous_on T g"
   6.132 +  by (simp add: homeomorphism_def)
   6.133 +
   6.134  text \<open>Relatively weak hypotheses if a set is compact.\<close>
   6.135  
   6.136  lemma homeomorphism_compact:
   6.137 @@ -8332,7 +8413,109 @@
   6.138      done
   6.139  qed
   6.140  
   6.141 -text\<open>"Isometry" (up to constant bounds) of injective linear map etc.\<close>
   6.142 +subsection\<open>Inverse function property for open/closed maps\<close>
   6.143 +
   6.144 +lemma continuous_on_inverse_open_map:
   6.145 +  assumes contf: "continuous_on S f"
   6.146 +      and imf: "f ` S = T"
   6.147 +      and injf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
   6.148 +      and oo: "\<And>U. openin (subtopology euclidean S) U
   6.149 +                    \<Longrightarrow> openin (subtopology euclidean T) (f ` U)"
   6.150 +    shows "continuous_on T g"
   6.151 +proof -
   6.152 +  have gTS: "g ` T = S"
   6.153 +    using imf injf by force
   6.154 +  have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = {x \<in> T. g x \<in> U}" for U
   6.155 +    using imf injf by force
   6.156 +  show ?thesis
   6.157 +    apply (simp add: continuous_on_open [of T g] gTS)
   6.158 +    apply (metis openin_imp_subset fU oo)
   6.159 +    done
   6.160 +qed
   6.161 +
   6.162 +lemma continuous_on_inverse_closed_map:
   6.163 +  assumes contf: "continuous_on S f"
   6.164 +      and imf: "f ` S = T"
   6.165 +      and injf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
   6.166 +      and oo: "\<And>U. closedin (subtopology euclidean S) U
   6.167 +                    \<Longrightarrow> closedin (subtopology euclidean T) (f ` U)"
   6.168 +    shows "continuous_on T g"
   6.169 +proof -
   6.170 +  have gTS: "g ` T = S"
   6.171 +    using imf injf by force
   6.172 +  have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = {x \<in> T. g x \<in> U}" for U
   6.173 +    using imf injf by force
   6.174 +  show ?thesis
   6.175 +    apply (simp add: continuous_on_closed [of T g] gTS)
   6.176 +    apply (metis closedin_imp_subset fU oo)
   6.177 +    done
   6.178 +qed
   6.179 +
   6.180 +lemma homeomorphism_injective_open_map:
   6.181 +  assumes contf: "continuous_on S f"
   6.182 +      and imf: "f ` S = T"
   6.183 +      and injf: "inj_on f S"
   6.184 +      and oo: "\<And>U. openin (subtopology euclidean S) U
   6.185 +                    \<Longrightarrow> openin (subtopology euclidean T) (f ` U)"
   6.186 +  obtains g where "homeomorphism S T f g"
   6.187 +proof -
   6.188 +  have "continuous_on T (inv_into S f)"
   6.189 +    by (metis contf continuous_on_inverse_open_map imf injf inv_into_f_f oo)
   6.190 +  then show ?thesis
   6.191 +    apply (rule_tac g = "inv_into S f" in that)
   6.192 +    using imf injf contf apply (auto simp: homeomorphism_def)
   6.193 +    done
   6.194 +qed
   6.195 +
   6.196 +lemma homeomorphism_injective_closed_map:
   6.197 +  assumes contf: "continuous_on S f"
   6.198 +      and imf: "f ` S = T"
   6.199 +      and injf: "inj_on f S"
   6.200 +      and oo: "\<And>U. closedin (subtopology euclidean S) U
   6.201 +                    \<Longrightarrow> closedin (subtopology euclidean T) (f ` U)"
   6.202 +  obtains g where "homeomorphism S T f g"
   6.203 +proof -
   6.204 +  have "continuous_on T (inv_into S f)"
   6.205 +    by (metis contf continuous_on_inverse_closed_map imf injf inv_into_f_f oo)
   6.206 +  then show ?thesis
   6.207 +    apply (rule_tac g = "inv_into S f" in that)
   6.208 +    using imf injf contf apply (auto simp: homeomorphism_def)
   6.209 +    done
   6.210 +qed
   6.211 +
   6.212 +lemma homeomorphism_imp_open_map:
   6.213 +  assumes hom: "homeomorphism S T f g"
   6.214 +      and oo: "openin (subtopology euclidean S) U"
   6.215 +    shows "openin (subtopology euclidean T) (f ` U)"
   6.216 +proof -
   6.217 +  have [simp]: "f ` U = {y. y \<in> T \<and> g y \<in> U}"
   6.218 +    using assms openin_subset
   6.219 +    by (fastforce simp: homeomorphism_def rev_image_eqI)
   6.220 +  have "continuous_on T g"
   6.221 +    using hom homeomorphism_def by blast
   6.222 +  moreover have "g ` T = S"
   6.223 +    by (metis hom homeomorphism_def)
   6.224 +  ultimately show ?thesis
   6.225 +    by (simp add: continuous_on_open oo)
   6.226 +qed
   6.227 +
   6.228 +lemma homeomorphism_imp_closed_map:
   6.229 +  assumes hom: "homeomorphism S T f g"
   6.230 +      and oo: "closedin (subtopology euclidean S) U"
   6.231 +    shows "closedin (subtopology euclidean T) (f ` U)"
   6.232 +proof -
   6.233 +  have [simp]: "f ` U = {y. y \<in> T \<and> g y \<in> U}"
   6.234 +    using assms closedin_subset
   6.235 +    by (fastforce simp: homeomorphism_def rev_image_eqI)
   6.236 +  have "continuous_on T g"
   6.237 +    using hom homeomorphism_def by blast
   6.238 +  moreover have "g ` T = S"
   6.239 +    by (metis hom homeomorphism_def)
   6.240 +  ultimately show ?thesis
   6.241 +    by (simp add: continuous_on_closed oo)
   6.242 +qed
   6.243 +
   6.244 +subsection\<open>"Isometry" (up to constant bounds) of injective linear map etc.\<close>
   6.245  
   6.246  lemma cauchy_isometric:
   6.247    assumes e: "e > 0"
   6.248 @@ -8354,7 +8537,7 @@
   6.249        fix n
   6.250        assume "n\<ge>N"
   6.251        have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
   6.252 -        using subspace_sub[OF s, of "x n" "x N"]
   6.253 +        using subspace_diff[OF s, of "x n" "x N"]
   6.254          using xs[THEN spec[where x=N]] and xs[THEN spec[where x=n]]
   6.255          using normf[THEN bspec[where x="x n - x N"]]
   6.256          by auto
     7.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sat May 21 07:08:59 2016 +0200
     7.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon May 23 15:33:24 2016 +0100
     7.3 @@ -236,6 +236,18 @@
     7.4    apply (simp_all add: algebra_simps)
     7.5    done
     7.6  
     7.7 +lemma vector_add_divide_simps :
     7.8 +  fixes v :: "'a :: real_vector"
     7.9 +  shows "v + (b / z) *\<^sub>R w = (if z = 0 then v else (z *\<^sub>R v + b *\<^sub>R w) /\<^sub>R z)"
    7.10 +        "a *\<^sub>R v + (b / z) *\<^sub>R w = (if z = 0 then a *\<^sub>R v else ((a * z) *\<^sub>R v + b *\<^sub>R w) /\<^sub>R z)"
    7.11 +        "(a / z) *\<^sub>R v + w = (if z = 0 then w else (a *\<^sub>R v + z *\<^sub>R w) /\<^sub>R z)"
    7.12 +        "(a / z) *\<^sub>R v + b *\<^sub>R w = (if z = 0 then b *\<^sub>R w else (a *\<^sub>R v + (b * z) *\<^sub>R w) /\<^sub>R z)"
    7.13 +        "v - (b / z) *\<^sub>R w = (if z = 0 then v else (z *\<^sub>R v - b *\<^sub>R w) /\<^sub>R z)"
    7.14 +        "a *\<^sub>R v - (b / z) *\<^sub>R w = (if z = 0 then a *\<^sub>R v else ((a * z) *\<^sub>R v - b *\<^sub>R w) /\<^sub>R z)"
    7.15 +        "(a / z) *\<^sub>R v - w = (if z = 0 then -w else (a *\<^sub>R v - z *\<^sub>R w) /\<^sub>R z)"
    7.16 +        "(a / z) *\<^sub>R v - b *\<^sub>R w = (if z = 0 then -b *\<^sub>R w else (a *\<^sub>R v - (b * z) *\<^sub>R w) /\<^sub>R z)"
    7.17 +by (simp_all add: divide_inverse_commute scaleR_add_right real_vector.scale_right_diff_distrib)
    7.18 +
    7.19  lemma real_vector_affinity_eq:
    7.20    fixes x :: "'a :: real_vector"
    7.21    assumes m0: "m \<noteq> 0"
    7.22 @@ -769,6 +781,21 @@
    7.23      by (rule norm_minus_cancel)
    7.24    thus ?thesis by simp
    7.25  qed
    7.26 +  
    7.27 +lemma dist_add_cancel [simp]:
    7.28 +  fixes a :: "'a::real_normed_vector"
    7.29 +  shows "dist (a + b) (a + c) = dist b c"
    7.30 +by (simp add: dist_norm)
    7.31 +
    7.32 +lemma dist_add_cancel2 [simp]:
    7.33 +  fixes a :: "'a::real_normed_vector"
    7.34 +  shows "dist (b + a) (c + a) = dist b c"
    7.35 +by (simp add: dist_norm)
    7.36 +
    7.37 +lemma dist_scaleR [simp]:
    7.38 +  fixes a :: "'a::real_normed_vector"
    7.39 +  shows "dist (x *\<^sub>R a) (y *\<^sub>R a) = abs (x-y) * norm a"
    7.40 +by (metis dist_norm norm_scaleR scaleR_left.diff)
    7.41  
    7.42  lemma norm_uminus_minus: "norm (-x - y :: 'a :: real_normed_vector) = norm (x + y)"
    7.43    by (subst (2) norm_minus_cancel[symmetric], subst minus_add_distrib) simp
     8.1 --- a/src/HOL/Set.thy	Sat May 21 07:08:59 2016 +0200
     8.2 +++ b/src/HOL/Set.thy	Mon May 23 15:33:24 2016 +0100
     8.3 @@ -1934,6 +1934,14 @@
     8.4  lemma pairwise_singleton [simp]: "pairwise P {A}"
     8.5    by (simp add: pairwise_def)
     8.6  
     8.7 +lemma pairwise_insert:
     8.8 +   "pairwise r (insert x s) \<longleftrightarrow> (\<forall>y. y \<in> s \<and> y \<noteq> x \<longrightarrow> r x y \<and> r y x) \<and> pairwise r s"
     8.9 +by (force simp: pairwise_def)
    8.10 +
    8.11 +lemma pairwise_image:
    8.12 +   "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s"
    8.13 +by (force simp: pairwise_def)
    8.14 +
    8.15  lemma Int_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> False) \<Longrightarrow> A \<inter> B = {}"
    8.16    by blast
    8.17  
     9.1 --- a/src/HOL/Set_Interval.thy	Sat May 21 07:08:59 2016 +0200
     9.2 +++ b/src/HOL/Set_Interval.thy	Mon May 23 15:33:24 2016 +0100
     9.3 @@ -1168,19 +1168,18 @@
     9.4  by (rule finite_same_card_bij) auto
     9.5  
     9.6  lemma bij_betw_iff_card:
     9.7 -  assumes FIN: "finite A" and FIN': "finite B"
     9.8 -  shows BIJ: "(\<exists>f. bij_betw f A B) \<longleftrightarrow> (card A = card B)"
     9.9 -using assms
    9.10 -proof(auto simp add: bij_betw_same_card)
    9.11 -  assume *: "card A = card B"
    9.12 -  obtain f where "bij_betw f A {0 ..< card A}"
    9.13 -  using FIN ex_bij_betw_finite_nat by blast
    9.14 +  assumes "finite A" "finite B"
    9.15 +  shows "(\<exists>f. bij_betw f A B) \<longleftrightarrow> (card A = card B)"
    9.16 +proof
    9.17 +  assume "card A = card B"
    9.18 +  moreover obtain f where "bij_betw f A {0 ..< card A}"
    9.19 +    using assms ex_bij_betw_finite_nat by blast
    9.20    moreover obtain g where "bij_betw g {0 ..< card B} B"
    9.21 -  using FIN' ex_bij_betw_nat_finite by blast
    9.22 +    using assms ex_bij_betw_nat_finite by blast
    9.23    ultimately have "bij_betw (g o f) A B"
    9.24 -  using * by (auto simp add: bij_betw_trans)
    9.25 +    by (auto simp: bij_betw_trans)
    9.26    thus "(\<exists>f. bij_betw f A B)" by blast
    9.27 -qed
    9.28 +qed (auto simp: bij_betw_same_card)
    9.29  
    9.30  lemma inj_on_iff_card_le:
    9.31    assumes FIN: "finite A" and FIN': "finite B"