author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 69544 | 5aa5a8d6e5b5 |
child 69611 | 42cc3609fedf |
permissions | -rw-r--r-- |
63938 | 1 |
(* Author: L C Paulson, University of Cambridge |
33175 | 2 |
Author: Amine Chaieb, University of Cambridge |
3 |
Author: Robert Himmelmann, TU Muenchen |
|
44075 | 4 |
Author: Brian Huffman, Portland State University |
33175 | 5 |
*) |
6 |
||
69516
09bb8f470959
most of Topology_Euclidean_Space (now Elementary_Topology) requires fewer dependencies
immler
parents:
69508
diff
changeset
|
7 |
section \<open>Elementary Topology in Euclidean Space\<close> |
33175 | 8 |
|
9 |
theory Topology_Euclidean_Space |
|
69516
09bb8f470959
most of Topology_Euclidean_Space (now Elementary_Topology) requires fewer dependencies
immler
parents:
69508
diff
changeset
|
10 |
imports |
69544
5aa5a8d6e5b5
split off theorems involving classes below metric_space and real_normed_vector
immler
parents:
69516
diff
changeset
|
11 |
Elementary_Normed_Spaces |
69516
09bb8f470959
most of Topology_Euclidean_Space (now Elementary_Topology) requires fewer dependencies
immler
parents:
69508
diff
changeset
|
12 |
Linear_Algebra |
09bb8f470959
most of Topology_Euclidean_Space (now Elementary_Topology) requires fewer dependencies
immler
parents:
69508
diff
changeset
|
13 |
Norm_Arith |
51343
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
14 |
begin |
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51342
diff
changeset
|
15 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
16 |
lemma euclidean_dist_l2: |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
17 |
fixes x y :: "'a :: euclidean_space" |
67155 | 18 |
shows "dist x y = L2_set (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis" |
19 |
unfolding dist_norm norm_eq_sqrt_inner L2_set_def |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
20 |
by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
21 |
|
67685
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
22 |
lemma norm_nth_le: "norm (x \<bullet> i) \<le> norm x" if "i \<in> Basis" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
23 |
proof - |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
24 |
have "(x \<bullet> i)\<^sup>2 = (\<Sum>i\<in>{i}. (x \<bullet> i)\<^sup>2)" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
25 |
by simp |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
26 |
also have "\<dots> \<le> (\<Sum>i\<in>Basis. (x \<bullet> i)\<^sup>2)" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
27 |
by (intro sum_mono2) (auto simp: that) |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
28 |
finally show ?thesis |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
29 |
unfolding norm_conv_dist euclidean_dist_l2[of x] L2_set_def |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
30 |
by (auto intro!: real_le_rsqrt) |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
31 |
qed |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
32 |
|
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
33 |
|
60420 | 34 |
subsection \<open>Boxes\<close> |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
35 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
36 |
abbreviation One :: "'a::euclidean_space" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
37 |
where "One \<equiv> \<Sum>Basis" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
38 |
|
63114
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset
|
39 |
lemma One_non_0: assumes "One = (0::'a::euclidean_space)" shows False |
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset
|
40 |
proof - |
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset
|
41 |
have "dependent (Basis :: 'a set)" |
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset
|
42 |
apply (simp add: dependent_finite) |
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset
|
43 |
apply (rule_tac x="\<lambda>i. 1" in exI) |
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset
|
44 |
using SOME_Basis apply (auto simp: assms) |
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset
|
45 |
done |
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset
|
46 |
with independent_Basis show False by force |
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset
|
47 |
qed |
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset
|
48 |
|
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset
|
49 |
corollary One_neq_0[iff]: "One \<noteq> 0" |
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset
|
50 |
by (metis One_non_0) |
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset
|
51 |
|
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset
|
52 |
corollary Zero_neq_One[iff]: "0 \<noteq> One" |
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset
|
53 |
by (metis One_non_0) |
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63105
diff
changeset
|
54 |
|
67962 | 55 |
definition%important (in euclidean_space) eucl_less (infix "<e" 50) |
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
56 |
where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)" |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
57 |
|
67962 | 58 |
definition%important box_eucl_less: "box a b = {x. a <e x \<and> x <e b}" |
59 |
definition%important "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}" |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
60 |
|
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
61 |
lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}" |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
62 |
and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b" |
56188 | 63 |
and mem_box: "x \<in> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i)" |
64 |
"x \<in> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)" |
|
65 |
by (auto simp: box_eucl_less eucl_less_def cbox_def) |
|
66 |
||
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset
|
67 |
lemma cbox_Pair_eq: "cbox (a, c) (b, d) = cbox a b \<times> cbox c d" |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset
|
68 |
by (force simp: cbox_def Basis_prod_def) |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset
|
69 |
|
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset
|
70 |
lemma cbox_Pair_iff [iff]: "(x, y) \<in> cbox (a, c) (b, d) \<longleftrightarrow> x \<in> cbox a b \<and> y \<in> cbox c d" |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset
|
71 |
by (force simp: cbox_Pair_eq) |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset
|
72 |
|
65587
16a8991ab398
New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents:
65585
diff
changeset
|
73 |
lemma cbox_Complex_eq: "cbox (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (cbox a b \<times> cbox c d)" |
16a8991ab398
New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents:
65585
diff
changeset
|
74 |
apply (auto simp: cbox_def Basis_complex_def) |
16a8991ab398
New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents:
65585
diff
changeset
|
75 |
apply (rule_tac x = "(Re x, Im x)" in image_eqI) |
16a8991ab398
New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents:
65585
diff
changeset
|
76 |
using complex_eq by auto |
16a8991ab398
New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents:
65585
diff
changeset
|
77 |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset
|
78 |
lemma cbox_Pair_eq_0: "cbox (a, c) (b, d) = {} \<longleftrightarrow> cbox a b = {} \<or> cbox c d = {}" |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset
|
79 |
by (force simp: cbox_Pair_eq) |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset
|
80 |
|
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset
|
81 |
lemma swap_cbox_Pair [simp]: "prod.swap ` cbox (c, a) (d, b) = cbox (a,c) (b,d)" |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset
|
82 |
by auto |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset
|
83 |
|
56188 | 84 |
lemma mem_box_real[simp]: |
85 |
"(x::real) \<in> box a b \<longleftrightarrow> a < x \<and> x < b" |
|
86 |
"(x::real) \<in> cbox a b \<longleftrightarrow> a \<le> x \<and> x \<le> b" |
|
87 |
by (auto simp: mem_box) |
|
88 |
||
89 |
lemma box_real[simp]: |
|
90 |
fixes a b:: real |
|
91 |
shows "box a b = {a <..< b}" "cbox a b = {a .. b}" |
|
92 |
by auto |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
93 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
94 |
lemma box_Int_box: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
95 |
fixes a :: "'a::euclidean_space" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
96 |
shows "box a b \<inter> box c d = |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
97 |
box (\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
98 |
unfolding set_eq_iff and Int_iff and mem_box by auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
99 |
|
50087 | 100 |
lemma rational_boxes: |
61076 | 101 |
fixes x :: "'a::euclidean_space" |
53291 | 102 |
assumes "e > 0" |
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset
|
103 |
shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat>) \<and> x \<in> box a b \<and> box a b \<subseteq> ball x e" |
50087 | 104 |
proof - |
63040 | 105 |
define e' where "e' = e / (2 * sqrt (real (DIM ('a))))" |
53291 | 106 |
then have e: "e' > 0" |
56541 | 107 |
using assms by (auto simp: DIM_positive) |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
108 |
have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i") |
50087 | 109 |
proof |
53255 | 110 |
fix i |
111 |
from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e |
|
112 |
show "?th i" by auto |
|
50087 | 113 |
qed |
55522 | 114 |
from choice[OF this] obtain a where |
115 |
a: "\<forall>xa. a xa \<in> \<rat> \<and> a xa < x \<bullet> xa \<and> x \<bullet> xa - a xa < e'" .. |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
116 |
have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i") |
50087 | 117 |
proof |
53255 | 118 |
fix i |
119 |
from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e |
|
120 |
show "?th i" by auto |
|
50087 | 121 |
qed |
55522 | 122 |
from choice[OF this] obtain b where |
123 |
b: "\<forall>xa. b xa \<in> \<rat> \<and> x \<bullet> xa < b xa \<and> b xa - x \<bullet> xa < e'" .. |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
124 |
let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
125 |
show ?thesis |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
126 |
proof (rule exI[of _ ?a], rule exI[of _ ?b], safe) |
53255 | 127 |
fix y :: 'a |
128 |
assume *: "y \<in> box ?a ?b" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52625
diff
changeset
|
129 |
have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)" |
67155 | 130 |
unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2) |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
131 |
also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))" |
64267 | 132 |
proof (rule real_sqrt_less_mono, rule sum_strict_mono) |
53255 | 133 |
fix i :: "'a" |
134 |
assume i: "i \<in> Basis" |
|
135 |
have "a i < y\<bullet>i \<and> y\<bullet>i < b i" |
|
136 |
using * i by (auto simp: box_def) |
|
137 |
moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'" |
|
138 |
using a by auto |
|
139 |
moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'" |
|
140 |
using b by auto |
|
141 |
ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'" |
|
142 |
by auto |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
143 |
then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))" |
50087 | 144 |
unfolding e'_def by (auto simp: dist_real_def) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52625
diff
changeset
|
145 |
then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2" |
50087 | 146 |
by (rule power_strict_mono) auto |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52625
diff
changeset
|
147 |
then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)" |
50087 | 148 |
by (simp add: power_divide) |
149 |
qed auto |
|
53255 | 150 |
also have "\<dots> = e" |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset
|
151 |
using \<open>0 < e\<close> by simp |
53255 | 152 |
finally show "y \<in> ball x e" |
153 |
by (auto simp: ball_def) |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
154 |
qed (insert a b, auto simp: box_def) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
155 |
qed |
51103 | 156 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
157 |
lemma open_UNION_box: |
61076 | 158 |
fixes M :: "'a::euclidean_space set" |
53282 | 159 |
assumes "open M" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
160 |
defines "a' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
161 |
defines "b' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52625
diff
changeset
|
162 |
defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (a' f) (b' f) \<subseteq> M}" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
163 |
shows "M = (\<Union>f\<in>I. box (a' f) (b' f))" |
52624 | 164 |
proof - |
60462 | 165 |
have "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))" if "x \<in> M" for x |
166 |
proof - |
|
52624 | 167 |
obtain e where e: "e > 0" "ball x e \<subseteq> M" |
60420 | 168 |
using openE[OF \<open>open M\<close> \<open>x \<in> M\<close>] by auto |
53282 | 169 |
moreover obtain a b where ab: |
170 |
"x \<in> box a b" |
|
171 |
"\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>" |
|
172 |
"\<forall>i\<in>Basis. b \<bullet> i \<in> \<rat>" |
|
173 |
"box a b \<subseteq> ball x e" |
|
52624 | 174 |
using rational_boxes[OF e(1)] by metis |
60462 | 175 |
ultimately show ?thesis |
52624 | 176 |
by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"]) |
177 |
(auto simp: euclidean_representation I_def a'_def b'_def) |
|
60462 | 178 |
qed |
52624 | 179 |
then show ?thesis by (auto simp: I_def) |
180 |
qed |
|
181 |
||
66154
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
182 |
corollary open_countable_Union_open_box: |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
183 |
fixes S :: "'a :: euclidean_space set" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
184 |
assumes "open S" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
185 |
obtains \<D> where "countable \<D>" "\<D> \<subseteq> Pow S" "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = box a b" "\<Union>\<D> = S" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
186 |
proof - |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
187 |
let ?a = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
188 |
let ?b = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
189 |
let ?I = "{f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (?a f) (?b f) \<subseteq> S}" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
190 |
let ?\<D> = "(\<lambda>f. box (?a f) (?b f)) ` ?I" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
191 |
show ?thesis |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
192 |
proof |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
193 |
have "countable ?I" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
194 |
by (simp add: countable_PiE countable_rat) |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
195 |
then show "countable ?\<D>" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
196 |
by blast |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
197 |
show "\<Union>?\<D> = S" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
198 |
using open_UNION_box [OF assms] by metis |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
199 |
qed auto |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
200 |
qed |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
201 |
|
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
202 |
lemma rational_cboxes: |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
203 |
fixes x :: "'a::euclidean_space" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
204 |
assumes "e > 0" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
205 |
shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat>) \<and> x \<in> cbox a b \<and> cbox a b \<subseteq> ball x e" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
206 |
proof - |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
207 |
define e' where "e' = e / (2 * sqrt (real (DIM ('a))))" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
208 |
then have e: "e' > 0" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
209 |
using assms by auto |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
210 |
have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i") |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
211 |
proof |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
212 |
fix i |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
213 |
from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
214 |
show "?th i" by auto |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
215 |
qed |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
216 |
from choice[OF this] obtain a where |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
217 |
a: "\<forall>u. a u \<in> \<rat> \<and> a u < x \<bullet> u \<and> x \<bullet> u - a u < e'" .. |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
218 |
have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i") |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
219 |
proof |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
220 |
fix i |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
221 |
from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
222 |
show "?th i" by auto |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
223 |
qed |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
224 |
from choice[OF this] obtain b where |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
225 |
b: "\<forall>u. b u \<in> \<rat> \<and> x \<bullet> u < b u \<and> b u - x \<bullet> u < e'" .. |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
226 |
let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
227 |
show ?thesis |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
228 |
proof (rule exI[of _ ?a], rule exI[of _ ?b], safe) |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
229 |
fix y :: 'a |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
230 |
assume *: "y \<in> cbox ?a ?b" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
231 |
have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)" |
67155 | 232 |
unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2) |
66154
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
233 |
also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
234 |
proof (rule real_sqrt_less_mono, rule sum_strict_mono) |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
235 |
fix i :: "'a" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
236 |
assume i: "i \<in> Basis" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
237 |
have "a i \<le> y\<bullet>i \<and> y\<bullet>i \<le> b i" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
238 |
using * i by (auto simp: cbox_def) |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
239 |
moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
240 |
using a by auto |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
241 |
moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
242 |
using b by auto |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
243 |
ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
244 |
by auto |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
245 |
then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
246 |
unfolding e'_def by (auto simp: dist_real_def) |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
247 |
then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
248 |
by (rule power_strict_mono) auto |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
249 |
then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
250 |
by (simp add: power_divide) |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
251 |
qed auto |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
252 |
also have "\<dots> = e" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
253 |
using \<open>0 < e\<close> by simp |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
254 |
finally show "y \<in> ball x e" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
255 |
by (auto simp: ball_def) |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
256 |
next |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
257 |
show "x \<in> cbox (\<Sum>i\<in>Basis. a i *\<^sub>R i) (\<Sum>i\<in>Basis. b i *\<^sub>R i)" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
258 |
using a b less_imp_le by (auto simp: cbox_def) |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
259 |
qed (use a b cbox_def in auto) |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
260 |
qed |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
261 |
|
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
262 |
lemma open_UNION_cbox: |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
263 |
fixes M :: "'a::euclidean_space set" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
264 |
assumes "open M" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
265 |
defines "a' \<equiv> \<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
266 |
defines "b' \<equiv> \<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
267 |
defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. cbox (a' f) (b' f) \<subseteq> M}" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
268 |
shows "M = (\<Union>f\<in>I. cbox (a' f) (b' f))" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
269 |
proof - |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
270 |
have "x \<in> (\<Union>f\<in>I. cbox (a' f) (b' f))" if "x \<in> M" for x |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
271 |
proof - |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
272 |
obtain e where e: "e > 0" "ball x e \<subseteq> M" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
273 |
using openE[OF \<open>open M\<close> \<open>x \<in> M\<close>] by auto |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
274 |
moreover obtain a b where ab: "x \<in> cbox a b" "\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
275 |
"\<forall>i \<in> Basis. b \<bullet> i \<in> \<rat>" "cbox a b \<subseteq> ball x e" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
276 |
using rational_cboxes[OF e(1)] by metis |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
277 |
ultimately show ?thesis |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
278 |
by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"]) |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
279 |
(auto simp: euclidean_representation I_def a'_def b'_def) |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
280 |
qed |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
281 |
then show ?thesis by (auto simp: I_def) |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
282 |
qed |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
283 |
|
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
284 |
corollary open_countable_Union_open_cbox: |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
285 |
fixes S :: "'a :: euclidean_space set" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
286 |
assumes "open S" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
287 |
obtains \<D> where "countable \<D>" "\<D> \<subseteq> Pow S" "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = cbox a b" "\<Union>\<D> = S" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
288 |
proof - |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
289 |
let ?a = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
290 |
let ?b = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
291 |
let ?I = "{f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. cbox (?a f) (?b f) \<subseteq> S}" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
292 |
let ?\<D> = "(\<lambda>f. cbox (?a f) (?b f)) ` ?I" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
293 |
show ?thesis |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
294 |
proof |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
295 |
have "countable ?I" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
296 |
by (simp add: countable_PiE countable_rat) |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
297 |
then show "countable ?\<D>" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
298 |
by blast |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
299 |
show "\<Union>?\<D> = S" |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
300 |
using open_UNION_cbox [OF assms] by metis |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
301 |
qed auto |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
302 |
qed |
bc5e6461f759
Tidying up integration theory and some new theorems
paulson <lp15@cam.ac.uk>
parents:
66112
diff
changeset
|
303 |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
304 |
lemma box_eq_empty: |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
305 |
fixes a :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
306 |
shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
307 |
and "(cbox a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
308 |
proof - |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
309 |
{ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
310 |
fix i x |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
311 |
assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
312 |
then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
313 |
unfolding mem_box by (auto simp: box_def) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
314 |
then have "a\<bullet>i < b\<bullet>i" by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
315 |
then have False using as by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
316 |
} |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
317 |
moreover |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
318 |
{ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
319 |
assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
320 |
let ?x = "(1/2) *\<^sub>R (a + b)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
321 |
{ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
322 |
fix i :: 'a |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
323 |
assume i: "i \<in> Basis" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
324 |
have "a\<bullet>i < b\<bullet>i" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
325 |
using as[THEN bspec[where x=i]] i by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
326 |
then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
327 |
by (auto simp: inner_add_left) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
328 |
} |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
329 |
then have "box a b \<noteq> {}" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
330 |
using mem_box(1)[of "?x" a b] by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
331 |
} |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
332 |
ultimately show ?th1 by blast |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
333 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
334 |
{ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
335 |
fix i x |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
336 |
assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>cbox a b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
337 |
then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
338 |
unfolding mem_box by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
339 |
then have "a\<bullet>i \<le> b\<bullet>i" by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
340 |
then have False using as by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
341 |
} |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
342 |
moreover |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
343 |
{ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
344 |
assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
345 |
let ?x = "(1/2) *\<^sub>R (a + b)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
346 |
{ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
347 |
fix i :: 'a |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
348 |
assume i:"i \<in> Basis" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
349 |
have "a\<bullet>i \<le> b\<bullet>i" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
350 |
using as[THEN bspec[where x=i]] i by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
351 |
then have "a\<bullet>i \<le> ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i \<le> b\<bullet>i" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
352 |
by (auto simp: inner_add_left) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
353 |
} |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
354 |
then have "cbox a b \<noteq> {}" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
355 |
using mem_box(2)[of "?x" a b] by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
356 |
} |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
357 |
ultimately show ?th2 by blast |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
358 |
qed |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
359 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
360 |
lemma box_ne_empty: |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
361 |
fixes a :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
362 |
shows "cbox a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
363 |
and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
364 |
unfolding box_eq_empty[of a b] by fastforce+ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
365 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
366 |
lemma |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
367 |
fixes a :: "'a::euclidean_space" |
66112
0e640e04fc56
New theorems; stronger theorems; tidier theorems. Also some renaming
paulson <lp15@cam.ac.uk>
parents:
66089
diff
changeset
|
368 |
shows cbox_sing [simp]: "cbox a a = {a}" |
0e640e04fc56
New theorems; stronger theorems; tidier theorems. Also some renaming
paulson <lp15@cam.ac.uk>
parents:
66089
diff
changeset
|
369 |
and box_sing [simp]: "box a a = {}" |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
370 |
unfolding set_eq_iff mem_box eq_iff [symmetric] |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
371 |
by (auto intro!: euclidean_eqI[where 'a='a]) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
372 |
(metis all_not_in_conv nonempty_Basis) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
373 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
374 |
lemma subset_box_imp: |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
375 |
fixes a :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
376 |
shows "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> cbox c d \<subseteq> cbox a b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
377 |
and "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> cbox c d \<subseteq> box a b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
378 |
and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> cbox a b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
379 |
and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> box a b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
380 |
unfolding subset_eq[unfolded Ball_def] unfolding mem_box |
58757 | 381 |
by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+ |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
382 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
383 |
lemma box_subset_cbox: |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
384 |
fixes a :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
385 |
shows "box a b \<subseteq> cbox a b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
386 |
unfolding subset_eq [unfolded Ball_def] mem_box |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
387 |
by (fast intro: less_imp_le) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
388 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
389 |
lemma subset_box: |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
390 |
fixes a :: "'a::euclidean_space" |
64539 | 391 |
shows "cbox c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th1) |
392 |
and "cbox c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2) |
|
393 |
and "box c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3) |
|
394 |
and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4) |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
395 |
proof - |
68120 | 396 |
let ?lesscd = "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i" |
397 |
let ?lerhs = "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" |
|
398 |
show ?th1 ?th2 |
|
399 |
by (fastforce simp: mem_box)+ |
|
400 |
have acdb: "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" |
|
401 |
if i: "i \<in> Basis" and box: "box c d \<subseteq> cbox a b" and cd: "\<And>i. i \<in> Basis \<Longrightarrow> c\<bullet>i < d\<bullet>i" for i |
|
402 |
proof - |
|
403 |
have "box c d \<noteq> {}" |
|
404 |
using that |
|
405 |
unfolding box_eq_empty by force |
|
406 |
{ let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((min (a\<bullet>j) (d\<bullet>j))+c\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a" |
|
407 |
assume *: "a\<bullet>i > c\<bullet>i" |
|
408 |
then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j" if "j \<in> Basis" for j |
|
409 |
using cd that by (fastforce simp add: i *) |
|
410 |
then have "?x \<in> box c d" |
|
411 |
unfolding mem_box by auto |
|
412 |
moreover have "?x \<notin> cbox a b" |
|
413 |
using i cd * by (force simp: mem_box) |
|
414 |
ultimately have False using box by auto |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
415 |
} |
68120 | 416 |
then have "a\<bullet>i \<le> c\<bullet>i" by force |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
417 |
moreover |
68120 | 418 |
{ let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((max (b\<bullet>j) (c\<bullet>j))+d\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a" |
419 |
assume *: "b\<bullet>i < d\<bullet>i" |
|
420 |
then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j" if "j \<in> Basis" for j |
|
421 |
using cd that by (fastforce simp add: i *) |
|
422 |
then have "?x \<in> box c d" |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
423 |
unfolding mem_box by auto |
68120 | 424 |
moreover have "?x \<notin> cbox a b" |
425 |
using i cd * by (force simp: mem_box) |
|
426 |
ultimately have False using box by auto |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
427 |
} |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
428 |
then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto |
68120 | 429 |
ultimately show ?thesis by auto |
430 |
qed |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
431 |
show ?th3 |
68120 | 432 |
using acdb by (fastforce simp add: mem_box) |
433 |
have acdb': "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" |
|
434 |
if "i \<in> Basis" "box c d \<subseteq> box a b" "\<And>i. i \<in> Basis \<Longrightarrow> c\<bullet>i < d\<bullet>i" for i |
|
435 |
using box_subset_cbox[of a b] that acdb by auto |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
436 |
show ?th4 |
68120 | 437 |
using acdb' by (fastforce simp add: mem_box) |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
438 |
qed |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
439 |
|
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
440 |
lemma eq_cbox: "cbox a b = cbox c d \<longleftrightarrow> cbox a b = {} \<and> cbox c d = {} \<or> a = c \<and> b = d" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
441 |
(is "?lhs = ?rhs") |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
442 |
proof |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
443 |
assume ?lhs |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
444 |
then have "cbox a b \<subseteq> cbox c d" "cbox c d \<subseteq> cbox a b" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
445 |
by auto |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
446 |
then show ?rhs |
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset
|
447 |
by (force simp: subset_box box_eq_empty intro: antisym euclidean_eqI) |
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
448 |
next |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
449 |
assume ?rhs |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
450 |
then show ?lhs |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
451 |
by force |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
452 |
qed |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
453 |
|
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
454 |
lemma eq_cbox_box [simp]: "cbox a b = box c d \<longleftrightarrow> cbox a b = {} \<and> box c d = {}" |
64539 | 455 |
(is "?lhs \<longleftrightarrow> ?rhs") |
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
456 |
proof |
68120 | 457 |
assume L: ?lhs |
458 |
then have "cbox a b \<subseteq> box c d" "box c d \<subseteq> cbox a b" |
|
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
459 |
by auto |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
460 |
then show ?rhs |
63957
c3da799b1b45
HOL-Analysis: move gauges and (tagged) divisions to its own theory file
hoelzl
parents:
63955
diff
changeset
|
461 |
apply (simp add: subset_box) |
68120 | 462 |
using L box_ne_empty box_sing apply (fastforce simp add:) |
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
463 |
done |
68120 | 464 |
qed force |
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
465 |
|
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
466 |
lemma eq_box_cbox [simp]: "box a b = cbox c d \<longleftrightarrow> box a b = {} \<and> cbox c d = {}" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
467 |
by (metis eq_cbox_box) |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
468 |
|
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
469 |
lemma eq_box: "box a b = box c d \<longleftrightarrow> box a b = {} \<and> box c d = {} \<or> a = c \<and> b = d" |
64539 | 470 |
(is "?lhs \<longleftrightarrow> ?rhs") |
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
471 |
proof |
68120 | 472 |
assume L: ?lhs |
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
473 |
then have "box a b \<subseteq> box c d" "box c d \<subseteq> box a b" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
474 |
by auto |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
475 |
then show ?rhs |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
476 |
apply (simp add: subset_box) |
68120 | 477 |
using box_ne_empty(2) L |
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
478 |
apply auto |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
479 |
apply (meson euclidean_eqI less_eq_real_def not_less)+ |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
480 |
done |
68120 | 481 |
qed force |
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
482 |
|
66466
aec5d9c88d69
More lemmas for HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
66453
diff
changeset
|
483 |
lemma subset_box_complex: |
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset
|
484 |
"cbox a b \<subseteq> cbox c d \<longleftrightarrow> |
66466
aec5d9c88d69
More lemmas for HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
66453
diff
changeset
|
485 |
(Re a \<le> Re b \<and> Im a \<le> Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d" |
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset
|
486 |
"cbox a b \<subseteq> box c d \<longleftrightarrow> |
66466
aec5d9c88d69
More lemmas for HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
66453
diff
changeset
|
487 |
(Re a \<le> Re b \<and> Im a \<le> Im b) \<longrightarrow> Re a > Re c \<and> Im a > Im c \<and> Re b < Re d \<and> Im b < Im d" |
aec5d9c88d69
More lemmas for HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
66453
diff
changeset
|
488 |
"box a b \<subseteq> cbox c d \<longleftrightarrow> |
aec5d9c88d69
More lemmas for HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
66453
diff
changeset
|
489 |
(Re a < Re b \<and> Im a < Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d" |
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset
|
490 |
"box a b \<subseteq> box c d \<longleftrightarrow> |
66466
aec5d9c88d69
More lemmas for HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
66453
diff
changeset
|
491 |
(Re a < Re b \<and> Im a < Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d" |
aec5d9c88d69
More lemmas for HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
66453
diff
changeset
|
492 |
by (subst subset_box; force simp: Basis_complex_def)+ |
aec5d9c88d69
More lemmas for HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
66453
diff
changeset
|
493 |
|
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
494 |
lemma Int_interval: |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
495 |
fixes a :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
496 |
shows "cbox a b \<inter> cbox c d = |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
497 |
cbox (\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
498 |
unfolding set_eq_iff and Int_iff and mem_box |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
499 |
by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
500 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
501 |
lemma disjoint_interval: |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
502 |
fixes a::"'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
503 |
shows "cbox a b \<inter> cbox c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i < c\<bullet>i \<or> d\<bullet>i < a\<bullet>i))" (is ?th1) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
504 |
and "cbox a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th2) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
505 |
and "box a b \<inter> cbox c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th3) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
506 |
and "box a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th4) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
507 |
proof - |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
508 |
let ?z = "(\<Sum>i\<in>Basis. (((max (a\<bullet>i) (c\<bullet>i)) + (min (b\<bullet>i) (d\<bullet>i))) / 2) *\<^sub>R i)::'a" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
509 |
have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow> |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
510 |
(\<And>i x :: 'a. i \<in> Basis \<Longrightarrow> P i \<Longrightarrow> Q x i) \<Longrightarrow> (\<forall>x. \<exists>i\<in>Basis. Q x i) \<longleftrightarrow> (\<exists>i\<in>Basis. P i)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
511 |
by blast |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
512 |
note * = set_eq_iff Int_iff empty_iff mem_box ball_conj_distrib[symmetric] eq_False ball_simps(10) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
513 |
show ?th1 unfolding * by (intro **) auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
514 |
show ?th2 unfolding * by (intro **) auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
515 |
show ?th3 unfolding * by (intro **) auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
516 |
show ?th4 unfolding * by (intro **) auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
517 |
qed |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
518 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
519 |
lemma UN_box_eq_UNIV: "(\<Union>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One)) = UNIV" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
520 |
proof - |
61942 | 521 |
have "\<bar>x \<bullet> b\<bar> < real_of_int (\<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil> + 1)" |
60462 | 522 |
if [simp]: "b \<in> Basis" for x b :: 'a |
523 |
proof - |
|
61942 | 524 |
have "\<bar>x \<bullet> b\<bar> \<le> real_of_int \<lceil>\<bar>x \<bullet> b\<bar>\<rceil>" |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset
|
525 |
by (rule le_of_int_ceiling) |
61942 | 526 |
also have "\<dots> \<le> real_of_int \<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil>" |
59587
8ea7b22525cb
Removed the obsolete functions "natfloor" and "natceiling"
nipkow
parents:
58877
diff
changeset
|
527 |
by (auto intro!: ceiling_mono) |
61942 | 528 |
also have "\<dots> < real_of_int (\<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil> + 1)" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
529 |
by simp |
60462 | 530 |
finally show ?thesis . |
531 |
qed |
|
532 |
then have "\<exists>n::nat. \<forall>b\<in>Basis. \<bar>x \<bullet> b\<bar> < real n" for x :: 'a |
|
59587
8ea7b22525cb
Removed the obsolete functions "natfloor" and "natceiling"
nipkow
parents:
58877
diff
changeset
|
533 |
by (metis order.strict_trans reals_Archimedean2) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
534 |
moreover have "\<And>x b::'a. \<And>n::nat. \<bar>x \<bullet> b\<bar> < real n \<longleftrightarrow> - real n < x \<bullet> b \<and> x \<bullet> b < real n" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
535 |
by auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
536 |
ultimately show ?thesis |
64267 | 537 |
by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
538 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
539 |
|
69516
09bb8f470959
most of Topology_Euclidean_Space (now Elementary_Topology) requires fewer dependencies
immler
parents:
69508
diff
changeset
|
540 |
|
69508 | 541 |
subsection \<open>General Intervals\<close> |
67962 | 542 |
|
543 |
definition%important "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow> |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
544 |
(\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
545 |
|
67685
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
546 |
lemma is_interval_1: |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
547 |
"is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
548 |
unfolding is_interval_def by auto |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
549 |
|
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
550 |
lemma is_interval_inter: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
551 |
unfolding is_interval_def |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
552 |
by blast |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
553 |
|
66089
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
554 |
lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1) |
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
555 |
and is_interval_box [simp]: "is_interval (box a b)" (is ?th2) |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
556 |
unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
557 |
by (meson order_trans le_less_trans less_le_trans less_trans)+ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
558 |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset
|
559 |
lemma is_interval_empty [iff]: "is_interval {}" |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset
|
560 |
unfolding is_interval_def by simp |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset
|
561 |
|
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset
|
562 |
lemma is_interval_univ [iff]: "is_interval UNIV" |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset
|
563 |
unfolding is_interval_def by simp |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
564 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
565 |
lemma mem_is_intervalI: |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
566 |
assumes "is_interval s" |
64539 | 567 |
and "a \<in> s" "b \<in> s" |
568 |
and "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i \<or> b \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> a \<bullet> i" |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
569 |
shows "x \<in> s" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
570 |
by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)]) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
571 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
572 |
lemma interval_subst: |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
573 |
fixes S::"'a::euclidean_space set" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
574 |
assumes "is_interval S" |
64539 | 575 |
and "x \<in> S" "y j \<in> S" |
576 |
and "j \<in> Basis" |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
577 |
shows "(\<Sum>i\<in>Basis. (if i = j then y i \<bullet> i else x \<bullet> i) *\<^sub>R i) \<in> S" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
578 |
by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
579 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
580 |
lemma mem_box_componentwiseI: |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
581 |
fixes S::"'a::euclidean_space set" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
582 |
assumes "is_interval S" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
583 |
assumes "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<in> ((\<lambda>x. x \<bullet> i) ` S)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
584 |
shows "x \<in> S" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
585 |
proof - |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
586 |
from assms have "\<forall>i \<in> Basis. \<exists>s \<in> S. x \<bullet> i = s \<bullet> i" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
587 |
by auto |
64539 | 588 |
with finite_Basis obtain s and bs::"'a list" |
589 |
where s: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i = s i \<bullet> i" "\<And>i. i \<in> Basis \<Longrightarrow> s i \<in> S" |
|
590 |
and bs: "set bs = Basis" "distinct bs" |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
591 |
by (metis finite_distinct_list) |
64539 | 592 |
from nonempty_Basis s obtain j where j: "j \<in> Basis" "s j \<in> S" |
593 |
by blast |
|
63040 | 594 |
define y where |
595 |
"y = rec_list (s j) (\<lambda>j _ Y. (\<Sum>i\<in>Basis. (if i = j then s i \<bullet> i else Y \<bullet> i) *\<^sub>R i))" |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
596 |
have "x = (\<Sum>i\<in>Basis. (if i \<in> set bs then s i \<bullet> i else s j \<bullet> i) *\<^sub>R i)" |
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset
|
597 |
using bs by (auto simp: s(1)[symmetric] euclidean_representation) |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
598 |
also have [symmetric]: "y bs = \<dots>" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
599 |
using bs(2) bs(1)[THEN equalityD1] |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
600 |
by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a]) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
601 |
also have "y bs \<in> S" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
602 |
using bs(1)[THEN equalityD1] |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
603 |
apply (induct bs) |
64539 | 604 |
apply (auto simp: y_def j) |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
605 |
apply (rule interval_subst[OF assms(1)]) |
64539 | 606 |
apply (auto simp: s) |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
607 |
done |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
608 |
finally show ?thesis . |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
609 |
qed |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
610 |
|
63007
aa894a49f77d
new theorems about convex hulls, etc.; also, renamed some theorems
paulson <lp15@cam.ac.uk>
parents:
62948
diff
changeset
|
611 |
lemma cbox01_nonempty [simp]: "cbox 0 One \<noteq> {}" |
64267 | 612 |
by (simp add: box_ne_empty inner_Basis inner_sum_left sum_nonneg) |
63007
aa894a49f77d
new theorems about convex hulls, etc.; also, renamed some theorems
paulson <lp15@cam.ac.uk>
parents:
62948
diff
changeset
|
613 |
|
aa894a49f77d
new theorems about convex hulls, etc.; also, renamed some theorems
paulson <lp15@cam.ac.uk>
parents:
62948
diff
changeset
|
614 |
lemma box01_nonempty [simp]: "box 0 One \<noteq> {}" |
66089
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
615 |
by (simp add: box_ne_empty inner_Basis inner_sum_left) |
63075
60a42a4166af
lemmas about dimension, hyperplanes, span, etc.
paulson <lp15@cam.ac.uk>
parents:
63040
diff
changeset
|
616 |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64758
diff
changeset
|
617 |
lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64758
diff
changeset
|
618 |
using nonempty_Basis box01_nonempty box_eq_empty(1) box_ne_empty(1) by blast |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64758
diff
changeset
|
619 |
|
66089
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
620 |
lemma interval_subset_is_interval: |
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
621 |
assumes "is_interval S" |
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
622 |
shows "cbox a b \<subseteq> S \<longleftrightarrow> cbox a b = {} \<or> a \<in> S \<and> b \<in> S" (is "?lhs = ?rhs") |
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
623 |
proof |
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
624 |
assume ?lhs |
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
625 |
then show ?rhs using box_ne_empty(1) mem_box(2) by fastforce |
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
626 |
next |
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
627 |
assume ?rhs |
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
628 |
have "cbox a b \<subseteq> S" if "a \<in> S" "b \<in> S" |
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
629 |
using assms unfolding is_interval_def |
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
630 |
apply (clarsimp simp add: mem_box) |
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
631 |
using that by blast |
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
632 |
with \<open>?rhs\<close> show ?lhs |
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
633 |
by blast |
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
634 |
qed |
def95e0bc529
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
paulson <lp15@cam.ac.uk>
parents:
65587
diff
changeset
|
635 |
|
67685
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
636 |
lemma is_real_interval_union: |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
637 |
"is_interval (X \<union> Y)" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
638 |
if X: "is_interval X" and Y: "is_interval Y" and I: "(X \<noteq> {} \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> X \<inter> Y \<noteq> {})" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
639 |
for X Y::"real set" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
640 |
proof - |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
641 |
consider "X \<noteq> {}" "Y \<noteq> {}" | "X = {}" | "Y = {}" by blast |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
642 |
then show ?thesis |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
643 |
proof cases |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
644 |
case 1 |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
645 |
then obtain r where "r \<in> X \<or> X \<inter> Y = {}" "r \<in> Y \<or> X \<inter> Y = {}" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
646 |
by blast |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
647 |
then show ?thesis |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
648 |
using I 1 X Y unfolding is_interval_1 |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
649 |
by (metis (full_types) Un_iff le_cases) |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
650 |
qed (use that in auto) |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
651 |
qed |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
652 |
|
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
653 |
lemma is_interval_translationI: |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
654 |
assumes "is_interval X" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
655 |
shows "is_interval ((+) x ` X)" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
656 |
unfolding is_interval_def |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
657 |
proof safe |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
658 |
fix b d e |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
659 |
assume "b \<in> X" "d \<in> X" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
660 |
"\<forall>i\<in>Basis. (x + b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + d) \<bullet> i \<or> |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
661 |
(x + d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + b) \<bullet> i" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
662 |
hence "e - x \<in> X" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
663 |
by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "e - x"]) |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
664 |
(auto simp: algebra_simps) |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
665 |
thus "e \<in> (+) x ` X" by force |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
666 |
qed |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
667 |
|
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
668 |
lemma is_interval_uminusI: |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
669 |
assumes "is_interval X" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
670 |
shows "is_interval (uminus ` X)" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
671 |
unfolding is_interval_def |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
672 |
proof safe |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
673 |
fix b d e |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
674 |
assume "b \<in> X" "d \<in> X" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
675 |
"\<forall>i\<in>Basis. (- b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- d) \<bullet> i \<or> |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
676 |
(- d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- b) \<bullet> i" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
677 |
hence "- e \<in> X" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
678 |
by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "- e"]) |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
679 |
(auto simp: algebra_simps) |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
680 |
thus "e \<in> uminus ` X" by force |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
681 |
qed |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
682 |
|
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
683 |
lemma is_interval_uminus[simp]: "is_interval (uminus ` x) = is_interval x" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
684 |
using is_interval_uminusI[of x] is_interval_uminusI[of "uminus ` x"] |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
685 |
by (auto simp: image_image) |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
686 |
|
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
687 |
lemma is_interval_neg_translationI: |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
688 |
assumes "is_interval X" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
689 |
shows "is_interval ((-) x ` X)" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
690 |
proof - |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
691 |
have "(-) x ` X = (+) x ` uminus ` X" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
692 |
by (force simp: algebra_simps) |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
693 |
also have "is_interval \<dots>" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
694 |
by (metis is_interval_uminusI is_interval_translationI assms) |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
695 |
finally show ?thesis . |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
696 |
qed |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
697 |
|
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
698 |
lemma is_interval_translation[simp]: |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
699 |
"is_interval ((+) x ` X) = is_interval X" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
700 |
using is_interval_neg_translationI[of "(+) x ` X" x] |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
701 |
by (auto intro!: is_interval_translationI simp: image_image) |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
702 |
|
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
703 |
lemma is_interval_minus_translation[simp]: |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
704 |
shows "is_interval ((-) x ` X) = is_interval X" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
705 |
proof - |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
706 |
have "(-) x ` X = (+) x ` uminus ` X" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
707 |
by (force simp: algebra_simps) |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
708 |
also have "is_interval \<dots> = is_interval X" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
709 |
by simp |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
710 |
finally show ?thesis . |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
711 |
qed |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
712 |
|
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
713 |
lemma is_interval_minus_translation'[simp]: |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
714 |
shows "is_interval ((\<lambda>x. x - c) ` X) = is_interval X" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
715 |
using is_interval_translation[of "-c" X] |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
716 |
by (metis image_cong uminus_add_conv_diff) |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67613
diff
changeset
|
717 |
|
62127 | 718 |
lemma compact_lemma: |
719 |
fixes f :: "nat \<Rightarrow> 'a::euclidean_space" |
|
720 |
assumes "bounded (range f)" |
|
721 |
shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r. |
|
66447
a1f5c5c26fa6
Replaced subseq with strict_mono
eberlm <eberlm@in.tum.de>
parents:
66408
diff
changeset
|
722 |
strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)" |
62127 | 723 |
by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"]) |
724 |
(auto intro!: assms bounded_linear_inner_left bounded_linear_image |
|
725 |
simp: euclidean_representation) |
|
726 |
||
67962 | 727 |
instance%important euclidean_space \<subseteq> heine_borel |
728 |
proof%unimportant |
|
50998 | 729 |
fix f :: "nat \<Rightarrow> 'a" |
730 |
assume f: "bounded (range f)" |
|
66447
a1f5c5c26fa6
Replaced subseq with strict_mono
eberlm <eberlm@in.tum.de>
parents:
66408
diff
changeset
|
731 |
then obtain l::'a and r where r: "strict_mono r" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
732 |
and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially" |
50998 | 733 |
using compact_lemma [OF f] by blast |
52624 | 734 |
{ |
735 |
fix e::real |
|
53282 | 736 |
assume "e > 0" |
56541 | 737 |
hence "e / real_of_nat DIM('a) > 0" by (simp add: DIM_positive) |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
738 |
with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))) sequentially" |
33175 | 739 |
by simp |
740 |
moreover |
|
52624 | 741 |
{ |
742 |
fix n |
|
743 |
assume n: "\<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))" |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
744 |
have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i))" |
52624 | 745 |
apply (subst euclidean_dist_l2) |
746 |
using zero_le_dist |
|
67155 | 747 |
apply (rule L2_set_le_sum) |
53282 | 748 |
done |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
749 |
also have "\<dots> < (\<Sum>i\<in>(Basis::'a set). e / (real_of_nat DIM('a)))" |
64267 | 750 |
apply (rule sum_strict_mono) |
52624 | 751 |
using n |
53282 | 752 |
apply auto |
753 |
done |
|
754 |
finally have "dist (f (r n)) l < e" |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50324
diff
changeset
|
755 |
by auto |
33175 | 756 |
} |
757 |
ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially" |
|
61810 | 758 |
by (rule eventually_mono) |
33175 | 759 |
} |
61973 | 760 |
then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially" |
52624 | 761 |
unfolding o_def tendsto_iff by simp |
66447
a1f5c5c26fa6
Replaced subseq with strict_mono
eberlm <eberlm@in.tum.de>
parents:
66408
diff
changeset
|
762 |
with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" |
52624 | 763 |
by auto |
33175 | 764 |
qed |
765 |
||
44632 | 766 |
instance euclidean_space \<subseteq> banach .. |
767 |
||
53282 | 768 |
|
67962 | 769 |
subsubsection%unimportant \<open>Structural rules for pointwise continuity\<close> |
33175 | 770 |
|
51361
21e5b6efb317
changed continuous_intros into a named theorems collection
hoelzl
parents:
51351
diff
changeset
|
771 |
lemma continuous_infnorm[continuous_intros]: |
53282 | 772 |
"continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))" |
44647
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44632
diff
changeset
|
773 |
unfolding continuous_def by (rule tendsto_infnorm) |
33175 | 774 |
|
51361
21e5b6efb317
changed continuous_intros into a named theorems collection
hoelzl
parents:
51351
diff
changeset
|
775 |
lemma continuous_inner[continuous_intros]: |
53282 | 776 |
assumes "continuous F f" |
777 |
and "continuous F g" |
|
44647
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44632
diff
changeset
|
778 |
shows "continuous F (\<lambda>x. inner (f x) (g x))" |
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44632
diff
changeset
|
779 |
using assms unfolding continuous_def by (rule tendsto_inner) |
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44632
diff
changeset
|
780 |
|
69516
09bb8f470959
most of Topology_Euclidean_Space (now Elementary_Topology) requires fewer dependencies
immler
parents:
69508
diff
changeset
|
781 |
|
67962 | 782 |
subsubsection%unimportant \<open>Structural rules for setwise continuity\<close> |
33175 | 783 |
|
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56290
diff
changeset
|
784 |
lemma continuous_on_infnorm[continuous_intros]: |
53282 | 785 |
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))" |
44647
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44632
diff
changeset
|
786 |
unfolding continuous_on by (fast intro: tendsto_infnorm) |
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44632
diff
changeset
|
787 |
|
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56290
diff
changeset
|
788 |
lemma continuous_on_inner[continuous_intros]: |
44531
1d477a2b1572
replace some continuous_on lemmas with more general versions
huffman
parents:
44530
diff
changeset
|
789 |
fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner" |
53282 | 790 |
assumes "continuous_on s f" |
791 |
and "continuous_on s g" |
|
44531
1d477a2b1572
replace some continuous_on lemmas with more general versions
huffman
parents:
44530
diff
changeset
|
792 |
shows "continuous_on s (\<lambda>x. inner (f x) (g x))" |
1d477a2b1572
replace some continuous_on lemmas with more general versions
huffman
parents:
44530
diff
changeset
|
793 |
using bounded_bilinear_inner assms |
1d477a2b1572
replace some continuous_on lemmas with more general versions
huffman
parents:
44530
diff
changeset
|
794 |
by (rule bounded_bilinear.continuous_on) |
1d477a2b1572
replace some continuous_on lemmas with more general versions
huffman
parents:
44530
diff
changeset
|
795 |
|
67962 | 796 |
subsection%unimportant \<open>Intervals\<close> |
60974
6a6f15d8fbc4
New material and fixes related to the forthcoming Stone-Weierstrass development
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
797 |
|
60420 | 798 |
text \<open>Openness of halfspaces.\<close> |
33175 | 799 |
|
800 |
lemma open_halfspace_lt: "open {x. inner a x < b}" |
|
63332 | 801 |
by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) |
33175 | 802 |
|
803 |
lemma open_halfspace_gt: "open {x. inner a x > b}" |
|
63332 | 804 |
by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) |
33175 | 805 |
|
53282 | 806 |
lemma open_halfspace_component_lt: "open {x::'a::euclidean_space. x\<bullet>i < a}" |
63332 | 807 |
by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) |
33175 | 808 |
|
53282 | 809 |
lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. x\<bullet>i > a}" |
63332 | 810 |
by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) |
33175 | 811 |
|
60420 | 812 |
text \<open>This gives a simple derivation of limit component bounds.\<close> |
33175 | 813 |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
814 |
lemma open_box[intro]: "open (box a b)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
815 |
proof - |
67399 | 816 |
have "open (\<Inter>i\<in>Basis. ((\<bullet>) i) -` {a \<bullet> i <..< b \<bullet> i})" |
62533
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62466
diff
changeset
|
817 |
by (auto intro!: continuous_open_vimage continuous_inner continuous_ident continuous_const) |
67399 | 818 |
also have "(\<Inter>i\<in>Basis. ((\<bullet>) i) -` {a \<bullet> i <..< b \<bullet> i}) = box a b" |
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset
|
819 |
by (auto simp: box_def inner_commute) |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
820 |
finally show ?thesis . |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
821 |
qed |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
822 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
823 |
instance euclidean_space \<subseteq> second_countable_topology |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
824 |
proof |
63040 | 825 |
define a where "a f = (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real" |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
826 |
then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
827 |
by simp |
63040 | 828 |
define b where "b f = (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real" |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
829 |
then have b: "\<And>f. (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i) = b f" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
830 |
by simp |
63040 | 831 |
define B where "B = (\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^sub>E (\<rat> \<times> \<rat>))" |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
832 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
833 |
have "Ball B open" by (simp add: B_def open_box) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
834 |
moreover have "(\<forall>A. open A \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = A))" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
835 |
proof safe |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
836 |
fix A::"'a set" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
837 |
assume "open A" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
838 |
show "\<exists>B'\<subseteq>B. \<Union>B' = A" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
839 |
apply (rule exI[of _ "{b\<in>B. b \<subseteq> A}"]) |
60420 | 840 |
apply (subst (3) open_UNION_box[OF \<open>open A\<close>]) |
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset
|
841 |
apply (auto simp: a b B_def) |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
842 |
done |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
843 |
qed |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
844 |
ultimately |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
845 |
have "topological_basis B" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
846 |
unfolding topological_basis_def by blast |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
847 |
moreover |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
848 |
have "countable B" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
849 |
unfolding B_def |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
850 |
by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
851 |
ultimately show "\<exists>B::'a set set. countable B \<and> open = generate_topology B" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
852 |
by (blast intro: topological_basis_imp_subbasis) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
853 |
qed |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
854 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
855 |
instance euclidean_space \<subseteq> polish_space .. |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
856 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
857 |
lemma closed_cbox[intro]: |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
858 |
fixes a b :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
859 |
shows "closed (cbox a b)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
860 |
proof - |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
861 |
have "closed (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i})" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
862 |
by (intro closed_INT ballI continuous_closed_vimage allI |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
863 |
linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
864 |
also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i}) = cbox a b" |
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset
|
865 |
by (auto simp: cbox_def) |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
866 |
finally show "closed (cbox a b)" . |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
867 |
qed |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
868 |
|
62618
f7f2467ab854
Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset
|
869 |
lemma interior_cbox [simp]: |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
870 |
fixes a b :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
871 |
shows "interior (cbox a b) = box a b" (is "?L = ?R") |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
872 |
proof(rule subset_antisym) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
873 |
show "?R \<subseteq> ?L" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
874 |
using box_subset_cbox open_box |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
875 |
by (rule interior_maximal) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
876 |
{ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
877 |
fix x |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
878 |
assume "x \<in> interior (cbox a b)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
879 |
then obtain s where s: "open s" "x \<in> s" "s \<subseteq> cbox a b" .. |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
880 |
then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> cbox a b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
881 |
unfolding open_dist and subset_eq by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
882 |
{ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
883 |
fix i :: 'a |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
884 |
assume i: "i \<in> Basis" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
885 |
have "dist (x - (e / 2) *\<^sub>R i) x < e" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
886 |
and "dist (x + (e / 2) *\<^sub>R i) x < e" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
887 |
unfolding dist_norm |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
888 |
apply auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
889 |
unfolding norm_minus_cancel |
60420 | 890 |
using norm_Basis[OF i] \<open>e>0\<close> |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
891 |
apply auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
892 |
done |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
893 |
then have "a \<bullet> i \<le> (x - (e / 2) *\<^sub>R i) \<bullet> i" and "(x + (e / 2) *\<^sub>R i) \<bullet> i \<le> b \<bullet> i" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
894 |
using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]] |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
895 |
and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]] |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
896 |
unfolding mem_box |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
897 |
using i |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
898 |
by blast+ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
899 |
then have "a \<bullet> i < x \<bullet> i" and "x \<bullet> i < b \<bullet> i" |
60420 | 900 |
using \<open>e>0\<close> i |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
901 |
by (auto simp: inner_diff_left inner_Basis inner_add_left) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
902 |
} |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
903 |
then have "x \<in> box a b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
904 |
unfolding mem_box by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
905 |
} |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
906 |
then show "?L \<subseteq> ?R" .. |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
907 |
qed |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
908 |
|
63928
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63881
diff
changeset
|
909 |
lemma bounded_cbox [simp]: |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
910 |
fixes a :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
911 |
shows "bounded (cbox a b)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
912 |
proof - |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
913 |
let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
914 |
{ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
915 |
fix x :: "'a" |
68120 | 916 |
assume "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i" |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
917 |
then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b" |
68120 | 918 |
by (force simp: intro!: sum_mono) |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
919 |
then have "norm x \<le> ?b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
920 |
using norm_le_l1[of x] by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
921 |
} |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
922 |
then show ?thesis |
68120 | 923 |
unfolding cbox_def bounded_iff by force |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
924 |
qed |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
925 |
|
62618
f7f2467ab854
Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset
|
926 |
lemma bounded_box [simp]: |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
927 |
fixes a :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
928 |
shows "bounded (box a b)" |
68120 | 929 |
using bounded_cbox[of a b] box_subset_cbox[of a b] bounded_subset[of "cbox a b" "box a b"] |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
930 |
by simp |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
931 |
|
62618
f7f2467ab854
Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset
|
932 |
lemma not_interval_UNIV [simp]: |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
933 |
fixes a :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
934 |
shows "cbox a b \<noteq> UNIV" "box a b \<noteq> UNIV" |
62618
f7f2467ab854
Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset
|
935 |
using bounded_box[of a b] bounded_cbox[of a b] by force+ |
f7f2467ab854
Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset
|
936 |
|
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
937 |
lemma not_interval_UNIV2 [simp]: |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
938 |
fixes a :: "'a::euclidean_space" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
939 |
shows "UNIV \<noteq> cbox a b" "UNIV \<noteq> box a b" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
940 |
using bounded_box[of a b] bounded_cbox[of a b] by force+ |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63938
diff
changeset
|
941 |
|
62618
f7f2467ab854
Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset
|
942 |
lemma compact_cbox [simp]: |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
943 |
fixes a :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
944 |
shows "compact (cbox a b)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
945 |
using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b] |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
946 |
by (auto simp: compact_eq_seq_compact_metric) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
947 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
948 |
lemma box_midpoint: |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
949 |
fixes a :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
950 |
assumes "box a b \<noteq> {}" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
951 |
shows "((1/2) *\<^sub>R (a + b)) \<in> box a b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
952 |
proof - |
68120 | 953 |
have "a \<bullet> i < ((1 / 2) *\<^sub>R (a + b)) \<bullet> i \<and> ((1 / 2) *\<^sub>R (a + b)) \<bullet> i < b \<bullet> i" if "i \<in> Basis" for i |
954 |
using assms that by (auto simp: inner_add_left box_ne_empty) |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
955 |
then show ?thesis unfolding mem_box by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
956 |
qed |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
957 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
958 |
lemma open_cbox_convex: |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
959 |
fixes x :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
960 |
assumes x: "x \<in> box a b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
961 |
and y: "y \<in> cbox a b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
962 |
and e: "0 < e" "e \<le> 1" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
963 |
shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
964 |
proof - |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
965 |
{ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
966 |
fix i :: 'a |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
967 |
assume i: "i \<in> Basis" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
968 |
have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
969 |
unfolding left_diff_distrib by simp |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
970 |
also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)" |
68120 | 971 |
proof (rule add_less_le_mono) |
972 |
show "e * (a \<bullet> i) < e * (x \<bullet> i)" |
|
973 |
using \<open>0 < e\<close> i mem_box(1) x by auto |
|
974 |
show "(1 - e) * (a \<bullet> i) \<le> (1 - e) * (y \<bullet> i)" |
|
975 |
by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y) |
|
976 |
qed |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
977 |
finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
978 |
unfolding inner_simps by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
979 |
moreover |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
980 |
{ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
981 |
have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
982 |
unfolding left_diff_distrib by simp |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
983 |
also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)" |
66827
c94531b5007d
Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
paulson <lp15@cam.ac.uk>
parents:
66794
diff
changeset
|
984 |
proof (rule add_less_le_mono) |
c94531b5007d
Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
paulson <lp15@cam.ac.uk>
parents:
66794
diff
changeset
|
985 |
show "e * (x \<bullet> i) < e * (b \<bullet> i)" |
68120 | 986 |
using \<open>0 < e\<close> i mem_box(1) x by auto |
66827
c94531b5007d
Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
paulson <lp15@cam.ac.uk>
parents:
66794
diff
changeset
|
987 |
show "(1 - e) * (y \<bullet> i) \<le> (1 - e) * (b \<bullet> i)" |
68120 | 988 |
by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y) |
66827
c94531b5007d
Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
paulson <lp15@cam.ac.uk>
parents:
66794
diff
changeset
|
989 |
qed |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
990 |
finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
991 |
unfolding inner_simps by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
992 |
} |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
993 |
ultimately have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i \<and> (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
994 |
by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
995 |
} |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
996 |
then show ?thesis |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
997 |
unfolding mem_box by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
998 |
qed |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
999 |
|
63881
b746b19197bd
lots of new results about topology, affine dimension etc
paulson <lp15@cam.ac.uk>
parents:
63627
diff
changeset
|
1000 |
lemma closure_cbox [simp]: "closure (cbox a b) = cbox a b" |
b746b19197bd
lots of new results about topology, affine dimension etc
paulson <lp15@cam.ac.uk>
parents:
63627
diff
changeset
|
1001 |
by (simp add: closed_cbox) |
b746b19197bd
lots of new results about topology, affine dimension etc
paulson <lp15@cam.ac.uk>
parents:
63627
diff
changeset
|
1002 |
|
b746b19197bd
lots of new results about topology, affine dimension etc
paulson <lp15@cam.ac.uk>
parents:
63627
diff
changeset
|
1003 |
lemma closure_box [simp]: |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1004 |
fixes a :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1005 |
assumes "box a b \<noteq> {}" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1006 |
shows "closure (box a b) = cbox a b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1007 |
proof - |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1008 |
have ab: "a <e b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1009 |
using assms by (simp add: eucl_less_def box_ne_empty) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1010 |
let ?c = "(1 / 2) *\<^sub>R (a + b)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1011 |
{ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1012 |
fix x |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1013 |
assume as:"x \<in> cbox a b" |
63040 | 1014 |
define f where [abs_def]: "f n = x + (inverse (real n + 1)) *\<^sub>R (?c - x)" for n |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1015 |
{ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1016 |
fix n |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1017 |
assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1018 |
have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1019 |
unfolding inverse_le_1_iff by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1020 |
have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x = |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1021 |
x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)" |
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset
|
1022 |
by (auto simp: algebra_simps) |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1023 |
then have "f n <e b" and "a <e f n" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1024 |
using open_cbox_convex[OF box_midpoint[OF assms] as *] |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1025 |
unfolding f_def by (auto simp: box_def eucl_less_def) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1026 |
then have False |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1027 |
using fn unfolding f_def using xc by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1028 |
} |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1029 |
moreover |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1030 |
{ |
61973 | 1031 |
assume "\<not> (f \<longlongrightarrow> x) sequentially" |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1032 |
{ |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1033 |
fix e :: real |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1034 |
assume "e > 0" |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset
|
1035 |
then obtain N :: nat where N: "inverse (real (N + 1)) < e" |
68120 | 1036 |
using reals_Archimedean by auto |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset
|
1037 |
have "inverse (real n + 1) < e" if "N \<le> n" for n |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset
|
1038 |
by (auto intro!: that le_less_trans [OF _ N]) |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1039 |
then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1040 |
} |
61973 | 1041 |
then have "((\<lambda>n. inverse (real n + 1)) \<longlongrightarrow> 0) sequentially" |
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset
|
1042 |
unfolding lim_sequentially by(auto simp: dist_norm) |
61973 | 1043 |
then have "(f \<longlongrightarrow> x) sequentially" |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1044 |
unfolding f_def |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1045 |
using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x] |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1046 |
using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1047 |
by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1048 |
} |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1049 |
ultimately have "x \<in> closure (box a b)" |
68120 | 1050 |
using as box_midpoint[OF assms] |
1051 |
unfolding closure_def islimpt_sequential |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1052 |
by (cases "x=?c") (auto simp: in_box_eucl_less) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1053 |
} |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1054 |
then show ?thesis |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1055 |
using closure_minimal[OF box_subset_cbox, of a b] by blast |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1056 |
qed |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1057 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1058 |
lemma bounded_subset_box_symmetric: |
68120 | 1059 |
fixes S :: "('a::euclidean_space) set" |
1060 |
assumes "bounded S" |
|
1061 |
obtains a where "S \<subseteq> box (-a) a" |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1062 |
proof - |
68120 | 1063 |
obtain b where "b>0" and b: "\<forall>x\<in>S. norm x \<le> b" |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1064 |
using assms[unfolded bounded_pos] by auto |
63040 | 1065 |
define a :: 'a where "a = (\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)" |
68120 | 1066 |
have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i" if "x \<in> S" and i: "i \<in> Basis" for x i |
1067 |
using b Basis_le_norm[OF i, of x] that by (auto simp: a_def) |
|
1068 |
then have "S \<subseteq> box (-a) a" |
|
1069 |
by (auto simp: simp add: box_def) |
|
1070 |
then show ?thesis .. |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1071 |
qed |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1072 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1073 |
lemma bounded_subset_cbox_symmetric: |
68120 | 1074 |
fixes S :: "('a::euclidean_space) set" |
1075 |
assumes "bounded S" |
|
1076 |
obtains a where "S \<subseteq> cbox (-a) a" |
|
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1077 |
proof - |
68120 | 1078 |
obtain a where "S \<subseteq> box (-a) a" |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1079 |
using bounded_subset_box_symmetric[OF assms] by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1080 |
then show ?thesis |
68120 | 1081 |
by (meson box_subset_cbox dual_order.trans that) |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1082 |
qed |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1083 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1084 |
lemma frontier_cbox: |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1085 |
fixes a b :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1086 |
shows "frontier (cbox a b) = cbox a b - box a b" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1087 |
unfolding frontier_def unfolding interior_cbox and closure_closed[OF closed_cbox] .. |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1088 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1089 |
lemma frontier_box: |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1090 |
fixes a b :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1091 |
shows "frontier (box a b) = (if box a b = {} then {} else cbox a b - box a b)" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1092 |
proof (cases "box a b = {}") |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1093 |
case True |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1094 |
then show ?thesis |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1095 |
using frontier_empty by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1096 |
next |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1097 |
case False |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1098 |
then show ?thesis |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1099 |
unfolding frontier_def and closure_box[OF False] and interior_open[OF open_box] |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1100 |
by auto |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1101 |
qed |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1102 |
|
66884
c2128ab11f61
Switching to inverse image and constant_on, plus some new material
paulson <lp15@cam.ac.uk>
parents:
66827
diff
changeset
|
1103 |
lemma Int_interval_mixed_eq_empty: |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1104 |
fixes a :: "'a::euclidean_space" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1105 |
assumes "box c d \<noteq> {}" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1106 |
shows "box a b \<inter> cbox c d = {} \<longleftrightarrow> box a b \<inter> box c d = {}" |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1107 |
unfolding closure_box[OF assms, symmetric] |
62843
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62623
diff
changeset
|
1108 |
unfolding open_Int_closure_eq_empty[OF open_box] .. |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1109 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1110 |
lemma eucl_less_eq_halfspaces: |
61076 | 1111 |
fixes a :: "'a::euclidean_space" |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1112 |
shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})" |
68120 | 1113 |
"{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})" |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1114 |
by (auto simp: eucl_less_def) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1115 |
|
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1116 |
lemma open_Collect_eucl_less[simp, intro]: |
61076 | 1117 |
fixes a :: "'a::euclidean_space" |
68120 | 1118 |
shows "open {x. x <e a}" "open {x. a <e x}" |
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1119 |
by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt) |
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset
|
1120 |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
1121 |
no_notation |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
1122 |
eucl_less (infix "<e" 50) |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
1123 |
|
33175 | 1124 |
end |