author  paulson <lp15@cam.ac.uk> 
Thu, 05 Oct 2017 15:35:24 +0100  
changeset 66765  c1dfa973b269 
parent 66641  ff2e0115fea4 
child 66793  deabce3ccf1f 
permissions  rwrr 
66289
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1 
(* Title: HOL/Analysis/Starlike.thy 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

2 
Author: L C Paulson, University of Cambridge 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

3 
Author: Robert Himmelmann, TU Muenchen 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

4 
Author: Bogdan Grechuk, University of Edinburgh 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

5 
Author: Armin Heller, TU Muenchen 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

6 
Author: Johannes Hoelzl, TU Muenchen 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

7 
*) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

8 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

9 
section \<open>Line segments, Starlike Sets, etc.\<close> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

10 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

11 
theory Starlike 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

12 
imports Convex_Euclidean_Space 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

13 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

14 
begin 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

15 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

16 
definition midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

17 
where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

18 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

19 
definition closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

20 
where "closed_segment a b = {(1  u) *\<^sub>R a + u *\<^sub>R b  u::real. 0 \<le> u \<and> u \<le> 1}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

21 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

22 
definition open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

23 
"open_segment a b \<equiv> closed_segment a b  {a,b}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

24 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

25 
lemmas segment = open_segment_def closed_segment_def 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

26 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

27 
lemma in_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

28 
"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)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

29 
"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)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

30 
using less_eq_real_def by (auto simp: segment algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

31 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

32 
lemma closed_segment_linear_image: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

33 
"linear f \<Longrightarrow> closed_segment (f a) (f b) = f ` (closed_segment a b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

34 
by (force simp add: in_segment linear_add_cmul) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

35 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

36 
lemma open_segment_linear_image: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

37 
"\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> open_segment (f a) (f b) = f ` (open_segment a b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

38 
by (force simp: open_segment_def closed_segment_linear_image inj_on_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

39 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

40 
lemma closed_segment_translation: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

41 
"closed_segment (c + a) (c + b) = image (\<lambda>x. c + x) (closed_segment a b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

42 
apply safe 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

43 
apply (rule_tac x="xc" in image_eqI) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

44 
apply (auto simp: in_segment algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

45 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

46 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

47 
lemma open_segment_translation: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

48 
"open_segment (c + a) (c + b) = image (\<lambda>x. c + x) (open_segment a b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

49 
by (simp add: open_segment_def closed_segment_translation translation_diff) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

50 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

51 
lemma closed_segment_of_real: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

52 
"closed_segment (of_real x) (of_real y) = of_real ` closed_segment x y" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

53 
apply (auto simp: image_iff in_segment scaleR_conv_of_real) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

54 
apply (rule_tac x="(1u)*x + u*y" in bexI) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

55 
apply (auto simp: in_segment) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

56 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

57 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

58 
lemma open_segment_of_real: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

59 
"open_segment (of_real x) (of_real y) = of_real ` open_segment x y" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

60 
apply (auto simp: image_iff in_segment scaleR_conv_of_real) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

61 
apply (rule_tac x="(1u)*x + u*y" in bexI) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

62 
apply (auto simp: in_segment) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

63 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

64 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

65 
lemma closed_segment_Reals: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

66 
"\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> closed_segment x y = of_real ` closed_segment (Re x) (Re y)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

67 
by (metis closed_segment_of_real of_real_Re) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

68 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

69 
lemma open_segment_Reals: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

70 
"\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> open_segment x y = of_real ` open_segment (Re x) (Re y)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

71 
by (metis open_segment_of_real of_real_Re) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

72 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

73 
lemma open_segment_PairD: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

74 
"(x, x') \<in> open_segment (a, a') (b, b') 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

75 
\<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

76 
by (auto simp: in_segment) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

77 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

78 
lemma closed_segment_PairD: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

79 
"(x, x') \<in> closed_segment (a, a') (b, b') \<Longrightarrow> x \<in> closed_segment a b \<and> x' \<in> closed_segment a' b'" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

80 
by (auto simp: closed_segment_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

81 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

82 
lemma closed_segment_translation_eq [simp]: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

83 
"d + x \<in> closed_segment (d + a) (d + b) \<longleftrightarrow> x \<in> closed_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

84 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

85 
have *: "\<And>d x a b. x \<in> closed_segment a b \<Longrightarrow> d + x \<in> closed_segment (d + a) (d + b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

86 
apply (simp add: closed_segment_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

87 
apply (erule ex_forward) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

88 
apply (simp add: algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

89 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

90 
show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

91 
using * [where d = "d"] * 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

92 
by (fastforce simp add:) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

93 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

94 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

95 
lemma open_segment_translation_eq [simp]: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

96 
"d + x \<in> open_segment (d + a) (d + b) \<longleftrightarrow> x \<in> open_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

97 
by (simp add: open_segment_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

98 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

99 
lemma of_real_closed_segment [simp]: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

100 
"of_real x \<in> closed_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> closed_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

101 
apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

102 
using of_real_eq_iff by fastforce 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

103 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

104 
lemma of_real_open_segment [simp]: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

105 
"of_real x \<in> open_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> open_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

106 
apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

107 
using of_real_eq_iff by fastforce 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

108 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

109 
lemma midpoint_idem [simp]: "midpoint x x = x" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

110 
unfolding midpoint_def 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

111 
unfolding scaleR_right_distrib 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

112 
unfolding scaleR_left_distrib[symmetric] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

113 
by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

114 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

115 
lemma midpoint_sym: "midpoint a b = midpoint b a" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

116 
unfolding midpoint_def by (auto simp add: scaleR_right_distrib) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

117 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

118 
lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

119 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

120 
have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

121 
by simp 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

122 
then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

123 
unfolding midpoint_def scaleR_2 [symmetric] by simp 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

124 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

125 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

126 
lemma 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

127 
fixes a::real 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

128 
assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

129 
and le_midpoint_1: "midpoint a b \<le> b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

130 
by (simp_all add: midpoint_def assms) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

131 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

132 
lemma dist_midpoint: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

133 
fixes a b :: "'a::real_normed_vector" shows 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

134 
"dist a (midpoint a b) = (dist a b) / 2" (is ?t1) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

135 
"dist b (midpoint a b) = (dist a b) / 2" (is ?t2) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

136 
"dist (midpoint a b) a = (dist a b) / 2" (is ?t3) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

137 
"dist (midpoint a b) b = (dist a b) / 2" (is ?t4) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

138 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

139 
have *: "\<And>x y::'a. 2 *\<^sub>R x =  y \<Longrightarrow> norm x = (norm y) / 2" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

140 
unfolding equation_minus_iff by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

141 
have **: "\<And>x y::'a. 2 *\<^sub>R x = y \<Longrightarrow> norm x = (norm y) / 2" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

142 
by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

143 
note scaleR_right_distrib [simp] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

144 
show ?t1 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

145 
unfolding midpoint_def dist_norm 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

146 
apply (rule **) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

147 
apply (simp add: scaleR_right_diff_distrib) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

148 
apply (simp add: scaleR_2) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

149 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

150 
show ?t2 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

151 
unfolding midpoint_def dist_norm 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

152 
apply (rule *) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

153 
apply (simp add: scaleR_right_diff_distrib) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

154 
apply (simp add: scaleR_2) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

155 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

156 
show ?t3 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

157 
unfolding midpoint_def dist_norm 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

158 
apply (rule *) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

159 
apply (simp add: scaleR_right_diff_distrib) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

160 
apply (simp add: scaleR_2) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

161 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

162 
show ?t4 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

163 
unfolding midpoint_def dist_norm 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

164 
apply (rule **) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

165 
apply (simp add: scaleR_right_diff_distrib) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

166 
apply (simp add: scaleR_2) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

167 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

168 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

169 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

170 
lemma midpoint_eq_endpoint [simp]: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

171 
"midpoint a b = a \<longleftrightarrow> a = b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

172 
"midpoint a b = b \<longleftrightarrow> a = b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

173 
unfolding midpoint_eq_iff by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

174 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

175 
lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

176 
using midpoint_eq_iff by metis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

177 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

178 
lemma midpoint_linear_image: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

179 
"linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

180 
by (simp add: linear_iff midpoint_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

181 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

182 
subsection\<open>Starlike sets\<close> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

183 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

184 
definition "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

185 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

186 
lemma starlike_UNIV [simp]: "starlike UNIV" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

187 
by (simp add: starlike_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

188 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

189 
lemma convex_contains_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

190 
"convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

191 
unfolding convex_alt closed_segment_def by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

192 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

193 
lemma closed_segment_subset: "\<lbrakk>x \<in> S; y \<in> S; convex S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> S" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

194 
by (simp add: convex_contains_segment) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

195 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

196 
lemma closed_segment_subset_convex_hull: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

197 
"\<lbrakk>x \<in> convex hull S; y \<in> convex hull S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull S" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

198 
using convex_contains_segment by blast 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

199 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

200 
lemma convex_imp_starlike: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

201 
"convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

202 
unfolding convex_contains_segment starlike_def by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

203 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

204 
lemma segment_convex_hull: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

205 
"closed_segment a b = convex hull {a,b}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

206 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

207 
have *: "\<And>x. {x} \<noteq> {}" by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

208 
show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

209 
unfolding segment convex_hull_insert[OF *] convex_hull_singleton 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

210 
by (safe; rule_tac x="1  u" in exI; force) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

211 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

212 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

213 
lemma open_closed_segment: "u \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

214 
by (auto simp add: closed_segment_def open_segment_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

215 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

216 
lemma segment_open_subset_closed: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

217 
"open_segment a b \<subseteq> closed_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

218 
by (auto simp: closed_segment_def open_segment_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

219 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

220 
lemma bounded_closed_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

221 
fixes a :: "'a::euclidean_space" shows "bounded (closed_segment a b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

222 
by (simp add: segment_convex_hull compact_convex_hull compact_imp_bounded) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

223 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

224 
lemma bounded_open_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

225 
fixes a :: "'a::euclidean_space" shows "bounded (open_segment a b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

226 
by (rule bounded_subset [OF bounded_closed_segment segment_open_subset_closed]) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

227 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

228 
lemmas bounded_segment = bounded_closed_segment open_closed_segment 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

229 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

230 
lemma ends_in_segment [iff]: "a \<in> closed_segment a b" "b \<in> closed_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

231 
unfolding segment_convex_hull 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

232 
by (auto intro!: hull_subset[unfolded subset_eq, rule_format]) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

233 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

234 
lemma eventually_closed_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

235 
fixes x0::"'a::real_normed_vector" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

236 
assumes "open X0" "x0 \<in> X0" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

237 
shows "\<forall>\<^sub>F x in at x0 within U. closed_segment x0 x \<subseteq> X0" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

238 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

239 
from openE[OF assms] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

240 
obtain e where e: "0 < e" "ball x0 e \<subseteq> X0" . 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

241 
then have "\<forall>\<^sub>F x in at x0 within U. x \<in> ball x0 e" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

242 
by (auto simp: dist_commute eventually_at) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

243 
then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

244 
proof eventually_elim 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

245 
case (elim x) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

246 
have "x0 \<in> ball x0 e" using \<open>e > 0\<close> by simp 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

247 
from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

248 
have "closed_segment x0 x \<subseteq> ball x0 e" . 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

249 
also note \<open>\<dots> \<subseteq> X0\<close> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

250 
finally show ?case . 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

251 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

252 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

253 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

254 
lemma segment_furthest_le: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

255 
fixes a b x y :: "'a::euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

256 
assumes "x \<in> closed_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

257 
shows "norm (y  x) \<le> norm (y  a) \<or> norm (y  x) \<le> norm (y  b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

258 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

259 
obtain z where "z \<in> {a, b}" "norm (x  y) \<le> norm (z  y)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

260 
using simplex_furthest_le[of "{a, b}" y] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

261 
using assms[unfolded segment_convex_hull] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

262 
by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

263 
then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

264 
by (auto simp add:norm_minus_commute) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

265 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

266 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

267 
lemma closed_segment_commute: "closed_segment a b = closed_segment b a" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

268 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

269 
have "{a, b} = {b, a}" by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

270 
thus ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

271 
by (simp add: segment_convex_hull) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

272 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

273 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

274 
lemma segment_bound1: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

275 
assumes "x \<in> closed_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

276 
shows "norm (x  a) \<le> norm (b  a)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

277 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

278 
obtain u where "x = (1  u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

279 
using assms by (auto simp add: closed_segment_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

280 
then show "norm (x  a) \<le> norm (b  a)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

281 
apply clarify 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

282 
apply (auto simp: algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

283 
apply (simp add: scaleR_diff_right [symmetric] mult_left_le_one_le) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

284 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

285 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

286 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

287 
lemma segment_bound: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

288 
assumes "x \<in> closed_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

289 
shows "norm (x  a) \<le> norm (b  a)" "norm (x  b) \<le> norm (b  a)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

290 
apply (simp add: assms segment_bound1) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

291 
by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

292 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

293 
lemma open_segment_commute: "open_segment a b = open_segment b a" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

294 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

295 
have "{a, b} = {b, a}" by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

296 
thus ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

297 
by (simp add: closed_segment_commute open_segment_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

298 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

299 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

300 
lemma closed_segment_idem [simp]: "closed_segment a a = {a}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

301 
unfolding segment by (auto simp add: algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

302 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

303 
lemma open_segment_idem [simp]: "open_segment a a = {}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

304 
by (simp add: open_segment_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

305 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

306 
lemma closed_segment_eq_open: "closed_segment a b = open_segment a b \<union> {a,b}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

307 
using open_segment_def by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

308 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

309 
lemma convex_contains_open_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

310 
"convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. open_segment a b \<subseteq> s)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

311 
by (simp add: convex_contains_segment closed_segment_eq_open) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

312 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

313 
lemma closed_segment_eq_real_ivl: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

314 
fixes a b::real 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

315 
shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

316 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

317 
have "b \<le> a \<Longrightarrow> closed_segment b a = {b .. a}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

318 
and "a \<le> b \<Longrightarrow> closed_segment a b = {a .. b}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

319 
by (auto simp: convex_hull_eq_real_cbox segment_convex_hull) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

320 
thus ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

321 
by (auto simp: closed_segment_commute) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

322 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

323 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

324 
lemma open_segment_eq_real_ivl: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

325 
fixes a b::real 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

326 
shows "open_segment a b = (if a \<le> b then {a<..<b} else {b<..<a})" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

327 
by (auto simp: closed_segment_eq_real_ivl open_segment_def split: if_split_asm) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

328 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

329 
lemma closed_segment_real_eq: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

330 
fixes u::real shows "closed_segment u v = (\<lambda>x. (v  u) * x + u) ` {0..1}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

331 
by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

332 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

333 
lemma dist_in_closed_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

334 
fixes a :: "'a :: euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

335 
assumes "x \<in> closed_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

336 
shows "dist x a \<le> dist a b \<and> dist x b \<le> dist a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

337 
proof (intro conjI) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

338 
obtain u where u: "0 \<le> u" "u \<le> 1" and x: "x = (1  u) *\<^sub>R a + u *\<^sub>R b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

339 
using assms by (force simp: in_segment algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

340 
have "dist x a = u * dist a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

341 
apply (simp add: dist_norm algebra_simps x) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

342 
by (metis \<open>0 \<le> u\<close> abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

343 
also have "... \<le> dist a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

344 
by (simp add: mult_left_le_one_le u) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

345 
finally show "dist x a \<le> dist a b" . 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

346 
have "dist x b = norm ((1u) *\<^sub>R a  (1u) *\<^sub>R b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

347 
by (simp add: dist_norm algebra_simps x) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

348 
also have "... = (1u) * dist a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

349 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

350 
have "norm ((1  1 * u) *\<^sub>R (a  b)) = (1  1 * u) * norm (a  b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

351 
using \<open>u \<le> 1\<close> by force 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

352 
then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

353 
by (simp add: dist_norm real_vector.scale_right_diff_distrib) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

354 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

355 
also have "... \<le> dist a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

356 
by (simp add: mult_left_le_one_le u) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

357 
finally show "dist x b \<le> dist a b" . 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

358 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

359 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

360 
lemma dist_in_open_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

361 
fixes a :: "'a :: euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

362 
assumes "x \<in> open_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

363 
shows "dist x a < dist a b \<and> dist x b < dist a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

364 
proof (intro conjI) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

365 
obtain u where u: "0 < u" "u < 1" and x: "x = (1  u) *\<^sub>R a + u *\<^sub>R b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

366 
using assms by (force simp: in_segment algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

367 
have "dist x a = u * dist a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

368 
apply (simp add: dist_norm algebra_simps x) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

369 
by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib \<open>0 < u\<close>) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

370 
also have *: "... < dist a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

371 
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>) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

372 
finally show "dist x a < dist a b" . 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

373 
have ab_ne0: "dist a b \<noteq> 0" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

374 
using * by fastforce 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

375 
have "dist x b = norm ((1u) *\<^sub>R a  (1u) *\<^sub>R b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

376 
by (simp add: dist_norm algebra_simps x) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

377 
also have "... = (1u) * dist a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

378 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

379 
have "norm ((1  1 * u) *\<^sub>R (a  b)) = (1  1 * u) * norm (a  b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

380 
using \<open>u < 1\<close> by force 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

381 
then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

382 
by (simp add: dist_norm real_vector.scale_right_diff_distrib) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

383 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

384 
also have "... < dist a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

385 
using ab_ne0 \<open>0 < u\<close> by simp 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

386 
finally show "dist x b < dist a b" . 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

387 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

388 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

389 
lemma dist_decreases_open_segment_0: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

390 
fixes x :: "'a :: euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

391 
assumes "x \<in> open_segment 0 b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

392 
shows "dist c x < dist c 0 \<or> dist c x < dist c b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

393 
proof (rule ccontr, clarsimp simp: not_less) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

394 
obtain u where u: "0 \<noteq> b" "0 < u" "u < 1" and x: "x = u *\<^sub>R b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

395 
using assms by (auto simp: in_segment) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

396 
have xb: "x \<bullet> b < b \<bullet> b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

397 
using u x by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

398 
assume "norm c \<le> dist c x" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

399 
then have "c \<bullet> c \<le> (c  x) \<bullet> (c  x)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

400 
by (simp add: dist_norm norm_le) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

401 
moreover have "0 < x \<bullet> b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

402 
using u x by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

403 
ultimately have less: "c \<bullet> b < x \<bullet> b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

404 
by (simp add: x algebra_simps inner_commute u) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

405 
assume "dist c b \<le> dist c x" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

406 
then have "(c  b) \<bullet> (c  b) \<le> (c  x) \<bullet> (c  x)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

407 
by (simp add: dist_norm norm_le) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

408 
then have "(b \<bullet> b) * (1  u*u) \<le> 2 * (b \<bullet> c) * (1u)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

409 
by (simp add: x algebra_simps inner_commute) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

410 
then have "(1+u) * (b \<bullet> b) * (1u) \<le> 2 * (b \<bullet> c) * (1u)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

411 
by (simp add: algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

412 
then have "(1+u) * (b \<bullet> b) \<le> 2 * (b \<bullet> c)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

413 
using \<open>u < 1\<close> by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

414 
with xb have "c \<bullet> b \<ge> x \<bullet> b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

415 
by (auto simp: x algebra_simps inner_commute) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

416 
with less show False by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

417 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

418 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

419 
proposition dist_decreases_open_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

420 
fixes a :: "'a :: euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

421 
assumes "x \<in> open_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

422 
shows "dist c x < dist c a \<or> dist c x < dist c b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

423 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

424 
have *: "x  a \<in> open_segment 0 (b  a)" using assms 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

425 
by (metis diff_self open_segment_translation_eq uminus_add_conv_diff) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

426 
show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

427 
using dist_decreases_open_segment_0 [OF *, of "ca"] assms 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

428 
by (simp add: dist_norm) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

429 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

430 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

431 
corollary open_segment_furthest_le: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

432 
fixes a b x y :: "'a::euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

433 
assumes "x \<in> open_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

434 
shows "norm (y  x) < norm (y  a) \<or> norm (y  x) < norm (y  b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

435 
by (metis assms dist_decreases_open_segment dist_norm) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

436 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

437 
corollary dist_decreases_closed_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

438 
fixes a :: "'a :: euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

439 
assumes "x \<in> closed_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

440 
shows "dist c x \<le> dist c a \<or> dist c x \<le> dist c b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

441 
apply (cases "x \<in> open_segment a b") 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

442 
using dist_decreases_open_segment less_eq_real_def apply blast 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

443 
by (metis DiffI assms empty_iff insertE open_segment_def order_refl) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

444 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

445 
lemma convex_intermediate_ball: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

446 
fixes a :: "'a :: euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

447 
shows "\<lbrakk>ball a r \<subseteq> T; T \<subseteq> cball a r\<rbrakk> \<Longrightarrow> convex T" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

448 
apply (simp add: convex_contains_open_segment, clarify) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

449 
by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

450 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

451 
lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b \<subseteq> closed_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

452 
apply (clarsimp simp: midpoint_def in_segment) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

453 
apply (rule_tac x="(1 + u) / 2" in exI) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

454 
apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

455 
by (metis real_sum_of_halves scaleR_left.add) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

456 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

457 
lemma notin_segment_midpoint: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

458 
fixes a :: "'a :: euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

459 
shows "a \<noteq> b \<Longrightarrow> a \<notin> closed_segment (midpoint a b) b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

460 
by (auto simp: dist_midpoint dest!: dist_in_closed_segment) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

461 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

462 
lemma segment_to_closest_point: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

463 
fixes S :: "'a :: euclidean_space set" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

464 
shows "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> open_segment a (closest_point S a) \<inter> S = {}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

465 
apply (subst disjoint_iff_not_equal) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

466 
apply (clarify dest!: dist_in_open_segment) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

467 
by (metis closest_point_le dist_commute le_less_trans less_irrefl) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

468 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

469 
lemma segment_to_point_exists: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

470 
fixes S :: "'a :: euclidean_space set" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

471 
assumes "closed S" "S \<noteq> {}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

472 
obtains b where "b \<in> S" "open_segment a b \<inter> S = {}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

473 
by (metis assms segment_to_closest_point closest_point_exists that) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

474 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

475 
subsubsection\<open>More lemmas, especially for working with the underlying formula\<close> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

476 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

477 
lemma segment_eq_compose: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

478 
fixes a :: "'a :: real_vector" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

479 
shows "(\<lambda>u. (1  u) *\<^sub>R a + u *\<^sub>R b) = (\<lambda>x. a + x) o (\<lambda>u. u *\<^sub>R (b  a))" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

480 
by (simp add: o_def algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

481 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

482 
lemma segment_degen_1: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

483 
fixes a :: "'a :: real_vector" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

484 
shows "(1  u) *\<^sub>R a + u *\<^sub>R b = b \<longleftrightarrow> a=b \<or> u=1" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

485 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

486 
{ assume "(1  u) *\<^sub>R a + u *\<^sub>R b = b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

487 
then have "(1  u) *\<^sub>R a = (1  u) *\<^sub>R b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

488 
by (simp add: algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

489 
then have "a=b \<or> u=1" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

490 
by simp 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

491 
} then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

492 
by (auto simp: algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

493 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

494 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

495 
lemma segment_degen_0: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

496 
fixes a :: "'a :: real_vector" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

497 
shows "(1  u) *\<^sub>R a + u *\<^sub>R b = a \<longleftrightarrow> a=b \<or> u=0" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

498 
using segment_degen_1 [of "1u" b a] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

499 
by (auto simp: algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

500 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

501 
lemma add_scaleR_degen: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

502 
fixes a b ::"'a::real_vector" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

503 
assumes "(u *\<^sub>R b + v *\<^sub>R a) = (u *\<^sub>R a + v *\<^sub>R b)" "u \<noteq> v" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

504 
shows "a=b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

505 
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) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

506 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

507 
lemma closed_segment_image_interval: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

508 
"closed_segment a b = (\<lambda>u. (1  u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

509 
by (auto simp: set_eq_iff image_iff closed_segment_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

510 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

511 
lemma open_segment_image_interval: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

512 
"open_segment a b = (if a=b then {} else (\<lambda>u. (1  u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1})" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

513 
by (auto simp: open_segment_def closed_segment_def segment_degen_0 segment_degen_1) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

514 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

515 
lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

516 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

517 
lemma open_segment_bound1: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

518 
assumes "x \<in> open_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

519 
shows "norm (x  a) < norm (b  a)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

520 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

521 
obtain u where "x = (1  u) *\<^sub>R a + u *\<^sub>R b" "0 < u" "u < 1" "a \<noteq> b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

522 
using assms by (auto simp add: open_segment_image_interval split: if_split_asm) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

523 
then show "norm (x  a) < norm (b  a)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

524 
apply clarify 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

525 
apply (auto simp: algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

526 
apply (simp add: scaleR_diff_right [symmetric]) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

527 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

528 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

529 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

530 
lemma compact_segment [simp]: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

531 
fixes a :: "'a::real_normed_vector" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

532 
shows "compact (closed_segment a b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

533 
by (auto simp: segment_image_interval intro!: compact_continuous_image continuous_intros) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

534 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

535 
lemma closed_segment [simp]: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

536 
fixes a :: "'a::real_normed_vector" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

537 
shows "closed (closed_segment a b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

538 
by (simp add: compact_imp_closed) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

539 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

540 
lemma closure_closed_segment [simp]: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

541 
fixes a :: "'a::real_normed_vector" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

542 
shows "closure(closed_segment a b) = closed_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

543 
by simp 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

544 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

545 
lemma open_segment_bound: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

546 
assumes "x \<in> open_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

547 
shows "norm (x  a) < norm (b  a)" "norm (x  b) < norm (b  a)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

548 
apply (simp add: assms open_segment_bound1) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

549 
by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

550 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

551 
lemma closure_open_segment [simp]: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

552 
fixes a :: "'a::euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

553 
shows "closure(open_segment a b) = (if a = b then {} else closed_segment a b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

554 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

555 
have "closure ((\<lambda>u. u *\<^sub>R (b  a)) ` {0<..<1}) = (\<lambda>u. u *\<^sub>R (b  a)) ` closure {0<..<1}" if "a \<noteq> b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

556 
apply (rule closure_injective_linear_image [symmetric]) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

557 
apply (simp add:) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

558 
using that by (simp add: inj_on_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

559 
then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

560 
by (simp add: segment_image_interval segment_eq_compose closure_greaterThanLessThan [symmetric] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

561 
closure_translation image_comp [symmetric] del: closure_greaterThanLessThan) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

562 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

563 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

564 
lemma closed_open_segment_iff [simp]: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

565 
fixes a :: "'a::euclidean_space" shows "closed(open_segment a b) \<longleftrightarrow> a = b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

566 
by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2)) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

567 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

568 
lemma compact_open_segment_iff [simp]: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

569 
fixes a :: "'a::euclidean_space" shows "compact(open_segment a b) \<longleftrightarrow> a = b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

570 
by (simp add: bounded_open_segment compact_eq_bounded_closed) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

571 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

572 
lemma convex_closed_segment [iff]: "convex (closed_segment a b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

573 
unfolding segment_convex_hull by(rule convex_convex_hull) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

574 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

575 
lemma convex_open_segment [iff]: "convex(open_segment a b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

576 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

577 
have "convex ((\<lambda>u. u *\<^sub>R (ba)) ` {0<..<1})" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

578 
by (rule convex_linear_image) auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

579 
then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

580 
apply (simp add: open_segment_image_interval segment_eq_compose) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

581 
by (metis image_comp convex_translation) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

582 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

583 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

584 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

585 
lemmas convex_segment = convex_closed_segment convex_open_segment 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

586 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

587 
lemma connected_segment [iff]: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

588 
fixes x :: "'a :: real_normed_vector" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

589 
shows "connected (closed_segment x y)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

590 
by (simp add: convex_connected) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

591 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

592 
lemma affine_hull_closed_segment [simp]: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

593 
"affine hull (closed_segment a b) = affine hull {a,b}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

594 
by (simp add: segment_convex_hull) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

595 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

596 
lemma affine_hull_open_segment [simp]: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

597 
fixes a :: "'a::euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

598 
shows "affine hull (open_segment a b) = (if a = b then {} else affine hull {a,b})" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

599 
by (metis affine_hull_convex_hull affine_hull_empty closure_open_segment closure_same_affine_hull segment_convex_hull) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

600 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

601 
lemma rel_interior_closure_convex_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

602 
fixes S :: "_::euclidean_space set" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

603 
assumes "convex S" "a \<in> rel_interior S" "b \<in> closure S" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

604 
shows "open_segment a b \<subseteq> rel_interior S" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

605 
proof 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

606 
fix x 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

607 
have [simp]: "(1  u) *\<^sub>R a + u *\<^sub>R b = b  (1  u) *\<^sub>R (b  a)" for u 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

608 
by (simp add: algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

609 
assume "x \<in> open_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

610 
then show "x \<in> rel_interior S" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

611 
unfolding closed_segment_def open_segment_def using assms 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

612 
by (auto intro: rel_interior_closure_convex_shrink) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

613 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

614 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

615 
lemma convex_hull_insert_segments: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

616 
"convex hull (insert a S) = 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

617 
(if S = {} then {a} else \<Union>x \<in> convex hull S. closed_segment a x)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

618 
by (force simp add: convex_hull_insert_alt in_segment) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

619 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

620 
lemma Int_convex_hull_insert_rel_exterior: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

621 
fixes z :: "'a::euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

622 
assumes "convex C" "T \<subseteq> C" and z: "z \<in> rel_interior C" and dis: "disjnt S (rel_interior C)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

623 
shows "S \<inter> (convex hull (insert z T)) = S \<inter> (convex hull T)" (is "?lhs = ?rhs") 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

624 
proof 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

625 
have "T = {} \<Longrightarrow> z \<notin> S" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

626 
using dis z by (auto simp add: disjnt_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

627 
then show "?lhs \<subseteq> ?rhs" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

628 
proof (clarsimp simp add: convex_hull_insert_segments) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

629 
fix x y 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

630 
assume "x \<in> S" and y: "y \<in> convex hull T" and "x \<in> closed_segment z y" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

631 
have "y \<in> closure C" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

632 
by (metis y \<open>convex C\<close> \<open>T \<subseteq> C\<close> closure_subset contra_subsetD convex_hull_eq hull_mono) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

633 
moreover have "x \<notin> rel_interior C" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

634 
by (meson \<open>x \<in> S\<close> dis disjnt_iff) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

635 
moreover have "x \<in> open_segment z y \<union> {z, y}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

636 
using \<open>x \<in> closed_segment z y\<close> closed_segment_eq_open by blast 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

637 
ultimately show "x \<in> convex hull T" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

638 
using rel_interior_closure_convex_segment [OF \<open>convex C\<close> z] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

639 
using y z by blast 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

640 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

641 
show "?rhs \<subseteq> ?lhs" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

642 
by (meson hull_mono inf_mono subset_insertI subset_refl) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

643 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

644 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

645 
subsection\<open>More results about segments\<close> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

646 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

647 
lemma dist_half_times2: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

648 
fixes a :: "'a :: real_normed_vector" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

649 
shows "dist ((1 / 2) *\<^sub>R (a + b)) x * 2 = dist (a+b) (2 *\<^sub>R x)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

650 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

651 
have "norm ((1 / 2) *\<^sub>R (a + b)  x) * 2 = norm (2 *\<^sub>R ((1 / 2) *\<^sub>R (a + b)  x))" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

652 
by simp 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

653 
also have "... = norm ((a + b)  2 *\<^sub>R x)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

654 
by (simp add: real_vector.scale_right_diff_distrib) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

655 
finally show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

656 
by (simp only: dist_norm) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

657 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

658 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

659 
lemma closed_segment_as_ball: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

660 
"closed_segment a b = affine hull {a,b} \<inter> cball(inverse 2 *\<^sub>R (a + b))(norm(b  a) / 2)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

661 
proof (cases "b = a") 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

662 
case True then show ?thesis by (auto simp: hull_inc) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

663 
next 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

664 
case False 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

665 
then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

666 
dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b  a)) = 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

667 
(\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)" for x 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

668 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

669 
have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

670 
dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b  a)) = 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

671 
((\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b) \<and> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

672 
dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b  a))" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

673 
unfolding eq_diff_eq [symmetric] by simp 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

674 
also have "... = (\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b \<and> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

675 
norm ((a+b)  (2 *\<^sub>R x)) \<le> norm (b  a))" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

676 
by (simp add: dist_half_times2) (simp add: dist_norm) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

677 
also have "... = (\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b \<and> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

678 
norm ((a+b)  (2 *\<^sub>R ((1  u) *\<^sub>R a + u *\<^sub>R b))) \<le> norm (b  a))" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

679 
by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

680 
also have "... = (\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b \<and> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

681 
norm ((1  u * 2) *\<^sub>R (b  a)) \<le> norm (b  a))" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

682 
by (simp add: algebra_simps scaleR_2) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

683 
also have "... = (\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b \<and> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

684 
\<bar>1  u * 2\<bar> * norm (b  a) \<le> norm (b  a))" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

685 
by simp 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

686 
also have "... = (\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1  u * 2\<bar> \<le> 1)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

687 
by (simp add: mult_le_cancel_right2 False) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

688 
also have "... = (\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

689 
by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

690 
finally show ?thesis . 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

691 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

692 
show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

693 
by (simp add: affine_hull_2 Set.set_eq_iff closed_segment_def *) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

694 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

695 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

696 
lemma open_segment_as_ball: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

697 
"open_segment a b = 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

698 
affine hull {a,b} \<inter> ball(inverse 2 *\<^sub>R (a + b))(norm(b  a) / 2)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

699 
proof (cases "b = a") 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

700 
case True then show ?thesis by (auto simp: hull_inc) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

701 
next 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

702 
case False 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

703 
then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

704 
dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b  a)) = 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

705 
(\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)" for x 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

706 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

707 
have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

708 
dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b  a)) = 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

709 
((\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b) \<and> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

710 
dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b  a))" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

711 
unfolding eq_diff_eq [symmetric] by simp 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

712 
also have "... = (\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b \<and> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

713 
norm ((a+b)  (2 *\<^sub>R x)) < norm (b  a))" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

714 
by (simp add: dist_half_times2) (simp add: dist_norm) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

715 
also have "... = (\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b \<and> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

716 
norm ((a+b)  (2 *\<^sub>R ((1  u) *\<^sub>R a + u *\<^sub>R b))) < norm (b  a))" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

717 
by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

718 
also have "... = (\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b \<and> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

719 
norm ((1  u * 2) *\<^sub>R (b  a)) < norm (b  a))" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

720 
by (simp add: algebra_simps scaleR_2) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

721 
also have "... = (\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b \<and> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

722 
\<bar>1  u * 2\<bar> * norm (b  a) < norm (b  a))" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

723 
by simp 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

724 
also have "... = (\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1  u * 2\<bar> < 1)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

725 
by (simp add: mult_le_cancel_right2 False) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

726 
also have "... = (\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

727 
by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

728 
finally show ?thesis . 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

729 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

730 
show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

731 
using False by (force simp: affine_hull_2 Set.set_eq_iff open_segment_image_interval *) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

732 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

733 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

734 
lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

735 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

736 
lemma closed_segment_neq_empty [simp]: "closed_segment a b \<noteq> {}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

737 
by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

738 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

739 
lemma open_segment_eq_empty [simp]: "open_segment a b = {} \<longleftrightarrow> a = b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

740 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

741 
{ assume a1: "open_segment a b = {}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

742 
have "{} \<noteq> {0::real<..<1}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

743 
by simp 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

744 
then have "a = b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

745 
using a1 open_segment_image_interval by fastforce 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

746 
} then show ?thesis by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

747 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

748 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

749 
lemma open_segment_eq_empty' [simp]: "{} = open_segment a b \<longleftrightarrow> a = b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

750 
using open_segment_eq_empty by blast 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

751 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

752 
lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

753 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

754 
lemma inj_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

755 
fixes a :: "'a :: real_vector" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

756 
assumes "a \<noteq> b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

757 
shows "inj_on (\<lambda>u. (1  u) *\<^sub>R a + u *\<^sub>R b) I" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

758 
proof 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

759 
fix x y 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

760 
assume "(1  x) *\<^sub>R a + x *\<^sub>R b = (1  y) *\<^sub>R a + y *\<^sub>R b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

761 
then have "x *\<^sub>R (b  a) = y *\<^sub>R (b  a)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

762 
by (simp add: algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

763 
with assms show "x = y" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

764 
by (simp add: real_vector.scale_right_imp_eq) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

765 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

766 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

767 
lemma finite_closed_segment [simp]: "finite(closed_segment a b) \<longleftrightarrow> a = b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

768 
apply auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

769 
apply (rule ccontr) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

770 
apply (simp add: segment_image_interval) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

771 
using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

772 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

773 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

774 
lemma finite_open_segment [simp]: "finite(open_segment a b) \<longleftrightarrow> a = b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

775 
by (auto simp: open_segment_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

776 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

777 
lemmas finite_segment = finite_closed_segment finite_open_segment 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

778 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

779 
lemma closed_segment_eq_sing: "closed_segment a b = {c} \<longleftrightarrow> a = c \<and> b = c" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

780 
by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

781 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

782 
lemma open_segment_eq_sing: "open_segment a b \<noteq> {c}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

783 
by (metis finite_insert finite_open_segment insert_not_empty open_segment_image_interval) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

784 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

785 
lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

786 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

787 
lemma subset_closed_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

788 
"closed_segment a b \<subseteq> closed_segment c d \<longleftrightarrow> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

789 
a \<in> closed_segment c d \<and> b \<in> closed_segment c d" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

790 
by auto (meson contra_subsetD convex_closed_segment convex_contains_segment) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

791 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

792 
lemma subset_co_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

793 
"closed_segment a b \<subseteq> open_segment c d \<longleftrightarrow> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

794 
a \<in> open_segment c d \<and> b \<in> open_segment c d" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

795 
using closed_segment_subset by blast 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

796 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

797 
lemma subset_open_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

798 
fixes a :: "'a::euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

799 
shows "open_segment a b \<subseteq> open_segment c d \<longleftrightarrow> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

800 
a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

801 
(is "?lhs = ?rhs") 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

802 
proof (cases "a = b") 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

803 
case True then show ?thesis by simp 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

804 
next 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

805 
case False show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

806 
proof 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

807 
assume rhs: ?rhs 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

808 
with \<open>a \<noteq> b\<close> have "c \<noteq> d" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

809 
using closed_segment_idem singleton_iff by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

810 
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) = 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

811 
(1  uc) *\<^sub>R c + uc *\<^sub>R d \<and> 0 < uc \<and> uc < 1" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

812 
if neq: "(1  ua) *\<^sub>R c + ua *\<^sub>R d \<noteq> (1  ub) *\<^sub>R c + ub *\<^sub>R d" "c \<noteq> d" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

813 
and "a = (1  ua) *\<^sub>R c + ua *\<^sub>R d" "b = (1  ub) *\<^sub>R c + ub *\<^sub>R d" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

814 
and u: "0 < u" "u < 1" and uab: "0 \<le> ua" "ua \<le> 1" "0 \<le> ub" "ub \<le> 1" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

815 
for u ua ub 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

816 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

817 
have "ua \<noteq> ub" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

818 
using neq by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

819 
moreover have "(u  1) * ua \<le> 0" using u uab 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

820 
by (simp add: mult_nonpos_nonneg) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

821 
ultimately have lt: "(u  1) * ua < u * ub" using u uab 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

822 
by (metis antisym_conv diff_ge_0_iff_ge le_less_trans mult_eq_0_iff mult_le_0_iff not_less) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

823 
have "p * ua + q * ub < p+q" if p: "0 < p" and q: "0 < q" for p q 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

824 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

825 
have "\<not> p \<le> 0" "\<not> q \<le> 0" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

826 
using p q not_less by blast+ 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

827 
then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

828 
by (metis \<open>ua \<noteq> ub\<close> add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

829 
less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4)) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

830 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

831 
then have "(1  u) * ua + u * ub < 1" using u \<open>ua \<noteq> ub\<close> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

832 
by (metis diff_add_cancel diff_gt_0_iff_gt) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

833 
with lt show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

834 
by (rule_tac x="ua + u*(ubua)" in exI) (simp add: algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

835 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

836 
with rhs \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close> show ?lhs 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

837 
unfolding open_segment_image_interval closed_segment_def 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

838 
by (fastforce simp add:) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

839 
next 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

840 
assume lhs: ?lhs 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

841 
with \<open>a \<noteq> b\<close> have "c \<noteq> d" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

842 
by (meson finite_open_segment rev_finite_subset) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

843 
have "closure (open_segment a b) \<subseteq> closure (open_segment c d)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

844 
using lhs closure_mono by blast 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

845 
then have "closed_segment a b \<subseteq> closed_segment c d" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

846 
by (simp add: \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close>) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

847 
then show ?rhs 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

848 
by (force simp: \<open>a \<noteq> b\<close>) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

849 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

850 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

851 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

852 
lemma subset_oc_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

853 
fixes a :: "'a::euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

854 
shows "open_segment a b \<subseteq> closed_segment c d \<longleftrightarrow> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

855 
a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

856 
apply (simp add: subset_open_segment [symmetric]) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

857 
apply (rule iffI) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

858 
apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

859 
apply (meson dual_order.trans segment_open_subset_closed) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

860 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

861 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

862 
lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

863 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

864 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

865 
subsection\<open>Betweenness\<close> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

866 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

867 
definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

868 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

869 
lemma betweenI: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

870 
assumes "0 \<le> u" "u \<le> 1" "x = (1  u) *\<^sub>R a + u *\<^sub>R b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

871 
shows "between (a, b) x" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

872 
using assms unfolding between_def closed_segment_def by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

873 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

874 
lemma betweenE: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

875 
assumes "between (a, b) x" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

876 
obtains u where "0 \<le> u" "u \<le> 1" "x = (1  u) *\<^sub>R a + u *\<^sub>R b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

877 
using assms unfolding between_def closed_segment_def by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

878 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

879 
lemma between_implies_scaled_diff: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

880 
assumes "between (S, T) X" "between (S, T) Y" "S \<noteq> Y" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

881 
obtains c where "(X  Y) = c *\<^sub>R (S  Y)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

882 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

883 
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" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

884 
by (metis add.commute betweenE eq_diff_eq) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

885 
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" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

886 
by (metis add.commute betweenE eq_diff_eq) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

887 
have "X  Y = (u\<^sub>X  u\<^sub>Y) *\<^sub>R (S  T)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

888 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

889 
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 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

890 
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) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

891 
finally show ?thesis by (simp add: real_vector.scale_right_diff_distrib) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

892 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

893 
moreover from Y have "S  Y = (1  u\<^sub>Y) *\<^sub>R (S  T)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

894 
by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

895 
moreover note \<open>S \<noteq> Y\<close> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

896 
ultimately have "(X  Y) = ((u\<^sub>X  u\<^sub>Y) / (1  u\<^sub>Y)) *\<^sub>R (S  Y)" by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

897 
from this that show thesis by blast 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

898 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

899 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

900 
lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

901 
unfolding between_def by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

902 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

903 
lemma between: "between (a, b) (x::'a::euclidean_space) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

904 
proof (cases "a = b") 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

905 
case True 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

906 
then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

907 
unfolding between_def split_conv 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

908 
by (auto simp add: dist_commute) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

909 
next 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

910 
case False 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

911 
then have Fal: "norm (a  b) \<noteq> 0" and Fal2: "norm (a  b) > 0" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

912 
by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

913 
have *: "\<And>u. a  ((1  u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a  b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

914 
by (auto simp add: algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

915 
show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

916 
unfolding between_def split_conv closed_segment_def mem_Collect_eq 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

917 
apply rule 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

918 
apply (elim exE conjE) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

919 
apply (subst dist_triangle_eq) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

920 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

921 
fix u 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

922 
assume as: "x = (1  u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

923 
then have *: "a  x = u *\<^sub>R (a  b)" "x  b = (1  u) *\<^sub>R (a  b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

924 
unfolding as(1) by (auto simp add:algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

925 
show "norm (a  x) *\<^sub>R (x  b) = norm (x  b) *\<^sub>R (a  x)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

926 
unfolding norm_minus_commute[of x a] * using as(2,3) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

927 
by (auto simp add: field_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

928 
next 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

929 
assume as: "dist a b = dist a x + dist x b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

930 
have "norm (a  x) / norm (a  b) \<le> 1" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

931 
using Fal2 unfolding as[unfolded dist_norm] norm_ge_zero by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

932 
then show "\<exists>u. x = (1  u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

933 
apply (rule_tac x="dist a x / dist a b" in exI) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

934 
unfolding dist_norm 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

935 
apply (subst euclidean_eq_iff) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

936 
apply rule 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

937 
defer 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

938 
apply rule 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

939 
prefer 3 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

940 
apply rule 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

941 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

942 
fix i :: 'a 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

943 
assume i: "i \<in> Basis" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

944 
have "((1  norm (a  x) / norm (a  b)) *\<^sub>R a + (norm (a  x) / norm (a  b)) *\<^sub>R b) \<bullet> i = 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

945 
((norm (a  b)  norm (a  x)) * (a \<bullet> i) + norm (a  x) * (b \<bullet> i)) / norm (a  b)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

946 
using Fal by (auto simp add: field_simps inner_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

947 
also have "\<dots> = x\<bullet>i" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

948 
apply (rule divide_eq_imp[OF Fal]) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

949 
unfolding as[unfolded dist_norm] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

950 
using as[unfolded dist_triangle_eq] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

951 
apply  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

952 
apply (subst (asm) euclidean_eq_iff) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

953 
using i 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

954 
apply (erule_tac x=i in ballE) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

955 
apply (auto simp add: field_simps inner_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

956 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

957 
finally show "x \<bullet> i = 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

958 
((1  norm (a  x) / norm (a  b)) *\<^sub>R a + (norm (a  x) / norm (a  b)) *\<^sub>R b) \<bullet> i" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

959 
by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

960 
qed (insert Fal2, auto) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

961 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

962 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

963 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

964 
lemma between_midpoint: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

965 
fixes a :: "'a::euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

966 
shows "between (a,b) (midpoint a b)" (is ?t1) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

967 
and "between (b,a) (midpoint a b)" (is ?t2) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

968 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

969 
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" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

970 
by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

971 
show ?t1 ?t2 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

972 
unfolding between midpoint_def dist_norm 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

973 
apply(rule_tac[!] *) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

974 
unfolding euclidean_eq_iff[where 'a='a] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

975 
apply (auto simp add: field_simps inner_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

976 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

977 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

978 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

979 
lemma between_mem_convex_hull: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

980 
"between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

981 
unfolding between_mem_segment segment_convex_hull .. 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

982 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

983 
lemma between_triv_iff [simp]: "between (a,a) b \<longleftrightarrow> a=b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

984 
by (auto simp: between_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

985 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

986 
lemma between_triv1 [simp]: "between (a,b) a" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

987 
by (auto simp: between_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

988 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

989 
lemma between_triv2 [simp]: "between (a,b) b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

990 
by (auto simp: between_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

991 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

992 
lemma between_commute: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

993 
"between (a,b) = between (b,a)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

994 
by (auto simp: between_def closed_segment_commute) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

995 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

996 
lemma between_antisym: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

997 
fixes a :: "'a :: euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

998 
shows "\<lbrakk>between (b,c) a; between (a,c) b\<rbrakk> \<Longrightarrow> a = b" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

999 
by (auto simp: between dist_commute) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1000 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1001 
lemma between_trans: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1002 
fixes a :: "'a :: euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1003 
shows "\<lbrakk>between (b,c) a; between (a,c) d\<rbrakk> \<Longrightarrow> between (b,c) d" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1004 
using dist_triangle2 [of b c d] dist_triangle3 [of b d a] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1005 
by (auto simp: between dist_commute) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1006 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1007 
lemma between_norm: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1008 
fixes a :: "'a :: euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1009 
shows "between (a,b) x \<longleftrightarrow> norm(x  a) *\<^sub>R (b  x) = norm(b  x) *\<^sub>R (x  a)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1010 
by (auto simp: between dist_triangle_eq norm_minus_commute algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1011 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1012 
lemma between_swap: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1013 
fixes A B X Y :: "'a::euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1014 
assumes "between (A, B) X" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1015 
assumes "between (A, B) Y" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1016 
shows "between (X, B) Y \<longleftrightarrow> between (A, Y) X" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1017 
using assms by (auto simp add: between) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1018 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1019 
lemma between_translation [simp]: "between (a + y,a + z) (a + x) \<longleftrightarrow> between (y,z) x" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1020 
by (auto simp: between_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1021 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1022 
lemma between_trans_2: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1023 
fixes a :: "'a :: euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1024 
shows "\<lbrakk>between (b,c) a; between (a,b) d\<rbrakk> \<Longrightarrow> between (c,d) a" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1025 
by (metis between_commute between_swap between_trans) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1026 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1027 
lemma between_scaleR_lift [simp]: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1028 
fixes v :: "'a::euclidean_space" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1029 
shows "between (a *\<^sub>R v, b *\<^sub>R v) (c *\<^sub>R v) \<longleftrightarrow> v = 0 \<or> between (a, b) c" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1030 
by (simp add: between dist_norm scaleR_left_diff_distrib [symmetric] distrib_right [symmetric]) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1031 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1032 
lemma between_1: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1033 
fixes x::real 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1034 
shows "between (a,b) x \<longleftrightarrow> (a \<le> x \<and> x \<le> b) \<or> (b \<le> x \<and> x \<le> a)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1035 
by (auto simp: between_mem_segment closed_segment_eq_real_ivl) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1036 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1037 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1038 
subsection \<open>Shrinking towards the interior of a convex set\<close> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1039 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1040 
lemma mem_interior_convex_shrink: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1041 
fixes s :: "'a::euclidean_space set" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1042 
assumes "convex s" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1043 
and "c \<in> interior s" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1044 
and "x \<in> s" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1045 
and "0 < e" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1046 
and "e \<le> 1" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1047 
shows "x  e *\<^sub>R (x  c) \<in> interior s" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1048 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1049 
obtain d where "d > 0" and d: "ball c d \<subseteq> s" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1050 
using assms(2) unfolding mem_interior by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1051 
show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1052 
unfolding mem_interior 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1053 
apply (rule_tac x="e*d" in exI) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1054 
apply rule 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1055 
defer 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1056 
unfolding subset_eq Ball_def mem_ball 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1057 
proof (rule, rule) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1058 
fix y 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1059 
assume as: "dist (x  e *\<^sub>R (x  c)) y < e * d" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1060 
have *: "y = (1  (1  e)) *\<^sub>R ((1 / e) *\<^sub>R y  ((1  e) / e) *\<^sub>R x) + (1  e) *\<^sub>R x" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1061 
using \<open>e > 0\<close> by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1062 
have "dist c ((1 / e) *\<^sub>R y  ((1  e) / e) *\<^sub>R x) = \<bar>1/e\<bar> * norm (e *\<^sub>R c  y + (1  e) *\<^sub>R x)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1063 
unfolding dist_norm 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1064 
unfolding norm_scaleR[symmetric] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1065 
apply (rule arg_cong[where f=norm]) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1066 
using \<open>e > 0\<close> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1067 
by (auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1068 
also have "\<dots> = \<bar>1/e\<bar> * norm (x  e *\<^sub>R (x  c)  y)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1069 
by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1070 
also have "\<dots> < d" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1071 
using as[unfolded dist_norm] and \<open>e > 0\<close> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1072 
by (auto simp add:pos_divide_less_eq[OF \<open>e > 0\<close>] mult.commute) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1073 
finally show "y \<in> s" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1074 
apply (subst *) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1075 
apply (rule assms(1)[unfolded convex_alt,rule_format]) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1076 
apply (rule d[unfolded subset_eq,rule_format]) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1077 
unfolding mem_ball 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1078 
using assms(35) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1079 
apply auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1080 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1081 
qed (insert \<open>e>0\<close> \<open>d>0\<close>, auto) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1082 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1083 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1084 
lemma mem_interior_closure_convex_shrink: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1085 
fixes s :: "'a::euclidean_space set" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1086 
assumes "convex s" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1087 
and "c \<in> interior s" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1088 
and "x \<in> closure s" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1089 
and "0 < e" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1090 
and "e \<le> 1" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1091 
shows "x  e *\<^sub>R (x  c) \<in> interior s" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1092 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1093 
obtain d where "d > 0" and d: "ball c d \<subseteq> s" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1094 
using assms(2) unfolding mem_interior by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1095 
have "\<exists>y\<in>s. norm (y  x) * (1  e) < e * d" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1096 
proof (cases "x \<in> s") 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1097 
case True 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1098 
then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1099 
using \<open>e > 0\<close> \<open>d > 0\<close> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1100 
apply (rule_tac bexI[where x=x]) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1101 
apply (auto) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1102 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1103 
next 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1104 
case False 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1105 
then have x: "x islimpt s" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1106 
using assms(3)[unfolded closure_def] by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1107 
show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1108 
proof (cases "e = 1") 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1109 
case True 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1110 
obtain y where "y \<in> s" "y \<noteq> x" "dist y x < 1" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1111 
using x[unfolded islimpt_approachable,THEN spec[where x=1]] by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1112 
then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1113 
apply (rule_tac x=y in bexI) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1114 
unfolding True 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1115 
using \<open>d > 0\<close> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1116 
apply auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1117 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1118 
next 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1119 
case False 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1120 
then have "0 < e * d / (1  e)" and *: "1  e > 0" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1121 
using \<open>e \<le> 1\<close> \<open>e > 0\<close> \<open>d > 0\<close> by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1122 
then obtain y where "y \<in> s" "y \<noteq> x" "dist y x < e * d / (1  e)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1123 
using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1  e)"]] by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1124 
then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1125 
apply (rule_tac x=y in bexI) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1126 
unfolding dist_norm 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1127 
using pos_less_divide_eq[OF *] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1128 
apply auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1129 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1130 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1131 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1132 
then obtain y where "y \<in> s" and y: "norm (y  x) * (1  e) < e * d" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1133 
by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1134 
define z where "z = c + ((1  e) / e) *\<^sub>R (x  y)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1135 
have *: "x  e *\<^sub>R (x  c) = y  e *\<^sub>R (y  z)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1136 
unfolding z_def using \<open>e > 0\<close> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1137 
by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1138 
have "z \<in> interior s" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1139 
apply (rule interior_mono[OF d,unfolded subset_eq,rule_format]) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1140 
unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1141 
apply (auto simp add:field_simps norm_minus_commute) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1142 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1143 
then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1144 
unfolding * 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1145 
apply  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1146 
apply (rule mem_interior_convex_shrink) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1147 
using assms(1,45) \<open>y\<in>s\<close> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1148 
apply auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1149 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1150 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1151 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1152 
lemma in_interior_closure_convex_segment: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1153 
fixes S :: "'a::euclidean_space set" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1154 
assumes "convex S" and a: "a \<in> interior S" and b: "b \<in> closure S" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1155 
shows "open_segment a b \<subseteq> interior S" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1156 
proof (clarsimp simp: in_segment) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1157 
fix u::real 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1158 
assume u: "0 < u" "u < 1" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1159 
have "(1  u) *\<^sub>R a + u *\<^sub>R b = b  (1  u) *\<^sub>R (b  a)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1160 
by (simp add: algebra_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1161 
also have "... \<in> interior S" using mem_interior_closure_convex_shrink [OF assms] u 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1162 
by simp 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1163 
finally show "(1  u) *\<^sub>R a + u *\<^sub>R b \<in> interior S" . 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1164 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1165 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1166 
lemma closure_open_Int_superset: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1167 
assumes "open S" "S \<subseteq> closure T" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1168 
shows "closure(S \<inter> T) = closure S" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1169 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1170 
have "closure S \<subseteq> closure(S \<inter> T)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1171 
by (metis assms closed_closure closure_minimal inf.orderE open_Int_closure_subset) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1172 
then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1173 
by (simp add: closure_mono dual_order.antisym) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1174 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1175 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1176 
lemma convex_closure_interior: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1177 
fixes S :: "'a::euclidean_space set" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1178 
assumes "convex S" and int: "interior S \<noteq> {}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1179 
shows "closure(interior S) = closure S" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1180 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1181 
obtain a where a: "a \<in> interior S" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1182 
using int by auto 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1183 
have "closure S \<subseteq> closure(interior S)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1184 
proof 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1185 
fix x 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1186 
assume x: "x \<in> closure S" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1187 
show "x \<in> closure (interior S)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1188 
proof (cases "x=a") 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1189 
case True 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1190 
then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1191 
using \<open>a \<in> interior S\<close> closure_subset by blast 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1192 
next 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1193 
case False 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1194 
show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1195 
proof (clarsimp simp add: closure_def islimpt_approachable) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1196 
fix e::real 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1197 
assume xnotS: "x \<notin> interior S" and "0 < e" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1198 
show "\<exists>x'\<in>interior S. x' \<noteq> x \<and> dist x' x < e" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1199 
proof (intro bexI conjI) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1200 
show "x  min (e/2 / norm (x  a)) 1 *\<^sub>R (x  a) \<noteq> x" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1201 
using False \<open>0 < e\<close> by (auto simp: algebra_simps min_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1202 
show "dist (x  min (e/2 / norm (x  a)) 1 *\<^sub>R (x  a)) x < e" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1203 
using \<open>0 < e\<close> by (auto simp: dist_norm min_def) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1204 
show "x  min (e/2 / norm (x  a)) 1 *\<^sub>R (x  a) \<in> interior S" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1205 
apply (clarsimp simp add: min_def a) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1206 
apply (rule mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a x]) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1207 
using \<open>0 < e\<close> False apply (auto simp: divide_simps) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1208 
done 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1209 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1210 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1211 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1212 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1213 
then show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1214 
by (simp add: closure_mono interior_subset subset_antisym) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1215 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1216 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1217 
lemma closure_convex_Int_superset: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1218 
fixes S :: "'a::euclidean_space set" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1219 
assumes "convex S" "interior S \<noteq> {}" "interior S \<subseteq> closure T" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1220 
shows "closure(S \<inter> T) = closure S" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1221 
proof  
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1222 
have "closure S \<subseteq> closure(interior S)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1223 
by (simp add: convex_closure_interior assms) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1224 
also have "... \<subseteq> closure (S \<inter> T)" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1225 
using interior_subset [of S] assms 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1226 
by (metis (no_types, lifting) Int_assoc Int_lower2 closure_mono closure_open_Int_superset inf.orderE open_interior) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1227 
finally show ?thesis 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1228 
by (simp add: closure_mono dual_order.antisym) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1229 
qed 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1230 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1231 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1232 
subsection \<open>Some obvious but surprisingly hard simplex lemmas\<close> 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1233 

2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1234 
lemma simplex: 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1235 
assumes "finite s" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1236 
and "0 \<notin> s" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1237 
shows "convex hull (insert 0 s) = 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1238 
{y. (\<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> sum u s \<le> 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) s = y)}" 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1239 
unfolding convex_hull_finite[OF finite.insertI[OF assms(1)]] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1240 
apply (rule set_eqI, rule) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1241 
unfolding mem_Collect_eq 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1242 
apply (erule_tac[!] exE) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1243 
apply (erule_tac[!] conjE)+ 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1244 
unfolding sum_clauses(2)[OF \<open>finite s\<close>] 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1245 
apply (rule_tac x=u in exI) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1246 
defer 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1247 
apply (rule_tac x="\<lambda>x. if x = 0 then 1  sum u s else u x" in exI) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1248 
using assms(2) 
2562f151541c
Divided Convex_Euclidean_Space.thy in half, creating new theory Sta 