author | wenzelm |
Fri, 27 Nov 2020 11:41:43 +0100 | |
changeset 72740 | 082200ee003d |
parent 72569 | d56e4eeae967 |
child 73932 | fd21b4a93043 |
permissions | -rw-r--r-- |
71028 | 1 |
(* Title: HOL/Analysis/Line_Segment.thy |
2 |
Author: L C Paulson, University of Cambridge |
|
3 |
Author: Robert Himmelmann, TU Muenchen |
|
4 |
Author: Bogdan Grechuk, University of Edinburgh |
|
5 |
Author: Armin Heller, TU Muenchen |
|
6 |
Author: Johannes Hoelzl, TU Muenchen |
|
7 |
*) |
|
8 |
||
9 |
section \<open>Line Segment\<close> |
|
10 |
||
11 |
theory Line_Segment |
|
12 |
imports |
|
13 |
Convex |
|
14 |
Topology_Euclidean_Space |
|
15 |
begin |
|
16 |
||
71169
df1d96114754
Fixed a few messy proofs and adjusted inconsistent section headings
paulson <lp15@cam.ac.uk>
parents:
71028
diff
changeset
|
17 |
subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological Properties of Convex Sets, Metric Spaces and Functions\<close> |
71028 | 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) |
|
71169
df1d96114754
Fixed a few messy proofs and adjusted inconsistent section headings
paulson <lp15@cam.ac.uk>
parents:
71028
diff
changeset
|
26 |
then have "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}" |
71028 | 27 |
by (force intro: sum.mono_neutral_left simp: supp_sum_def support_on_def) |
71169
df1d96114754
Fixed a few messy proofs and adjusted inconsistent section headings
paulson <lp15@cam.ac.uk>
parents:
71028
diff
changeset
|
28 |
also have "... \<in> S" |
df1d96114754
Fixed a few messy proofs and adjusted inconsistent section headings
paulson <lp15@cam.ac.uk>
parents:
71028
diff
changeset
|
29 |
using 1 assms by (force simp: supp_sum_def support_on_def intro: convex_sum [OF fin \<open>convex S\<close>]) |
df1d96114754
Fixed a few messy proofs and adjusted inconsistent section headings
paulson <lp15@cam.ac.uk>
parents:
71028
diff
changeset
|
30 |
finally show ?thesis . |
71028 | 31 |
qed |
32 |
||
33 |
lemma sphere_eq_empty [simp]: |
|
34 |
fixes a :: "'a::{real_normed_vector, perfect_space}" |
|
35 |
shows "sphere a r = {} \<longleftrightarrow> r < 0" |
|
36 |
by (auto simp: sphere_def dist_norm) (metis dist_norm le_less_linear vector_choose_dist) |
|
37 |
||
38 |
lemma cone_closure: |
|
39 |
fixes S :: "'a::real_normed_vector set" |
|
40 |
assumes "cone S" |
|
41 |
shows "cone (closure S)" |
|
42 |
proof (cases "S = {}") |
|
43 |
case True |
|
44 |
then show ?thesis by auto |
|
45 |
next |
|
46 |
case False |
|
47 |
then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)" |
|
48 |
using cone_iff[of S] assms by auto |
|
49 |
then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` closure S = closure S)" |
|
50 |
using closure_subset by (auto simp: closure_scaleR) |
|
51 |
then show ?thesis |
|
52 |
using False cone_iff[of "closure S"] by auto |
|
53 |
qed |
|
54 |
||
55 |
||
56 |
corollary component_complement_connected: |
|
57 |
fixes S :: "'a::real_normed_vector set" |
|
58 |
assumes "connected S" "C \<in> components (-S)" |
|
59 |
shows "connected(-C)" |
|
60 |
using component_diff_connected [of S UNIV] assms |
|
61 |
by (auto simp: Compl_eq_Diff_UNIV) |
|
62 |
||
63 |
proposition clopen: |
|
64 |
fixes S :: "'a :: real_normed_vector set" |
|
65 |
shows "closed S \<and> open S \<longleftrightarrow> S = {} \<or> S = UNIV" |
|
71169
df1d96114754
Fixed a few messy proofs and adjusted inconsistent section headings
paulson <lp15@cam.ac.uk>
parents:
71028
diff
changeset
|
66 |
by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format]) |
71028 | 67 |
|
68 |
corollary compact_open: |
|
69 |
fixes S :: "'a :: euclidean_space set" |
|
70 |
shows "compact S \<and> open S \<longleftrightarrow> S = {}" |
|
71 |
by (auto simp: compact_eq_bounded_closed clopen) |
|
72 |
||
73 |
corollary finite_imp_not_open: |
|
71169
df1d96114754
Fixed a few messy proofs and adjusted inconsistent section headings
paulson <lp15@cam.ac.uk>
parents:
71028
diff
changeset
|
74 |
fixes S :: "'a::{real_normed_vector, perfect_space} set" |
df1d96114754
Fixed a few messy proofs and adjusted inconsistent section headings
paulson <lp15@cam.ac.uk>
parents:
71028
diff
changeset
|
75 |
shows "\<lbrakk>finite S; open S\<rbrakk> \<Longrightarrow> S={}" |
71028 | 76 |
using clopen [of S] finite_imp_closed not_bounded_UNIV by blast |
77 |
||
78 |
corollary empty_interior_finite: |
|
79 |
fixes S :: "'a::{real_normed_vector, perfect_space} set" |
|
80 |
shows "finite S \<Longrightarrow> interior S = {}" |
|
81 |
by (metis interior_subset finite_subset open_interior [of S] finite_imp_not_open) |
|
82 |
||
83 |
text \<open>Balls, being convex, are connected.\<close> |
|
84 |
||
85 |
lemma convex_local_global_minimum: |
|
86 |
fixes s :: "'a::real_normed_vector set" |
|
87 |
assumes "e > 0" |
|
88 |
and "convex_on s f" |
|
89 |
and "ball x e \<subseteq> s" |
|
90 |
and "\<forall>y\<in>ball x e. f x \<le> f y" |
|
91 |
shows "\<forall>y\<in>s. f x \<le> f y" |
|
92 |
proof (rule ccontr) |
|
93 |
have "x \<in> s" using assms(1,3) by auto |
|
94 |
assume "\<not> ?thesis" |
|
95 |
then obtain y where "y\<in>s" and y: "f x > f y" by auto |
|
96 |
then have xy: "0 < dist x y" by auto |
|
97 |
then obtain u where "0 < u" "u \<le> 1" and u: "u < e / dist x y" |
|
98 |
using field_lbound_gt_zero[of 1 "e / dist x y"] xy \<open>e>0\<close> by auto |
|
99 |
then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y" |
|
100 |
using \<open>x\<in>s\<close> \<open>y\<in>s\<close> |
|
101 |
using assms(2)[unfolded convex_on_def, |
|
102 |
THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]] |
|
103 |
by auto |
|
104 |
moreover |
|
105 |
have *: "x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)" |
|
106 |
by (simp add: algebra_simps) |
|
107 |
have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> ball x e" |
|
108 |
unfolding mem_ball dist_norm |
|
109 |
unfolding * and norm_scaleR and abs_of_pos[OF \<open>0<u\<close>] |
|
110 |
unfolding dist_norm[symmetric] |
|
111 |
using u |
|
112 |
unfolding pos_less_divide_eq[OF xy] |
|
113 |
by auto |
|
114 |
then have "f x \<le> f ((1 - u) *\<^sub>R x + u *\<^sub>R y)" |
|
115 |
using assms(4) by auto |
|
116 |
ultimately show False |
|
117 |
using mult_strict_left_mono[OF y \<open>u>0\<close>] |
|
118 |
unfolding left_diff_distrib |
|
119 |
by auto |
|
120 |
qed |
|
121 |
||
122 |
lemma convex_ball [iff]: |
|
123 |
fixes x :: "'a::real_normed_vector" |
|
124 |
shows "convex (ball x e)" |
|
125 |
proof (auto simp: convex_def) |
|
126 |
fix y z |
|
127 |
assume yz: "dist x y < e" "dist x z < e" |
|
128 |
fix u v :: real |
|
129 |
assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1" |
|
130 |
have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" |
|
131 |
using uv yz |
|
132 |
using convex_on_dist [of "ball x e" x, unfolded convex_on_def, |
|
133 |
THEN bspec[where x=y], THEN bspec[where x=z]] |
|
134 |
by auto |
|
135 |
then show "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" |
|
136 |
using convex_bound_lt[OF yz uv] by auto |
|
137 |
qed |
|
138 |
||
139 |
lemma convex_cball [iff]: |
|
140 |
fixes x :: "'a::real_normed_vector" |
|
141 |
shows "convex (cball x e)" |
|
142 |
proof - |
|
143 |
{ |
|
144 |
fix y z |
|
145 |
assume yz: "dist x y \<le> e" "dist x z \<le> e" |
|
146 |
fix u v :: real |
|
147 |
assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1" |
|
148 |
have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" |
|
149 |
using uv yz |
|
150 |
using convex_on_dist [of "cball x e" x, unfolded convex_on_def, |
|
151 |
THEN bspec[where x=y], THEN bspec[where x=z]] |
|
152 |
by auto |
|
153 |
then have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e" |
|
154 |
using convex_bound_le[OF yz uv] by auto |
|
155 |
} |
|
156 |
then show ?thesis by (auto simp: convex_def Ball_def) |
|
157 |
qed |
|
158 |
||
159 |
lemma connected_ball [iff]: |
|
160 |
fixes x :: "'a::real_normed_vector" |
|
161 |
shows "connected (ball x e)" |
|
162 |
using convex_connected convex_ball by auto |
|
163 |
||
164 |
lemma connected_cball [iff]: |
|
165 |
fixes x :: "'a::real_normed_vector" |
|
166 |
shows "connected (cball x e)" |
|
167 |
using convex_connected convex_cball by auto |
|
168 |
||
169 |
lemma bounded_convex_hull: |
|
170 |
fixes s :: "'a::real_normed_vector set" |
|
171 |
assumes "bounded s" |
|
172 |
shows "bounded (convex hull s)" |
|
173 |
proof - |
|
174 |
from assms obtain B where B: "\<forall>x\<in>s. norm x \<le> B" |
|
175 |
unfolding bounded_iff by auto |
|
176 |
show ?thesis |
|
71169
df1d96114754
Fixed a few messy proofs and adjusted inconsistent section headings
paulson <lp15@cam.ac.uk>
parents:
71028
diff
changeset
|
177 |
by (simp add: bounded_subset[OF bounded_cball, of _ 0 B] B subsetI subset_hull) |
71028 | 178 |
qed |
179 |
||
180 |
lemma finite_imp_bounded_convex_hull: |
|
181 |
fixes s :: "'a::real_normed_vector set" |
|
182 |
shows "finite s \<Longrightarrow> bounded (convex hull s)" |
|
183 |
using bounded_convex_hull finite_imp_bounded |
|
184 |
by auto |
|
185 |
||
186 |
||
187 |
subsection \<open>Midpoint\<close> |
|
188 |
||
189 |
definition\<^marker>\<open>tag important\<close> midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a" |
|
190 |
where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)" |
|
191 |
||
192 |
lemma midpoint_idem [simp]: "midpoint x x = x" |
|
193 |
unfolding midpoint_def by simp |
|
194 |
||
195 |
lemma midpoint_sym: "midpoint a b = midpoint b a" |
|
196 |
unfolding midpoint_def by (auto simp add: scaleR_right_distrib) |
|
197 |
||
198 |
lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c" |
|
199 |
proof - |
|
200 |
have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c" |
|
201 |
by simp |
|
202 |
then show ?thesis |
|
203 |
unfolding midpoint_def scaleR_2 [symmetric] by simp |
|
204 |
qed |
|
205 |
||
206 |
lemma |
|
207 |
fixes a::real |
|
208 |
assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b" |
|
209 |
and le_midpoint_1: "midpoint a b \<le> b" |
|
210 |
by (simp_all add: midpoint_def assms) |
|
211 |
||
212 |
lemma dist_midpoint: |
|
213 |
fixes a b :: "'a::real_normed_vector" shows |
|
214 |
"dist a (midpoint a b) = (dist a b) / 2" (is ?t1) |
|
215 |
"dist b (midpoint a b) = (dist a b) / 2" (is ?t2) |
|
216 |
"dist (midpoint a b) a = (dist a b) / 2" (is ?t3) |
|
217 |
"dist (midpoint a b) b = (dist a b) / 2" (is ?t4) |
|
218 |
proof - |
|
219 |
have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2" |
|
220 |
unfolding equation_minus_iff by auto |
|
221 |
have **: "\<And>x y::'a. 2 *\<^sub>R x = y \<Longrightarrow> norm x = (norm y) / 2" |
|
222 |
by auto |
|
223 |
note scaleR_right_distrib [simp] |
|
224 |
show ?t1 |
|
225 |
unfolding midpoint_def dist_norm |
|
226 |
apply (rule **) |
|
227 |
apply (simp add: scaleR_right_diff_distrib) |
|
228 |
apply (simp add: scaleR_2) |
|
229 |
done |
|
230 |
show ?t2 |
|
231 |
unfolding midpoint_def dist_norm |
|
232 |
apply (rule *) |
|
233 |
apply (simp add: scaleR_right_diff_distrib) |
|
234 |
apply (simp add: scaleR_2) |
|
235 |
done |
|
236 |
show ?t3 |
|
237 |
unfolding midpoint_def dist_norm |
|
238 |
apply (rule *) |
|
239 |
apply (simp add: scaleR_right_diff_distrib) |
|
240 |
apply (simp add: scaleR_2) |
|
241 |
done |
|
242 |
show ?t4 |
|
243 |
unfolding midpoint_def dist_norm |
|
244 |
apply (rule **) |
|
245 |
apply (simp add: scaleR_right_diff_distrib) |
|
246 |
apply (simp add: scaleR_2) |
|
247 |
done |
|
248 |
qed |
|
249 |
||
250 |
lemma midpoint_eq_endpoint [simp]: |
|
251 |
"midpoint a b = a \<longleftrightarrow> a = b" |
|
252 |
"midpoint a b = b \<longleftrightarrow> a = b" |
|
253 |
unfolding midpoint_eq_iff by auto |
|
254 |
||
255 |
lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b" |
|
256 |
using midpoint_eq_iff by metis |
|
257 |
||
258 |
lemma midpoint_linear_image: |
|
259 |
"linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)" |
|
260 |
by (simp add: linear_iff midpoint_def) |
|
261 |
||
262 |
||
71169
df1d96114754
Fixed a few messy proofs and adjusted inconsistent section headings
paulson <lp15@cam.ac.uk>
parents:
71028
diff
changeset
|
263 |
subsection \<open>Open and closed segments\<close> |
71028 | 264 |
|
265 |
definition\<^marker>\<open>tag important\<close> closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" |
|
266 |
where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}" |
|
267 |
||
268 |
definition\<^marker>\<open>tag important\<close> open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where |
|
269 |
"open_segment a b \<equiv> closed_segment a b - {a,b}" |
|
270 |
||
271 |
lemmas segment = open_segment_def closed_segment_def |
|
272 |
||
273 |
lemma in_segment: |
|
274 |
"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)" |
|
275 |
"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)" |
|
276 |
using less_eq_real_def by (auto simp: segment algebra_simps) |
|
277 |
||
278 |
lemma closed_segment_linear_image: |
|
279 |
"closed_segment (f a) (f b) = f ` (closed_segment a b)" if "linear f" |
|
280 |
proof - |
|
281 |
interpret linear f by fact |
|
282 |
show ?thesis |
|
283 |
by (force simp add: in_segment add scale) |
|
284 |
qed |
|
285 |
||
286 |
lemma open_segment_linear_image: |
|
287 |
"\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> open_segment (f a) (f b) = f ` (open_segment a b)" |
|
288 |
by (force simp: open_segment_def closed_segment_linear_image inj_on_def) |
|
289 |
||
290 |
lemma closed_segment_translation: |
|
291 |
"closed_segment (c + a) (c + b) = image (\<lambda>x. c + x) (closed_segment a b)" |
|
292 |
apply safe |
|
293 |
apply (rule_tac x="x-c" in image_eqI) |
|
294 |
apply (auto simp: in_segment algebra_simps) |
|
295 |
done |
|
296 |
||
297 |
lemma open_segment_translation: |
|
298 |
"open_segment (c + a) (c + b) = image (\<lambda>x. c + x) (open_segment a b)" |
|
299 |
by (simp add: open_segment_def closed_segment_translation translation_diff) |
|
300 |
||
301 |
lemma closed_segment_of_real: |
|
302 |
"closed_segment (of_real x) (of_real y) = of_real ` closed_segment x y" |
|
303 |
apply (auto simp: image_iff in_segment scaleR_conv_of_real) |
|
304 |
apply (rule_tac x="(1-u)*x + u*y" in bexI) |
|
305 |
apply (auto simp: in_segment) |
|
306 |
done |
|
307 |
||
308 |
lemma open_segment_of_real: |
|
309 |
"open_segment (of_real x) (of_real y) = of_real ` open_segment x y" |
|
310 |
apply (auto simp: image_iff in_segment scaleR_conv_of_real) |
|
311 |
apply (rule_tac x="(1-u)*x + u*y" in bexI) |
|
312 |
apply (auto simp: in_segment) |
|
313 |
done |
|
314 |
||
315 |
lemma closed_segment_Reals: |
|
316 |
"\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> closed_segment x y = of_real ` closed_segment (Re x) (Re y)" |
|
317 |
by (metis closed_segment_of_real of_real_Re) |
|
318 |
||
319 |
lemma open_segment_Reals: |
|
320 |
"\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> open_segment x y = of_real ` open_segment (Re x) (Re y)" |
|
321 |
by (metis open_segment_of_real of_real_Re) |
|
322 |
||
323 |
lemma open_segment_PairD: |
|
324 |
"(x, x') \<in> open_segment (a, a') (b, b') |
|
325 |
\<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')" |
|
326 |
by (auto simp: in_segment) |
|
327 |
||
328 |
lemma closed_segment_PairD: |
|
329 |
"(x, x') \<in> closed_segment (a, a') (b, b') \<Longrightarrow> x \<in> closed_segment a b \<and> x' \<in> closed_segment a' b'" |
|
330 |
by (auto simp: closed_segment_def) |
|
331 |
||
332 |
lemma closed_segment_translation_eq [simp]: |
|
333 |
"d + x \<in> closed_segment (d + a) (d + b) \<longleftrightarrow> x \<in> closed_segment a b" |
|
334 |
proof - |
|
335 |
have *: "\<And>d x a b. x \<in> closed_segment a b \<Longrightarrow> d + x \<in> closed_segment (d + a) (d + b)" |
|
336 |
apply (simp add: closed_segment_def) |
|
337 |
apply (erule ex_forward) |
|
338 |
apply (simp add: algebra_simps) |
|
339 |
done |
|
340 |
show ?thesis |
|
341 |
using * [where d = "-d"] * |
|
342 |
by (fastforce simp add:) |
|
343 |
qed |
|
344 |
||
345 |
lemma open_segment_translation_eq [simp]: |
|
346 |
"d + x \<in> open_segment (d + a) (d + b) \<longleftrightarrow> x \<in> open_segment a b" |
|
347 |
by (simp add: open_segment_def) |
|
348 |
||
349 |
lemma of_real_closed_segment [simp]: |
|
350 |
"of_real x \<in> closed_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> closed_segment a b" |
|
351 |
apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward) |
|
352 |
using of_real_eq_iff by fastforce |
|
353 |
||
354 |
lemma of_real_open_segment [simp]: |
|
355 |
"of_real x \<in> open_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> open_segment a b" |
|
356 |
apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE) |
|
357 |
using of_real_eq_iff by fastforce |
|
358 |
||
359 |
lemma convex_contains_segment: |
|
360 |
"convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)" |
|
361 |
unfolding convex_alt closed_segment_def by auto |
|
362 |
||
363 |
lemma closed_segment_in_Reals: |
|
364 |
"\<lbrakk>x \<in> closed_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals" |
|
365 |
by (meson subsetD convex_Reals convex_contains_segment) |
|
366 |
||
367 |
lemma open_segment_in_Reals: |
|
368 |
"\<lbrakk>x \<in> open_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals" |
|
369 |
by (metis Diff_iff closed_segment_in_Reals open_segment_def) |
|
370 |
||
371 |
lemma closed_segment_subset: "\<lbrakk>x \<in> S; y \<in> S; convex S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> S" |
|
372 |
by (simp add: convex_contains_segment) |
|
373 |
||
374 |
lemma closed_segment_subset_convex_hull: |
|
375 |
"\<lbrakk>x \<in> convex hull S; y \<in> convex hull S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull S" |
|
376 |
using convex_contains_segment by blast |
|
377 |
||
378 |
lemma segment_convex_hull: |
|
379 |
"closed_segment a b = convex hull {a,b}" |
|
380 |
proof - |
|
381 |
have *: "\<And>x. {x} \<noteq> {}" by auto |
|
382 |
show ?thesis |
|
383 |
unfolding segment convex_hull_insert[OF *] convex_hull_singleton |
|
384 |
by (safe; rule_tac x="1 - u" in exI; force) |
|
385 |
qed |
|
386 |
||
387 |
lemma open_closed_segment: "u \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z" |
|
388 |
by (auto simp add: closed_segment_def open_segment_def) |
|
389 |
||
390 |
lemma segment_open_subset_closed: |
|
391 |
"open_segment a b \<subseteq> closed_segment a b" |
|
392 |
by (auto simp: closed_segment_def open_segment_def) |
|
393 |
||
394 |
lemma bounded_closed_segment: |
|
395 |
fixes a :: "'a::real_normed_vector" shows "bounded (closed_segment a b)" |
|
396 |
by (rule boundedI[where B="max (norm a) (norm b)"]) |
|
397 |
(auto simp: closed_segment_def max_def convex_bound_le intro!: norm_triangle_le) |
|
398 |
||
399 |
lemma bounded_open_segment: |
|
400 |
fixes a :: "'a::real_normed_vector" shows "bounded (open_segment a b)" |
|
401 |
by (rule bounded_subset [OF bounded_closed_segment segment_open_subset_closed]) |
|
402 |
||
403 |
lemmas bounded_segment = bounded_closed_segment open_closed_segment |
|
404 |
||
405 |
lemma ends_in_segment [iff]: "a \<in> closed_segment a b" "b \<in> closed_segment a b" |
|
406 |
unfolding segment_convex_hull |
|
407 |
by (auto intro!: hull_subset[unfolded subset_eq, rule_format]) |
|
408 |
||
409 |
||
410 |
lemma eventually_closed_segment: |
|
411 |
fixes x0::"'a::real_normed_vector" |
|
412 |
assumes "open X0" "x0 \<in> X0" |
|
413 |
shows "\<forall>\<^sub>F x in at x0 within U. closed_segment x0 x \<subseteq> X0" |
|
414 |
proof - |
|
415 |
from openE[OF assms] |
|
416 |
obtain e where e: "0 < e" "ball x0 e \<subseteq> X0" . |
|
417 |
then have "\<forall>\<^sub>F x in at x0 within U. x \<in> ball x0 e" |
|
418 |
by (auto simp: dist_commute eventually_at) |
|
419 |
then show ?thesis |
|
420 |
proof eventually_elim |
|
421 |
case (elim x) |
|
422 |
have "x0 \<in> ball x0 e" using \<open>e > 0\<close> by simp |
|
423 |
from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim] |
|
424 |
have "closed_segment x0 x \<subseteq> ball x0 e" . |
|
425 |
also note \<open>\<dots> \<subseteq> X0\<close> |
|
426 |
finally show ?case . |
|
427 |
qed |
|
428 |
qed |
|
429 |
||
430 |
lemma closed_segment_commute: "closed_segment a b = closed_segment b a" |
|
431 |
proof - |
|
432 |
have "{a, b} = {b, a}" by auto |
|
433 |
thus ?thesis |
|
434 |
by (simp add: segment_convex_hull) |
|
435 |
qed |
|
436 |
||
437 |
lemma segment_bound1: |
|
438 |
assumes "x \<in> closed_segment a b" |
|
439 |
shows "norm (x - a) \<le> norm (b - a)" |
|
440 |
proof - |
|
441 |
obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1" |
|
442 |
using assms by (auto simp add: closed_segment_def) |
|
443 |
then show "norm (x - a) \<le> norm (b - a)" |
|
444 |
apply clarify |
|
445 |
apply (auto simp: algebra_simps) |
|
446 |
apply (simp add: scaleR_diff_right [symmetric] mult_left_le_one_le) |
|
447 |
done |
|
448 |
qed |
|
449 |
||
450 |
lemma segment_bound: |
|
451 |
assumes "x \<in> closed_segment a b" |
|
452 |
shows "norm (x - a) \<le> norm (b - a)" "norm (x - b) \<le> norm (b - a)" |
|
71169
df1d96114754
Fixed a few messy proofs and adjusted inconsistent section headings
paulson <lp15@cam.ac.uk>
parents:
71028
diff
changeset
|
453 |
by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1)+ |
71028 | 454 |
|
455 |
lemma open_segment_commute: "open_segment a b = open_segment b a" |
|
456 |
proof - |
|
457 |
have "{a, b} = {b, a}" by auto |
|
458 |
thus ?thesis |
|
459 |
by (simp add: closed_segment_commute open_segment_def) |
|
460 |
qed |
|
461 |
||
462 |
lemma closed_segment_idem [simp]: "closed_segment a a = {a}" |
|
463 |
unfolding segment by (auto simp add: algebra_simps) |
|
464 |
||
465 |
lemma open_segment_idem [simp]: "open_segment a a = {}" |
|
466 |
by (simp add: open_segment_def) |
|
467 |
||
468 |
lemma closed_segment_eq_open: "closed_segment a b = open_segment a b \<union> {a,b}" |
|
469 |
using open_segment_def by auto |
|
470 |
||
471 |
lemma convex_contains_open_segment: |
|
472 |
"convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. open_segment a b \<subseteq> s)" |
|
473 |
by (simp add: convex_contains_segment closed_segment_eq_open) |
|
474 |
||
475 |
lemma closed_segment_eq_real_ivl1: |
|
476 |
fixes a b::real |
|
477 |
assumes "a \<le> b" |
|
478 |
shows "closed_segment a b = {a .. b}" |
|
479 |
proof safe |
|
480 |
fix x |
|
481 |
assume "x \<in> closed_segment a b" |
|
482 |
then obtain u where u: "0 \<le> u" "u \<le> 1" and x_def: "x = (1 - u) * a + u * b" |
|
483 |
by (auto simp: closed_segment_def) |
|
484 |
have "u * a \<le> u * b" "(1 - u) * a \<le> (1 - u) * b" |
|
485 |
by (auto intro!: mult_left_mono u assms) |
|
486 |
then show "x \<in> {a .. b}" |
|
487 |
unfolding x_def by (auto simp: algebra_simps) |
|
71169
df1d96114754
Fixed a few messy proofs and adjusted inconsistent section headings
paulson <lp15@cam.ac.uk>
parents:
71028
diff
changeset
|
488 |
next |
df1d96114754
Fixed a few messy proofs and adjusted inconsistent section headings
paulson <lp15@cam.ac.uk>
parents:
71028
diff
changeset
|
489 |
show "\<And>x. x \<in> {a..b} \<Longrightarrow> x \<in> closed_segment a b" |
df1d96114754
Fixed a few messy proofs and adjusted inconsistent section headings
paulson <lp15@cam.ac.uk>
parents:
71028
diff
changeset
|
490 |
by (force simp: closed_segment_def divide_simps algebra_simps |
df1d96114754
Fixed a few messy proofs and adjusted inconsistent section headings
paulson <lp15@cam.ac.uk>
parents:
71028
diff
changeset
|
491 |
intro: exI[where x="(x - a) / (b - a)" for x]) |
df1d96114754
Fixed a few messy proofs and adjusted inconsistent section headings
paulson <lp15@cam.ac.uk>
parents:
71028
diff
changeset
|
492 |
qed |
71028 | 493 |
|
494 |
lemma closed_segment_eq_real_ivl: |
|
495 |
fixes a b::real |
|
496 |
shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})" |
|
497 |
using closed_segment_eq_real_ivl1[of a b] closed_segment_eq_real_ivl1[of b a] |
|
498 |
by (auto simp: closed_segment_commute) |
|
499 |
||
500 |
lemma open_segment_eq_real_ivl: |
|
501 |
fixes a b::real |
|
502 |
shows "open_segment a b = (if a \<le> b then {a<..<b} else {b<..<a})" |
|
503 |
by (auto simp: closed_segment_eq_real_ivl open_segment_def split: if_split_asm) |
|
504 |
||
505 |
lemma closed_segment_real_eq: |
|
506 |
fixes u::real shows "closed_segment u v = (\<lambda>x. (v - u) * x + u) ` {0..1}" |
|
507 |
by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl) |
|
508 |
||
71189
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
509 |
lemma closed_segment_same_Re: |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
510 |
assumes "Re a = Re b" |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
511 |
shows "closed_segment a b = {z. Re z = Re a \<and> Im z \<in> closed_segment (Im a) (Im b)}" |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
512 |
proof safe |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
513 |
fix z assume "z \<in> closed_segment a b" |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
514 |
then obtain u where u: "u \<in> {0..1}" "z = a + of_real u * (b - a)" |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
515 |
by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps) |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
516 |
from assms show "Re z = Re a" by (auto simp: u) |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
517 |
from u(1) show "Im z \<in> closed_segment (Im a) (Im b)" |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
518 |
by (force simp: u closed_segment_def algebra_simps) |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
519 |
next |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
520 |
fix z assume [simp]: "Re z = Re a" and "Im z \<in> closed_segment (Im a) (Im b)" |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
521 |
then obtain u where u: "u \<in> {0..1}" "Im z = Im a + of_real u * (Im b - Im a)" |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
522 |
by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps) |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
523 |
from u(1) show "z \<in> closed_segment a b" using assms |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
524 |
by (force simp: u closed_segment_def algebra_simps scaleR_conv_of_real complex_eq_iff) |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
525 |
qed |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
526 |
|
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
527 |
lemma closed_segment_same_Im: |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
528 |
assumes "Im a = Im b" |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
529 |
shows "closed_segment a b = {z. Im z = Im a \<and> Re z \<in> closed_segment (Re a) (Re b)}" |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
530 |
proof safe |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
531 |
fix z assume "z \<in> closed_segment a b" |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
532 |
then obtain u where u: "u \<in> {0..1}" "z = a + of_real u * (b - a)" |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
533 |
by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps) |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
534 |
from assms show "Im z = Im a" by (auto simp: u) |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
535 |
from u(1) show "Re z \<in> closed_segment (Re a) (Re b)" |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
536 |
by (force simp: u closed_segment_def algebra_simps) |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
537 |
next |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
538 |
fix z assume [simp]: "Im z = Im a" and "Re z \<in> closed_segment (Re a) (Re b)" |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
539 |
then obtain u where u: "u \<in> {0..1}" "Re z = Re a + of_real u * (Re b - Re a)" |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
540 |
by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps) |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
541 |
from u(1) show "z \<in> closed_segment a b" using assms |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
542 |
by (force simp: u closed_segment_def algebra_simps scaleR_conv_of_real complex_eq_iff) |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
543 |
qed |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71169
diff
changeset
|
544 |
|
71028 | 545 |
lemma dist_in_closed_segment: |
546 |
fixes a :: "'a :: euclidean_space" |
|
547 |
assumes "x \<in> closed_segment a b" |
|
548 |
shows "dist x a \<le> dist a b \<and> dist x b \<le> dist a b" |
|
549 |
proof (intro conjI) |
|
550 |
obtain u where u: "0 \<le> u" "u \<le> 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" |
|
551 |
using assms by (force simp: in_segment algebra_simps) |
|
552 |
have "dist x a = u * dist a b" |
|
553 |
apply (simp add: dist_norm algebra_simps x) |
|
554 |
by (metis \<open>0 \<le> u\<close> abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib) |
|
555 |
also have "... \<le> dist a b" |
|
556 |
by (simp add: mult_left_le_one_le u) |
|
557 |
finally show "dist x a \<le> dist a b" . |
|
558 |
have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)" |
|
559 |
by (simp add: dist_norm algebra_simps x) |
|
560 |
also have "... = (1-u) * dist a b" |
|
561 |
proof - |
|
562 |
have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)" |
|
563 |
using \<open>u \<le> 1\<close> by force |
|
564 |
then show ?thesis |
|
565 |
by (simp add: dist_norm real_vector.scale_right_diff_distrib) |
|
566 |
qed |
|
567 |
also have "... \<le> dist a b" |
|
568 |
by (simp add: mult_left_le_one_le u) |
|
569 |
finally show "dist x b \<le> dist a b" . |
|
570 |
qed |
|
571 |
||
572 |
lemma dist_in_open_segment: |
|
573 |
fixes a :: "'a :: euclidean_space" |
|
574 |
assumes "x \<in> open_segment a b" |
|
575 |
shows "dist x a < dist a b \<and> dist x b < dist a b" |
|
576 |
proof (intro conjI) |
|
577 |
obtain u where u: "0 < u" "u < 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" |
|
578 |
using assms by (force simp: in_segment algebra_simps) |
|
579 |
have "dist x a = u * dist a b" |
|
580 |
apply (simp add: dist_norm algebra_simps x) |
|
581 |
by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib \<open>0 < u\<close>) |
|
582 |
also have *: "... < dist a b" |
|
72569
d56e4eeae967
mult_le_cancel_iff1, mult_le_cancel_iff2, mult_less_iff1 generalised from the real_ versions
paulson <lp15@cam.ac.uk>
parents:
71255
diff
changeset
|
583 |
using assms mult_less_cancel_right2 u(2) by fastforce |
71028 | 584 |
finally show "dist x a < dist a b" . |
585 |
have ab_ne0: "dist a b \<noteq> 0" |
|
586 |
using * by fastforce |
|
587 |
have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)" |
|
588 |
by (simp add: dist_norm algebra_simps x) |
|
589 |
also have "... = (1-u) * dist a b" |
|
590 |
proof - |
|
591 |
have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)" |
|
592 |
using \<open>u < 1\<close> by force |
|
593 |
then show ?thesis |
|
594 |
by (simp add: dist_norm real_vector.scale_right_diff_distrib) |
|
595 |
qed |
|
596 |
also have "... < dist a b" |
|
597 |
using ab_ne0 \<open>0 < u\<close> by simp |
|
598 |
finally show "dist x b < dist a b" . |
|
599 |
qed |
|
600 |
||
601 |
lemma dist_decreases_open_segment_0: |
|
602 |
fixes x :: "'a :: euclidean_space" |
|
603 |
assumes "x \<in> open_segment 0 b" |
|
604 |
shows "dist c x < dist c 0 \<or> dist c x < dist c b" |
|
605 |
proof (rule ccontr, clarsimp simp: not_less) |
|
606 |
obtain u where u: "0 \<noteq> b" "0 < u" "u < 1" and x: "x = u *\<^sub>R b" |
|
607 |
using assms by (auto simp: in_segment) |
|
608 |
have xb: "x \<bullet> b < b \<bullet> b" |
|
609 |
using u x by auto |
|
610 |
assume "norm c \<le> dist c x" |
|
611 |
then have "c \<bullet> c \<le> (c - x) \<bullet> (c - x)" |
|
612 |
by (simp add: dist_norm norm_le) |
|
613 |
moreover have "0 < x \<bullet> b" |
|
614 |
using u x by auto |
|
615 |
ultimately have less: "c \<bullet> b < x \<bullet> b" |
|
616 |
by (simp add: x algebra_simps inner_commute u) |
|
617 |
assume "dist c b \<le> dist c x" |
|
618 |
then have "(c - b) \<bullet> (c - b) \<le> (c - x) \<bullet> (c - x)" |
|
619 |
by (simp add: dist_norm norm_le) |
|
620 |
then have "(b \<bullet> b) * (1 - u*u) \<le> 2 * (b \<bullet> c) * (1-u)" |
|
621 |
by (simp add: x algebra_simps inner_commute) |
|
622 |
then have "(1+u) * (b \<bullet> b) * (1-u) \<le> 2 * (b \<bullet> c) * (1-u)" |
|
623 |
by (simp add: algebra_simps) |
|
624 |
then have "(1+u) * (b \<bullet> b) \<le> 2 * (b \<bullet> c)" |
|
625 |
using \<open>u < 1\<close> by auto |
|
626 |
with xb have "c \<bullet> b \<ge> x \<bullet> b" |
|
627 |
by (auto simp: x algebra_simps inner_commute) |
|
628 |
with less show False by auto |
|
629 |
qed |
|
630 |
||
631 |
proposition dist_decreases_open_segment: |
|
632 |
fixes a :: "'a :: euclidean_space" |
|
633 |
assumes "x \<in> open_segment a b" |
|
634 |
shows "dist c x < dist c a \<or> dist c x < dist c b" |
|
635 |
proof - |
|
636 |
have *: "x - a \<in> open_segment 0 (b - a)" using assms |
|
637 |
by (metis diff_self open_segment_translation_eq uminus_add_conv_diff) |
|
638 |
show ?thesis |
|
639 |
using dist_decreases_open_segment_0 [OF *, of "c-a"] assms |
|
640 |
by (simp add: dist_norm) |
|
641 |
qed |
|
642 |
||
643 |
corollary open_segment_furthest_le: |
|
644 |
fixes a b x y :: "'a::euclidean_space" |
|
645 |
assumes "x \<in> open_segment a b" |
|
646 |
shows "norm (y - x) < norm (y - a) \<or> norm (y - x) < norm (y - b)" |
|
647 |
by (metis assms dist_decreases_open_segment dist_norm) |
|
648 |
||
649 |
corollary dist_decreases_closed_segment: |
|
650 |
fixes a :: "'a :: euclidean_space" |
|
651 |
assumes "x \<in> closed_segment a b" |
|
652 |
shows "dist c x \<le> dist c a \<or> dist c x \<le> dist c b" |
|
653 |
apply (cases "x \<in> open_segment a b") |
|
654 |
using dist_decreases_open_segment less_eq_real_def apply blast |
|
655 |
by (metis DiffI assms empty_iff insertE open_segment_def order_refl) |
|
656 |
||
657 |
corollary segment_furthest_le: |
|
658 |
fixes a b x y :: "'a::euclidean_space" |
|
659 |
assumes "x \<in> closed_segment a b" |
|
660 |
shows "norm (y - x) \<le> norm (y - a) \<or> norm (y - x) \<le> norm (y - b)" |
|
661 |
by (metis assms dist_decreases_closed_segment dist_norm) |
|
662 |
||
663 |
lemma convex_intermediate_ball: |
|
664 |
fixes a :: "'a :: euclidean_space" |
|
665 |
shows "\<lbrakk>ball a r \<subseteq> T; T \<subseteq> cball a r\<rbrakk> \<Longrightarrow> convex T" |
|
666 |
apply (simp add: convex_contains_open_segment, clarify) |
|
667 |
by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment) |
|
668 |
||
669 |
lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b \<subseteq> closed_segment a b" |
|
670 |
apply (clarsimp simp: midpoint_def in_segment) |
|
671 |
apply (rule_tac x="(1 + u) / 2" in exI) |
|
672 |
apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib) |
|
673 |
by (metis field_sum_of_halves scaleR_left.add) |
|
674 |
||
675 |
lemma notin_segment_midpoint: |
|
676 |
fixes a :: "'a :: euclidean_space" |
|
677 |
shows "a \<noteq> b \<Longrightarrow> a \<notin> closed_segment (midpoint a b) b" |
|
678 |
by (auto simp: dist_midpoint dest!: dist_in_closed_segment) |
|
679 |
||
680 |
subsubsection\<open>More lemmas, especially for working with the underlying formula\<close> |
|
681 |
||
682 |
lemma segment_eq_compose: |
|
683 |
fixes a :: "'a :: real_vector" |
|
684 |
shows "(\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) = (\<lambda>x. a + x) o (\<lambda>u. u *\<^sub>R (b - a))" |
|
685 |
by (simp add: o_def algebra_simps) |
|
686 |
||
687 |
lemma segment_degen_1: |
|
688 |
fixes a :: "'a :: real_vector" |
|
689 |
shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = b \<longleftrightarrow> a=b \<or> u=1" |
|
690 |
proof - |
|
691 |
{ assume "(1 - u) *\<^sub>R a + u *\<^sub>R b = b" |
|
692 |
then have "(1 - u) *\<^sub>R a = (1 - u) *\<^sub>R b" |
|
693 |
by (simp add: algebra_simps) |
|
694 |
then have "a=b \<or> u=1" |
|
695 |
by simp |
|
696 |
} then show ?thesis |
|
697 |
by (auto simp: algebra_simps) |
|
698 |
qed |
|
699 |
||
700 |
lemma segment_degen_0: |
|
701 |
fixes a :: "'a :: real_vector" |
|
702 |
shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = a \<longleftrightarrow> a=b \<or> u=0" |
|
703 |
using segment_degen_1 [of "1-u" b a] |
|
704 |
by (auto simp: algebra_simps) |
|
705 |
||
706 |
lemma add_scaleR_degen: |
|
707 |
fixes a b ::"'a::real_vector" |
|
708 |
assumes "(u *\<^sub>R b + v *\<^sub>R a) = (u *\<^sub>R a + v *\<^sub>R b)" "u \<noteq> v" |
|
709 |
shows "a=b" |
|
710 |
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) |
|
711 |
||
712 |
lemma closed_segment_image_interval: |
|
713 |
"closed_segment a b = (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}" |
|
714 |
by (auto simp: set_eq_iff image_iff closed_segment_def) |
|
715 |
||
716 |
lemma open_segment_image_interval: |
|
717 |
"open_segment a b = (if a=b then {} else (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1})" |
|
718 |
by (auto simp: open_segment_def closed_segment_def segment_degen_0 segment_degen_1) |
|
719 |
||
720 |
lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval |
|
721 |
||
71230 | 722 |
lemma closed_segment_neq_empty [simp]: "closed_segment a b \<noteq> {}" |
723 |
by auto |
|
724 |
||
725 |
lemma open_segment_eq_empty [simp]: "open_segment a b = {} \<longleftrightarrow> a = b" |
|
726 |
proof - |
|
727 |
{ assume a1: "open_segment a b = {}" |
|
728 |
have "{} \<noteq> {0::real<..<1}" |
|
729 |
by simp |
|
730 |
then have "a = b" |
|
731 |
using a1 open_segment_image_interval by fastforce |
|
732 |
} then show ?thesis by auto |
|
733 |
qed |
|
734 |
||
735 |
lemma open_segment_eq_empty' [simp]: "{} = open_segment a b \<longleftrightarrow> a = b" |
|
736 |
using open_segment_eq_empty by blast |
|
737 |
||
738 |
lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty |
|
739 |
||
740 |
lemma inj_segment: |
|
741 |
fixes a :: "'a :: real_vector" |
|
742 |
assumes "a \<noteq> b" |
|
743 |
shows "inj_on (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) I" |
|
744 |
proof |
|
745 |
fix x y |
|
746 |
assume "(1 - x) *\<^sub>R a + x *\<^sub>R b = (1 - y) *\<^sub>R a + y *\<^sub>R b" |
|
747 |
then have "x *\<^sub>R (b - a) = y *\<^sub>R (b - a)" |
|
748 |
by (simp add: algebra_simps) |
|
749 |
with assms show "x = y" |
|
750 |
by (simp add: real_vector.scale_right_imp_eq) |
|
751 |
qed |
|
752 |
||
753 |
lemma finite_closed_segment [simp]: "finite(closed_segment a b) \<longleftrightarrow> a = b" |
|
754 |
apply auto |
|
755 |
apply (rule ccontr) |
|
756 |
apply (simp add: segment_image_interval) |
|
757 |
using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast |
|
758 |
done |
|
759 |
||
760 |
lemma finite_open_segment [simp]: "finite(open_segment a b) \<longleftrightarrow> a = b" |
|
761 |
by (auto simp: open_segment_def) |
|
762 |
||
763 |
lemmas finite_segment = finite_closed_segment finite_open_segment |
|
764 |
||
765 |
lemma closed_segment_eq_sing: "closed_segment a b = {c} \<longleftrightarrow> a = c \<and> b = c" |
|
766 |
by auto |
|
767 |
||
768 |
lemma open_segment_eq_sing: "open_segment a b \<noteq> {c}" |
|
769 |
by (metis finite_insert finite_open_segment insert_not_empty open_segment_image_interval) |
|
770 |
||
771 |
lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing |
|
772 |
||
71028 | 773 |
lemma open_segment_bound1: |
774 |
assumes "x \<in> open_segment a b" |
|
775 |
shows "norm (x - a) < norm (b - a)" |
|
776 |
proof - |
|
777 |
obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 < u" "u < 1" "a \<noteq> b" |
|
778 |
using assms by (auto simp add: open_segment_image_interval split: if_split_asm) |
|
779 |
then show "norm (x - a) < norm (b - a)" |
|
780 |
apply clarify |
|
781 |
apply (auto simp: algebra_simps) |
|
782 |
apply (simp add: scaleR_diff_right [symmetric]) |
|
783 |
done |
|
784 |
qed |
|
785 |
||
786 |
lemma compact_segment [simp]: |
|
787 |
fixes a :: "'a::real_normed_vector" |
|
788 |
shows "compact (closed_segment a b)" |
|
789 |
by (auto simp: segment_image_interval intro!: compact_continuous_image continuous_intros) |
|
790 |
||
791 |
lemma closed_segment [simp]: |
|
792 |
fixes a :: "'a::real_normed_vector" |
|
793 |
shows "closed (closed_segment a b)" |
|
794 |
by (simp add: compact_imp_closed) |
|
795 |
||
796 |
lemma closure_closed_segment [simp]: |
|
797 |
fixes a :: "'a::real_normed_vector" |
|
798 |
shows "closure(closed_segment a b) = closed_segment a b" |
|
799 |
by simp |
|
800 |
||
801 |
lemma open_segment_bound: |
|
802 |
assumes "x \<in> open_segment a b" |
|
803 |
shows "norm (x - a) < norm (b - a)" "norm (x - b) < norm (b - a)" |
|
804 |
apply (simp add: assms open_segment_bound1) |
|
805 |
by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute) |
|
806 |
||
807 |
lemma closure_open_segment [simp]: |
|
808 |
"closure (open_segment a b) = (if a = b then {} else closed_segment a b)" |
|
809 |
for a :: "'a::euclidean_space" |
|
810 |
proof (cases "a = b") |
|
811 |
case True |
|
812 |
then show ?thesis |
|
813 |
by simp |
|
814 |
next |
|
815 |
case False |
|
816 |
have "closure ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1}) = (\<lambda>u. u *\<^sub>R (b - a)) ` closure {0<..<1}" |
|
817 |
apply (rule closure_injective_linear_image [symmetric]) |
|
818 |
apply (use False in \<open>auto intro!: injI\<close>) |
|
819 |
done |
|
820 |
then have "closure |
|
821 |
((\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1}) = |
|
822 |
(\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b) ` closure {0<..<1}" |
|
823 |
using closure_translation [of a "((\<lambda>x. x *\<^sub>R b - x *\<^sub>R a) ` {0<..<1})"] |
|
824 |
by (simp add: segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right image_image) |
|
825 |
then show ?thesis |
|
826 |
by (simp add: segment_image_interval closure_greaterThanLessThan [symmetric] del: closure_greaterThanLessThan) |
|
827 |
qed |
|
828 |
||
829 |
lemma closed_open_segment_iff [simp]: |
|
830 |
fixes a :: "'a::euclidean_space" shows "closed(open_segment a b) \<longleftrightarrow> a = b" |
|
831 |
by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2)) |
|
832 |
||
833 |
lemma compact_open_segment_iff [simp]: |
|
834 |
fixes a :: "'a::euclidean_space" shows "compact(open_segment a b) \<longleftrightarrow> a = b" |
|
835 |
by (simp add: bounded_open_segment compact_eq_bounded_closed) |
|
836 |
||
837 |
lemma convex_closed_segment [iff]: "convex (closed_segment a b)" |
|
838 |
unfolding segment_convex_hull by(rule convex_convex_hull) |
|
839 |
||
840 |
lemma convex_open_segment [iff]: "convex (open_segment a b)" |
|
841 |
proof - |
|
842 |
have "convex ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})" |
|
843 |
by (rule convex_linear_image) auto |
|
844 |
then have "convex ((+) a ` (\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})" |
|
845 |
by (rule convex_translation) |
|
846 |
then show ?thesis |
|
847 |
by (simp add: image_image open_segment_image_interval segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right) |
|
848 |
qed |
|
849 |
||
850 |
lemmas convex_segment = convex_closed_segment convex_open_segment |
|
851 |
||
71230 | 852 |
lemma subset_closed_segment: |
853 |
"closed_segment a b \<subseteq> closed_segment c d \<longleftrightarrow> |
|
854 |
a \<in> closed_segment c d \<and> b \<in> closed_segment c d" |
|
855 |
by auto (meson contra_subsetD convex_closed_segment convex_contains_segment) |
|
856 |
||
857 |
lemma subset_co_segment: |
|
858 |
"closed_segment a b \<subseteq> open_segment c d \<longleftrightarrow> |
|
859 |
a \<in> open_segment c d \<and> b \<in> open_segment c d" |
|
860 |
using closed_segment_subset by blast |
|
861 |
||
862 |
lemma subset_open_segment: |
|
863 |
fixes a :: "'a::euclidean_space" |
|
864 |
shows "open_segment a b \<subseteq> open_segment c d \<longleftrightarrow> |
|
865 |
a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d" |
|
866 |
(is "?lhs = ?rhs") |
|
867 |
proof (cases "a = b") |
|
868 |
case True then show ?thesis by simp |
|
869 |
next |
|
870 |
case False show ?thesis |
|
871 |
proof |
|
872 |
assume rhs: ?rhs |
|
873 |
with \<open>a \<noteq> b\<close> have "c \<noteq> d" |
|
874 |
using closed_segment_idem singleton_iff by auto |
|
875 |
have "\<exists>uc. (1 - u) *\<^sub>R ((1 - ua) *\<^sub>R c + ua *\<^sub>R d) + u *\<^sub>R ((1 - ub) *\<^sub>R c + ub *\<^sub>R d) = |
|
876 |
(1 - uc) *\<^sub>R c + uc *\<^sub>R d \<and> 0 < uc \<and> uc < 1" |
|
877 |
if neq: "(1 - ua) *\<^sub>R c + ua *\<^sub>R d \<noteq> (1 - ub) *\<^sub>R c + ub *\<^sub>R d" "c \<noteq> d" |
|
878 |
and "a = (1 - ua) *\<^sub>R c + ua *\<^sub>R d" "b = (1 - ub) *\<^sub>R c + ub *\<^sub>R d" |
|
879 |
and u: "0 < u" "u < 1" and uab: "0 \<le> ua" "ua \<le> 1" "0 \<le> ub" "ub \<le> 1" |
|
880 |
for u ua ub |
|
881 |
proof - |
|
882 |
have "ua \<noteq> ub" |
|
883 |
using neq by auto |
|
884 |
moreover have "(u - 1) * ua \<le> 0" using u uab |
|
885 |
by (simp add: mult_nonpos_nonneg) |
|
886 |
ultimately have lt: "(u - 1) * ua < u * ub" using u uab |
|
887 |
by (metis antisym_conv diff_ge_0_iff_ge le_less_trans mult_eq_0_iff mult_le_0_iff not_less) |
|
888 |
have "p * ua + q * ub < p+q" if p: "0 < p" and q: "0 < q" for p q |
|
889 |
proof - |
|
890 |
have "\<not> p \<le> 0" "\<not> q \<le> 0" |
|
891 |
using p q not_less by blast+ |
|
892 |
then show ?thesis |
|
893 |
by (metis \<open>ua \<noteq> ub\<close> add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5) |
|
894 |
less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4)) |
|
895 |
qed |
|
896 |
then have "(1 - u) * ua + u * ub < 1" using u \<open>ua \<noteq> ub\<close> |
|
897 |
by (metis diff_add_cancel diff_gt_0_iff_gt) |
|
898 |
with lt show ?thesis |
|
899 |
by (rule_tac x="ua + u*(ub-ua)" in exI) (simp add: algebra_simps) |
|
900 |
qed |
|
901 |
with rhs \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close> show ?lhs |
|
902 |
unfolding open_segment_image_interval closed_segment_def |
|
903 |
by (fastforce simp add:) |
|
904 |
next |
|
905 |
assume lhs: ?lhs |
|
906 |
with \<open>a \<noteq> b\<close> have "c \<noteq> d" |
|
907 |
by (meson finite_open_segment rev_finite_subset) |
|
908 |
have "closure (open_segment a b) \<subseteq> closure (open_segment c d)" |
|
909 |
using lhs closure_mono by blast |
|
910 |
then have "closed_segment a b \<subseteq> closed_segment c d" |
|
911 |
by (simp add: \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close>) |
|
912 |
then show ?rhs |
|
913 |
by (force simp: \<open>a \<noteq> b\<close>) |
|
914 |
qed |
|
915 |
qed |
|
916 |
||
917 |
lemma subset_oc_segment: |
|
918 |
fixes a :: "'a::euclidean_space" |
|
919 |
shows "open_segment a b \<subseteq> closed_segment c d \<longleftrightarrow> |
|
920 |
a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d" |
|
921 |
apply (simp add: subset_open_segment [symmetric]) |
|
922 |
apply (rule iffI) |
|
923 |
apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment) |
|
924 |
apply (meson dual_order.trans segment_open_subset_closed) |
|
925 |
done |
|
926 |
||
927 |
lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment |
|
928 |
||
929 |
lemma dist_half_times2: |
|
930 |
fixes a :: "'a :: real_normed_vector" |
|
931 |
shows "dist ((1 / 2) *\<^sub>R (a + b)) x * 2 = dist (a+b) (2 *\<^sub>R x)" |
|
932 |
proof - |
|
933 |
have "norm ((1 / 2) *\<^sub>R (a + b) - x) * 2 = norm (2 *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x))" |
|
934 |
by simp |
|
935 |
also have "... = norm ((a + b) - 2 *\<^sub>R x)" |
|
936 |
by (simp add: real_vector.scale_right_diff_distrib) |
|
937 |
finally show ?thesis |
|
938 |
by (simp only: dist_norm) |
|
939 |
qed |
|
940 |
||
941 |
lemma closed_segment_as_ball: |
|
942 |
"closed_segment a b = affine hull {a,b} \<inter> cball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)" |
|
943 |
proof (cases "b = a") |
|
944 |
case True then show ?thesis by (auto simp: hull_inc) |
|
945 |
next |
|
946 |
case False |
|
947 |
then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and> |
|
948 |
dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) = |
|
949 |
(\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)" for x |
|
950 |
proof - |
|
951 |
have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and> |
|
952 |
dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) = |
|
953 |
((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and> |
|
954 |
dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a))" |
|
955 |
unfolding eq_diff_eq [symmetric] by simp |
|
956 |
also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> |
|
957 |
norm ((a+b) - (2 *\<^sub>R x)) \<le> norm (b - a))" |
|
958 |
by (simp add: dist_half_times2) (simp add: dist_norm) |
|
959 |
also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> |
|
960 |
norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) \<le> norm (b - a))" |
|
961 |
by auto |
|
962 |
also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> |
|
963 |
norm ((1 - u * 2) *\<^sub>R (b - a)) \<le> norm (b - a))" |
|
964 |
by (simp add: algebra_simps scaleR_2) |
|
965 |
also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> |
|
966 |
\<bar>1 - u * 2\<bar> * norm (b - a) \<le> norm (b - a))" |
|
967 |
by simp |
|
968 |
also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> \<le> 1)" |
|
969 |
by (simp add: mult_le_cancel_right2 False) |
|
970 |
also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)" |
|
971 |
by auto |
|
972 |
finally show ?thesis . |
|
973 |
qed |
|
974 |
show ?thesis |
|
975 |
by (simp add: affine_hull_2 Set.set_eq_iff closed_segment_def *) |
|
976 |
qed |
|
977 |
||
978 |
lemma open_segment_as_ball: |
|
979 |
"open_segment a b = |
|
980 |
affine hull {a,b} \<inter> ball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)" |
|
981 |
proof (cases "b = a") |
|
982 |
case True then show ?thesis by (auto simp: hull_inc) |
|
983 |
next |
|
984 |
case False |
|
985 |
then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and> |
|
986 |
dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) = |
|
987 |
(\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)" for x |
|
988 |
proof - |
|
989 |
have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and> |
|
990 |
dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) = |
|
991 |
((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and> |
|
992 |
dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a))" |
|
993 |
unfolding eq_diff_eq [symmetric] by simp |
|
994 |
also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> |
|
995 |
norm ((a+b) - (2 *\<^sub>R x)) < norm (b - a))" |
|
996 |
by (simp add: dist_half_times2) (simp add: dist_norm) |
|
997 |
also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> |
|
998 |
norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) < norm (b - a))" |
|
999 |
by auto |
|
1000 |
also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> |
|
1001 |
norm ((1 - u * 2) *\<^sub>R (b - a)) < norm (b - a))" |
|
1002 |
by (simp add: algebra_simps scaleR_2) |
|
1003 |
also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> |
|
1004 |
\<bar>1 - u * 2\<bar> * norm (b - a) < norm (b - a))" |
|
1005 |
by simp |
|
1006 |
also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> < 1)" |
|
1007 |
by (simp add: mult_le_cancel_right2 False) |
|
1008 |
also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)" |
|
1009 |
by auto |
|
1010 |
finally show ?thesis . |
|
1011 |
qed |
|
1012 |
show ?thesis |
|
1013 |
using False by (force simp: affine_hull_2 Set.set_eq_iff open_segment_image_interval *) |
|
1014 |
qed |
|
1015 |
||
1016 |
lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball |
|
1017 |
||
71028 | 1018 |
lemma connected_segment [iff]: |
1019 |
fixes x :: "'a :: real_normed_vector" |
|
1020 |
shows "connected (closed_segment x y)" |
|
1021 |
by (simp add: convex_connected) |
|
1022 |
||
1023 |
lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real |
|
1024 |
unfolding closed_segment_eq_real_ivl |
|
1025 |
by (auto simp: is_interval_def) |
|
1026 |
||
1027 |
lemma IVT'_closed_segment_real: |
|
1028 |
fixes f :: "real \<Rightarrow> real" |
|
1029 |
assumes "y \<in> closed_segment (f a) (f b)" |
|
1030 |
assumes "continuous_on (closed_segment a b) f" |
|
1031 |
shows "\<exists>x \<in> closed_segment a b. f x = y" |
|
1032 |
using IVT'[of f a y b] |
|
1033 |
IVT'[of "-f" a "-y" b] |
|
1034 |
IVT'[of f b y a] |
|
1035 |
IVT'[of "-f" b "-y" a] assms |
|
1036 |
by (cases "a \<le> b"; cases "f b \<ge> f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus) |
|
1037 |
||
1038 |
subsection \<open>Betweenness\<close> |
|
1039 |
||
1040 |
definition\<^marker>\<open>tag important\<close> "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)" |
|
1041 |
||
1042 |
lemma betweenI: |
|
1043 |
assumes "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" |
|
1044 |
shows "between (a, b) x" |
|
1045 |
using assms unfolding between_def closed_segment_def by auto |
|
1046 |
||
1047 |
lemma betweenE: |
|
1048 |
assumes "between (a, b) x" |
|
1049 |
obtains u where "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" |
|
1050 |
using assms unfolding between_def closed_segment_def by auto |
|
1051 |
||
1052 |
lemma between_implies_scaled_diff: |
|
1053 |
assumes "between (S, T) X" "between (S, T) Y" "S \<noteq> Y" |
|
1054 |
obtains c where "(X - Y) = c *\<^sub>R (S - Y)" |
|
1055 |
proof - |
|
1056 |
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" |
|
1057 |
by (metis add.commute betweenE eq_diff_eq) |
|
1058 |
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" |
|
1059 |
by (metis add.commute betweenE eq_diff_eq) |
|
1060 |
have "X - Y = (u\<^sub>X - u\<^sub>Y) *\<^sub>R (S - T)" |
|
1061 |
proof - |
|
1062 |
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 |
|
1063 |
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) |
|
1064 |
finally show ?thesis by (simp add: real_vector.scale_right_diff_distrib) |
|
1065 |
qed |
|
1066 |
moreover from Y have "S - Y = (1 - u\<^sub>Y) *\<^sub>R (S - T)" |
|
1067 |
by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib) |
|
1068 |
moreover note \<open>S \<noteq> Y\<close> |
|
1069 |
ultimately have "(X - Y) = ((u\<^sub>X - u\<^sub>Y) / (1 - u\<^sub>Y)) *\<^sub>R (S - Y)" by auto |
|
1070 |
from this that show thesis by blast |
|
1071 |
qed |
|
1072 |
||
1073 |
lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b" |
|
1074 |
unfolding between_def by auto |
|
1075 |
||
1076 |
lemma between: "between (a, b) (x::'a::euclidean_space) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)" |
|
1077 |
proof (cases "a = b") |
|
1078 |
case True |
|
1079 |
then show ?thesis |
|
1080 |
by (auto simp add: between_def dist_commute) |
|
1081 |
next |
|
1082 |
case False |
|
1083 |
then have Fal: "norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0" |
|
1084 |
by auto |
|
1085 |
have *: "\<And>u. a - ((1 - u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)" |
|
1086 |
by (auto simp add: algebra_simps) |
|
1087 |
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 |
|
1088 |
proof - |
|
1089 |
have *: "a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)" |
|
1090 |
unfolding that(1) by (auto simp add:algebra_simps) |
|
1091 |
show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)" |
|
1092 |
unfolding norm_minus_commute[of x a] * using \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> |
|
1093 |
by simp |
|
1094 |
qed |
|
1095 |
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" |
|
1096 |
proof - |
|
1097 |
let ?\<beta> = "norm (a - x) / norm (a - b)" |
|
1098 |
show "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" |
|
1099 |
proof (intro exI conjI) |
|
1100 |
show "?\<beta> \<le> 1" |
|
1101 |
using Fal2 unfolding that[unfolded dist_norm] norm_ge_zero by auto |
|
1102 |
show "x = (1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b" |
|
1103 |
proof (subst euclidean_eq_iff; intro ballI) |
|
1104 |
fix i :: 'a |
|
1105 |
assume i: "i \<in> Basis" |
|
1106 |
have "((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> i |
|
1107 |
= ((norm (a - b) - norm (a - x)) * (a \<bullet> i) + norm (a - x) * (b \<bullet> i)) / norm (a - b)" |
|
1108 |
using Fal by (auto simp add: field_simps inner_simps) |
|
1109 |
also have "\<dots> = x\<bullet>i" |
|
1110 |
apply (rule divide_eq_imp[OF Fal]) |
|
1111 |
unfolding that[unfolded dist_norm] |
|
1112 |
using that[unfolded dist_triangle_eq] i |
|
1113 |
apply (subst (asm) euclidean_eq_iff) |
|
1114 |
apply (auto simp add: field_simps inner_simps) |
|
1115 |
done |
|
1116 |
finally show "x \<bullet> i = ((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> i" |
|
1117 |
by auto |
|
1118 |
qed |
|
1119 |
qed (use Fal2 in auto) |
|
1120 |
qed |
|
1121 |
ultimately show ?thesis |
|
1122 |
by (force simp add: between_def closed_segment_def dist_triangle_eq) |
|
1123 |
qed |
|
1124 |
||
1125 |
lemma between_midpoint: |
|
1126 |
fixes a :: "'a::euclidean_space" |
|
1127 |
shows "between (a,b) (midpoint a b)" (is ?t1) |
|
1128 |
and "between (b,a) (midpoint a b)" (is ?t2) |
|
1129 |
proof - |
|
1130 |
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" |
|
1131 |
by auto |
|
1132 |
show ?t1 ?t2 |
|
1133 |
unfolding between midpoint_def dist_norm |
|
1134 |
by (auto simp add: field_simps inner_simps euclidean_eq_iff[where 'a='a] intro!: *) |
|
1135 |
qed |
|
1136 |
||
1137 |
lemma between_mem_convex_hull: |
|
1138 |
"between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}" |
|
1139 |
unfolding between_mem_segment segment_convex_hull .. |
|
1140 |
||
1141 |
lemma between_triv_iff [simp]: "between (a,a) b \<longleftrightarrow> a=b" |
|
1142 |
by (auto simp: between_def) |
|
1143 |
||
1144 |
lemma between_triv1 [simp]: "between (a,b) a" |
|
1145 |
by (auto simp: between_def) |
|
1146 |
||
1147 |
lemma between_triv2 [simp]: "between (a,b) b" |
|
1148 |
by (auto simp: between_def) |
|
1149 |
||
1150 |
lemma between_commute: |
|
1151 |
"between (a,b) = between (b,a)" |
|
1152 |
by (auto simp: between_def closed_segment_commute) |
|
1153 |
||
1154 |
lemma between_antisym: |
|
1155 |
fixes a :: "'a :: euclidean_space" |
|
1156 |
shows "\<lbrakk>between (b,c) a; between (a,c) b\<rbrakk> \<Longrightarrow> a = b" |
|
1157 |
by (auto simp: between dist_commute) |
|
1158 |
||
1159 |
lemma between_trans: |
|
1160 |
fixes a :: "'a :: euclidean_space" |
|
1161 |
shows "\<lbrakk>between (b,c) a; between (a,c) d\<rbrakk> \<Longrightarrow> between (b,c) d" |
|
1162 |
using dist_triangle2 [of b c d] dist_triangle3 [of b d a] |
|
1163 |
by (auto simp: between dist_commute) |
|
1164 |
||
1165 |
lemma between_norm: |
|
1166 |
fixes a :: "'a :: euclidean_space" |
|
1167 |
shows "between (a,b) x \<longleftrightarrow> norm(x - a) *\<^sub>R (b - x) = norm(b - x) *\<^sub>R (x - a)" |
|
1168 |
by (auto simp: between dist_triangle_eq norm_minus_commute algebra_simps) |
|
1169 |
||
1170 |
lemma between_swap: |
|
1171 |
fixes A B X Y :: "'a::euclidean_space" |
|
1172 |
assumes "between (A, B) X" |
|
1173 |
assumes "between (A, B) Y" |
|
1174 |
shows "between (X, B) Y \<longleftrightarrow> between (A, Y) X" |
|
1175 |
using assms by (auto simp add: between) |
|
1176 |
||
1177 |
lemma between_translation [simp]: "between (a + y,a + z) (a + x) \<longleftrightarrow> between (y,z) x" |
|
1178 |
by (auto simp: between_def) |
|
1179 |
||
1180 |
lemma between_trans_2: |
|
1181 |
fixes a :: "'a :: euclidean_space" |
|
1182 |
shows "\<lbrakk>between (b,c) a; between (a,b) d\<rbrakk> \<Longrightarrow> between (c,d) a" |
|
1183 |
by (metis between_commute between_swap between_trans) |
|
1184 |
||
1185 |
lemma between_scaleR_lift [simp]: |
|
1186 |
fixes v :: "'a::euclidean_space" |
|
1187 |
shows "between (a *\<^sub>R v, b *\<^sub>R v) (c *\<^sub>R v) \<longleftrightarrow> v = 0 \<or> between (a, b) c" |
|
1188 |
by (simp add: between dist_norm scaleR_left_diff_distrib [symmetric] distrib_right [symmetric]) |
|
1189 |
||
1190 |
lemma between_1: |
|
1191 |
fixes x::real |
|
1192 |
shows "between (a,b) x \<longleftrightarrow> (a \<le> x \<and> x \<le> b) \<or> (b \<le> x \<and> x \<le> a)" |
|
1193 |
by (auto simp: between_mem_segment closed_segment_eq_real_ivl) |
|
1194 |
||
1195 |
end |