8 chapter \<open>Unsorted\<close> |
8 chapter \<open>Unsorted\<close> |
9 |
9 |
10 theory Starlike |
10 theory Starlike |
11 imports Convex_Euclidean_Space Abstract_Limits |
11 imports Convex_Euclidean_Space Abstract_Limits |
12 begin |
12 begin |
13 |
|
14 section \<open>Line Segments\<close> |
|
15 |
|
16 subsection \<open>Midpoint\<close> |
|
17 |
|
18 definition\<^marker>\<open>tag important\<close> midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a" |
|
19 where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)" |
|
20 |
|
21 lemma midpoint_idem [simp]: "midpoint x x = x" |
|
22 unfolding midpoint_def by simp |
|
23 |
|
24 lemma midpoint_sym: "midpoint a b = midpoint b a" |
|
25 unfolding midpoint_def by (auto simp add: scaleR_right_distrib) |
|
26 |
|
27 lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c" |
|
28 proof - |
|
29 have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c" |
|
30 by simp |
|
31 then show ?thesis |
|
32 unfolding midpoint_def scaleR_2 [symmetric] by simp |
|
33 qed |
|
34 |
|
35 lemma |
|
36 fixes a::real |
|
37 assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b" |
|
38 and le_midpoint_1: "midpoint a b \<le> b" |
|
39 by (simp_all add: midpoint_def assms) |
|
40 |
|
41 lemma dist_midpoint: |
|
42 fixes a b :: "'a::real_normed_vector" shows |
|
43 "dist a (midpoint a b) = (dist a b) / 2" (is ?t1) |
|
44 "dist b (midpoint a b) = (dist a b) / 2" (is ?t2) |
|
45 "dist (midpoint a b) a = (dist a b) / 2" (is ?t3) |
|
46 "dist (midpoint a b) b = (dist a b) / 2" (is ?t4) |
|
47 proof - |
|
48 have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2" |
|
49 unfolding equation_minus_iff by auto |
|
50 have **: "\<And>x y::'a. 2 *\<^sub>R x = y \<Longrightarrow> norm x = (norm y) / 2" |
|
51 by auto |
|
52 note scaleR_right_distrib [simp] |
|
53 show ?t1 |
|
54 unfolding midpoint_def dist_norm |
|
55 apply (rule **) |
|
56 apply (simp add: scaleR_right_diff_distrib) |
|
57 apply (simp add: scaleR_2) |
|
58 done |
|
59 show ?t2 |
|
60 unfolding midpoint_def dist_norm |
|
61 apply (rule *) |
|
62 apply (simp add: scaleR_right_diff_distrib) |
|
63 apply (simp add: scaleR_2) |
|
64 done |
|
65 show ?t3 |
|
66 unfolding midpoint_def dist_norm |
|
67 apply (rule *) |
|
68 apply (simp add: scaleR_right_diff_distrib) |
|
69 apply (simp add: scaleR_2) |
|
70 done |
|
71 show ?t4 |
|
72 unfolding midpoint_def dist_norm |
|
73 apply (rule **) |
|
74 apply (simp add: scaleR_right_diff_distrib) |
|
75 apply (simp add: scaleR_2) |
|
76 done |
|
77 qed |
|
78 |
|
79 lemma midpoint_eq_endpoint [simp]: |
|
80 "midpoint a b = a \<longleftrightarrow> a = b" |
|
81 "midpoint a b = b \<longleftrightarrow> a = b" |
|
82 unfolding midpoint_eq_iff by auto |
|
83 |
|
84 lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b" |
|
85 using midpoint_eq_iff by metis |
|
86 |
|
87 lemma midpoint_linear_image: |
|
88 "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)" |
|
89 by (simp add: linear_iff midpoint_def) |
|
90 |
|
91 |
|
92 subsection \<open>Line segments\<close> |
|
93 |
|
94 definition\<^marker>\<open>tag important\<close> closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" |
|
95 where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}" |
|
96 |
|
97 definition\<^marker>\<open>tag important\<close> open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where |
|
98 "open_segment a b \<equiv> closed_segment a b - {a,b}" |
|
99 |
|
100 lemmas segment = open_segment_def closed_segment_def |
|
101 |
|
102 lemma in_segment: |
|
103 "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)" |
|
104 "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)" |
|
105 using less_eq_real_def by (auto simp: segment algebra_simps) |
|
106 |
|
107 lemma closed_segment_linear_image: |
|
108 "closed_segment (f a) (f b) = f ` (closed_segment a b)" if "linear f" |
|
109 proof - |
|
110 interpret linear f by fact |
|
111 show ?thesis |
|
112 by (force simp add: in_segment add scale) |
|
113 qed |
|
114 |
|
115 lemma open_segment_linear_image: |
|
116 "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> open_segment (f a) (f b) = f ` (open_segment a b)" |
|
117 by (force simp: open_segment_def closed_segment_linear_image inj_on_def) |
|
118 |
|
119 lemma closed_segment_translation: |
|
120 "closed_segment (c + a) (c + b) = image (\<lambda>x. c + x) (closed_segment a b)" |
|
121 apply safe |
|
122 apply (rule_tac x="x-c" in image_eqI) |
|
123 apply (auto simp: in_segment algebra_simps) |
|
124 done |
|
125 |
|
126 lemma open_segment_translation: |
|
127 "open_segment (c + a) (c + b) = image (\<lambda>x. c + x) (open_segment a b)" |
|
128 by (simp add: open_segment_def closed_segment_translation translation_diff) |
|
129 |
|
130 lemma closed_segment_of_real: |
|
131 "closed_segment (of_real x) (of_real y) = of_real ` closed_segment x y" |
|
132 apply (auto simp: image_iff in_segment scaleR_conv_of_real) |
|
133 apply (rule_tac x="(1-u)*x + u*y" in bexI) |
|
134 apply (auto simp: in_segment) |
|
135 done |
|
136 |
|
137 lemma open_segment_of_real: |
|
138 "open_segment (of_real x) (of_real y) = of_real ` open_segment x y" |
|
139 apply (auto simp: image_iff in_segment scaleR_conv_of_real) |
|
140 apply (rule_tac x="(1-u)*x + u*y" in bexI) |
|
141 apply (auto simp: in_segment) |
|
142 done |
|
143 |
|
144 lemma closed_segment_Reals: |
|
145 "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> closed_segment x y = of_real ` closed_segment (Re x) (Re y)" |
|
146 by (metis closed_segment_of_real of_real_Re) |
|
147 |
|
148 lemma open_segment_Reals: |
|
149 "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> open_segment x y = of_real ` open_segment (Re x) (Re y)" |
|
150 by (metis open_segment_of_real of_real_Re) |
|
151 |
|
152 lemma open_segment_PairD: |
|
153 "(x, x') \<in> open_segment (a, a') (b, b') |
|
154 \<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')" |
|
155 by (auto simp: in_segment) |
|
156 |
|
157 lemma closed_segment_PairD: |
|
158 "(x, x') \<in> closed_segment (a, a') (b, b') \<Longrightarrow> x \<in> closed_segment a b \<and> x' \<in> closed_segment a' b'" |
|
159 by (auto simp: closed_segment_def) |
|
160 |
|
161 lemma closed_segment_translation_eq [simp]: |
|
162 "d + x \<in> closed_segment (d + a) (d + b) \<longleftrightarrow> x \<in> closed_segment a b" |
|
163 proof - |
|
164 have *: "\<And>d x a b. x \<in> closed_segment a b \<Longrightarrow> d + x \<in> closed_segment (d + a) (d + b)" |
|
165 apply (simp add: closed_segment_def) |
|
166 apply (erule ex_forward) |
|
167 apply (simp add: algebra_simps) |
|
168 done |
|
169 show ?thesis |
|
170 using * [where d = "-d"] * |
|
171 by (fastforce simp add:) |
|
172 qed |
|
173 |
|
174 lemma open_segment_translation_eq [simp]: |
|
175 "d + x \<in> open_segment (d + a) (d + b) \<longleftrightarrow> x \<in> open_segment a b" |
|
176 by (simp add: open_segment_def) |
|
177 |
|
178 lemma of_real_closed_segment [simp]: |
|
179 "of_real x \<in> closed_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> closed_segment a b" |
|
180 apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward) |
|
181 using of_real_eq_iff by fastforce |
|
182 |
|
183 lemma of_real_open_segment [simp]: |
|
184 "of_real x \<in> open_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> open_segment a b" |
|
185 apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE) |
|
186 using of_real_eq_iff by fastforce |
|
187 |
|
188 lemma convex_contains_segment: |
|
189 "convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)" |
|
190 unfolding convex_alt closed_segment_def by auto |
|
191 |
|
192 lemma closed_segment_in_Reals: |
|
193 "\<lbrakk>x \<in> closed_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals" |
|
194 by (meson subsetD convex_Reals convex_contains_segment) |
|
195 |
|
196 lemma open_segment_in_Reals: |
|
197 "\<lbrakk>x \<in> open_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals" |
|
198 by (metis Diff_iff closed_segment_in_Reals open_segment_def) |
|
199 |
|
200 lemma closed_segment_subset: "\<lbrakk>x \<in> S; y \<in> S; convex S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> S" |
|
201 by (simp add: convex_contains_segment) |
|
202 |
|
203 lemma closed_segment_subset_convex_hull: |
|
204 "\<lbrakk>x \<in> convex hull S; y \<in> convex hull S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull S" |
|
205 using convex_contains_segment by blast |
|
206 |
|
207 lemma segment_convex_hull: |
|
208 "closed_segment a b = convex hull {a,b}" |
|
209 proof - |
|
210 have *: "\<And>x. {x} \<noteq> {}" by auto |
|
211 show ?thesis |
|
212 unfolding segment convex_hull_insert[OF *] convex_hull_singleton |
|
213 by (safe; rule_tac x="1 - u" in exI; force) |
|
214 qed |
|
215 |
|
216 lemma open_closed_segment: "u \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z" |
|
217 by (auto simp add: closed_segment_def open_segment_def) |
|
218 |
|
219 lemma segment_open_subset_closed: |
|
220 "open_segment a b \<subseteq> closed_segment a b" |
|
221 by (auto simp: closed_segment_def open_segment_def) |
|
222 |
|
223 lemma bounded_closed_segment: |
|
224 fixes a :: "'a::euclidean_space" shows "bounded (closed_segment a b)" |
|
225 by (simp add: segment_convex_hull compact_convex_hull compact_imp_bounded) |
|
226 |
|
227 lemma bounded_open_segment: |
|
228 fixes a :: "'a::euclidean_space" shows "bounded (open_segment a b)" |
|
229 by (rule bounded_subset [OF bounded_closed_segment segment_open_subset_closed]) |
|
230 |
|
231 lemmas bounded_segment = bounded_closed_segment open_closed_segment |
|
232 |
|
233 lemma ends_in_segment [iff]: "a \<in> closed_segment a b" "b \<in> closed_segment a b" |
|
234 unfolding segment_convex_hull |
|
235 by (auto intro!: hull_subset[unfolded subset_eq, rule_format]) |
|
236 |
|
237 lemma eventually_closed_segment: |
|
238 fixes x0::"'a::real_normed_vector" |
|
239 assumes "open X0" "x0 \<in> X0" |
|
240 shows "\<forall>\<^sub>F x in at x0 within U. closed_segment x0 x \<subseteq> X0" |
|
241 proof - |
|
242 from openE[OF assms] |
|
243 obtain e where e: "0 < e" "ball x0 e \<subseteq> X0" . |
|
244 then have "\<forall>\<^sub>F x in at x0 within U. x \<in> ball x0 e" |
|
245 by (auto simp: dist_commute eventually_at) |
|
246 then show ?thesis |
|
247 proof eventually_elim |
|
248 case (elim x) |
|
249 have "x0 \<in> ball x0 e" using \<open>e > 0\<close> by simp |
|
250 from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim] |
|
251 have "closed_segment x0 x \<subseteq> ball x0 e" . |
|
252 also note \<open>\<dots> \<subseteq> X0\<close> |
|
253 finally show ?case . |
|
254 qed |
|
255 qed |
|
256 |
|
257 lemma segment_furthest_le: |
|
258 fixes a b x y :: "'a::euclidean_space" |
|
259 assumes "x \<in> closed_segment a b" |
|
260 shows "norm (y - x) \<le> norm (y - a) \<or> norm (y - x) \<le> norm (y - b)" |
|
261 proof - |
|
262 obtain z where "z \<in> {a, b}" "norm (x - y) \<le> norm (z - y)" |
|
263 using simplex_furthest_le[of "{a, b}" y] |
|
264 using assms[unfolded segment_convex_hull] |
|
265 by auto |
|
266 then show ?thesis |
|
267 by (auto simp add:norm_minus_commute) |
|
268 qed |
|
269 |
|
270 lemma closed_segment_commute: "closed_segment a b = closed_segment b a" |
|
271 proof - |
|
272 have "{a, b} = {b, a}" by auto |
|
273 thus ?thesis |
|
274 by (simp add: segment_convex_hull) |
|
275 qed |
|
276 |
|
277 lemma segment_bound1: |
|
278 assumes "x \<in> closed_segment a b" |
|
279 shows "norm (x - a) \<le> norm (b - a)" |
|
280 proof - |
|
281 obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1" |
|
282 using assms by (auto simp add: closed_segment_def) |
|
283 then show "norm (x - a) \<le> norm (b - a)" |
|
284 apply clarify |
|
285 apply (auto simp: algebra_simps) |
|
286 apply (simp add: scaleR_diff_right [symmetric] mult_left_le_one_le) |
|
287 done |
|
288 qed |
|
289 |
|
290 lemma segment_bound: |
|
291 assumes "x \<in> closed_segment a b" |
|
292 shows "norm (x - a) \<le> norm (b - a)" "norm (x - b) \<le> norm (b - a)" |
|
293 apply (simp add: assms segment_bound1) |
|
294 by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1) |
|
295 |
|
296 lemma open_segment_commute: "open_segment a b = open_segment b a" |
|
297 proof - |
|
298 have "{a, b} = {b, a}" by auto |
|
299 thus ?thesis |
|
300 by (simp add: closed_segment_commute open_segment_def) |
|
301 qed |
|
302 |
|
303 lemma closed_segment_idem [simp]: "closed_segment a a = {a}" |
|
304 unfolding segment by (auto simp add: algebra_simps) |
|
305 |
|
306 lemma open_segment_idem [simp]: "open_segment a a = {}" |
|
307 by (simp add: open_segment_def) |
|
308 |
|
309 lemma closed_segment_eq_open: "closed_segment a b = open_segment a b \<union> {a,b}" |
|
310 using open_segment_def by auto |
|
311 |
|
312 lemma convex_contains_open_segment: |
|
313 "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. open_segment a b \<subseteq> s)" |
|
314 by (simp add: convex_contains_segment closed_segment_eq_open) |
|
315 |
|
316 lemma closed_segment_eq_real_ivl: |
|
317 fixes a b::real |
|
318 shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})" |
|
319 proof - |
|
320 have "b \<le> a \<Longrightarrow> closed_segment b a = {b .. a}" |
|
321 and "a \<le> b \<Longrightarrow> closed_segment a b = {a .. b}" |
|
322 by (auto simp: convex_hull_eq_real_cbox segment_convex_hull) |
|
323 thus ?thesis |
|
324 by (auto simp: closed_segment_commute) |
|
325 qed |
|
326 |
|
327 lemma open_segment_eq_real_ivl: |
|
328 fixes a b::real |
|
329 shows "open_segment a b = (if a \<le> b then {a<..<b} else {b<..<a})" |
|
330 by (auto simp: closed_segment_eq_real_ivl open_segment_def split: if_split_asm) |
|
331 |
|
332 lemma closed_segment_real_eq: |
|
333 fixes u::real shows "closed_segment u v = (\<lambda>x. (v - u) * x + u) ` {0..1}" |
|
334 by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl) |
|
335 |
|
336 lemma dist_in_closed_segment: |
|
337 fixes a :: "'a :: euclidean_space" |
|
338 assumes "x \<in> closed_segment a b" |
|
339 shows "dist x a \<le> dist a b \<and> dist x b \<le> dist a b" |
|
340 proof (intro conjI) |
|
341 obtain u where u: "0 \<le> u" "u \<le> 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" |
|
342 using assms by (force simp: in_segment algebra_simps) |
|
343 have "dist x a = u * dist a b" |
|
344 apply (simp add: dist_norm algebra_simps x) |
|
345 by (metis \<open>0 \<le> u\<close> abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib) |
|
346 also have "... \<le> dist a b" |
|
347 by (simp add: mult_left_le_one_le u) |
|
348 finally show "dist x a \<le> dist a b" . |
|
349 have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)" |
|
350 by (simp add: dist_norm algebra_simps x) |
|
351 also have "... = (1-u) * dist a b" |
|
352 proof - |
|
353 have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)" |
|
354 using \<open>u \<le> 1\<close> by force |
|
355 then show ?thesis |
|
356 by (simp add: dist_norm real_vector.scale_right_diff_distrib) |
|
357 qed |
|
358 also have "... \<le> dist a b" |
|
359 by (simp add: mult_left_le_one_le u) |
|
360 finally show "dist x b \<le> dist a b" . |
|
361 qed |
|
362 |
|
363 lemma dist_in_open_segment: |
|
364 fixes a :: "'a :: euclidean_space" |
|
365 assumes "x \<in> open_segment a b" |
|
366 shows "dist x a < dist a b \<and> dist x b < dist a b" |
|
367 proof (intro conjI) |
|
368 obtain u where u: "0 < u" "u < 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" |
|
369 using assms by (force simp: in_segment algebra_simps) |
|
370 have "dist x a = u * dist a b" |
|
371 apply (simp add: dist_norm algebra_simps x) |
|
372 by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib \<open>0 < u\<close>) |
|
373 also have *: "... < dist a b" |
|
374 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>) |
|
375 finally show "dist x a < dist a b" . |
|
376 have ab_ne0: "dist a b \<noteq> 0" |
|
377 using * by fastforce |
|
378 have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)" |
|
379 by (simp add: dist_norm algebra_simps x) |
|
380 also have "... = (1-u) * dist a b" |
|
381 proof - |
|
382 have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)" |
|
383 using \<open>u < 1\<close> by force |
|
384 then show ?thesis |
|
385 by (simp add: dist_norm real_vector.scale_right_diff_distrib) |
|
386 qed |
|
387 also have "... < dist a b" |
|
388 using ab_ne0 \<open>0 < u\<close> by simp |
|
389 finally show "dist x b < dist a b" . |
|
390 qed |
|
391 |
|
392 lemma dist_decreases_open_segment_0: |
|
393 fixes x :: "'a :: euclidean_space" |
|
394 assumes "x \<in> open_segment 0 b" |
|
395 shows "dist c x < dist c 0 \<or> dist c x < dist c b" |
|
396 proof (rule ccontr, clarsimp simp: not_less) |
|
397 obtain u where u: "0 \<noteq> b" "0 < u" "u < 1" and x: "x = u *\<^sub>R b" |
|
398 using assms by (auto simp: in_segment) |
|
399 have xb: "x \<bullet> b < b \<bullet> b" |
|
400 using u x by auto |
|
401 assume "norm c \<le> dist c x" |
|
402 then have "c \<bullet> c \<le> (c - x) \<bullet> (c - x)" |
|
403 by (simp add: dist_norm norm_le) |
|
404 moreover have "0 < x \<bullet> b" |
|
405 using u x by auto |
|
406 ultimately have less: "c \<bullet> b < x \<bullet> b" |
|
407 by (simp add: x algebra_simps inner_commute u) |
|
408 assume "dist c b \<le> dist c x" |
|
409 then have "(c - b) \<bullet> (c - b) \<le> (c - x) \<bullet> (c - x)" |
|
410 by (simp add: dist_norm norm_le) |
|
411 then have "(b \<bullet> b) * (1 - u*u) \<le> 2 * (b \<bullet> c) * (1-u)" |
|
412 by (simp add: x algebra_simps inner_commute) |
|
413 then have "(1+u) * (b \<bullet> b) * (1-u) \<le> 2 * (b \<bullet> c) * (1-u)" |
|
414 by (simp add: algebra_simps) |
|
415 then have "(1+u) * (b \<bullet> b) \<le> 2 * (b \<bullet> c)" |
|
416 using \<open>u < 1\<close> by auto |
|
417 with xb have "c \<bullet> b \<ge> x \<bullet> b" |
|
418 by (auto simp: x algebra_simps inner_commute) |
|
419 with less show False by auto |
|
420 qed |
|
421 |
|
422 proposition dist_decreases_open_segment: |
|
423 fixes a :: "'a :: euclidean_space" |
|
424 assumes "x \<in> open_segment a b" |
|
425 shows "dist c x < dist c a \<or> dist c x < dist c b" |
|
426 proof - |
|
427 have *: "x - a \<in> open_segment 0 (b - a)" using assms |
|
428 by (metis diff_self open_segment_translation_eq uminus_add_conv_diff) |
|
429 show ?thesis |
|
430 using dist_decreases_open_segment_0 [OF *, of "c-a"] assms |
|
431 by (simp add: dist_norm) |
|
432 qed |
|
433 |
|
434 corollary open_segment_furthest_le: |
|
435 fixes a b x y :: "'a::euclidean_space" |
|
436 assumes "x \<in> open_segment a b" |
|
437 shows "norm (y - x) < norm (y - a) \<or> norm (y - x) < norm (y - b)" |
|
438 by (metis assms dist_decreases_open_segment dist_norm) |
|
439 |
|
440 corollary dist_decreases_closed_segment: |
|
441 fixes a :: "'a :: euclidean_space" |
|
442 assumes "x \<in> closed_segment a b" |
|
443 shows "dist c x \<le> dist c a \<or> dist c x \<le> dist c b" |
|
444 apply (cases "x \<in> open_segment a b") |
|
445 using dist_decreases_open_segment less_eq_real_def apply blast |
|
446 by (metis DiffI assms empty_iff insertE open_segment_def order_refl) |
|
447 |
|
448 lemma convex_intermediate_ball: |
|
449 fixes a :: "'a :: euclidean_space" |
|
450 shows "\<lbrakk>ball a r \<subseteq> T; T \<subseteq> cball a r\<rbrakk> \<Longrightarrow> convex T" |
|
451 apply (simp add: convex_contains_open_segment, clarify) |
|
452 by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment) |
|
453 |
|
454 lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b \<subseteq> closed_segment a b" |
|
455 apply (clarsimp simp: midpoint_def in_segment) |
|
456 apply (rule_tac x="(1 + u) / 2" in exI) |
|
457 apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib) |
|
458 by (metis field_sum_of_halves scaleR_left.add) |
|
459 |
|
460 lemma notin_segment_midpoint: |
|
461 fixes a :: "'a :: euclidean_space" |
|
462 shows "a \<noteq> b \<Longrightarrow> a \<notin> closed_segment (midpoint a b) b" |
|
463 by (auto simp: dist_midpoint dest!: dist_in_closed_segment) |
|
464 |
|
465 lemma segment_to_closest_point: |
|
466 fixes S :: "'a :: euclidean_space set" |
|
467 shows "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> open_segment a (closest_point S a) \<inter> S = {}" |
|
468 apply (subst disjoint_iff_not_equal) |
|
469 apply (clarify dest!: dist_in_open_segment) |
|
470 by (metis closest_point_le dist_commute le_less_trans less_irrefl) |
|
471 |
|
472 lemma segment_to_point_exists: |
|
473 fixes S :: "'a :: euclidean_space set" |
|
474 assumes "closed S" "S \<noteq> {}" |
|
475 obtains b where "b \<in> S" "open_segment a b \<inter> S = {}" |
|
476 by (metis assms segment_to_closest_point closest_point_exists that) |
|
477 |
|
478 subsubsection\<open>More lemmas, especially for working with the underlying formula\<close> |
|
479 |
|
480 lemma segment_eq_compose: |
|
481 fixes a :: "'a :: real_vector" |
|
482 shows "(\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) = (\<lambda>x. a + x) o (\<lambda>u. u *\<^sub>R (b - a))" |
|
483 by (simp add: o_def algebra_simps) |
|
484 |
|
485 lemma segment_degen_1: |
|
486 fixes a :: "'a :: real_vector" |
|
487 shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = b \<longleftrightarrow> a=b \<or> u=1" |
|
488 proof - |
|
489 { assume "(1 - u) *\<^sub>R a + u *\<^sub>R b = b" |
|
490 then have "(1 - u) *\<^sub>R a = (1 - u) *\<^sub>R b" |
|
491 by (simp add: algebra_simps) |
|
492 then have "a=b \<or> u=1" |
|
493 by simp |
|
494 } then show ?thesis |
|
495 by (auto simp: algebra_simps) |
|
496 qed |
|
497 |
|
498 lemma segment_degen_0: |
|
499 fixes a :: "'a :: real_vector" |
|
500 shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = a \<longleftrightarrow> a=b \<or> u=0" |
|
501 using segment_degen_1 [of "1-u" b a] |
|
502 by (auto simp: algebra_simps) |
|
503 |
|
504 lemma add_scaleR_degen: |
|
505 fixes a b ::"'a::real_vector" |
|
506 assumes "(u *\<^sub>R b + v *\<^sub>R a) = (u *\<^sub>R a + v *\<^sub>R b)" "u \<noteq> v" |
|
507 shows "a=b" |
|
508 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) |
|
509 |
|
510 lemma closed_segment_image_interval: |
|
511 "closed_segment a b = (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}" |
|
512 by (auto simp: set_eq_iff image_iff closed_segment_def) |
|
513 |
|
514 lemma open_segment_image_interval: |
|
515 "open_segment a b = (if a=b then {} else (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1})" |
|
516 by (auto simp: open_segment_def closed_segment_def segment_degen_0 segment_degen_1) |
|
517 |
|
518 lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval |
|
519 |
|
520 lemma open_segment_bound1: |
|
521 assumes "x \<in> open_segment a b" |
|
522 shows "norm (x - a) < norm (b - a)" |
|
523 proof - |
|
524 obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 < u" "u < 1" "a \<noteq> b" |
|
525 using assms by (auto simp add: open_segment_image_interval split: if_split_asm) |
|
526 then show "norm (x - a) < norm (b - a)" |
|
527 apply clarify |
|
528 apply (auto simp: algebra_simps) |
|
529 apply (simp add: scaleR_diff_right [symmetric]) |
|
530 done |
|
531 qed |
|
532 |
|
533 lemma compact_segment [simp]: |
|
534 fixes a :: "'a::real_normed_vector" |
|
535 shows "compact (closed_segment a b)" |
|
536 by (auto simp: segment_image_interval intro!: compact_continuous_image continuous_intros) |
|
537 |
|
538 lemma closed_segment [simp]: |
|
539 fixes a :: "'a::real_normed_vector" |
|
540 shows "closed (closed_segment a b)" |
|
541 by (simp add: compact_imp_closed) |
|
542 |
|
543 lemma closure_closed_segment [simp]: |
|
544 fixes a :: "'a::real_normed_vector" |
|
545 shows "closure(closed_segment a b) = closed_segment a b" |
|
546 by simp |
|
547 |
|
548 lemma open_segment_bound: |
|
549 assumes "x \<in> open_segment a b" |
|
550 shows "norm (x - a) < norm (b - a)" "norm (x - b) < norm (b - a)" |
|
551 apply (simp add: assms open_segment_bound1) |
|
552 by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute) |
|
553 |
|
554 lemma closure_open_segment [simp]: |
|
555 "closure (open_segment a b) = (if a = b then {} else closed_segment a b)" |
|
556 for a :: "'a::euclidean_space" |
|
557 proof (cases "a = b") |
|
558 case True |
|
559 then show ?thesis |
|
560 by simp |
|
561 next |
|
562 case False |
|
563 have "closure ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1}) = (\<lambda>u. u *\<^sub>R (b - a)) ` closure {0<..<1}" |
|
564 apply (rule closure_injective_linear_image [symmetric]) |
|
565 apply (use False in \<open>auto intro!: injI\<close>) |
|
566 done |
|
567 then have "closure |
|
568 ((\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1}) = |
|
569 (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b) ` closure {0<..<1}" |
|
570 using closure_translation [of a "((\<lambda>x. x *\<^sub>R b - x *\<^sub>R a) ` {0<..<1})"] |
|
571 by (simp add: segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right image_image) |
|
572 then show ?thesis |
|
573 by (simp add: segment_image_interval closure_greaterThanLessThan [symmetric] del: closure_greaterThanLessThan) |
|
574 qed |
|
575 |
|
576 lemma closed_open_segment_iff [simp]: |
|
577 fixes a :: "'a::euclidean_space" shows "closed(open_segment a b) \<longleftrightarrow> a = b" |
|
578 by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2)) |
|
579 |
|
580 lemma compact_open_segment_iff [simp]: |
|
581 fixes a :: "'a::euclidean_space" shows "compact(open_segment a b) \<longleftrightarrow> a = b" |
|
582 by (simp add: bounded_open_segment compact_eq_bounded_closed) |
|
583 |
|
584 lemma convex_closed_segment [iff]: "convex (closed_segment a b)" |
|
585 unfolding segment_convex_hull by(rule convex_convex_hull) |
|
586 |
|
587 lemma convex_open_segment [iff]: "convex (open_segment a b)" |
|
588 proof - |
|
589 have "convex ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})" |
|
590 by (rule convex_linear_image) auto |
|
591 then have "convex ((+) a ` (\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})" |
|
592 by (rule convex_translation) |
|
593 then show ?thesis |
|
594 by (simp add: image_image open_segment_image_interval segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right) |
|
595 qed |
|
596 |
|
597 lemmas convex_segment = convex_closed_segment convex_open_segment |
|
598 |
|
599 lemma connected_segment [iff]: |
|
600 fixes x :: "'a :: real_normed_vector" |
|
601 shows "connected (closed_segment x y)" |
|
602 by (simp add: convex_connected) |
|
603 |
|
604 lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real |
|
605 by (auto simp: is_interval_convex_1) |
|
606 |
|
607 lemma IVT'_closed_segment_real: |
|
608 fixes f :: "real \<Rightarrow> real" |
|
609 assumes "y \<in> closed_segment (f a) (f b)" |
|
610 assumes "continuous_on (closed_segment a b) f" |
|
611 shows "\<exists>x \<in> closed_segment a b. f x = y" |
|
612 using IVT'[of f a y b] |
|
613 IVT'[of "-f" a "-y" b] |
|
614 IVT'[of f b y a] |
|
615 IVT'[of "-f" b "-y" a] assms |
|
616 by (cases "a \<le> b"; cases "f b \<ge> f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus) |
|
617 |
|
618 |
13 |
619 subsection\<open>Starlike sets\<close> |
14 subsection\<open>Starlike sets\<close> |
620 |
15 |
621 definition\<^marker>\<open>tag important\<close> "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)" |
16 definition\<^marker>\<open>tag important\<close> "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)" |
622 |
17 |