13 Convex |
13 Convex |
14 Topology_Euclidean_Space |
14 Topology_Euclidean_Space |
15 begin |
15 begin |
16 |
16 |
17 subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological Properties of Convex Sets and Functions\<close> |
17 subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological Properties of Convex Sets and Functions\<close> |
18 |
|
19 lemma convex_supp_sum: |
|
20 assumes "convex S" and 1: "supp_sum u I = 1" |
|
21 and "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> u i \<and> (u i = 0 \<or> f i \<in> S)" |
|
22 shows "supp_sum (\<lambda>i. u i *\<^sub>R f i) I \<in> S" |
|
23 proof - |
|
24 have fin: "finite {i \<in> I. u i \<noteq> 0}" |
|
25 using 1 sum.infinite by (force simp: supp_sum_def support_on_def) |
|
26 then have eq: "supp_sum (\<lambda>i. u i *\<^sub>R f i) I = sum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}" |
|
27 by (force intro: sum.mono_neutral_left simp: supp_sum_def support_on_def) |
|
28 show ?thesis |
|
29 apply (simp add: eq) |
|
30 apply (rule convex_sum [OF fin \<open>convex S\<close>]) |
|
31 using 1 assms apply (auto simp: supp_sum_def support_on_def) |
|
32 done |
|
33 qed |
|
34 |
|
35 lemma closure_bounded_linear_image_subset: |
|
36 assumes f: "bounded_linear f" |
|
37 shows "f ` closure S \<subseteq> closure (f ` S)" |
|
38 using linear_continuous_on [OF f] closed_closure closure_subset |
|
39 by (rule image_closure_subset) |
|
40 |
|
41 lemma closure_linear_image_subset: |
|
42 fixes f :: "'m::euclidean_space \<Rightarrow> 'n::real_normed_vector" |
|
43 assumes "linear f" |
|
44 shows "f ` (closure S) \<subseteq> closure (f ` S)" |
|
45 using assms unfolding linear_conv_bounded_linear |
|
46 by (rule closure_bounded_linear_image_subset) |
|
47 |
|
48 lemma closed_injective_linear_image: |
|
49 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
50 assumes S: "closed S" and f: "linear f" "inj f" |
|
51 shows "closed (f ` S)" |
|
52 proof - |
|
53 obtain g where g: "linear g" "g \<circ> f = id" |
|
54 using linear_injective_left_inverse [OF f] by blast |
|
55 then have confg: "continuous_on (range f) g" |
|
56 using linear_continuous_on linear_conv_bounded_linear by blast |
|
57 have [simp]: "g ` f ` S = S" |
|
58 using g by (simp add: image_comp) |
|
59 have cgf: "closed (g ` f ` S)" |
|
60 by (simp add: \<open>g \<circ> f = id\<close> S image_comp) |
|
61 have [simp]: "(range f \<inter> g -` S) = f ` S" |
|
62 using g unfolding o_def id_def image_def by auto metis+ |
|
63 show ?thesis |
|
64 proof (rule closedin_closed_trans [of "range f"]) |
|
65 show "closedin (top_of_set (range f)) (f ` S)" |
|
66 using continuous_closedin_preimage [OF confg cgf] by simp |
|
67 show "closed (range f)" |
|
68 apply (rule closed_injective_image_subspace) |
|
69 using f apply (auto simp: linear_linear linear_injective_0) |
|
70 done |
|
71 qed |
|
72 qed |
|
73 |
|
74 lemma closed_injective_linear_image_eq: |
|
75 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
76 assumes f: "linear f" "inj f" |
|
77 shows "(closed(image f s) \<longleftrightarrow> closed s)" |
|
78 by (metis closed_injective_linear_image closure_eq closure_linear_image_subset closure_subset_eq f(1) f(2) inj_image_subset_iff) |
|
79 |
|
80 lemma closure_injective_linear_image: |
|
81 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
82 shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)" |
|
83 apply (rule subset_antisym) |
|
84 apply (simp add: closure_linear_image_subset) |
|
85 by (simp add: closure_minimal closed_injective_linear_image closure_subset image_mono) |
|
86 |
|
87 lemma closure_bounded_linear_image: |
|
88 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
89 shows "\<lbrakk>linear f; bounded S\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)" |
|
90 apply (rule subset_antisym, simp add: closure_linear_image_subset) |
|
91 apply (rule closure_minimal, simp add: closure_subset image_mono) |
|
92 by (meson bounded_closure closed_closure compact_continuous_image compact_eq_bounded_closed linear_continuous_on linear_conv_bounded_linear) |
|
93 |
|
94 lemma closure_scaleR: |
|
95 fixes S :: "'a::real_normed_vector set" |
|
96 shows "((*\<^sub>R) c) ` (closure S) = closure (((*\<^sub>R) c) ` S)" |
|
97 proof |
|
98 show "((*\<^sub>R) c) ` (closure S) \<subseteq> closure (((*\<^sub>R) c) ` S)" |
|
99 using bounded_linear_scaleR_right |
|
100 by (rule closure_bounded_linear_image_subset) |
|
101 show "closure (((*\<^sub>R) c) ` S) \<subseteq> ((*\<^sub>R) c) ` (closure S)" |
|
102 by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure) |
|
103 qed |
|
104 |
|
105 lemma sphere_eq_empty [simp]: |
|
106 fixes a :: "'a::{real_normed_vector, perfect_space}" |
|
107 shows "sphere a r = {} \<longleftrightarrow> r < 0" |
|
108 by (auto simp: sphere_def dist_norm) (metis dist_norm le_less_linear vector_choose_dist) |
|
109 |
|
110 lemma cone_closure: |
|
111 fixes S :: "'a::real_normed_vector set" |
|
112 assumes "cone S" |
|
113 shows "cone (closure S)" |
|
114 proof (cases "S = {}") |
|
115 case True |
|
116 then show ?thesis by auto |
|
117 next |
|
118 case False |
|
119 then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)" |
|
120 using cone_iff[of S] assms by auto |
|
121 then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` closure S = closure S)" |
|
122 using closure_subset by (auto simp: closure_scaleR) |
|
123 then show ?thesis |
|
124 using False cone_iff[of "closure S"] by auto |
|
125 qed |
|
126 |
|
127 corollary component_complement_connected: |
|
128 fixes S :: "'a::real_normed_vector set" |
|
129 assumes "connected S" "C \<in> components (-S)" |
|
130 shows "connected(-C)" |
|
131 using component_diff_connected [of S UNIV] assms |
|
132 by (auto simp: Compl_eq_Diff_UNIV) |
|
133 |
|
134 proposition clopen: |
|
135 fixes S :: "'a :: real_normed_vector set" |
|
136 shows "closed S \<and> open S \<longleftrightarrow> S = {} \<or> S = UNIV" |
|
137 by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format]) |
|
138 |
|
139 corollary compact_open: |
|
140 fixes S :: "'a :: euclidean_space set" |
|
141 shows "compact S \<and> open S \<longleftrightarrow> S = {}" |
|
142 by (auto simp: compact_eq_bounded_closed clopen) |
|
143 |
|
144 corollary finite_imp_not_open: |
|
145 fixes S :: "'a::{real_normed_vector, perfect_space} set" |
|
146 shows "\<lbrakk>finite S; open S\<rbrakk> \<Longrightarrow> S={}" |
|
147 using clopen [of S] finite_imp_closed not_bounded_UNIV by blast |
|
148 |
|
149 corollary empty_interior_finite: |
|
150 fixes S :: "'a::{real_normed_vector, perfect_space} set" |
|
151 shows "finite S \<Longrightarrow> interior S = {}" |
|
152 by (metis interior_subset finite_subset open_interior [of S] finite_imp_not_open) |
|
153 |
|
154 text \<open>Balls, being convex, are connected.\<close> |
|
155 |
|
156 lemma convex_local_global_minimum: |
|
157 fixes s :: "'a::real_normed_vector set" |
|
158 assumes "e > 0" |
|
159 and "convex_on s f" |
|
160 and "ball x e \<subseteq> s" |
|
161 and "\<forall>y\<in>ball x e. f x \<le> f y" |
|
162 shows "\<forall>y\<in>s. f x \<le> f y" |
|
163 proof (rule ccontr) |
|
164 have "x \<in> s" using assms(1,3) by auto |
|
165 assume "\<not> ?thesis" |
|
166 then obtain y where "y\<in>s" and y: "f x > f y" by auto |
|
167 then have xy: "0 < dist x y" by auto |
|
168 then obtain u where "0 < u" "u \<le> 1" and u: "u < e / dist x y" |
|
169 using field_lbound_gt_zero[of 1 "e / dist x y"] xy \<open>e>0\<close> by auto |
|
170 then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y" |
|
171 using \<open>x\<in>s\<close> \<open>y\<in>s\<close> |
|
172 using assms(2)[unfolded convex_on_def, |
|
173 THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]] |
|
174 by auto |
|
175 moreover |
|
176 have *: "x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)" |
|
177 by (simp add: algebra_simps) |
|
178 have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> ball x e" |
|
179 unfolding mem_ball dist_norm |
|
180 unfolding * and norm_scaleR and abs_of_pos[OF \<open>0<u\<close>] |
|
181 unfolding dist_norm[symmetric] |
|
182 using u |
|
183 unfolding pos_less_divide_eq[OF xy] |
|
184 by auto |
|
185 then have "f x \<le> f ((1 - u) *\<^sub>R x + u *\<^sub>R y)" |
|
186 using assms(4) by auto |
|
187 ultimately show False |
|
188 using mult_strict_left_mono[OF y \<open>u>0\<close>] |
|
189 unfolding left_diff_distrib |
|
190 by auto |
|
191 qed |
|
192 |
|
193 lemma convex_ball [iff]: |
|
194 fixes x :: "'a::real_normed_vector" |
|
195 shows "convex (ball x e)" |
|
196 proof (auto simp: convex_def) |
|
197 fix y z |
|
198 assume yz: "dist x y < e" "dist x z < e" |
|
199 fix u v :: real |
|
200 assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1" |
|
201 have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" |
|
202 using uv yz |
|
203 using convex_on_dist [of "ball x e" x, unfolded convex_on_def, |
|
204 THEN bspec[where x=y], THEN bspec[where x=z]] |
|
205 by auto |
|
206 then show "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" |
|
207 using convex_bound_lt[OF yz uv] by auto |
|
208 qed |
|
209 |
|
210 lemma convex_cball [iff]: |
|
211 fixes x :: "'a::real_normed_vector" |
|
212 shows "convex (cball x e)" |
|
213 proof - |
|
214 { |
|
215 fix y z |
|
216 assume yz: "dist x y \<le> e" "dist x z \<le> e" |
|
217 fix u v :: real |
|
218 assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1" |
|
219 have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" |
|
220 using uv yz |
|
221 using convex_on_dist [of "cball x e" x, unfolded convex_on_def, |
|
222 THEN bspec[where x=y], THEN bspec[where x=z]] |
|
223 by auto |
|
224 then have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e" |
|
225 using convex_bound_le[OF yz uv] by auto |
|
226 } |
|
227 then show ?thesis by (auto simp: convex_def Ball_def) |
|
228 qed |
|
229 |
|
230 lemma connected_ball [iff]: |
|
231 fixes x :: "'a::real_normed_vector" |
|
232 shows "connected (ball x e)" |
|
233 using convex_connected convex_ball by auto |
|
234 |
|
235 lemma connected_cball [iff]: |
|
236 fixes x :: "'a::real_normed_vector" |
|
237 shows "connected (cball x e)" |
|
238 using convex_connected convex_cball by auto |
|
239 |
|
240 |
|
241 lemma bounded_convex_hull: |
|
242 fixes s :: "'a::real_normed_vector set" |
|
243 assumes "bounded s" |
|
244 shows "bounded (convex hull s)" |
|
245 proof - |
|
246 from assms obtain B where B: "\<forall>x\<in>s. norm x \<le> B" |
|
247 unfolding bounded_iff by auto |
|
248 show ?thesis |
|
249 apply (rule bounded_subset[OF bounded_cball, of _ 0 B]) |
|
250 unfolding subset_hull[of convex, OF convex_cball] |
|
251 unfolding subset_eq mem_cball dist_norm using B |
|
252 apply auto |
|
253 done |
|
254 qed |
|
255 |
|
256 lemma finite_imp_bounded_convex_hull: |
|
257 fixes s :: "'a::real_normed_vector set" |
|
258 shows "finite s \<Longrightarrow> bounded (convex hull s)" |
|
259 using bounded_convex_hull finite_imp_bounded |
|
260 by auto |
|
261 |
18 |
262 lemma aff_dim_cball: |
19 lemma aff_dim_cball: |
263 fixes a :: "'n::euclidean_space" |
20 fixes a :: "'n::euclidean_space" |
264 assumes "e > 0" |
21 assumes "e > 0" |
265 shows "aff_dim (cball a e) = int (DIM('n))" |
22 shows "aff_dim (cball a e) = int (DIM('n))" |
2519 then show "continuous (at x) f" |
2270 then show "continuous (at x) f" |
2520 unfolding continuous_on_eq_continuous_at[OF open_ball] |
2271 unfolding continuous_on_eq_continuous_at[OF open_ball] |
2521 using \<open>d > 0\<close> by auto |
2272 using \<open>d > 0\<close> by auto |
2522 qed |
2273 qed |
2523 |
2274 |
2524 |
|
2525 section \<open>Line Segments\<close> |
|
2526 |
|
2527 subsection \<open>Midpoint\<close> |
|
2528 |
|
2529 definition\<^marker>\<open>tag important\<close> midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a" |
|
2530 where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)" |
|
2531 |
|
2532 lemma midpoint_idem [simp]: "midpoint x x = x" |
|
2533 unfolding midpoint_def by simp |
|
2534 |
|
2535 lemma midpoint_sym: "midpoint a b = midpoint b a" |
|
2536 unfolding midpoint_def by (auto simp add: scaleR_right_distrib) |
|
2537 |
|
2538 lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c" |
|
2539 proof - |
|
2540 have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c" |
|
2541 by simp |
|
2542 then show ?thesis |
|
2543 unfolding midpoint_def scaleR_2 [symmetric] by simp |
|
2544 qed |
|
2545 |
|
2546 lemma |
|
2547 fixes a::real |
|
2548 assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b" |
|
2549 and le_midpoint_1: "midpoint a b \<le> b" |
|
2550 by (simp_all add: midpoint_def assms) |
|
2551 |
|
2552 lemma dist_midpoint: |
|
2553 fixes a b :: "'a::real_normed_vector" shows |
|
2554 "dist a (midpoint a b) = (dist a b) / 2" (is ?t1) |
|
2555 "dist b (midpoint a b) = (dist a b) / 2" (is ?t2) |
|
2556 "dist (midpoint a b) a = (dist a b) / 2" (is ?t3) |
|
2557 "dist (midpoint a b) b = (dist a b) / 2" (is ?t4) |
|
2558 proof - |
|
2559 have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2" |
|
2560 unfolding equation_minus_iff by auto |
|
2561 have **: "\<And>x y::'a. 2 *\<^sub>R x = y \<Longrightarrow> norm x = (norm y) / 2" |
|
2562 by auto |
|
2563 note scaleR_right_distrib [simp] |
|
2564 show ?t1 |
|
2565 unfolding midpoint_def dist_norm |
|
2566 apply (rule **) |
|
2567 apply (simp add: scaleR_right_diff_distrib) |
|
2568 apply (simp add: scaleR_2) |
|
2569 done |
|
2570 show ?t2 |
|
2571 unfolding midpoint_def dist_norm |
|
2572 apply (rule *) |
|
2573 apply (simp add: scaleR_right_diff_distrib) |
|
2574 apply (simp add: scaleR_2) |
|
2575 done |
|
2576 show ?t3 |
|
2577 unfolding midpoint_def dist_norm |
|
2578 apply (rule *) |
|
2579 apply (simp add: scaleR_right_diff_distrib) |
|
2580 apply (simp add: scaleR_2) |
|
2581 done |
|
2582 show ?t4 |
|
2583 unfolding midpoint_def dist_norm |
|
2584 apply (rule **) |
|
2585 apply (simp add: scaleR_right_diff_distrib) |
|
2586 apply (simp add: scaleR_2) |
|
2587 done |
|
2588 qed |
|
2589 |
|
2590 lemma midpoint_eq_endpoint [simp]: |
|
2591 "midpoint a b = a \<longleftrightarrow> a = b" |
|
2592 "midpoint a b = b \<longleftrightarrow> a = b" |
|
2593 unfolding midpoint_eq_iff by auto |
|
2594 |
|
2595 lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b" |
|
2596 using midpoint_eq_iff by metis |
|
2597 |
|
2598 lemma midpoint_linear_image: |
|
2599 "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)" |
|
2600 by (simp add: linear_iff midpoint_def) |
|
2601 |
|
2602 |
|
2603 subsection \<open>Line segments\<close> |
|
2604 |
|
2605 definition\<^marker>\<open>tag important\<close> closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" |
|
2606 where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}" |
|
2607 |
|
2608 definition\<^marker>\<open>tag important\<close> open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where |
|
2609 "open_segment a b \<equiv> closed_segment a b - {a,b}" |
|
2610 |
|
2611 lemmas segment = open_segment_def closed_segment_def |
|
2612 |
|
2613 lemma in_segment: |
|
2614 "x \<in> closed_segment a b \<longleftrightarrow> (\<exists>u. 0 \<le> u \<and> u \<le> 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)" |
|
2615 "x \<in> open_segment a b \<longleftrightarrow> a \<noteq> b \<and> (\<exists>u. 0 < u \<and> u < 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)" |
|
2616 using less_eq_real_def by (auto simp: segment algebra_simps) |
|
2617 |
|
2618 lemma closed_segment_linear_image: |
|
2619 "closed_segment (f a) (f b) = f ` (closed_segment a b)" if "linear f" |
|
2620 proof - |
|
2621 interpret linear f by fact |
|
2622 show ?thesis |
|
2623 by (force simp add: in_segment add scale) |
|
2624 qed |
|
2625 |
|
2626 lemma open_segment_linear_image: |
|
2627 "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> open_segment (f a) (f b) = f ` (open_segment a b)" |
|
2628 by (force simp: open_segment_def closed_segment_linear_image inj_on_def) |
|
2629 |
|
2630 lemma closed_segment_translation: |
|
2631 "closed_segment (c + a) (c + b) = image (\<lambda>x. c + x) (closed_segment a b)" |
|
2632 apply safe |
|
2633 apply (rule_tac x="x-c" in image_eqI) |
|
2634 apply (auto simp: in_segment algebra_simps) |
|
2635 done |
|
2636 |
|
2637 lemma open_segment_translation: |
|
2638 "open_segment (c + a) (c + b) = image (\<lambda>x. c + x) (open_segment a b)" |
|
2639 by (simp add: open_segment_def closed_segment_translation translation_diff) |
|
2640 |
|
2641 lemma closed_segment_of_real: |
|
2642 "closed_segment (of_real x) (of_real y) = of_real ` closed_segment x y" |
|
2643 apply (auto simp: image_iff in_segment scaleR_conv_of_real) |
|
2644 apply (rule_tac x="(1-u)*x + u*y" in bexI) |
|
2645 apply (auto simp: in_segment) |
|
2646 done |
|
2647 |
|
2648 lemma open_segment_of_real: |
|
2649 "open_segment (of_real x) (of_real y) = of_real ` open_segment x y" |
|
2650 apply (auto simp: image_iff in_segment scaleR_conv_of_real) |
|
2651 apply (rule_tac x="(1-u)*x + u*y" in bexI) |
|
2652 apply (auto simp: in_segment) |
|
2653 done |
|
2654 |
|
2655 lemma closed_segment_Reals: |
|
2656 "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> closed_segment x y = of_real ` closed_segment (Re x) (Re y)" |
|
2657 by (metis closed_segment_of_real of_real_Re) |
|
2658 |
|
2659 lemma open_segment_Reals: |
|
2660 "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> open_segment x y = of_real ` open_segment (Re x) (Re y)" |
|
2661 by (metis open_segment_of_real of_real_Re) |
|
2662 |
|
2663 lemma open_segment_PairD: |
|
2664 "(x, x') \<in> open_segment (a, a') (b, b') |
|
2665 \<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')" |
|
2666 by (auto simp: in_segment) |
|
2667 |
|
2668 lemma closed_segment_PairD: |
|
2669 "(x, x') \<in> closed_segment (a, a') (b, b') \<Longrightarrow> x \<in> closed_segment a b \<and> x' \<in> closed_segment a' b'" |
|
2670 by (auto simp: closed_segment_def) |
|
2671 |
|
2672 lemma closed_segment_translation_eq [simp]: |
|
2673 "d + x \<in> closed_segment (d + a) (d + b) \<longleftrightarrow> x \<in> closed_segment a b" |
|
2674 proof - |
|
2675 have *: "\<And>d x a b. x \<in> closed_segment a b \<Longrightarrow> d + x \<in> closed_segment (d + a) (d + b)" |
|
2676 apply (simp add: closed_segment_def) |
|
2677 apply (erule ex_forward) |
|
2678 apply (simp add: algebra_simps) |
|
2679 done |
|
2680 show ?thesis |
|
2681 using * [where d = "-d"] * |
|
2682 by (fastforce simp add:) |
|
2683 qed |
|
2684 |
|
2685 lemma open_segment_translation_eq [simp]: |
|
2686 "d + x \<in> open_segment (d + a) (d + b) \<longleftrightarrow> x \<in> open_segment a b" |
|
2687 by (simp add: open_segment_def) |
|
2688 |
|
2689 lemma of_real_closed_segment [simp]: |
|
2690 "of_real x \<in> closed_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> closed_segment a b" |
|
2691 apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward) |
|
2692 using of_real_eq_iff by fastforce |
|
2693 |
|
2694 lemma of_real_open_segment [simp]: |
|
2695 "of_real x \<in> open_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> open_segment a b" |
|
2696 apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE) |
|
2697 using of_real_eq_iff by fastforce |
|
2698 |
|
2699 lemma convex_contains_segment: |
|
2700 "convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)" |
|
2701 unfolding convex_alt closed_segment_def by auto |
|
2702 |
|
2703 lemma closed_segment_in_Reals: |
|
2704 "\<lbrakk>x \<in> closed_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals" |
|
2705 by (meson subsetD convex_Reals convex_contains_segment) |
|
2706 |
|
2707 lemma open_segment_in_Reals: |
|
2708 "\<lbrakk>x \<in> open_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals" |
|
2709 by (metis Diff_iff closed_segment_in_Reals open_segment_def) |
|
2710 |
|
2711 lemma closed_segment_subset: "\<lbrakk>x \<in> S; y \<in> S; convex S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> S" |
|
2712 by (simp add: convex_contains_segment) |
|
2713 |
|
2714 lemma closed_segment_subset_convex_hull: |
|
2715 "\<lbrakk>x \<in> convex hull S; y \<in> convex hull S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull S" |
|
2716 using convex_contains_segment by blast |
|
2717 |
|
2718 lemma segment_convex_hull: |
|
2719 "closed_segment a b = convex hull {a,b}" |
|
2720 proof - |
|
2721 have *: "\<And>x. {x} \<noteq> {}" by auto |
|
2722 show ?thesis |
|
2723 unfolding segment convex_hull_insert[OF *] convex_hull_singleton |
|
2724 by (safe; rule_tac x="1 - u" in exI; force) |
|
2725 qed |
|
2726 |
|
2727 lemma open_closed_segment: "u \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z" |
|
2728 by (auto simp add: closed_segment_def open_segment_def) |
|
2729 |
|
2730 lemma segment_open_subset_closed: |
|
2731 "open_segment a b \<subseteq> closed_segment a b" |
|
2732 by (auto simp: closed_segment_def open_segment_def) |
|
2733 |
|
2734 lemma bounded_closed_segment: |
|
2735 fixes a :: "'a::euclidean_space" shows "bounded (closed_segment a b)" |
|
2736 by (simp add: segment_convex_hull compact_convex_hull compact_imp_bounded) |
|
2737 |
|
2738 lemma bounded_open_segment: |
|
2739 fixes a :: "'a::euclidean_space" shows "bounded (open_segment a b)" |
|
2740 by (rule bounded_subset [OF bounded_closed_segment segment_open_subset_closed]) |
|
2741 |
|
2742 lemmas bounded_segment = bounded_closed_segment open_closed_segment |
|
2743 |
|
2744 lemma ends_in_segment [iff]: "a \<in> closed_segment a b" "b \<in> closed_segment a b" |
|
2745 unfolding segment_convex_hull |
|
2746 by (auto intro!: hull_subset[unfolded subset_eq, rule_format]) |
|
2747 |
|
2748 lemma eventually_closed_segment: |
|
2749 fixes x0::"'a::real_normed_vector" |
|
2750 assumes "open X0" "x0 \<in> X0" |
|
2751 shows "\<forall>\<^sub>F x in at x0 within U. closed_segment x0 x \<subseteq> X0" |
|
2752 proof - |
|
2753 from openE[OF assms] |
|
2754 obtain e where e: "0 < e" "ball x0 e \<subseteq> X0" . |
|
2755 then have "\<forall>\<^sub>F x in at x0 within U. x \<in> ball x0 e" |
|
2756 by (auto simp: dist_commute eventually_at) |
|
2757 then show ?thesis |
|
2758 proof eventually_elim |
|
2759 case (elim x) |
|
2760 have "x0 \<in> ball x0 e" using \<open>e > 0\<close> by simp |
|
2761 from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim] |
|
2762 have "closed_segment x0 x \<subseteq> ball x0 e" . |
|
2763 also note \<open>\<dots> \<subseteq> X0\<close> |
|
2764 finally show ?case . |
|
2765 qed |
|
2766 qed |
|
2767 |
|
2768 lemma segment_furthest_le: |
|
2769 fixes a b x y :: "'a::euclidean_space" |
|
2770 assumes "x \<in> closed_segment a b" |
|
2771 shows "norm (y - x) \<le> norm (y - a) \<or> norm (y - x) \<le> norm (y - b)" |
|
2772 proof - |
|
2773 obtain z where "z \<in> {a, b}" "norm (x - y) \<le> norm (z - y)" |
|
2774 using simplex_furthest_le[of "{a, b}" y] |
|
2775 using assms[unfolded segment_convex_hull] |
|
2776 by auto |
|
2777 then show ?thesis |
|
2778 by (auto simp add:norm_minus_commute) |
|
2779 qed |
|
2780 |
|
2781 lemma closed_segment_commute: "closed_segment a b = closed_segment b a" |
|
2782 proof - |
|
2783 have "{a, b} = {b, a}" by auto |
|
2784 thus ?thesis |
|
2785 by (simp add: segment_convex_hull) |
|
2786 qed |
|
2787 |
|
2788 lemma segment_bound1: |
|
2789 assumes "x \<in> closed_segment a b" |
|
2790 shows "norm (x - a) \<le> norm (b - a)" |
|
2791 proof - |
|
2792 obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1" |
|
2793 using assms by (auto simp add: closed_segment_def) |
|
2794 then show "norm (x - a) \<le> norm (b - a)" |
|
2795 apply clarify |
|
2796 apply (auto simp: algebra_simps) |
|
2797 apply (simp add: scaleR_diff_right [symmetric] mult_left_le_one_le) |
|
2798 done |
|
2799 qed |
|
2800 |
|
2801 lemma segment_bound: |
|
2802 assumes "x \<in> closed_segment a b" |
|
2803 shows "norm (x - a) \<le> norm (b - a)" "norm (x - b) \<le> norm (b - a)" |
|
2804 apply (simp add: assms segment_bound1) |
|
2805 by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1) |
|
2806 |
|
2807 lemma open_segment_commute: "open_segment a b = open_segment b a" |
|
2808 proof - |
|
2809 have "{a, b} = {b, a}" by auto |
|
2810 thus ?thesis |
|
2811 by (simp add: closed_segment_commute open_segment_def) |
|
2812 qed |
|
2813 |
|
2814 lemma closed_segment_idem [simp]: "closed_segment a a = {a}" |
|
2815 unfolding segment by (auto simp add: algebra_simps) |
|
2816 |
|
2817 lemma open_segment_idem [simp]: "open_segment a a = {}" |
|
2818 by (simp add: open_segment_def) |
|
2819 |
|
2820 lemma closed_segment_eq_open: "closed_segment a b = open_segment a b \<union> {a,b}" |
|
2821 using open_segment_def by auto |
|
2822 |
|
2823 lemma convex_contains_open_segment: |
|
2824 "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. open_segment a b \<subseteq> s)" |
|
2825 by (simp add: convex_contains_segment closed_segment_eq_open) |
|
2826 |
|
2827 lemma closed_segment_eq_real_ivl: |
|
2828 fixes a b::real |
|
2829 shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})" |
|
2830 proof - |
|
2831 have "b \<le> a \<Longrightarrow> closed_segment b a = {b .. a}" |
|
2832 and "a \<le> b \<Longrightarrow> closed_segment a b = {a .. b}" |
|
2833 by (auto simp: convex_hull_eq_real_cbox segment_convex_hull) |
|
2834 thus ?thesis |
|
2835 by (auto simp: closed_segment_commute) |
|
2836 qed |
|
2837 |
|
2838 lemma open_segment_eq_real_ivl: |
|
2839 fixes a b::real |
|
2840 shows "open_segment a b = (if a \<le> b then {a<..<b} else {b<..<a})" |
|
2841 by (auto simp: closed_segment_eq_real_ivl open_segment_def split: if_split_asm) |
|
2842 |
|
2843 lemma closed_segment_real_eq: |
|
2844 fixes u::real shows "closed_segment u v = (\<lambda>x. (v - u) * x + u) ` {0..1}" |
|
2845 by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl) |
|
2846 |
|
2847 lemma dist_in_closed_segment: |
|
2848 fixes a :: "'a :: euclidean_space" |
|
2849 assumes "x \<in> closed_segment a b" |
|
2850 shows "dist x a \<le> dist a b \<and> dist x b \<le> dist a b" |
|
2851 proof (intro conjI) |
|
2852 obtain u where u: "0 \<le> u" "u \<le> 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" |
|
2853 using assms by (force simp: in_segment algebra_simps) |
|
2854 have "dist x a = u * dist a b" |
|
2855 apply (simp add: dist_norm algebra_simps x) |
|
2856 by (metis \<open>0 \<le> u\<close> abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib) |
|
2857 also have "... \<le> dist a b" |
|
2858 by (simp add: mult_left_le_one_le u) |
|
2859 finally show "dist x a \<le> dist a b" . |
|
2860 have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)" |
|
2861 by (simp add: dist_norm algebra_simps x) |
|
2862 also have "... = (1-u) * dist a b" |
|
2863 proof - |
|
2864 have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)" |
|
2865 using \<open>u \<le> 1\<close> by force |
|
2866 then show ?thesis |
|
2867 by (simp add: dist_norm real_vector.scale_right_diff_distrib) |
|
2868 qed |
|
2869 also have "... \<le> dist a b" |
|
2870 by (simp add: mult_left_le_one_le u) |
|
2871 finally show "dist x b \<le> dist a b" . |
|
2872 qed |
|
2873 |
|
2874 lemma dist_in_open_segment: |
|
2875 fixes a :: "'a :: euclidean_space" |
|
2876 assumes "x \<in> open_segment a b" |
|
2877 shows "dist x a < dist a b \<and> dist x b < dist a b" |
|
2878 proof (intro conjI) |
|
2879 obtain u where u: "0 < u" "u < 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" |
|
2880 using assms by (force simp: in_segment algebra_simps) |
|
2881 have "dist x a = u * dist a b" |
|
2882 apply (simp add: dist_norm algebra_simps x) |
|
2883 by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib \<open>0 < u\<close>) |
|
2884 also have *: "... < dist a b" |
|
2885 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>) |
|
2886 finally show "dist x a < dist a b" . |
|
2887 have ab_ne0: "dist a b \<noteq> 0" |
|
2888 using * by fastforce |
|
2889 have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)" |
|
2890 by (simp add: dist_norm algebra_simps x) |
|
2891 also have "... = (1-u) * dist a b" |
|
2892 proof - |
|
2893 have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)" |
|
2894 using \<open>u < 1\<close> by force |
|
2895 then show ?thesis |
|
2896 by (simp add: dist_norm real_vector.scale_right_diff_distrib) |
|
2897 qed |
|
2898 also have "... < dist a b" |
|
2899 using ab_ne0 \<open>0 < u\<close> by simp |
|
2900 finally show "dist x b < dist a b" . |
|
2901 qed |
|
2902 |
|
2903 lemma dist_decreases_open_segment_0: |
|
2904 fixes x :: "'a :: euclidean_space" |
|
2905 assumes "x \<in> open_segment 0 b" |
|
2906 shows "dist c x < dist c 0 \<or> dist c x < dist c b" |
|
2907 proof (rule ccontr, clarsimp simp: not_less) |
|
2908 obtain u where u: "0 \<noteq> b" "0 < u" "u < 1" and x: "x = u *\<^sub>R b" |
|
2909 using assms by (auto simp: in_segment) |
|
2910 have xb: "x \<bullet> b < b \<bullet> b" |
|
2911 using u x by auto |
|
2912 assume "norm c \<le> dist c x" |
|
2913 then have "c \<bullet> c \<le> (c - x) \<bullet> (c - x)" |
|
2914 by (simp add: dist_norm norm_le) |
|
2915 moreover have "0 < x \<bullet> b" |
|
2916 using u x by auto |
|
2917 ultimately have less: "c \<bullet> b < x \<bullet> b" |
|
2918 by (simp add: x algebra_simps inner_commute u) |
|
2919 assume "dist c b \<le> dist c x" |
|
2920 then have "(c - b) \<bullet> (c - b) \<le> (c - x) \<bullet> (c - x)" |
|
2921 by (simp add: dist_norm norm_le) |
|
2922 then have "(b \<bullet> b) * (1 - u*u) \<le> 2 * (b \<bullet> c) * (1-u)" |
|
2923 by (simp add: x algebra_simps inner_commute) |
|
2924 then have "(1+u) * (b \<bullet> b) * (1-u) \<le> 2 * (b \<bullet> c) * (1-u)" |
|
2925 by (simp add: algebra_simps) |
|
2926 then have "(1+u) * (b \<bullet> b) \<le> 2 * (b \<bullet> c)" |
|
2927 using \<open>u < 1\<close> by auto |
|
2928 with xb have "c \<bullet> b \<ge> x \<bullet> b" |
|
2929 by (auto simp: x algebra_simps inner_commute) |
|
2930 with less show False by auto |
|
2931 qed |
|
2932 |
|
2933 proposition dist_decreases_open_segment: |
|
2934 fixes a :: "'a :: euclidean_space" |
|
2935 assumes "x \<in> open_segment a b" |
|
2936 shows "dist c x < dist c a \<or> dist c x < dist c b" |
|
2937 proof - |
|
2938 have *: "x - a \<in> open_segment 0 (b - a)" using assms |
|
2939 by (metis diff_self open_segment_translation_eq uminus_add_conv_diff) |
|
2940 show ?thesis |
|
2941 using dist_decreases_open_segment_0 [OF *, of "c-a"] assms |
|
2942 by (simp add: dist_norm) |
|
2943 qed |
|
2944 |
|
2945 corollary open_segment_furthest_le: |
|
2946 fixes a b x y :: "'a::euclidean_space" |
|
2947 assumes "x \<in> open_segment a b" |
|
2948 shows "norm (y - x) < norm (y - a) \<or> norm (y - x) < norm (y - b)" |
|
2949 by (metis assms dist_decreases_open_segment dist_norm) |
|
2950 |
|
2951 corollary dist_decreases_closed_segment: |
|
2952 fixes a :: "'a :: euclidean_space" |
|
2953 assumes "x \<in> closed_segment a b" |
|
2954 shows "dist c x \<le> dist c a \<or> dist c x \<le> dist c b" |
|
2955 apply (cases "x \<in> open_segment a b") |
|
2956 using dist_decreases_open_segment less_eq_real_def apply blast |
|
2957 by (metis DiffI assms empty_iff insertE open_segment_def order_refl) |
|
2958 |
|
2959 lemma convex_intermediate_ball: |
|
2960 fixes a :: "'a :: euclidean_space" |
|
2961 shows "\<lbrakk>ball a r \<subseteq> T; T \<subseteq> cball a r\<rbrakk> \<Longrightarrow> convex T" |
|
2962 apply (simp add: convex_contains_open_segment, clarify) |
|
2963 by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment) |
|
2964 |
|
2965 lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b \<subseteq> closed_segment a b" |
|
2966 apply (clarsimp simp: midpoint_def in_segment) |
|
2967 apply (rule_tac x="(1 + u) / 2" in exI) |
|
2968 apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib) |
|
2969 by (metis field_sum_of_halves scaleR_left.add) |
|
2970 |
|
2971 lemma notin_segment_midpoint: |
|
2972 fixes a :: "'a :: euclidean_space" |
|
2973 shows "a \<noteq> b \<Longrightarrow> a \<notin> closed_segment (midpoint a b) b" |
|
2974 by (auto simp: dist_midpoint dest!: dist_in_closed_segment) |
|
2975 |
|
2976 lemma segment_to_closest_point: |
|
2977 fixes S :: "'a :: euclidean_space set" |
|
2978 shows "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> open_segment a (closest_point S a) \<inter> S = {}" |
|
2979 apply (subst disjoint_iff_not_equal) |
|
2980 apply (clarify dest!: dist_in_open_segment) |
|
2981 by (metis closest_point_le dist_commute le_less_trans less_irrefl) |
|
2982 |
|
2983 lemma segment_to_point_exists: |
|
2984 fixes S :: "'a :: euclidean_space set" |
|
2985 assumes "closed S" "S \<noteq> {}" |
|
2986 obtains b where "b \<in> S" "open_segment a b \<inter> S = {}" |
|
2987 by (metis assms segment_to_closest_point closest_point_exists that) |
|
2988 |
|
2989 subsubsection\<open>More lemmas, especially for working with the underlying formula\<close> |
|
2990 |
|
2991 lemma segment_eq_compose: |
|
2992 fixes a :: "'a :: real_vector" |
|
2993 shows "(\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) = (\<lambda>x. a + x) o (\<lambda>u. u *\<^sub>R (b - a))" |
|
2994 by (simp add: o_def algebra_simps) |
|
2995 |
|
2996 lemma segment_degen_1: |
|
2997 fixes a :: "'a :: real_vector" |
|
2998 shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = b \<longleftrightarrow> a=b \<or> u=1" |
|
2999 proof - |
|
3000 { assume "(1 - u) *\<^sub>R a + u *\<^sub>R b = b" |
|
3001 then have "(1 - u) *\<^sub>R a = (1 - u) *\<^sub>R b" |
|
3002 by (simp add: algebra_simps) |
|
3003 then have "a=b \<or> u=1" |
|
3004 by simp |
|
3005 } then show ?thesis |
|
3006 by (auto simp: algebra_simps) |
|
3007 qed |
|
3008 |
|
3009 lemma segment_degen_0: |
|
3010 fixes a :: "'a :: real_vector" |
|
3011 shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = a \<longleftrightarrow> a=b \<or> u=0" |
|
3012 using segment_degen_1 [of "1-u" b a] |
|
3013 by (auto simp: algebra_simps) |
|
3014 |
|
3015 lemma add_scaleR_degen: |
|
3016 fixes a b ::"'a::real_vector" |
|
3017 assumes "(u *\<^sub>R b + v *\<^sub>R a) = (u *\<^sub>R a + v *\<^sub>R b)" "u \<noteq> v" |
|
3018 shows "a=b" |
|
3019 by (metis (no_types, hide_lams) add.commute add_diff_eq diff_add_cancel real_vector.scale_cancel_left real_vector.scale_left_diff_distrib assms) |
|
3020 |
|
3021 lemma closed_segment_image_interval: |
|
3022 "closed_segment a b = (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}" |
|
3023 by (auto simp: set_eq_iff image_iff closed_segment_def) |
|
3024 |
|
3025 lemma open_segment_image_interval: |
|
3026 "open_segment a b = (if a=b then {} else (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1})" |
|
3027 by (auto simp: open_segment_def closed_segment_def segment_degen_0 segment_degen_1) |
|
3028 |
|
3029 lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval |
|
3030 |
|
3031 lemma open_segment_bound1: |
|
3032 assumes "x \<in> open_segment a b" |
|
3033 shows "norm (x - a) < norm (b - a)" |
|
3034 proof - |
|
3035 obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 < u" "u < 1" "a \<noteq> b" |
|
3036 using assms by (auto simp add: open_segment_image_interval split: if_split_asm) |
|
3037 then show "norm (x - a) < norm (b - a)" |
|
3038 apply clarify |
|
3039 apply (auto simp: algebra_simps) |
|
3040 apply (simp add: scaleR_diff_right [symmetric]) |
|
3041 done |
|
3042 qed |
|
3043 |
|
3044 lemma compact_segment [simp]: |
|
3045 fixes a :: "'a::real_normed_vector" |
|
3046 shows "compact (closed_segment a b)" |
|
3047 by (auto simp: segment_image_interval intro!: compact_continuous_image continuous_intros) |
|
3048 |
|
3049 lemma closed_segment [simp]: |
|
3050 fixes a :: "'a::real_normed_vector" |
|
3051 shows "closed (closed_segment a b)" |
|
3052 by (simp add: compact_imp_closed) |
|
3053 |
|
3054 lemma closure_closed_segment [simp]: |
|
3055 fixes a :: "'a::real_normed_vector" |
|
3056 shows "closure(closed_segment a b) = closed_segment a b" |
|
3057 by simp |
|
3058 |
|
3059 lemma open_segment_bound: |
|
3060 assumes "x \<in> open_segment a b" |
|
3061 shows "norm (x - a) < norm (b - a)" "norm (x - b) < norm (b - a)" |
|
3062 apply (simp add: assms open_segment_bound1) |
|
3063 by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute) |
|
3064 |
|
3065 lemma closure_open_segment [simp]: |
|
3066 "closure (open_segment a b) = (if a = b then {} else closed_segment a b)" |
|
3067 for a :: "'a::euclidean_space" |
|
3068 proof (cases "a = b") |
|
3069 case True |
|
3070 then show ?thesis |
|
3071 by simp |
|
3072 next |
|
3073 case False |
|
3074 have "closure ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1}) = (\<lambda>u. u *\<^sub>R (b - a)) ` closure {0<..<1}" |
|
3075 apply (rule closure_injective_linear_image [symmetric]) |
|
3076 apply (use False in \<open>auto intro!: injI\<close>) |
|
3077 done |
|
3078 then have "closure |
|
3079 ((\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1}) = |
|
3080 (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b) ` closure {0<..<1}" |
|
3081 using closure_translation [of a "((\<lambda>x. x *\<^sub>R b - x *\<^sub>R a) ` {0<..<1})"] |
|
3082 by (simp add: segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right image_image) |
|
3083 then show ?thesis |
|
3084 by (simp add: segment_image_interval closure_greaterThanLessThan [symmetric] del: closure_greaterThanLessThan) |
|
3085 qed |
|
3086 |
|
3087 lemma closed_open_segment_iff [simp]: |
|
3088 fixes a :: "'a::euclidean_space" shows "closed(open_segment a b) \<longleftrightarrow> a = b" |
|
3089 by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2)) |
|
3090 |
|
3091 lemma compact_open_segment_iff [simp]: |
|
3092 fixes a :: "'a::euclidean_space" shows "compact(open_segment a b) \<longleftrightarrow> a = b" |
|
3093 by (simp add: bounded_open_segment compact_eq_bounded_closed) |
|
3094 |
|
3095 lemma convex_closed_segment [iff]: "convex (closed_segment a b)" |
|
3096 unfolding segment_convex_hull by(rule convex_convex_hull) |
|
3097 |
|
3098 lemma convex_open_segment [iff]: "convex (open_segment a b)" |
|
3099 proof - |
|
3100 have "convex ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})" |
|
3101 by (rule convex_linear_image) auto |
|
3102 then have "convex ((+) a ` (\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})" |
|
3103 by (rule convex_translation) |
|
3104 then show ?thesis |
|
3105 by (simp add: image_image open_segment_image_interval segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right) |
|
3106 qed |
|
3107 |
|
3108 lemmas convex_segment = convex_closed_segment convex_open_segment |
|
3109 |
|
3110 lemma connected_segment [iff]: |
|
3111 fixes x :: "'a :: real_normed_vector" |
|
3112 shows "connected (closed_segment x y)" |
|
3113 by (simp add: convex_connected) |
|
3114 |
|
3115 lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real |
|
3116 by (auto simp: is_interval_convex_1) |
|
3117 |
|
3118 lemma IVT'_closed_segment_real: |
|
3119 fixes f :: "real \<Rightarrow> real" |
|
3120 assumes "y \<in> closed_segment (f a) (f b)" |
|
3121 assumes "continuous_on (closed_segment a b) f" |
|
3122 shows "\<exists>x \<in> closed_segment a b. f x = y" |
|
3123 using IVT'[of f a y b] |
|
3124 IVT'[of "-f" a "-y" b] |
|
3125 IVT'[of f b y a] |
|
3126 IVT'[of "-f" b "-y" a] assms |
|
3127 by (cases "a \<le> b"; cases "f b \<ge> f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus) |
|
3128 |
|
3129 subsection \<open>Betweenness\<close> |
|
3130 |
|
3131 definition\<^marker>\<open>tag important\<close> "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)" |
|
3132 |
|
3133 lemma betweenI: |
|
3134 assumes "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" |
|
3135 shows "between (a, b) x" |
|
3136 using assms unfolding between_def closed_segment_def by auto |
|
3137 |
|
3138 lemma betweenE: |
|
3139 assumes "between (a, b) x" |
|
3140 obtains u where "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" |
|
3141 using assms unfolding between_def closed_segment_def by auto |
|
3142 |
|
3143 lemma between_implies_scaled_diff: |
|
3144 assumes "between (S, T) X" "between (S, T) Y" "S \<noteq> Y" |
|
3145 obtains c where "(X - Y) = c *\<^sub>R (S - Y)" |
|
3146 proof - |
|
3147 from \<open>between (S, T) X\<close> obtain u\<^sub>X where X: "X = u\<^sub>X *\<^sub>R S + (1 - u\<^sub>X) *\<^sub>R T" |
|
3148 by (metis add.commute betweenE eq_diff_eq) |
|
3149 from \<open>between (S, T) Y\<close> obtain u\<^sub>Y where Y: "Y = u\<^sub>Y *\<^sub>R S + (1 - u\<^sub>Y) *\<^sub>R T" |
|
3150 by (metis add.commute betweenE eq_diff_eq) |
|
3151 have "X - Y = (u\<^sub>X - u\<^sub>Y) *\<^sub>R (S - T)" |
|
3152 proof - |
|
3153 from X Y have "X - Y = u\<^sub>X *\<^sub>R S - u\<^sub>Y *\<^sub>R S + ((1 - u\<^sub>X) *\<^sub>R T - (1 - u\<^sub>Y) *\<^sub>R T)" by simp |
|
3154 also have "\<dots> = (u\<^sub>X - u\<^sub>Y) *\<^sub>R S - (u\<^sub>X - u\<^sub>Y) *\<^sub>R T" by (simp add: scaleR_left.diff) |
|
3155 finally show ?thesis by (simp add: real_vector.scale_right_diff_distrib) |
|
3156 qed |
|
3157 moreover from Y have "S - Y = (1 - u\<^sub>Y) *\<^sub>R (S - T)" |
|
3158 by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib) |
|
3159 moreover note \<open>S \<noteq> Y\<close> |
|
3160 ultimately have "(X - Y) = ((u\<^sub>X - u\<^sub>Y) / (1 - u\<^sub>Y)) *\<^sub>R (S - Y)" by auto |
|
3161 from this that show thesis by blast |
|
3162 qed |
|
3163 |
|
3164 lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b" |
|
3165 unfolding between_def by auto |
|
3166 |
|
3167 lemma between: "between (a, b) (x::'a::euclidean_space) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)" |
|
3168 proof (cases "a = b") |
|
3169 case True |
|
3170 then show ?thesis |
|
3171 by (auto simp add: between_def dist_commute) |
|
3172 next |
|
3173 case False |
|
3174 then have Fal: "norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0" |
|
3175 by auto |
|
3176 have *: "\<And>u. a - ((1 - u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)" |
|
3177 by (auto simp add: algebra_simps) |
|
3178 have "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)" if "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1" for u |
|
3179 proof - |
|
3180 have *: "a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)" |
|
3181 unfolding that(1) by (auto simp add:algebra_simps) |
|
3182 show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)" |
|
3183 unfolding norm_minus_commute[of x a] * using \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> |
|
3184 by simp |
|
3185 qed |
|
3186 moreover have "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" if "dist a b = dist a x + dist x b" |
|
3187 proof - |
|
3188 let ?\<beta> = "norm (a - x) / norm (a - b)" |
|
3189 show "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" |
|
3190 proof (intro exI conjI) |
|
3191 show "?\<beta> \<le> 1" |
|
3192 using Fal2 unfolding that[unfolded dist_norm] norm_ge_zero by auto |
|
3193 show "x = (1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b" |
|
3194 proof (subst euclidean_eq_iff; intro ballI) |
|
3195 fix i :: 'a |
|
3196 assume i: "i \<in> Basis" |
|
3197 have "((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> i |
|
3198 = ((norm (a - b) - norm (a - x)) * (a \<bullet> i) + norm (a - x) * (b \<bullet> i)) / norm (a - b)" |
|
3199 using Fal by (auto simp add: field_simps inner_simps) |
|
3200 also have "\<dots> = x\<bullet>i" |
|
3201 apply (rule divide_eq_imp[OF Fal]) |
|
3202 unfolding that[unfolded dist_norm] |
|
3203 using that[unfolded dist_triangle_eq] i |
|
3204 apply (subst (asm) euclidean_eq_iff) |
|
3205 apply (auto simp add: field_simps inner_simps) |
|
3206 done |
|
3207 finally show "x \<bullet> i = ((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> i" |
|
3208 by auto |
|
3209 qed |
|
3210 qed (use Fal2 in auto) |
|
3211 qed |
|
3212 ultimately show ?thesis |
|
3213 by (force simp add: between_def closed_segment_def dist_triangle_eq) |
|
3214 qed |
|
3215 |
|
3216 lemma between_midpoint: |
|
3217 fixes a :: "'a::euclidean_space" |
|
3218 shows "between (a,b) (midpoint a b)" (is ?t1) |
|
3219 and "between (b,a) (midpoint a b)" (is ?t2) |
|
3220 proof - |
|
3221 have *: "\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y" |
|
3222 by auto |
|
3223 show ?t1 ?t2 |
|
3224 unfolding between midpoint_def dist_norm |
|
3225 by (auto simp add: field_simps inner_simps euclidean_eq_iff[where 'a='a] intro!: *) |
|
3226 qed |
|
3227 |
|
3228 lemma between_mem_convex_hull: |
|
3229 "between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}" |
|
3230 unfolding between_mem_segment segment_convex_hull .. |
|
3231 |
|
3232 lemma between_triv_iff [simp]: "between (a,a) b \<longleftrightarrow> a=b" |
|
3233 by (auto simp: between_def) |
|
3234 |
|
3235 lemma between_triv1 [simp]: "between (a,b) a" |
|
3236 by (auto simp: between_def) |
|
3237 |
|
3238 lemma between_triv2 [simp]: "between (a,b) b" |
|
3239 by (auto simp: between_def) |
|
3240 |
|
3241 lemma between_commute: |
|
3242 "between (a,b) = between (b,a)" |
|
3243 by (auto simp: between_def closed_segment_commute) |
|
3244 |
|
3245 lemma between_antisym: |
|
3246 fixes a :: "'a :: euclidean_space" |
|
3247 shows "\<lbrakk>between (b,c) a; between (a,c) b\<rbrakk> \<Longrightarrow> a = b" |
|
3248 by (auto simp: between dist_commute) |
|
3249 |
|
3250 lemma between_trans: |
|
3251 fixes a :: "'a :: euclidean_space" |
|
3252 shows "\<lbrakk>between (b,c) a; between (a,c) d\<rbrakk> \<Longrightarrow> between (b,c) d" |
|
3253 using dist_triangle2 [of b c d] dist_triangle3 [of b d a] |
|
3254 by (auto simp: between dist_commute) |
|
3255 |
|
3256 lemma between_norm: |
|
3257 fixes a :: "'a :: euclidean_space" |
|
3258 shows "between (a,b) x \<longleftrightarrow> norm(x - a) *\<^sub>R (b - x) = norm(b - x) *\<^sub>R (x - a)" |
|
3259 by (auto simp: between dist_triangle_eq norm_minus_commute algebra_simps) |
|
3260 |
|
3261 lemma between_swap: |
|
3262 fixes A B X Y :: "'a::euclidean_space" |
|
3263 assumes "between (A, B) X" |
|
3264 assumes "between (A, B) Y" |
|
3265 shows "between (X, B) Y \<longleftrightarrow> between (A, Y) X" |
|
3266 using assms by (auto simp add: between) |
|
3267 |
|
3268 lemma between_translation [simp]: "between (a + y,a + z) (a + x) \<longleftrightarrow> between (y,z) x" |
|
3269 by (auto simp: between_def) |
|
3270 |
|
3271 lemma between_trans_2: |
|
3272 fixes a :: "'a :: euclidean_space" |
|
3273 shows "\<lbrakk>between (b,c) a; between (a,b) d\<rbrakk> \<Longrightarrow> between (c,d) a" |
|
3274 by (metis between_commute between_swap between_trans) |
|
3275 |
|
3276 lemma between_scaleR_lift [simp]: |
|
3277 fixes v :: "'a::euclidean_space" |
|
3278 shows "between (a *\<^sub>R v, b *\<^sub>R v) (c *\<^sub>R v) \<longleftrightarrow> v = 0 \<or> between (a, b) c" |
|
3279 by (simp add: between dist_norm scaleR_left_diff_distrib [symmetric] distrib_right [symmetric]) |
|
3280 |
|
3281 lemma between_1: |
|
3282 fixes x::real |
|
3283 shows "between (a,b) x \<longleftrightarrow> (a \<le> x \<and> x \<le> b) \<or> (b \<le> x \<and> x \<le> a)" |
|
3284 by (auto simp: between_mem_segment closed_segment_eq_real_ivl) |
|
3285 |
|
3286 |
|
3287 end |
2275 end |