author  paulson <lp15@cam.ac.uk> 
Fri, 29 Sep 2017 16:55:08 +0100  
changeset 66710  676258a1cf01 
parent 66690  6953b1a29e19 
child 66827  c94531b5007d 
permissions  rwrr 
63627  1 
(* Title: HOL/Analysis/Homeomorphism.thy 
63130  2 
Author: LC Paulson (ported from HOL Light) 
3 
*) 

4 

5 
section \<open>Homeomorphism Theorems\<close> 

6 

7 
theory Homeomorphism 

8 
imports Path_Connected 

9 
begin 

10 

64789
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

11 
lemma homeomorphic_spheres': 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

12 
fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space" 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

13 
assumes "0 < \<delta>" and dimeq: "DIM('a) = DIM('b)" 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

14 
shows "(sphere a \<delta>) homeomorphic (sphere b \<delta>)" 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

15 
proof  
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

16 
obtain f :: "'a\<Rightarrow>'b" and g where "linear f" "linear g" 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

17 
and fg: "\<And>x. norm(f x) = norm x" "\<And>y. norm(g y) = norm y" "\<And>x. g(f x) = x" "\<And>y. f(g y) = y" 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

18 
by (blast intro: isomorphisms_UNIV_UNIV [OF dimeq]) 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

19 
then have "continuous_on UNIV f" "continuous_on UNIV g" 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

20 
using linear_continuous_on linear_linear by blast+ 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

21 
then show ?thesis 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

22 
unfolding homeomorphic_minimal 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

23 
apply(rule_tac x="\<lambda>x. b + f(x  a)" in exI) 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

24 
apply(rule_tac x="\<lambda>x. a + g(x  b)" in exI) 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

25 
using assms 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

26 
apply (force intro: continuous_intros 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

27 
continuous_on_compose2 [of _ f] continuous_on_compose2 [of _ g] simp: dist_commute dist_norm fg) 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

28 
done 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

29 
qed 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

30 

6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

31 
lemma homeomorphic_spheres_gen: 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

32 
fixes a :: "'a::euclidean_space" and b :: "'b::euclidean_space" 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

33 
assumes "0 < r" "0 < s" "DIM('a::euclidean_space) = DIM('b::euclidean_space)" 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

34 
shows "(sphere a r homeomorphic sphere b s)" 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

35 
apply (rule homeomorphic_trans [OF homeomorphic_spheres homeomorphic_spheres']) 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

36 
using assms apply auto 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

37 
done 
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

38 

63130  39 
subsection \<open>Homeomorphism of all convex compact sets with nonempty interior\<close> 
40 

41 
proposition ray_to_rel_frontier: 

42 
fixes a :: "'a::real_inner" 

43 
assumes "bounded S" 

44 
and a: "a \<in> rel_interior S" 

45 
and aff: "(a + l) \<in> affine hull S" 

46 
and "l \<noteq> 0" 

47 
obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> rel_frontier S" 

48 
"\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S" 

49 
proof  

50 
have aaff: "a \<in> affine hull S" 

51 
by (meson a hull_subset rel_interior_subset rev_subsetD) 

52 
let ?D = "{d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}" 

53 
obtain B where "B > 0" and B: "S \<subseteq> ball a B" 

54 
using bounded_subset_ballD [OF \<open>bounded S\<close>] by blast 

55 
have "a + (B / norm l) *\<^sub>R l \<notin> ball a B" 

56 
by (simp add: dist_norm \<open>l \<noteq> 0\<close>) 

57 
with B have "a + (B / norm l) *\<^sub>R l \<notin> rel_interior S" 

58 
using rel_interior_subset subsetCE by blast 

59 
with \<open>B > 0\<close> \<open>l \<noteq> 0\<close> have nonMT: "?D \<noteq> {}" 

60 
using divide_pos_pos zero_less_norm_iff by fastforce 

61 
have bdd: "bdd_below ?D" 

62 
by (metis (no_types, lifting) bdd_belowI le_less mem_Collect_eq) 

63 
have relin_Ex: "\<And>x. x \<in> rel_interior S \<Longrightarrow> 

64 
\<exists>e>0. \<forall>x'\<in>affine hull S. dist x' x < e \<longrightarrow> x' \<in> rel_interior S" 

65 
using openin_rel_interior [of S] by (simp add: openin_euclidean_subtopology_iff) 

66 
define d where "d = Inf ?D" 

67 
obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "\<And>\<eta>. \<lbrakk>0 \<le> \<eta>; \<eta> < \<epsilon>\<rbrakk> \<Longrightarrow> (a + \<eta> *\<^sub>R l) \<in> rel_interior S" 

68 
proof  

69 
obtain e where "e>0" 

70 
and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' a < e \<Longrightarrow> x' \<in> rel_interior S" 

71 
using relin_Ex a by blast 

72 
show thesis 

73 
proof (rule_tac \<epsilon> = "e / norm l" in that) 

74 
show "0 < e / norm l" by (simp add: \<open>0 < e\<close> \<open>l \<noteq> 0\<close>) 

75 
next 

76 
show "a + \<eta> *\<^sub>R l \<in> rel_interior S" if "0 \<le> \<eta>" "\<eta> < e / norm l" for \<eta> 

77 
proof (rule e) 

78 
show "a + \<eta> *\<^sub>R l \<in> affine hull S" 

79 
by (metis (no_types) add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff) 

80 
show "dist (a + \<eta> *\<^sub>R l) a < e" 

81 
using that by (simp add: \<open>l \<noteq> 0\<close> dist_norm pos_less_divide_eq) 

82 
qed 

83 
qed 

84 
qed 

85 
have inint: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> a + e *\<^sub>R l \<in> rel_interior S" 

86 
unfolding d_def using cInf_lower [OF _ bdd] 

87 
by (metis (no_types, lifting) a add.right_neutral le_less mem_Collect_eq not_less real_vector.scale_zero_left) 

88 
have "\<epsilon> \<le> d" 

89 
unfolding d_def 

90 
apply (rule cInf_greatest [OF nonMT]) 

91 
using \<epsilon> dual_order.strict_implies_order le_less_linear by blast 

92 
with \<open>0 < \<epsilon>\<close> have "0 < d" by simp 

93 
have "a + d *\<^sub>R l \<notin> rel_interior S" 

94 
proof 

95 
assume adl: "a + d *\<^sub>R l \<in> rel_interior S" 

96 
obtain e where "e > 0" 

97 
and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' (a + d *\<^sub>R l) < e \<Longrightarrow> x' \<in> rel_interior S" 

98 
using relin_Ex adl by blast 

99 
have "d + e / norm l \<le> Inf {d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}" 

100 
proof (rule cInf_greatest [OF nonMT], clarsimp) 

101 
fix x::real 

102 
assume "0 < x" and nonrel: "a + x *\<^sub>R l \<notin> rel_interior S" 

103 
show "d + e / norm l \<le> x" 

104 
proof (cases "x < d") 

105 
case True with inint nonrel \<open>0 < x\<close> 

106 
show ?thesis by auto 

107 
next 

108 
case False 

109 
then have dle: "x < d + e / norm l \<Longrightarrow> dist (a + x *\<^sub>R l) (a + d *\<^sub>R l) < e" 

110 
by (simp add: field_simps \<open>l \<noteq> 0\<close>) 

111 
have ain: "a + x *\<^sub>R l \<in> affine hull S" 

112 
by (metis add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff) 

113 
show ?thesis 

114 
using e [OF ain] nonrel dle by force 

115 
qed 

116 
qed 

117 
then show False 

118 
using \<open>0 < e\<close> \<open>l \<noteq> 0\<close> by (simp add: d_def [symmetric] divide_simps) 

119 
qed 

120 
moreover have "a + d *\<^sub>R l \<in> closure S" 

121 
proof (clarsimp simp: closure_approachable) 

122 
fix \<eta>::real assume "0 < \<eta>" 

123 
have 1: "a + (d  min d (\<eta> / 2 / norm l)) *\<^sub>R l \<in> S" 

124 
apply (rule subsetD [OF rel_interior_subset inint]) 

125 
using \<open>l \<noteq> 0\<close> \<open>0 < d\<close> \<open>0 < \<eta>\<close> by auto 

126 
have "norm l * min d (\<eta> / (norm l * 2)) \<le> norm l * (\<eta> / (norm l * 2))" 

127 
by (metis min_def mult_left_mono norm_ge_zero order_refl) 

128 
also have "... < \<eta>" 

129 
using \<open>l \<noteq> 0\<close> \<open>0 < \<eta>\<close> by (simp add: divide_simps) 

130 
finally have 2: "norm l * min d (\<eta> / (norm l * 2)) < \<eta>" . 

131 
show "\<exists>y\<in>S. dist y (a + d *\<^sub>R l) < \<eta>" 

132 
apply (rule_tac x="a + (d  min d (\<eta> / 2 / norm l)) *\<^sub>R l" in bexI) 

133 
using 1 2 \<open>0 < d\<close> \<open>0 < \<eta>\<close> apply (auto simp: algebra_simps) 

134 
done 

135 
qed 

136 
ultimately have infront: "a + d *\<^sub>R l \<in> rel_frontier S" 

137 
by (simp add: rel_frontier_def) 

138 
show ?thesis 

139 
by (rule that [OF \<open>0 < d\<close> infront inint]) 

140 
qed 

141 

142 
corollary ray_to_frontier: 

143 
fixes a :: "'a::euclidean_space" 

144 
assumes "bounded S" 

145 
and a: "a \<in> interior S" 

146 
and "l \<noteq> 0" 

147 
obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> frontier S" 

148 
"\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> interior S" 

149 
proof  

150 
have "interior S = rel_interior S" 

151 
using a rel_interior_nonempty_interior by auto 

152 
then have "a \<in> rel_interior S" 

153 
using a by simp 

154 
then show ?thesis 

155 
apply (rule ray_to_rel_frontier [OF \<open>bounded S\<close> _ _ \<open>l \<noteq> 0\<close>]) 

156 
using a affine_hull_nonempty_interior apply blast 

157 
by (simp add: \<open>interior S = rel_interior S\<close> frontier_def rel_frontier_def that) 

158 
qed 

159 

66287
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

160 

005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

161 
lemma segment_to_rel_frontier_aux: 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

162 
fixes x :: "'a::euclidean_space" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

163 
assumes "convex S" "bounded S" and x: "x \<in> rel_interior S" and y: "y \<in> S" and xy: "x \<noteq> y" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

164 
obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

165 
"open_segment x z \<subseteq> rel_interior S" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

166 
proof  
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

167 
have "x + (y  x) \<in> affine hull S" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

168 
using hull_inc [OF y] by auto 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

169 
then obtain d where "0 < d" and df: "(x + d *\<^sub>R (yx)) \<in> rel_frontier S" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

170 
and di: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (x + e *\<^sub>R (yx)) \<in> rel_interior S" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

171 
by (rule ray_to_rel_frontier [OF \<open>bounded S\<close> x]) (use xy in auto) 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

172 
show ?thesis 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

173 
proof 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

174 
show "x + d *\<^sub>R (y  x) \<in> rel_frontier S" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

175 
by (simp add: df) 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

176 
next 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

177 
have "open_segment x y \<subseteq> rel_interior S" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

178 
using rel_interior_closure_convex_segment [OF \<open>convex S\<close> x] closure_subset y by blast 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

179 
moreover have "x + d *\<^sub>R (y  x) \<in> open_segment x y" if "d < 1" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

180 
using xy 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

181 
apply (auto simp: in_segment) 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

182 
apply (rule_tac x="d" in exI) 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

183 
using \<open>0 < d\<close> that apply (auto simp: divide_simps algebra_simps) 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

184 
done 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

185 
ultimately have "1 \<le> d" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

186 
using df rel_frontier_def by fastforce 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

187 
moreover have "x = (1 / d) *\<^sub>R x + ((d  1) / d) *\<^sub>R x" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

188 
by (metis \<open>0 < d\<close> add.commute add_divide_distrib diff_add_cancel divide_self_if less_irrefl scaleR_add_left scaleR_one) 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

189 
ultimately show "y \<in> closed_segment x (x + d *\<^sub>R (y  x))" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

190 
apply (auto simp: in_segment) 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

191 
apply (rule_tac x="1/d" in exI) 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

192 
apply (auto simp: divide_simps algebra_simps) 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

193 
done 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

194 
next 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

195 
show "open_segment x (x + d *\<^sub>R (y  x)) \<subseteq> rel_interior S" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

196 
apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> x]) 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

197 
using df rel_frontier_def by auto 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

198 
qed 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

199 
qed 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

200 

005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

201 
lemma segment_to_rel_frontier: 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

202 
fixes x :: "'a::euclidean_space" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

203 
assumes S: "convex S" "bounded S" and x: "x \<in> rel_interior S" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

204 
and y: "y \<in> S" and xy: "~(x = y \<and> S = {x})" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

205 
obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

206 
"open_segment x z \<subseteq> rel_interior S" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

207 
proof (cases "x=y") 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

208 
case True 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

209 
with xy have "S \<noteq> {x}" 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

210 
by blast 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

211 
with True show ?thesis 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

212 
by (metis Set.set_insert all_not_in_conv ends_in_segment(1) insert_iff segment_to_rel_frontier_aux[OF S x] that y) 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

213 
next 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

214 
case False 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

215 
then show ?thesis 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

216 
using segment_to_rel_frontier_aux [OF S x y] that by blast 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

217 
qed 
005a30862ed0
new material: Colinearity, convex sets, polytopes
paulson <lp15@cam.ac.uk>
parents:
65064
diff
changeset

218 

64394  219 
proposition rel_frontier_not_sing: 
220 
fixes a :: "'a::euclidean_space" 

221 
assumes "bounded S" 

222 
shows "rel_frontier S \<noteq> {a}" 

223 
proof (cases "S = {}") 

224 
case True then show ?thesis by simp 

225 
next 

226 
case False 

227 
then obtain z where "z \<in> S" 

228 
by blast 

229 
then show ?thesis 

230 
proof (cases "S = {z}") 

231 
case True then show ?thesis by simp 

232 
next 

233 
case False 

234 
then obtain w where "w \<in> S" "w \<noteq> z" 

235 
using \<open>z \<in> S\<close> by blast 

236 
show ?thesis 

237 
proof 

238 
assume "rel_frontier S = {a}" 

239 
then consider "w \<notin> rel_frontier S"  "z \<notin> rel_frontier S" 

240 
using \<open>w \<noteq> z\<close> by auto 

241 
then show False 

242 
proof cases 

243 
case 1 

244 
then have w: "w \<in> rel_interior S" 

245 
using \<open>w \<in> S\<close> closure_subset rel_frontier_def by fastforce 

246 
have "w + (w  z) \<in> affine hull S" 

247 
by (metis \<open>w \<in> S\<close> \<open>z \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one) 

248 
then obtain e where "0 < e" "(w + e *\<^sub>R (w  z)) \<in> rel_frontier S" 

249 
using \<open>w \<noteq> z\<close> \<open>z \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq w) 

250 
moreover obtain d where "0 < d" "(w + d *\<^sub>R (z  w)) \<in> rel_frontier S" 

251 
using ray_to_rel_frontier [OF \<open>bounded S\<close> w, of "1 *\<^sub>R (z  w)"] \<open>w \<noteq> z\<close> \<open>z \<in> S\<close> 

252 
by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one) 

253 
ultimately have "d *\<^sub>R (z  w) = e *\<^sub>R (w  z)" 

254 
using \<open>rel_frontier S = {a}\<close> by force 

255 
moreover have "e \<noteq> d " 

256 
using \<open>0 < e\<close> \<open>0 < d\<close> by force 

257 
ultimately show False 

258 
by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus) 

259 
next 

260 
case 2 

261 
then have z: "z \<in> rel_interior S" 

262 
using \<open>z \<in> S\<close> closure_subset rel_frontier_def by fastforce 

263 
have "z + (z  w) \<in> affine hull S" 

264 
by (metis \<open>z \<in> S\<close> \<open>w \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one) 

265 
then obtain e where "0 < e" "(z + e *\<^sub>R (z  w)) \<in> rel_frontier S" 

266 
using \<open>w \<noteq> z\<close> \<open>w \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq z) 

267 
moreover obtain d where "0 < d" "(z + d *\<^sub>R (w  z)) \<in> rel_frontier S" 

268 
using ray_to_rel_frontier [OF \<open>bounded S\<close> z, of "1 *\<^sub>R (w  z)"] \<open>w \<noteq> z\<close> \<open>w \<in> S\<close> 

269 
by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one) 

270 
ultimately have "d *\<^sub>R (w  z) = e *\<^sub>R (z  w)" 

271 
using \<open>rel_frontier S = {a}\<close> by force 

272 
moreover have "e \<noteq> d " 

273 
using \<open>0 < e\<close> \<open>0 < d\<close> by force 

274 
ultimately show False 

275 
by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus) 

276 
qed 

277 
qed 

278 
qed 

279 
qed 

280 

63130  281 
proposition 
282 
fixes S :: "'a::euclidean_space set" 

283 
assumes "compact S" and 0: "0 \<in> rel_interior S" 

284 
and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment 0 x \<subseteq> rel_interior S" 

285 
shows starlike_compact_projective1_0: 

286 
"S  rel_interior S homeomorphic sphere 0 1 \<inter> affine hull S" 

287 
(is "?SMINUS homeomorphic ?SPHER") 

288 
and starlike_compact_projective2_0: 

289 
"S homeomorphic cball 0 1 \<inter> affine hull S" 

290 
(is "S homeomorphic ?CBALL") 

291 
proof  

292 
have starI: "(u *\<^sub>R x) \<in> rel_interior S" if "x \<in> S" "0 \<le> u" "u < 1" for x u 

293 
proof (cases "x=0 \<or> u=0") 

294 
case True with 0 show ?thesis by force 

295 
next 

296 
case False with that show ?thesis 

297 
by (auto simp: in_segment intro: star [THEN subsetD]) 

298 
qed 

299 
have "0 \<in> S" using assms rel_interior_subset by auto 

300 
define proj where "proj \<equiv> \<lambda>x::'a. x /\<^sub>R norm x" 

301 
have eqI: "x = y" if "proj x = proj y" "norm x = norm y" for x y 

302 
using that by (force simp: proj_def) 

303 
then have iff_eq: "\<And>x y. (proj x = proj y \<and> norm x = norm y) \<longleftrightarrow> x = y" 

304 
by blast 

305 
have projI: "x \<in> affine hull S \<Longrightarrow> proj x \<in> affine hull S" for x 

306 
by (metis \<open>0 \<in> S\<close> affine_hull_span_0 hull_inc span_mul proj_def) 

307 
have nproj1 [simp]: "x \<noteq> 0 \<Longrightarrow> norm(proj x) = 1" for x 

308 
by (simp add: proj_def) 

309 
have proj0_iff [simp]: "proj x = 0 \<longleftrightarrow> x = 0" for x 

310 
by (simp add: proj_def) 

311 
have cont_proj: "continuous_on (UNIV  {0}) proj" 

312 
unfolding proj_def by (rule continuous_intros  force)+ 

313 
have proj_spherI: "\<And>x. \<lbrakk>x \<in> affine hull S; x \<noteq> 0\<rbrakk> \<Longrightarrow> proj x \<in> ?SPHER" 

314 
by (simp add: projI) 

315 
have "bounded S" "closed S" 

316 
using \<open>compact S\<close> compact_eq_bounded_closed by blast+ 

317 
have inj_on_proj: "inj_on proj (S  rel_interior S)" 

318 
proof 

319 
fix x y 

320 
assume x: "x \<in> S  rel_interior S" 

321 
and y: "y \<in> S  rel_interior S" and eq: "proj x = proj y" 

322 
then have xynot: "x \<noteq> 0" "y \<noteq> 0" "x \<in> S" "y \<in> S" "x \<notin> rel_interior S" "y \<notin> rel_interior S" 

323 
using 0 by auto 

324 
consider "norm x = norm y"  "norm x < norm y"  "norm x > norm y" by linarith 

325 
then show "x = y" 

326 
proof cases 

327 
assume "norm x = norm y" 

328 
with iff_eq eq show "x = y" by blast 

329 
next 

330 
assume *: "norm x < norm y" 

331 
have "x /\<^sub>R norm x = norm x *\<^sub>R (x /\<^sub>R norm x) /\<^sub>R norm (norm x *\<^sub>R (x /\<^sub>R norm x))" 

332 
by force 

333 
then have "proj ((norm x / norm y) *\<^sub>R y) = proj x" 

334 
by (metis (no_types) divide_inverse local.proj_def eq scaleR_scaleR) 

335 
then have [simp]: "(norm x / norm y) *\<^sub>R y = x" 

336 
by (rule eqI) (simp add: \<open>y \<noteq> 0\<close>) 

337 
have no: "0 \<le> norm x / norm y" "norm x / norm y < 1" 

338 
using * by (auto simp: divide_simps) 

339 
then show "x = y" 

340 
using starI [OF \<open>y \<in> S\<close> no] xynot by auto 

341 
next 

342 
assume *: "norm x > norm y" 

343 
have "y /\<^sub>R norm y = norm y *\<^sub>R (y /\<^sub>R norm y) /\<^sub>R norm (norm y *\<^sub>R (y /\<^sub>R norm y))" 

344 
by force 

345 
then have "proj ((norm y / norm x) *\<^sub>R x) = proj y" 

346 
by (metis (no_types) divide_inverse local.proj_def eq scaleR_scaleR) 

347 
then have [simp]: "(norm y / norm x) *\<^sub>R x = y" 

348 
by (rule eqI) (simp add: \<open>x \<noteq> 0\<close>) 

349 
have no: "0 \<le> norm y / norm x" "norm y / norm x < 1" 

350 
using * by (auto simp: divide_simps) 

351 
then show "x = y" 

352 
using starI [OF \<open>x \<in> S\<close> no] xynot by auto 

353 
qed 

354 
qed 

355 
have "\<exists>surf. homeomorphism (S  rel_interior S) ?SPHER proj surf" 

356 
proof (rule homeomorphism_compact) 

357 
show "compact (S  rel_interior S)" 

358 
using \<open>compact S\<close> compact_rel_boundary by blast 

359 
show "continuous_on (S  rel_interior S) proj" 

360 
using 0 by (blast intro: continuous_on_subset [OF cont_proj]) 

361 
show "proj ` (S  rel_interior S) = ?SPHER" 

362 
proof 

363 
show "proj ` (S  rel_interior S) \<subseteq> ?SPHER" 

364 
using 0 by (force simp: hull_inc projI intro: nproj1) 

365 
show "?SPHER \<subseteq> proj ` (S  rel_interior S)" 

366 
proof (clarsimp simp: proj_def) 

367 
fix x 

368 
assume "x \<in> affine hull S" and nox: "norm x = 1" 

369 
then have "x \<noteq> 0" by auto 

370 
obtain d where "0 < d" and dx: "(d *\<^sub>R x) \<in> rel_frontier S" 

371 
and ri: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (e *\<^sub>R x) \<in> rel_interior S" 

372 
using ray_to_rel_frontier [OF \<open>bounded S\<close> 0] \<open>x \<in> affine hull S\<close> \<open>x \<noteq> 0\<close> by auto 

373 
show "x \<in> (\<lambda>x. x /\<^sub>R norm x) ` (S  rel_interior S)" 

374 
apply (rule_tac x="d *\<^sub>R x" in image_eqI) 

375 
using \<open>0 < d\<close> 

376 
using dx \<open>closed S\<close> apply (auto simp: rel_frontier_def divide_simps nox) 

377 
done 

378 
qed 

379 
qed 

380 
qed (rule inj_on_proj) 

381 
then obtain surf where surf: "homeomorphism (S  rel_interior S) ?SPHER proj surf" 

382 
by blast 

383 
then have cont_surf: "continuous_on (proj ` (S  rel_interior S)) surf" 

384 
by (auto simp: homeomorphism_def) 

385 
have surf_nz: "\<And>x. x \<in> ?SPHER \<Longrightarrow> surf x \<noteq> 0" 

386 
by (metis "0" DiffE homeomorphism_def imageI surf) 

387 
have cont_nosp: "continuous_on (?SPHER) (\<lambda>x. norm x *\<^sub>R ((surf o proj) x))" 

388 
apply (rule continuous_intros)+ 

389 
apply (rule continuous_on_subset [OF cont_proj], force) 

390 
apply (rule continuous_on_subset [OF cont_surf]) 

391 
apply (force simp: homeomorphism_image1 [OF surf] dest: proj_spherI) 

392 
done 

393 
have surfpS: "\<And>x. \<lbrakk>norm x = 1; x \<in> affine hull S\<rbrakk> \<Longrightarrow> surf (proj x) \<in> S" 

394 
by (metis (full_types) DiffE \<open>0 \<in> S\<close> homeomorphism_def image_eqI norm_zero proj_spherI real_vector.scale_zero_left scaleR_one surf) 

395 
have *: "\<exists>y. norm y = 1 \<and> y \<in> affine hull S \<and> x = surf (proj y)" 

396 
if "x \<in> S" "x \<notin> rel_interior S" for x 

397 
proof  

398 
have "proj x \<in> ?SPHER" 

399 
by (metis (full_types) "0" hull_inc proj_spherI that) 

400 
moreover have "surf (proj x) = x" 

401 
by (metis Diff_iff homeomorphism_def surf that) 

402 
ultimately show ?thesis 

403 
by (metis \<open>\<And>x. x \<in> ?SPHER \<Longrightarrow> surf x \<noteq> 0\<close> hull_inc inverse_1 local.proj_def norm_sgn projI scaleR_one sgn_div_norm that(1)) 

404 
qed 

405 
have surfp_notin: "\<And>x. \<lbrakk>norm x = 1; x \<in> affine hull S\<rbrakk> \<Longrightarrow> surf (proj x) \<notin> rel_interior S" 

406 
by (metis (full_types) DiffE one_neq_zero homeomorphism_def image_eqI norm_zero proj_spherI surf) 

407 
have no_sp_im: "(\<lambda>x. norm x *\<^sub>R surf (proj x)) ` (?SPHER) = S  rel_interior S" 

408 
by (auto simp: surfpS image_def Bex_def surfp_notin *) 

409 
have inj_spher: "inj_on (\<lambda>x. norm x *\<^sub>R surf (proj x)) ?SPHER" 

410 
proof 

411 
fix x y 

412 
assume xy: "x \<in> ?SPHER" "y \<in> ?SPHER" 

413 
and eq: " norm x *\<^sub>R surf (proj x) = norm y *\<^sub>R surf (proj y)" 

414 
then have "norm x = 1" "norm y = 1" "x \<in> affine hull S" "y \<in> affine hull S" 

415 
using 0 by auto 

416 
with eq show "x = y" 

417 
by (simp add: proj_def) (metis surf xy homeomorphism_def) 

418 
qed 

419 
have co01: "compact ?SPHER" 

420 
by (simp add: closed_affine_hull compact_Int_closed) 

421 
show "?SMINUS homeomorphic ?SPHER" 

422 
apply (subst homeomorphic_sym) 

423 
apply (rule homeomorphic_compact [OF co01 cont_nosp [unfolded o_def] no_sp_im inj_spher]) 

424 
done 

425 
have proj_scaleR: "\<And>a x. 0 < a \<Longrightarrow> proj (a *\<^sub>R x) = proj x" 

426 
by (simp add: proj_def) 

427 
have cont_sp0: "continuous_on (affine hull S  {0}) (surf o proj)" 

428 
apply (rule continuous_on_compose [OF continuous_on_subset [OF cont_proj]], force) 

429 
apply (rule continuous_on_subset [OF cont_surf]) 

430 
using homeomorphism_image1 proj_spherI surf by fastforce 

431 
obtain B where "B>0" and B: "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B" 

432 
by (metis compact_imp_bounded \<open>compact S\<close> bounded_pos_less less_eq_real_def) 

433 
have cont_nosp: "continuous (at x within ?CBALL) (\<lambda>x. norm x *\<^sub>R surf (proj x))" 

434 
if "norm x \<le> 1" "x \<in> affine hull S" for x 

435 
proof (cases "x=0") 

436 
case True 

437 
show ?thesis using True 

438 
apply (simp add: continuous_within) 

439 
apply (rule lim_null_scaleR_bounded [where B=B]) 

440 
apply (simp_all add: tendsto_norm_zero eventually_at) 

441 
apply (rule_tac x=B in exI) 

442 
using B surfpS proj_def projI apply (auto simp: \<open>B > 0\<close>) 

443 
done 

444 
next 

445 
case False 

446 
then have "\<forall>\<^sub>F x in at x. (x \<in> affine hull S  {0}) = (x \<in> affine hull S)" 

447 
apply (simp add: eventually_at) 

448 
apply (rule_tac x="norm x" in exI) 

449 
apply (auto simp: False) 

450 
done 

451 
with cont_sp0 have *: "continuous (at x within affine hull S) (\<lambda>x. surf (proj x))" 

452 
apply (simp add: continuous_on_eq_continuous_within) 

453 
apply (drule_tac x=x in bspec, force simp: False that) 

454 
apply (simp add: continuous_within Lim_transform_within_set) 

455 
done 

456 
show ?thesis 

457 
apply (rule continuous_within_subset [where s = "affine hull S", OF _ Int_lower2]) 

458 
apply (rule continuous_intros *)+ 

459 
done 

460 
qed 

461 
have cont_nosp2: "continuous_on ?CBALL (\<lambda>x. norm x *\<^sub>R ((surf o proj) x))" 

462 
by (simp add: continuous_on_eq_continuous_within cont_nosp) 

463 
have "norm y *\<^sub>R surf (proj y) \<in> S" if "y \<in> cball 0 1" and yaff: "y \<in> affine hull S" for y 

464 
proof (cases "y=0") 

465 
case True then show ?thesis 

466 
by (simp add: \<open>0 \<in> S\<close>) 

467 
next 

468 
case False 

469 
then have "norm y *\<^sub>R surf (proj y) = norm y *\<^sub>R surf (proj (y /\<^sub>R norm y))" 

470 
by (simp add: proj_def) 

471 
have "norm y \<le> 1" using that by simp 

472 
have "surf (proj (y /\<^sub>R norm y)) \<in> S" 

473 
apply (rule surfpS) 

474 
using proj_def projI yaff 

475 
by (auto simp: False) 

476 
then have "surf (proj y) \<in> S" 

477 
by (simp add: False proj_def) 

478 
then show "norm y *\<^sub>R surf (proj y) \<in> S" 

479 
by (metis dual_order.antisym le_less_linear norm_ge_zero rel_interior_subset scaleR_one 

480 
starI subset_eq \<open>norm y \<le> 1\<close>) 

481 
qed 

482 
moreover have "x \<in> (\<lambda>x. norm x *\<^sub>R surf (proj x)) ` (?CBALL)" if "x \<in> S" for x 

483 
proof (cases "x=0") 

484 
case True with that hull_inc show ?thesis by fastforce 

485 
next 

486 
case False 

487 
then have psp: "proj (surf (proj x)) = proj x" 

488 
by (metis homeomorphism_def hull_inc proj_spherI surf that) 

489 
have nxx: "norm x *\<^sub>R proj x = x" 

490 
by (simp add: False local.proj_def) 

491 
have affineI: "(1 / norm (surf (proj x))) *\<^sub>R x \<in> affine hull S" 

492 
by (metis \<open>0 \<in> S\<close> affine_hull_span_0 hull_inc span_clauses(4) that) 

493 
have sproj_nz: "surf (proj x) \<noteq> 0" 

494 
by (metis False proj0_iff psp) 

495 
then have "proj x = proj (proj x)" 

496 
by (metis False nxx proj_scaleR zero_less_norm_iff) 

497 
moreover have scaleproj: "\<And>a r. r *\<^sub>R proj a = (r / norm a) *\<^sub>R a" 

498 
by (simp add: divide_inverse local.proj_def) 

499 
ultimately have "(norm (surf (proj x)) / norm x) *\<^sub>R x \<notin> rel_interior S" 

500 
by (metis (no_types) sproj_nz divide_self_if hull_inc norm_eq_zero nproj1 projI psp scaleR_one surfp_notin that) 

501 
then have "(norm (surf (proj x)) / norm x) \<ge> 1" 

502 
using starI [OF that] by (meson starI [OF that] le_less_linear norm_ge_zero zero_le_divide_iff) 

503 
then have nole: "norm x \<le> norm (surf (proj x))" 

504 
by (simp add: le_divide_eq_1) 

505 
show ?thesis 

506 
apply (rule_tac x="inverse(norm(surf (proj x))) *\<^sub>R x" in image_eqI) 

507 
apply (metis (no_types, hide_lams) mult.commute scaleproj abs_inverse abs_norm_cancel divide_inverse norm_scaleR nxx positive_imp_inverse_positive proj_scaleR psp sproj_nz zero_less_norm_iff) 

508 
apply (auto simp: divide_simps nole affineI) 

509 
done 

510 
qed 

511 
ultimately have im_cball: "(\<lambda>x. norm x *\<^sub>R surf (proj x)) ` ?CBALL = S" 

512 
by blast 

513 
have inj_cball: "inj_on (\<lambda>x. norm x *\<^sub>R surf (proj x)) ?CBALL" 

514 
proof 

515 
fix x y 

516 
assume "x \<in> ?CBALL" "y \<in> ?CBALL" 

517 
and eq: "norm x *\<^sub>R surf (proj x) = norm y *\<^sub>R surf (proj y)" 

518 
then have x: "x \<in> affine hull S" and y: "y \<in> affine hull S" 

519 
using 0 by auto 

520 
show "x = y" 

521 
proof (cases "x=0 \<or> y=0") 

522 
case True then show "x = y" using eq proj_spherI surf_nz x y by force 

523 
next 

524 
case False 

525 
with x y have speq: "surf (proj x) = surf (proj y)" 

526 
by (metis eq homeomorphism_apply2 proj_scaleR proj_spherI surf zero_less_norm_iff) 

527 
then have "norm x = norm y" 

528 
by (metis \<open>x \<in> affine hull S\<close> \<open>y \<in> affine hull S\<close> eq proj_spherI real_vector.scale_cancel_right surf_nz) 

529 
moreover have "proj x = proj y" 

530 
by (metis (no_types) False speq homeomorphism_apply2 proj_spherI surf x y) 

531 
ultimately show "x = y" 

532 
using eq eqI by blast 

533 
qed 

534 
qed 

535 
have co01: "compact ?CBALL" 

536 
by (simp add: closed_affine_hull compact_Int_closed) 

537 
show "S homeomorphic ?CBALL" 

538 
apply (subst homeomorphic_sym) 

539 
apply (rule homeomorphic_compact [OF co01 cont_nosp2 [unfolded o_def] im_cball inj_cball]) 

540 
done 

541 
qed 

542 

543 
corollary 

544 
fixes S :: "'a::euclidean_space set" 

545 
assumes "compact S" and a: "a \<in> rel_interior S" 

546 
and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment a x \<subseteq> rel_interior S" 

547 
shows starlike_compact_projective1: 

548 
"S  rel_interior S homeomorphic sphere a 1 \<inter> affine hull S" 

549 
and starlike_compact_projective2: 

550 
"S homeomorphic cball a 1 \<inter> affine hull S" 

551 
proof  

552 
have 1: "compact (op+ (a) ` S)" by (meson assms compact_translation) 

553 
have 2: "0 \<in> rel_interior (op+ (a) ` S)" 

554 
by (simp add: a rel_interior_translation) 

555 
have 3: "open_segment 0 x \<subseteq> rel_interior (op+ (a) ` S)" if "x \<in> (op+ (a) ` S)" for x 

556 
proof  

557 
have "x+a \<in> S" using that by auto 

558 
then have "open_segment a (x+a) \<subseteq> rel_interior S" by (metis star) 

559 
then show ?thesis using open_segment_translation 

560 
using rel_interior_translation by fastforce 

561 
qed 

562 
have "S  rel_interior S homeomorphic (op+ (a) ` S)  rel_interior (op+ (a) ` S)" 

563 
by (metis rel_interior_translation translation_diff homeomorphic_translation) 

564 
also have "... homeomorphic sphere 0 1 \<inter> affine hull (op+ (a) ` S)" 

565 
by (rule starlike_compact_projective1_0 [OF 1 2 3]) 

566 
also have "... = op+ (a) ` (sphere a 1 \<inter> affine hull S)" 

567 
by (metis affine_hull_translation left_minus sphere_translation translation_Int) 

568 
also have "... homeomorphic sphere a 1 \<inter> affine hull S" 

569 
using homeomorphic_translation homeomorphic_sym by blast 

570 
finally show "S  rel_interior S homeomorphic sphere a 1 \<inter> affine hull S" . 

571 

572 
have "S homeomorphic (op+ (a) ` S)" 

573 
by (metis homeomorphic_translation) 

574 
also have "... homeomorphic cball 0 1 \<inter> affine hull (op+ (a) ` S)" 

575 
by (rule starlike_compact_projective2_0 [OF 1 2 3]) 

576 
also have "... = op+ (a) ` (cball a 1 \<inter> affine hull S)" 

577 
by (metis affine_hull_translation left_minus cball_translation translation_Int) 

578 
also have "... homeomorphic cball a 1 \<inter> affine hull S" 

579 
using homeomorphic_translation homeomorphic_sym by blast 

580 
finally show "S homeomorphic cball a 1 \<inter> affine hull S" . 

581 
qed 

582 

583 
corollary starlike_compact_projective_special: 

584 
assumes "compact S" 

585 
and cb01: "cball (0::'a::euclidean_space) 1 \<subseteq> S" 

586 
and scale: "\<And>x u. \<lbrakk>x \<in> S; 0 \<le> u; u < 1\<rbrakk> \<Longrightarrow> u *\<^sub>R x \<in> S  frontier S" 

587 
shows "S homeomorphic (cball (0::'a::euclidean_space) 1)" 

588 
proof  

589 
have "ball 0 1 \<subseteq> interior S" 

590 
using cb01 interior_cball interior_mono by blast 

591 
then have 0: "0 \<in> rel_interior S" 

592 
by (meson centre_in_ball subsetD interior_subset_rel_interior le_numeral_extra(2) not_le) 

593 
have [simp]: "affine hull S = UNIV" 

594 
using \<open>ball 0 1 \<subseteq> interior S\<close> by (auto intro!: affine_hull_nonempty_interior) 

595 
have star: "open_segment 0 x \<subseteq> rel_interior S" if "x \<in> S" for x 

63627  596 
proof 
63130  597 
fix p assume "p \<in> open_segment 0 x" 
598 
then obtain u where "x \<noteq> 0" and u: "0 \<le> u" "u < 1" and p: "u *\<^sub>R x = p" 

63627  599 
by (auto simp: in_segment) 
63130  600 
then show "p \<in> rel_interior S" 
601 
using scale [OF that u] closure_subset frontier_def interior_subset_rel_interior by fastforce 

602 
qed 

603 
show ?thesis 

604 
using starlike_compact_projective2_0 [OF \<open>compact S\<close> 0 star] by simp 

605 
qed 

606 

607 
lemma homeomorphic_convex_lemma: 

608 
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" 

609 
assumes "convex S" "compact S" "convex T" "compact T" 

610 
and affeq: "aff_dim S = aff_dim T" 

611 
shows "(S  rel_interior S) homeomorphic (T  rel_interior T) \<and> 

612 
S homeomorphic T" 

613 
proof (cases "rel_interior S = {} \<or> rel_interior T = {}") 

614 
case True 

615 
then show ?thesis 

616 
by (metis Diff_empty affeq \<open>convex S\<close> \<open>convex T\<close> aff_dim_empty homeomorphic_empty rel_interior_eq_empty aff_dim_empty) 

617 
next 

618 
case False 

619 
then obtain a b where a: "a \<in> rel_interior S" and b: "b \<in> rel_interior T" by auto 

620 
have starS: "\<And>x. x \<in> S \<Longrightarrow> open_segment a x \<subseteq> rel_interior S" 

621 
using rel_interior_closure_convex_segment 

622 
a \<open>convex S\<close> closure_subset subsetCE by blast 

623 
have starT: "\<And>x. x \<in> T \<Longrightarrow> open_segment b x \<subseteq> rel_interior T" 

624 
using rel_interior_closure_convex_segment 

625 
b \<open>convex T\<close> closure_subset subsetCE by blast 

626 
let ?aS = "op+ (a) ` S" and ?bT = "op+ (b) ` T" 

627 
have 0: "0 \<in> affine hull ?aS" "0 \<in> affine hull ?bT" 

628 
by (metis a b subsetD hull_inc image_eqI left_minus rel_interior_subset)+ 

629 
have subs: "subspace (span ?aS)" "subspace (span ?bT)" 

630 
by (rule subspace_span)+ 

631 
moreover 

632 
have "dim (span (op + ( a) ` S)) = dim (span (op + ( b) ` T))" 

633 
by (metis 0 aff_dim_translation_eq aff_dim_zero affeq dim_span nat_int) 

634 
ultimately obtain f g where "linear f" "linear g" 

635 
and fim: "f ` span ?aS = span ?bT" 

636 
and gim: "g ` span ?bT = span ?aS" 

637 
and fno: "\<And>x. x \<in> span ?aS \<Longrightarrow> norm(f x) = norm x" 

638 
and gno: "\<And>x. x \<in> span ?bT \<Longrightarrow> norm(g x) = norm x" 

639 
and gf: "\<And>x. x \<in> span ?aS \<Longrightarrow> g(f x) = x" 

640 
and fg: "\<And>x. x \<in> span ?bT \<Longrightarrow> f(g x) = x" 

641 
by (rule isometries_subspaces) blast 

642 
have [simp]: "continuous_on A f" for A 

643 
using \<open>linear f\<close> linear_conv_bounded_linear linear_continuous_on by blast 

644 
have [simp]: "continuous_on B g" for B 

645 
using \<open>linear g\<close> linear_conv_bounded_linear linear_continuous_on by blast 

646 
have eqspanS: "affine hull ?aS = span ?aS" 

647 
by (metis a affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset) 

648 
have eqspanT: "affine hull ?bT = span ?bT" 

649 
by (metis b affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset) 

650 
have "S homeomorphic cball a 1 \<inter> affine hull S" 

651 
by (rule starlike_compact_projective2 [OF \<open>compact S\<close> a starS]) 

652 
also have "... homeomorphic op+ (a) ` (cball a 1 \<inter> affine hull S)" 

653 
by (metis homeomorphic_translation) 

654 
also have "... = cball 0 1 \<inter> op+ (a) ` (affine hull S)" 

655 
by (auto simp: dist_norm) 

656 
also have "... = cball 0 1 \<inter> span ?aS" 

657 
using eqspanS affine_hull_translation by blast 

658 
also have "... homeomorphic cball 0 1 \<inter> span ?bT" 

659 
proof (rule homeomorphicI [where f=f and g=g]) 

660 
show fim1: "f ` (cball 0 1 \<inter> span ?aS) = cball 0 1 \<inter> span ?bT" 

661 
apply (rule subset_antisym) 

662 
using fim fno apply (force simp:, clarify) 

663 
by (metis IntI fg gim gno image_eqI mem_cball_0) 

664 
show "g ` (cball 0 1 \<inter> span ?bT) = cball 0 1 \<inter> span ?aS" 

665 
apply (rule subset_antisym) 

666 
using gim gno apply (force simp:, clarify) 

667 
by (metis IntI fim1 gf image_eqI) 

668 
qed (auto simp: fg gf) 

669 
also have "... = cball 0 1 \<inter> op+ (b) ` (affine hull T)" 

670 
using eqspanT affine_hull_translation by blast 

671 
also have "... = op+ (b) ` (cball b 1 \<inter> affine hull T)" 

672 
by (auto simp: dist_norm) 

673 
also have "... homeomorphic (cball b 1 \<inter> affine hull T)" 

674 
by (metis homeomorphic_translation homeomorphic_sym) 

675 
also have "... homeomorphic T" 

676 
by (metis starlike_compact_projective2 [OF \<open>compact T\<close> b starT] homeomorphic_sym) 

677 
finally have 1: "S homeomorphic T" . 

678 

679 
have "S  rel_interior S homeomorphic sphere a 1 \<inter> affine hull S" 

680 
by (rule starlike_compact_projective1 [OF \<open>compact S\<close> a starS]) 

681 
also have "... homeomorphic op+ (a) ` (sphere a 1 \<inter> affine hull S)" 

682 
by (metis homeomorphic_translation) 

683 
also have "... = sphere 0 1 \<inter> op+ (a) ` (affine hull S)" 

684 
by (auto simp: dist_norm) 

685 
also have "... = sphere 0 1 \<inter> span ?aS" 

686 
using eqspanS affine_hull_translation by blast 

687 
also have "... homeomorphic sphere 0 1 \<inter> span ?bT" 

688 
proof (rule homeomorphicI [where f=f and g=g]) 

689 
show fim1: "f ` (sphere 0 1 \<inter> span ?aS) = sphere 0 1 \<inter> span ?bT" 

690 
apply (rule subset_antisym) 

691 
using fim fno apply (force simp:, clarify) 

692 
by (metis IntI fg gim gno image_eqI mem_sphere_0) 

693 
show "g ` (sphere 0 1 \<inter> span ?bT) = sphere 0 1 \<inter> span ?aS" 

694 
apply (rule subset_antisym) 

695 
using gim gno apply (force simp:, clarify) 

696 
by (metis IntI fim1 gf image_eqI) 

697 
qed (auto simp: fg gf) 

698 
also have "... = sphere 0 1 \<inter> op+ (b) ` (affine hull T)" 

699 
using eqspanT affine_hull_translation by blast 

700 
also have "... = op+ (b) ` (sphere b 1 \<inter> affine hull T)" 

701 
by (auto simp: dist_norm) 

702 
also have "... homeomorphic (sphere b 1 \<inter> affine hull T)" 

703 
by (metis homeomorphic_translation homeomorphic_sym) 

704 
also have "... homeomorphic T  rel_interior T" 

705 
by (metis starlike_compact_projective1 [OF \<open>compact T\<close> b starT] homeomorphic_sym) 

706 
finally have 2: "S  rel_interior S homeomorphic T  rel_interior T" . 

707 
show ?thesis 

708 
using 1 2 by blast 

709 
qed 

710 

711 
lemma homeomorphic_convex_compact_sets: 

712 
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" 

713 
assumes "convex S" "compact S" "convex T" "compact T" 

714 
and affeq: "aff_dim S = aff_dim T" 

715 
shows "S homeomorphic T" 

716 
using homeomorphic_convex_lemma [OF assms] assms 

717 
by (auto simp: rel_frontier_def) 

718 

719 
lemma homeomorphic_rel_frontiers_convex_bounded_sets: 

720 
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" 

721 
assumes "convex S" "bounded S" "convex T" "bounded T" 

722 
and affeq: "aff_dim S = aff_dim T" 

723 
shows "rel_frontier S homeomorphic rel_frontier T" 

724 
using assms homeomorphic_convex_lemma [of "closure S" "closure T"] 

725 
by (simp add: rel_frontier_def convex_rel_interior_closure) 

726 

727 

728 
subsection\<open>Homeomorphisms between punctured spheres and affine sets\<close> 

729 
text\<open>Including the famous stereoscopic projection of the 3D sphere to the complex plane\<close> 

730 

731 
text\<open>The special case with centre 0 and radius 1\<close> 

732 
lemma homeomorphic_punctured_affine_sphere_affine_01: 

733 
assumes "b \<in> sphere 0 1" "affine T" "0 \<in> T" "b \<in> T" "affine p" 

734 
and affT: "aff_dim T = aff_dim p + 1" 

735 
shows "(sphere 0 1 \<inter> T)  {b} homeomorphic p" 

736 
proof  

737 
have [simp]: "norm b = 1" "b\<bullet>b = 1" 

738 
using assms by (auto simp: norm_eq_1) 

739 
have [simp]: "T \<inter> {v. b\<bullet>v = 0} \<noteq> {}" 

740 
using \<open>0 \<in> T\<close> by auto 

741 
have [simp]: "\<not> T \<subseteq> {v. b\<bullet>v = 0}" 

742 
using \<open>norm b = 1\<close> \<open>b \<in> T\<close> by auto 

743 
define f where "f \<equiv> \<lambda>x. 2 *\<^sub>R b + (2 / (1  b\<bullet>x)) *\<^sub>R (x  b)" 

744 
define g where "g \<equiv> \<lambda>y. b + (4 / (norm y ^ 2 + 4)) *\<^sub>R (y  2 *\<^sub>R b)" 

745 
have [simp]: "\<And>x. \<lbrakk>x \<in> T; b\<bullet>x = 0\<rbrakk> \<Longrightarrow> f (g x) = x" 

746 
unfolding f_def g_def by (simp add: algebra_simps divide_simps add_nonneg_eq_0_iff) 

747 
have no: "\<And>x. \<lbrakk>norm x = 1; b\<bullet>x \<noteq> 1\<rbrakk> \<Longrightarrow> (norm (f x))\<^sup>2 = 4 * (1 + b\<bullet>x) / (1  b\<bullet>x)" 

748 
apply (simp add: dot_square_norm [symmetric]) 

749 
apply (simp add: f_def vector_add_divide_simps divide_simps norm_eq_1) 

750 
apply (simp add: algebra_simps inner_commute) 

751 
done 

752 
have [simp]: "\<And>u::real. 8 + u * (u * 8) = u * 16 \<longleftrightarrow> u=1" 

753 
by algebra 

754 
have [simp]: "\<And>x. \<lbrakk>norm x = 1; b \<bullet> x \<noteq> 1\<rbrakk> \<Longrightarrow> g (f x) = x" 

755 
unfolding g_def no by (auto simp: f_def divide_simps) 

756 
have [simp]: "\<And>x. \<lbrakk>x \<in> T; b \<bullet> x = 0\<rbrakk> \<Longrightarrow> norm (g x) = 1" 

757 
unfolding g_def 

758 
apply (rule power2_eq_imp_eq) 

759 
apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps) 

760 
apply (simp add: algebra_simps inner_commute) 

761 
done 

762 
have [simp]: "\<And>x. \<lbrakk>x \<in> T; b \<bullet> x = 0\<rbrakk> \<Longrightarrow> b \<bullet> g x \<noteq> 1" 

763 
unfolding g_def 

764 
apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps add_nonneg_eq_0_iff) 

765 
apply (auto simp: algebra_simps) 

766 
done 

767 
have "subspace T" 

768 
by (simp add: assms subspace_affine) 

769 
have [simp]: "\<And>x. \<lbrakk>x \<in> T; b \<bullet> x = 0\<rbrakk> \<Longrightarrow> g x \<in> T" 

770 
unfolding g_def 

771 
by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff) 

772 
have "f ` {x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<subseteq> {x. b\<bullet>x = 0}" 

773 
unfolding f_def using \<open>norm b = 1\<close> norm_eq_1 

774 
by (force simp: field_simps inner_add_right inner_diff_right) 

775 
moreover have "f ` T \<subseteq> T" 

776 
unfolding f_def using assms 

777 
apply (auto simp: field_simps inner_add_right inner_diff_right) 

778 
by (metis add_0 diff_zero mem_affine_3_minus) 

779 
moreover have "{x. b\<bullet>x = 0} \<inter> T \<subseteq> f ` ({x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T)" 

780 
apply clarify 

781 
apply (rule_tac x = "g x" in image_eqI, auto) 

782 
done 

783 
ultimately have imf: "f ` ({x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T) = {x. b\<bullet>x = 0} \<inter> T" 

784 
by blast 

785 
have no4: "\<And>y. b\<bullet>y = 0 \<Longrightarrow> norm ((y\<bullet>y + 4) *\<^sub>R b + 4 *\<^sub>R (y  2 *\<^sub>R b)) = y\<bullet>y + 4" 

786 
apply (rule power2_eq_imp_eq) 

787 
apply (simp_all add: dot_square_norm [symmetric]) 

788 
apply (auto simp: power2_eq_square algebra_simps inner_commute) 

789 
done 

790 
have [simp]: "\<And>x. \<lbrakk>norm x = 1; b \<bullet> x \<noteq> 1\<rbrakk> \<Longrightarrow> b \<bullet> f x = 0" 

791 
by (simp add: f_def algebra_simps divide_simps) 

792 
have [simp]: "\<And>x. \<lbrakk>x \<in> T; norm x = 1; b \<bullet> x \<noteq> 1\<rbrakk> \<Longrightarrow> f x \<in> T" 

793 
unfolding f_def 

794 
by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff) 

795 
have "g ` {x. b\<bullet>x = 0} \<subseteq> {x. norm x = 1 \<and> b\<bullet>x \<noteq> 1}" 

796 
unfolding g_def 

797 
apply (clarsimp simp: no4 vector_add_divide_simps divide_simps add_nonneg_eq_0_iff dot_square_norm [symmetric]) 

798 
apply (auto simp: algebra_simps) 

799 
done 

800 
moreover have "g ` T \<subseteq> T" 

801 
unfolding g_def 

802 
by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff) 

803 
moreover have "{x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T \<subseteq> g ` ({x. b\<bullet>x = 0} \<inter> T)" 

804 
apply clarify 

805 
apply (rule_tac x = "f x" in image_eqI, auto) 

806 
done 

807 
ultimately have img: "g ` ({x. b\<bullet>x = 0} \<inter> T) = {x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T" 

808 
by blast 

809 
have aff: "affine ({x. b\<bullet>x = 0} \<inter> T)" 

810 
by (blast intro: affine_hyperplane assms) 

811 
have contf: "continuous_on ({x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T) f" 

812 
unfolding f_def by (rule continuous_intros  force)+ 

813 
have contg: "continuous_on ({x. b\<bullet>x = 0} \<inter> T) g" 

814 
unfolding g_def by (rule continuous_intros  force simp: add_nonneg_eq_0_iff)+ 

815 
have "(sphere 0 1 \<inter> T)  {b} = {x. norm x = 1 \<and> (b\<bullet>x \<noteq> 1)} \<inter> T" 

816 
using \<open>norm b = 1\<close> by (auto simp: norm_eq_1) (metis vector_eq \<open>b\<bullet>b = 1\<close>) 

817 
also have "... homeomorphic {x. b\<bullet>x = 0} \<inter> T" 

818 
by (rule homeomorphicI [OF imf img contf contg]) auto 

819 
also have "... homeomorphic p" 

820 
apply (rule homeomorphic_affine_sets [OF aff \<open>affine p\<close>]) 

821 
apply (simp add: Int_commute aff_dim_affine_Int_hyperplane [OF \<open>affine T\<close>] affT) 

822 
done 

823 
finally show ?thesis . 

824 
qed 

825 

826 
theorem homeomorphic_punctured_affine_sphere_affine: 

827 
fixes a :: "'a :: euclidean_space" 

828 
assumes "0 < r" "b \<in> sphere a r" "affine T" "a \<in> T" "b \<in> T" "affine p" 

829 
and aff: "aff_dim T = aff_dim p + 1" 

66710
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

830 
shows "(sphere a r \<inter> T)  {b} homeomorphic p" 
63130  831 
proof  
832 
have "a \<noteq> b" using assms by auto 

833 
then have inj: "inj (\<lambda>x::'a. x /\<^sub>R norm (a  b))" 

834 
by (simp add: inj_on_def) 

835 
have "((sphere a r \<inter> T)  {b}) homeomorphic 

836 
op+ (a) ` ((sphere a r \<inter> T)  {b})" 

837 
by (rule homeomorphic_translation) 

838 
also have "... homeomorphic op *\<^sub>R (inverse r) ` op + ( a) ` (sphere a r \<inter> T  {b})" 

839 
by (metis \<open>0 < r\<close> homeomorphic_scaling inverse_inverse_eq inverse_zero less_irrefl) 

840 
also have "... = sphere 0 1 \<inter> (op *\<^sub>R (inverse r) ` op + ( a) ` T)  {(b  a) /\<^sub>R r}" 

841 
using assms by (auto simp: dist_norm norm_minus_commute divide_simps) 

842 
also have "... homeomorphic p" 

843 
apply (rule homeomorphic_punctured_affine_sphere_affine_01) 

844 
using assms 

845 
apply (auto simp: dist_norm norm_minus_commute affine_scaling affine_translation [symmetric] aff_dim_translation_eq inj) 

846 
done 

847 
finally show ?thesis . 

848 
qed 

849 

66710
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

850 
corollary homeomorphic_punctured_sphere_affine: 
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

851 
fixes a :: "'a :: euclidean_space" 
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

852 
assumes "0 < r" and b: "b \<in> sphere a r" 
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

853 
and "affine T" and affS: "aff_dim T + 1 = DIM('a)" 
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

854 
shows "(sphere a r  {b}) homeomorphic T" 
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

855 
using homeomorphic_punctured_affine_sphere_affine [of r b a UNIV T] assms by auto 
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

856 

676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

857 
corollary homeomorphic_punctured_sphere_hyperplane: 
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

858 
fixes a :: "'a :: euclidean_space" 
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

859 
assumes "0 < r" and b: "b \<in> sphere a r" 
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

860 
and "c \<noteq> 0" 
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

861 
shows "(sphere a r  {b}) homeomorphic {x::'a. c \<bullet> x = d}" 
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

862 
apply (rule homeomorphic_punctured_sphere_affine) 
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

863 
using assms 
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

864 
apply (auto simp: affine_hyperplane of_nat_diff) 
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

865 
done 
676258a1cf01
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66690
diff
changeset

866 

63130  867 
proposition homeomorphic_punctured_sphere_affine_gen: 
868 
fixes a :: "'a :: euclidean_space" 

869 
assumes "convex S" "bounded S" and a: "a \<in> rel_frontier S" 

870 
and "affine T" and affS: "aff_dim S = aff_dim T + 1" 

871 
shows "rel_frontier S  {a} homeomorphic T" 

872 
proof  

66690
6953b1a29e19
Tiny presentational improvements to homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66287
diff
changeset

873 
obtain U :: "'a set" where "affine U" "convex U" and affdS: "aff_dim U = aff_dim S" 
63130  874 
using choose_affine_subset [OF affine_UNIV aff_dim_geq] 
66690
6953b1a29e19
Tiny presentational improvements to homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66287
diff
changeset

875 
by (meson aff_dim_affine_hull affine_affine_hull affine_imp_convex) 
6953b1a29e19
Tiny presentational improvements to homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66287
diff
changeset

876 
have "S \<noteq> {}" using assms by auto 
63130  877 
then obtain z where "z \<in> U" 
66690
6953b1a29e19
Tiny presentational improvements to homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66287
diff
changeset

878 
by (metis aff_dim_negative_iff equals0I affdS) 
63130  879 
then have bne: "ball z 1 \<inter> U \<noteq> {}" by force 
66690
6953b1a29e19
Tiny presentational improvements to homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66287
diff
changeset

880 
then have [simp]: "aff_dim(ball z 1 \<inter> U) = aff_dim U" 
6953b1a29e19
Tiny presentational improvements to homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66287
diff
changeset

881 
using aff_dim_convex_Int_open [OF \<open>convex U\<close> open_ball] 
63130  882 
by (fastforce simp add: Int_commute) 
883 
have "rel_frontier S homeomorphic rel_frontier (ball z 1 \<inter> U)" 

884 
apply (rule homeomorphic_rel_frontiers_convex_bounded_sets) 

885 
apply (auto simp: \<open>affine U\<close> affine_imp_convex convex_Int affdS assms) 

886 
done 

887 
also have "... = sphere z 1 \<inter> U" 

888 
using convex_affine_rel_frontier_Int [of "ball z 1" U] 

889 
by (simp add: \<open>affine U\<close> bne) 

66690
6953b1a29e19
Tiny presentational improvements to homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66287
diff
changeset

890 
finally have "rel_frontier S homeomorphic sphere z 1 \<inter> U" . 
6953b1a29e19
Tiny presentational improvements to homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66287
diff
changeset

891 
then obtain h k where him: "h ` rel_frontier S = sphere z 1 \<inter> U" 
63130  892 
and kim: "k ` (sphere z 1 \<inter> U) = rel_frontier S" 
893 
and hcon: "continuous_on (rel_frontier S) h" 

894 
and kcon: "continuous_on (sphere z 1 \<inter> U) k" 

895 
and kh: "\<And>x. x \<in> rel_frontier S \<Longrightarrow> k(h(x)) = x" 

896 
and hk: "\<And>y. y \<in> sphere z 1 \<inter> U \<Longrightarrow> h(k(y)) = y" 

897 
unfolding homeomorphic_def homeomorphism_def by auto 

898 
have "rel_frontier S  {a} homeomorphic (sphere z 1 \<inter> U)  {h a}" 

66690
6953b1a29e19
Tiny presentational improvements to homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66287
diff
changeset

899 
proof (rule homeomorphicI) 
63130  900 
show h: "h ` (rel_frontier S  {a}) = sphere z 1 \<inter> U  {h a}" 
901 
using him a kh by auto metis 

902 
show "k ` (sphere z 1 \<inter> U  {h a}) = rel_frontier S  {a}" 

903 
by (force simp: h [symmetric] image_comp o_def kh) 

904 
qed (auto intro: continuous_on_subset hcon kcon simp: kh hk) 

905 
also have "... homeomorphic T" 

906 
apply (rule homeomorphic_punctured_affine_sphere_affine) 

907 
using a him 

66690
6953b1a29e19
Tiny presentational improvements to homeomorphic_punctured_sphere_affine_gen
paulson <lp15@cam.ac.uk>
parents:
66287
diff
changeset

908 
by (auto simp: affS affdS \<open>affine T\<close> \<open>affine U\<close> \<open>z \<in> U\<close>) 
63130  909 
finally show ?thesis . 
910 
qed 

911 

912 

913 
text\<open> When dealing with AR, ANR and ANR later, it's useful to know that every set 

914 
is homeomorphic to a closed subset of a convex set, and 

915 
if the set is locally compact we can take the convex set to be the universe.\<close> 

916 

917 
proposition homeomorphic_closedin_convex: 

918 
fixes S :: "'m::euclidean_space set" 

919 
assumes "aff_dim S < DIM('n)" 

920 
obtains U and T :: "'n::euclidean_space set" 

921 
where "convex U" "U \<noteq> {}" "closedin (subtopology euclidean U) T" 

922 
"S homeomorphic T" 

923 
proof (cases "S = {}") 

924 
case True then show ?thesis 

925 
by (rule_tac U=UNIV and T="{}" in that) auto 

926 
next 

927 
case False 

928 
then obtain a where "a \<in> S" by auto 

929 
obtain i::'n where i: "i \<in> Basis" "i \<noteq> 0" 

930 
using SOME_Basis Basis_zero by force 

931 
have "0 \<in> affine hull (op + ( a) ` S)" 

932 
by (simp add: \<open>a \<in> S\<close> hull_inc) 

933 
then have "dim (op + ( a) ` S) = aff_dim (op + ( a) ` S)" 

934 
by (simp add: aff_dim_zero) 

935 
also have "... < DIM('n)" 

936 
by (simp add: aff_dim_translation_eq assms) 

937 
finally have dd: "dim (op + ( a) ` S) < DIM('n)" 

938 
by linarith 

939 
obtain T where "subspace T" and Tsub: "T \<subseteq> {x. i \<bullet> x = 0}" 

940 
and dimT: "dim T = dim (op + ( a) ` S)" 

941 
apply (rule choose_subspace_of_subspace [of "dim (op + ( a) ` S)" "{x::'n. i \<bullet> x = 0}"]) 

942 
apply (simp add: dim_hyperplane [OF \<open>i \<noteq> 0\<close>]) 

943 
apply (metis DIM_positive Suc_pred dd not_le not_less_eq_eq) 

944 
apply (metis span_eq subspace_hyperplane) 

945 
done 

946 
have "subspace (span (op + ( a) ` S))" 

947 
using subspace_span by blast 

948 
then obtain h k where "linear h" "linear k" 

949 
and heq: "h ` span (op + ( a) ` S) = T" 

950 
and keq:"k ` T = span (op + ( a) ` S)" 

951 
and hinv [simp]: "\<And>x. x \<in> span (op + ( a) ` S) \<Longrightarrow> k(h x) = x" 

952 
and kinv [simp]: "\<And>x. x \<in> T \<Longrightarrow> h(k x) = x" 

953 
apply (rule isometries_subspaces [OF _ \<open>subspace T\<close>]) 

954 
apply (auto simp: dimT) 

955 
done 

956 
have hcont: "continuous_on A h" and kcont: "continuous_on B k" for A B 

957 
using \<open>linear h\<close> \<open>linear k\<close> linear_continuous_on linear_conv_bounded_linear by blast+ 

958 
have ihhhh[simp]: "\<And>x. x \<in> S \<Longrightarrow> i \<bullet> h (x  a) = 0" 

959 
using Tsub [THEN subsetD] heq span_inc by fastforce 

960 
have "sphere 0 1  {i} homeomorphic {x. i \<bullet> x = 0}" 

961 
apply (rule homeomorphic_punctured_sphere_affine) 

962 
using i 

963 
apply (auto simp: affine_hyperplane) 

964 
by (metis DIM_positive Suc_eq_plus1 add.left_neutral diff_add_cancel not_le not_less_eq_eq of_nat_1 of_nat_diff) 

965 
then obtain f g where fg: "homeomorphism (sphere 0 1  {i}) {x. i \<bullet> x = 0} f g" 

966 
by (force simp: homeomorphic_def) 

967 
have "h ` op + ( a) ` S \<subseteq> T" 

968 
using heq span_clauses(1) span_linear_image by blast 

969 
then have "g ` h ` op + ( a) ` S \<subseteq> g ` {x. i \<bullet> x = 0}" 

970 
using Tsub by (simp add: image_mono) 

971 
also have "... \<subseteq> sphere 0 1  {i}" 

972 
by (simp add: fg [unfolded homeomorphism_def]) 

973 
finally have gh_sub_sph: "(g \<circ> h) ` op + ( a) ` S \<subseteq> sphere 0 1  {i}" 

974 
by (metis image_comp) 

975 
then have gh_sub_cb: "(g \<circ> h) ` op + ( a) ` S \<subseteq> cball 0 1" 

976 
by (metis Diff_subset order_trans sphere_cball) 

977 
have [simp]: "\<And>u. u \<in> S \<Longrightarrow> norm (g (h (u  a))) = 1" 

978 
using gh_sub_sph [THEN subsetD] by (auto simp: o_def) 

979 
have ghcont: "continuous_on (op + ( a) ` S) (\<lambda>x. g (h x))" 

980 
apply (rule continuous_on_compose2 [OF homeomorphism_cont2 [OF fg] hcont], force) 

981 
done 

982 
have kfcont: "continuous_on ((g \<circ> h \<circ> op + ( a)) ` S) (\<lambda>x. k (f x))" 

983 
apply (rule continuous_on_compose2 [OF kcont]) 

984 
using homeomorphism_cont1 [OF fg] gh_sub_sph apply (force intro: continuous_on_subset, blast) 

985 
done 

986 
have "S homeomorphic op + ( a) ` S" 

987 
by (simp add: homeomorphic_translation) 

988 
also have Shom: "\<dots> homeomorphic (g \<circ> h) ` op + ( a) ` S" 

989 
apply (simp add: homeomorphic_def homeomorphism_def) 

990 
apply (rule_tac x="g \<circ> h" in exI) 

991 
apply (rule_tac x="k \<circ> f" in exI) 

992 
apply (auto simp: ghcont kfcont span_clauses(1) homeomorphism_apply2 [OF fg] image_comp) 

993 
apply (force simp: o_def homeomorphism_apply2 [OF fg] span_clauses(1)) 

994 
done 

995 
finally have Shom: "S homeomorphic (g \<circ> h) ` op + ( a) ` S" . 

996 
show ?thesis 

997 
apply (rule_tac U = "ball 0 1 \<union> image (g o h) (op + ( a) ` S)" 

998 
and T = "image (g o h) (op + ( a) ` S)" 

999 
in that) 

1000 
apply (rule convex_intermediate_ball [of 0 1], force) 

1001 
using gh_sub_cb apply force 

1002 
apply force 

1003 
apply (simp add: closedin_closed) 

1004 
apply (rule_tac x="sphere 0 1" in exI) 

1005 
apply (auto simp: Shom) 

1006 
done 

1007 
qed 

1008 

1009 
subsection\<open>Locally compact sets in an open set\<close> 

1010 

1011 
text\<open> Locally compact sets are closed in an open set and are homeomorphic 

1012 
to an absolutely closed set if we have one more dimension to play with.\<close> 

1013 

1014 
lemma locally_compact_open_Int_closure: 

1015 
fixes S :: "'a :: metric_space set" 

1016 
assumes "locally compact S" 

1017 
obtains T where "open T" "S = T \<inter> closure S" 

1018 
proof  

1019 
have "\<forall>x\<in>S. \<exists>T v u. u = S \<inter> T \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> S \<and> open T \<and> compact v" 

1020 
by (metis assms locally_compact openin_open) 

1021 
then obtain t v where 

1022 
tv: "\<And>x. x \<in> S 

1023 
\<Longrightarrow> v x \<subseteq> S \<and> open (t x) \<and> compact (v x) \<and> (\<exists>u. x \<in> u \<and> u \<subseteq> v x \<and> u = S \<inter> t x)" 

1024 
by metis 

1025 
then have o: "open (UNION S t)" 

1026 
by blast 

1027 
have "S = \<Union> (v ` S)" 

1028 
using tv by blast 

1029 
also have "... = UNION S t \<inter> closure S" 

1030 
proof 

1031 
show "UNION S v \<subseteq> UNION S t \<inter> closure S" 

1032 
apply safe 

1033 
apply (metis Int_iff subsetD UN_iff tv) 

1034 
apply (simp add: closure_def rev_subsetD tv) 

1035 
done 

1036 
have "t x \<inter> closure S \<subseteq> v x" if "x \<in> S" for x 

1037 
proof  

1038 
have "t x \<inter> closure S \<subseteq> closure (t x \<inter> S)" 

1039 
by (simp add: open_Int_closure_subset that tv) 

1040 
also have "... \<subseteq> v x" 

1041 
by (metis Int_commute closure_minimal compact_imp_closed that tv) 

1042 
finally show ?thesis . 

1043 
qed 

1044 
then show "UNION S t \<inter> closure S \<subseteq> UNION S v" 

1045 
by blast 

1046 
qed 

1047 
finally have e: "S = UNION S t \<inter> closure S" . 

1048 
show ?thesis 

1049 
by (rule that [OF o e]) 

1050 
qed 

1051 

1052 

1053 
lemma locally_compact_closedin_open: 

1054 
fixes S :: "'a :: metric_space set" 

1055 
assumes "locally compact S" 

1056 
obtains T where "open T" "closedin (subtopology euclidean T) S" 

1057 
by (metis locally_compact_open_Int_closure [OF assms] closed_closure closedin_closed_Int) 

1058 

1059 

1060 
lemma locally_compact_homeomorphism_projection_closed: 

1061 
assumes "locally compact S" 

1062 
obtains T and f :: "'a \<Rightarrow> 'a :: euclidean_space \<times> 'b :: euclidean_space" 

1063 
where "closed T" "homeomorphism S T f fst" 

1064 
proof (cases "closed S") 

1065 
case True 

1066 
then show ?thesis 

1067 
apply (rule_tac T = "S \<times> {0}" and f = "\<lambda>x. (x, 0)" in that) 

1068 
apply (auto simp: closed_Times homeomorphism_def continuous_intros) 

1069 
done 

1070 
next 

1071 
case False 

1072 
obtain U where "open U" and US: "U \<inter> closure S = S" 

1073 
by (metis locally_compact_open_Int_closure [OF assms]) 

1074 
with False have Ucomp: "U \<noteq> {}" 

1075 
using closure_eq by auto 

1076 
have [simp]: "closure ( U) = U" 

1077 
by (simp add: \<open>open U\<close> closed_Compl) 

1078 
define f :: "'a \<Rightarrow> 'a \<times> 'b" where "f \<equiv> \<lambda>x. (x, One /\<^sub>R setdist {x} ( U))" 

1079 
have "continuous_on U (\<lambda>x. (x, One /\<^sub>R setdist {x} ( U)))" 

63301  1080 
apply (intro continuous_intros continuous_on_setdist) 
1081 
by (simp add: Ucomp setdist_eq_0_sing_1) 

63130  1082 
then have homU: "homeomorphism U (f`U) f fst" 
1083 
by (auto simp: f_def homeomorphism_def image_iff continuous_intros) 

1084 
have cloS: "closedin (subtopology euclidean U) S" 

1085 
by (metis US closed_closure closedin_closed_Int) 

1086 
have cont: "isCont ((\<lambda>x. setdist {x} ( U)) o fst) z" for z :: "'a \<times> 'b" 

1087 
by (rule isCont_o continuous_intros continuous_at_setdist)+ 

1088 
have setdist1D: "setdist {a} ( U) *\<^sub>R b = One \<Longrightarrow> setdist {a} ( U) \<noteq> 0" for a::'a and b::'b 

1089 
by force 

1090 
have *: "r *\<^sub>R b = One \<Longrightarrow> b = (1 / r) *\<^sub>R One" for r and b::'b 

1091 
by (metis One_non_0 nonzero_divide_eq_eq real_vector.scale_eq_0_iff real_vector.scale_scale scaleR_one) 

1092 
have "f ` U = {z. (setdist {fst z} ( U) *\<^sub>R snd z) \<in> {One}}" 

63301  1093 
apply (auto simp: f_def setdist_eq_0_sing_1 field_simps Ucomp) 
63130  1094 
apply (rule_tac x=a in image_eqI) 
63301  1095 
apply (auto simp: * setdist_eq_0_sing_1 dest: setdist1D) 
63130  1096 
done 
1097 
then have clfU: "closed (f ` U)" 

1098 
apply (rule ssubst) 

1099 
apply (rule continuous_closed_preimage_univ) 

1100 
apply (auto intro: continuous_intros cont [unfolded o_def]) 

1101 
done 

1102 
have "closed (f ` S)" 

1103 
apply (rule closedin_closed_trans [OF _ clfU]) 

1104 
apply (rule homeomorphism_imp_closed_map [OF homU cloS]) 

1105 
done 

1106 
then show ?thesis 

1107 
apply (rule that) 

1108 
apply (rule homeomorphism_of_subsets [OF homU]) 

1109 
using US apply auto 

1110 
done 

1111 
qed 

1112 

1113 
lemma locally_compact_closed_Int_open: 

1114 
fixes S :: "'a :: euclidean_space set" 

1115 
shows 

1116 
"locally compact S \<longleftrightarrow> (\<exists>U u. closed U \<and> open u \<and> S = U \<inter> u)" 

1117 
by (metis closed_closure closed_imp_locally_compact inf_commute locally_compact_Int locally_compact_open_Int_closure open_imp_locally_compact) 

1118 

1119 

63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1120 
lemma lowerdim_embeddings: 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1121 
assumes "DIM('a) < DIM('b)" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1122 
obtains f :: "'a::euclidean_space*real \<Rightarrow> 'b::euclidean_space" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1123 
and g :: "'b \<Rightarrow> 'a*real" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1124 
and j :: 'b 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1125 
where "linear f" "linear g" "\<And>z. g (f z) = z" "j \<in> Basis" "\<And>x. f(x,0) \<bullet> j = 0" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1126 
proof  
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1127 
let ?B = "Basis :: ('a*real) set" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1128 
have b01: "(0,1) \<in> ?B" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1129 
by (simp add: Basis_prod_def) 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1130 
have "DIM('a * real) \<le> DIM('b)" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1131 
by (simp add: Suc_leI assms) 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1132 
then obtain basf :: "'a*real \<Rightarrow> 'b" where sbf: "basf ` ?B \<subseteq> Basis" and injbf: "inj_on basf Basis" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1133 
by (metis finite_Basis card_le_inj) 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1134 
define basg:: "'b \<Rightarrow> 'a * real" where 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1135 
"basg \<equiv> \<lambda>i. if i \<in> basf ` Basis then inv_into Basis basf i else (0,1)" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1136 
have bgf[simp]: "basg (basf i) = i" if "i \<in> Basis" for i 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1137 
using inv_into_f_f injbf that by (force simp: basg_def) 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1138 
have sbg: "basg ` Basis \<subseteq> ?B" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1139 
by (force simp: basg_def injbf b01) 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1140 
define f :: "'a*real \<Rightarrow> 'b" where "f \<equiv> \<lambda>u. \<Sum>j\<in>Basis. (u \<bullet> basg j) *\<^sub>R j" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1141 
define g :: "'b \<Rightarrow> 'a*real" where "g \<equiv> \<lambda>z. (\<Sum>i\<in>Basis. (z \<bullet> basf i) *\<^sub>R i)" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1142 
show ?thesis 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1143 
proof 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1144 
show "linear f" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1145 
unfolding f_def 
64267  1146 
by (intro linear_compose_sum linearI ballI) (auto simp: algebra_simps) 
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1147 
show "linear g" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1148 
unfolding g_def 
64267  1149 
by (intro linear_compose_sum linearI ballI) (auto simp: algebra_simps) 
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1150 
have *: "(\<Sum>a \<in> Basis. a \<bullet> basf b * (x \<bullet> basg a)) = x \<bullet> b" if "b \<in> Basis" for x b 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1151 
using sbf that by auto 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1152 
show gf: "g (f x) = x" for x 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1153 
apply (rule euclidean_eqI) 
64267  1154 
apply (simp add: f_def g_def inner_sum_left scaleR_sum_left algebra_simps) 
1155 
apply (simp add: Groups_Big.sum_distrib_left [symmetric] *) 

63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1156 
done 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1157 
show "basf(0,1) \<in> Basis" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1158 
using b01 sbf by auto 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1159 
then show "f(x,0) \<bullet> basf(0,1) = 0" for x 
64267  1160 
apply (simp add: f_def inner_sum_left) 
1161 
apply (rule comm_monoid_add_class.sum.neutral) 

63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1162 
using b01 inner_not_same_Basis by fastforce 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1163 
qed 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1164 
qed 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1165 

63130  1166 
proposition locally_compact_homeomorphic_closed: 
1167 
fixes S :: "'a::euclidean_space set" 

1168 
assumes "locally compact S" and dimlt: "DIM('a) < DIM('b)" 

1169 
obtains T :: "'b::euclidean_space set" where "closed T" "S homeomorphic T" 

1170 
proof  

1171 
obtain U:: "('a*real)set" and h 

1172 
where "closed U" and homU: "homeomorphism S U h fst" 

1173 
using locally_compact_homeomorphism_projection_closed assms by metis 

63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1174 
obtain f :: "'a*real \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'a*real" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1175 
where "linear f" "linear g" and gf [simp]: "\<And>z. g (f z) = z" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1176 
using lowerdim_embeddings [OF dimlt] by metis 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1177 
then have "inj f" 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1178 
by (metis injI) 
63130  1179 
have gfU: "g ` f ` U = U" 
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1180 
by (simp add: image_comp o_def) 
63130  1181 
have "S homeomorphic U" 
1182 
using homU homeomorphic_def by blast 

1183 
also have "... homeomorphic f ` U" 

1184 
apply (rule homeomorphicI [OF refl gfU]) 

1185 
apply (meson \<open>inj f\<close> \<open>linear f\<close> homeomorphism_cont2 linear_homeomorphism_image) 

63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1186 
using \<open>linear g\<close> linear_continuous_on linear_conv_bounded_linear apply blast 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1187 
apply (auto simp: o_def) 
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset

1188 
done 
63130  1189 
finally show ?thesis 
1190 
apply (rule_tac T = "f ` U" in that) 

1191 
apply (rule closed_injective_linear_image [OF \<open>closed U\<close> \<open>linear f\<close> \<open>inj f\<close>], assumption) 

1192 
done 

1193 
qed 

1194 

1195 

1196 
lemma homeomorphic_convex_compact_lemma: 

64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset

1197 
fixes S :: "'a::euclidean_space set" 
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset

1198 
assumes "convex S" 
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset

1199 
and "compact S" 
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset

1200 
and "cball 0 1 \<subseteq> S" 
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset

1201 
shows "S homeomorphic (cball (0::'a) 1)" 
63130  1202 
proof (rule starlike_compact_projective_special[OF assms(23)]) 
1203 
fix x u 

64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset

1204 
assume "x \<in> S" and "0 \<le> u" and "u < (1::real)" 
63130  1205 
have "open (ball (u *\<^sub>R x) (1  u))" 
1206 
by (rule open_ball) 

1207 
moreover have "u *\<^sub>R x \<in> ball (u *\<^sub>R x) (1  u)" 

1208 
unfolding centre_in_ball using \<open>u < 1\<close> by simp 

64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset

1209 
moreover have "ball (u *\<^sub>R x) (1  u) \<subseteq> S" 
63130  1210 
proof 