|
1 theory Ordered_Euclidean_Space |
|
2 imports |
|
3 Cartesian_Euclidean_Space |
|
4 "~~/src/HOL/Library/Product_Order" |
|
5 begin |
|
6 |
|
7 subsection \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close> |
|
8 |
|
9 class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space + |
|
10 assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)" |
|
11 assumes eucl_less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" |
|
12 assumes eucl_inf: "inf x y = (\<Sum>i\<in>Basis. inf (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)" |
|
13 assumes eucl_sup: "sup x y = (\<Sum>i\<in>Basis. sup (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)" |
|
14 assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x:X. x \<bullet> i) *\<^sub>R i)" |
|
15 assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x:X. x \<bullet> i) *\<^sub>R i)" |
|
16 assumes eucl_abs: "\<bar>x\<bar> = (\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar> *\<^sub>R i)" |
|
17 begin |
|
18 |
|
19 subclass order |
|
20 by standard |
|
21 (auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans) |
|
22 |
|
23 subclass ordered_ab_group_add_abs |
|
24 by standard (auto simp: eucl_le inner_add_left eucl_abs abs_leI) |
|
25 |
|
26 subclass ordered_real_vector |
|
27 by standard (auto simp: eucl_le intro!: mult_left_mono mult_right_mono) |
|
28 |
|
29 subclass lattice |
|
30 by standard (auto simp: eucl_inf eucl_sup eucl_le) |
|
31 |
|
32 subclass distrib_lattice |
|
33 by standard (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI) |
|
34 |
|
35 subclass conditionally_complete_lattice |
|
36 proof |
|
37 fix z::'a and X::"'a set" |
|
38 assume "X \<noteq> {}" |
|
39 hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp |
|
40 thus "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z" |
|
41 by (auto simp: eucl_Inf eucl_Sup eucl_le |
|
42 intro!: cInf_greatest cSup_least) |
|
43 qed (force intro!: cInf_lower cSup_upper |
|
44 simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def |
|
45 eucl_Inf eucl_Sup eucl_le)+ |
|
46 |
|
47 lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)" |
|
48 and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)" |
|
49 by (simp_all add: eucl_inf eucl_sup inner_setsum_left inner_Basis if_distrib comm_monoid_add_class.setsum.delta |
|
50 cong: if_cong) |
|
51 |
|
52 lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)" |
|
53 and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)" |
|
54 using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def) |
|
55 |
|
56 lemma abs_inner: "i \<in> Basis \<Longrightarrow> \<bar>x\<bar> \<bullet> i = \<bar>x \<bullet> i\<bar>" |
|
57 by (auto simp: eucl_abs) |
|
58 |
|
59 lemma |
|
60 abs_scaleR: "\<bar>a *\<^sub>R b\<bar> = \<bar>a\<bar> *\<^sub>R \<bar>b\<bar>" |
|
61 by (auto simp: eucl_abs abs_mult intro!: euclidean_eqI) |
|
62 |
|
63 lemma interval_inner_leI: |
|
64 assumes "x \<in> {a .. b}" "0 \<le> i" |
|
65 shows "a\<bullet>i \<le> x\<bullet>i" "x\<bullet>i \<le> b\<bullet>i" |
|
66 using assms |
|
67 unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i] |
|
68 by (auto intro!: ordered_comm_monoid_add_class.setsum_mono mult_right_mono simp: eucl_le) |
|
69 |
|
70 lemma inner_nonneg_nonneg: |
|
71 shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a \<bullet> b" |
|
72 using interval_inner_leI[of a 0 a b] |
|
73 by auto |
|
74 |
|
75 lemma inner_Basis_mono: |
|
76 shows "a \<le> b \<Longrightarrow> c \<in> Basis \<Longrightarrow> a \<bullet> c \<le> b \<bullet> c" |
|
77 by (simp add: eucl_le) |
|
78 |
|
79 lemma Basis_nonneg[intro, simp]: "i \<in> Basis \<Longrightarrow> 0 \<le> i" |
|
80 by (auto simp: eucl_le inner_Basis) |
|
81 |
|
82 lemma Sup_eq_maximum_componentwise: |
|
83 fixes s::"'a set" |
|
84 assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b" |
|
85 assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> x \<bullet> b \<le> X \<bullet> b" |
|
86 assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s" |
|
87 shows "Sup s = X" |
|
88 using assms |
|
89 unfolding eucl_Sup euclidean_representation_setsum |
|
90 by (auto intro!: conditionally_complete_lattice_class.cSup_eq_maximum) |
|
91 |
|
92 lemma Inf_eq_minimum_componentwise: |
|
93 assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b" |
|
94 assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> X \<bullet> b \<le> x \<bullet> b" |
|
95 assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s" |
|
96 shows "Inf s = X" |
|
97 using assms |
|
98 unfolding eucl_Inf euclidean_representation_setsum |
|
99 by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum) |
|
100 |
|
101 end |
|
102 |
|
103 lemma |
|
104 compact_attains_Inf_componentwise: |
|
105 fixes b::"'a::ordered_euclidean_space" |
|
106 assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X" |
|
107 obtains x where "x \<in> X" "x \<bullet> b = Inf X \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b" |
|
108 proof atomize_elim |
|
109 let ?proj = "(\<lambda>x. x \<bullet> b) ` X" |
|
110 from assms have "compact ?proj" "?proj \<noteq> {}" |
|
111 by (auto intro!: compact_continuous_image continuous_intros) |
|
112 from compact_attains_inf[OF this] |
|
113 obtain s x |
|
114 where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> s \<le> t" |
|
115 and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b" |
|
116 by auto |
|
117 hence "Inf ?proj = x \<bullet> b" |
|
118 by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum) |
|
119 hence "x \<bullet> b = Inf X \<bullet> b" |
|
120 by (auto simp: eucl_Inf inner_setsum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> setsum.delta |
|
121 cong: if_cong) |
|
122 with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Inf X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> x \<bullet> b \<le> y \<bullet> b)" by blast |
|
123 qed |
|
124 |
|
125 lemma |
|
126 compact_attains_Sup_componentwise: |
|
127 fixes b::"'a::ordered_euclidean_space" |
|
128 assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X" |
|
129 obtains x where "x \<in> X" "x \<bullet> b = Sup X \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b" |
|
130 proof atomize_elim |
|
131 let ?proj = "(\<lambda>x. x \<bullet> b) ` X" |
|
132 from assms have "compact ?proj" "?proj \<noteq> {}" |
|
133 by (auto intro!: compact_continuous_image continuous_intros) |
|
134 from compact_attains_sup[OF this] |
|
135 obtain s x |
|
136 where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> t \<le> s" |
|
137 and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b" |
|
138 by auto |
|
139 hence "Sup ?proj = x \<bullet> b" |
|
140 by (auto intro!: cSup_eq_maximum) |
|
141 hence "x \<bullet> b = Sup X \<bullet> b" |
|
142 by (auto simp: eucl_Sup[where 'a='a] inner_setsum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> setsum.delta |
|
143 cong: if_cong) |
|
144 with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Sup X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> y \<bullet> b \<le> x \<bullet> b)" by blast |
|
145 qed |
|
146 |
|
147 lemma (in order) atLeastatMost_empty'[simp]: |
|
148 "(~ a <= b) \<Longrightarrow> {a..b} = {}" |
|
149 by (auto) |
|
150 |
|
151 instance real :: ordered_euclidean_space |
|
152 by standard auto |
|
153 |
|
154 lemma in_Basis_prod_iff: |
|
155 fixes i::"'a::euclidean_space*'b::euclidean_space" |
|
156 shows "i \<in> Basis \<longleftrightarrow> fst i = 0 \<and> snd i \<in> Basis \<or> snd i = 0 \<and> fst i \<in> Basis" |
|
157 by (cases i) (auto simp: Basis_prod_def) |
|
158 |
|
159 instantiation prod :: (abs, abs) abs |
|
160 begin |
|
161 |
|
162 definition "\<bar>x\<bar> = (\<bar>fst x\<bar>, \<bar>snd x\<bar>)" |
|
163 |
|
164 instance .. |
|
165 |
|
166 end |
|
167 |
|
168 instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space |
|
169 by standard |
|
170 (auto intro!: add_mono simp add: euclidean_representation_setsum' Ball_def inner_prod_def |
|
171 in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def |
|
172 inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a] |
|
173 eucl_le[where 'a='b] abs_prod_def abs_inner) |
|
174 |
|
175 text\<open>Instantiation for intervals on \<open>ordered_euclidean_space\<close>\<close> |
|
176 |
|
177 lemma |
|
178 fixes a :: "'a::ordered_euclidean_space" |
|
179 shows cbox_interval: "cbox a b = {a..b}" |
|
180 and interval_cbox: "{a..b} = cbox a b" |
|
181 and eucl_le_atMost: "{x. \<forall>i\<in>Basis. x \<bullet> i <= a \<bullet> i} = {..a}" |
|
182 and eucl_le_atLeast: "{x. \<forall>i\<in>Basis. a \<bullet> i <= x \<bullet> i} = {a..}" |
|
183 by (auto simp: eucl_le[where 'a='a] eucl_less_def box_def cbox_def) |
|
184 |
|
185 lemma closed_eucl_atLeastAtMost[simp, intro]: |
|
186 fixes a :: "'a::ordered_euclidean_space" |
|
187 shows "closed {a..b}" |
|
188 by (simp add: cbox_interval[symmetric] closed_cbox) |
|
189 |
|
190 lemma closed_eucl_atMost[simp, intro]: |
|
191 fixes a :: "'a::ordered_euclidean_space" |
|
192 shows "closed {..a}" |
|
193 by (simp add: eucl_le_atMost[symmetric]) |
|
194 |
|
195 lemma closed_eucl_atLeast[simp, intro]: |
|
196 fixes a :: "'a::ordered_euclidean_space" |
|
197 shows "closed {a..}" |
|
198 by (simp add: eucl_le_atLeast[symmetric]) |
|
199 |
|
200 lemma bounded_closed_interval: |
|
201 fixes a :: "'a::ordered_euclidean_space" |
|
202 shows "bounded {a .. b}" |
|
203 using bounded_cbox[of a b] |
|
204 by (metis interval_cbox) |
|
205 |
|
206 lemma convex_closed_interval: |
|
207 fixes a :: "'a::ordered_euclidean_space" |
|
208 shows "convex {a .. b}" |
|
209 using convex_box[of a b] |
|
210 by (metis interval_cbox) |
|
211 |
|
212 lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a .. b} = |
|
213 (if {a .. b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a .. m *\<^sub>R b} else {m *\<^sub>R b .. m *\<^sub>R a})" |
|
214 using image_smult_cbox[of m a b] |
|
215 by (simp add: cbox_interval) |
|
216 |
|
217 lemma is_interval_closed_interval: |
|
218 "is_interval {a .. (b::'a::ordered_euclidean_space)}" |
|
219 by (metis cbox_interval is_interval_cbox) |
|
220 |
|
221 lemma compact_interval: |
|
222 fixes a b::"'a::ordered_euclidean_space" |
|
223 shows "compact {a .. b}" |
|
224 by (metis compact_cbox interval_cbox) |
|
225 |
|
226 lemma homeomorphic_closed_intervals: |
|
227 fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d |
|
228 assumes "box a b \<noteq> {}" and "box c d \<noteq> {}" |
|
229 shows "(cbox a b) homeomorphic (cbox c d)" |
|
230 apply (rule homeomorphic_convex_compact) |
|
231 using assms apply auto |
|
232 done |
|
233 |
|
234 lemma homeomorphic_closed_intervals_real: |
|
235 fixes a::real and b and c::real and d |
|
236 assumes "a<b" and "c<d" |
|
237 shows "{a..b} homeomorphic {c..d}" |
|
238 by (metis assms compact_interval continuous_on_id convex_real_interval(5) emptyE homeomorphic_convex_compact interior_atLeastAtMost_real mvt) |
|
239 |
|
240 no_notation |
|
241 eucl_less (infix "<e" 50) |
|
242 |
|
243 lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)" |
|
244 by (auto intro: setsum_nonneg) |
|
245 |
|
246 lemma content_closed_interval: |
|
247 fixes a :: "'a::ordered_euclidean_space" |
|
248 assumes "a \<le> b" |
|
249 shows "content {a .. b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)" |
|
250 using content_cbox[of a b] assms |
|
251 by (simp add: cbox_interval eucl_le[where 'a='a]) |
|
252 |
|
253 lemma integrable_const_ivl[intro]: |
|
254 fixes a::"'a::ordered_euclidean_space" |
|
255 shows "(\<lambda>x. c) integrable_on {a .. b}" |
|
256 unfolding cbox_interval[symmetric] |
|
257 by (rule integrable_const) |
|
258 |
|
259 lemma integrable_on_subinterval: |
|
260 fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach" |
|
261 assumes "f integrable_on s" |
|
262 and "{a .. b} \<subseteq> s" |
|
263 shows "f integrable_on {a .. b}" |
|
264 using integrable_on_subcbox[of f s a b] assms |
|
265 by (simp add: cbox_interval) |
|
266 |
|
267 lemma |
|
268 fixes a b::"'a::ordered_euclidean_space" |
|
269 shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)" |
|
270 and bdd_below_cbox[intro, simp]: "bdd_below (cbox a b)" |
|
271 and bdd_above_box[intro, simp]: "bdd_above (box a b)" |
|
272 and bdd_below_box[intro, simp]: "bdd_below (box a b)" |
|
273 unfolding atomize_conj |
|
274 by (metis bdd_above_Icc bdd_above_mono bdd_below_Icc bdd_below_mono bounded_box |
|
275 bounded_subset_cbox interval_cbox) |
|
276 |
|
277 instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space |
|
278 begin |
|
279 |
|
280 definition "inf x y = (\<chi> i. inf (x $ i) (y $ i))" |
|
281 definition "sup x y = (\<chi> i. sup (x $ i) (y $ i))" |
|
282 definition "Inf X = (\<chi> i. (INF x:X. x $ i))" |
|
283 definition "Sup X = (\<chi> i. (SUP x:X. x $ i))" |
|
284 definition "\<bar>x\<bar> = (\<chi> i. \<bar>x $ i\<bar>)" |
|
285 |
|
286 instance |
|
287 apply standard |
|
288 unfolding euclidean_representation_setsum' |
|
289 apply (auto simp: less_eq_vec_def inf_vec_def sup_vec_def Inf_vec_def Sup_vec_def inner_axis |
|
290 Basis_vec_def inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left |
|
291 inner_Basis_SUP_left eucl_le[where 'a='a] less_le_not_le abs_vec_def abs_inner) |
|
292 done |
|
293 |
|
294 end |
|
295 |
|
296 lemma ANR_interval [iff]: |
|
297 fixes a :: "'a::ordered_euclidean_space" |
|
298 shows "ANR{a..b}" |
|
299 by (simp add: interval_cbox) |
|
300 |
|
301 lemma ENR_interval [iff]: |
|
302 fixes a :: "'a::ordered_euclidean_space" |
|
303 shows "ENR{a..b}" |
|
304 by (auto simp: interval_cbox) |
|
305 |
|
306 end |
|
307 |