author | nipkow |
Fri, 11 Apr 2014 22:53:33 +0200 | |
changeset 56541 | 0e3abadbef39 |
parent 56536 | aefb4a8da31f |
child 58881 | b9556a055632 |
permissions | -rw-r--r-- |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
1 |
(* Title: HOL/Library/Product_Vector.thy |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
2 |
Author: Brian Huffman |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
3 |
*) |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
4 |
|
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
5 |
header {* Cartesian Products as Vector Spaces *} |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
6 |
|
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
7 |
theory Product_Vector |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
8 |
imports Inner_Product Product_plus |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
9 |
begin |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
10 |
|
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
11 |
subsection {* Product is a real vector space *} |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
12 |
|
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36661
diff
changeset
|
13 |
instantiation prod :: (real_vector, real_vector) real_vector |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
14 |
begin |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
15 |
|
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
16 |
definition scaleR_prod_def: |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
17 |
"scaleR r A = (scaleR r (fst A), scaleR r (snd A))" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
18 |
|
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
19 |
lemma fst_scaleR [simp]: "fst (scaleR r A) = scaleR r (fst A)" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
20 |
unfolding scaleR_prod_def by simp |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
21 |
|
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
22 |
lemma snd_scaleR [simp]: "snd (scaleR r A) = scaleR r (snd A)" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
23 |
unfolding scaleR_prod_def by simp |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
24 |
|
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
25 |
lemma scaleR_Pair [simp]: "scaleR r (a, b) = (scaleR r a, scaleR r b)" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
26 |
unfolding scaleR_prod_def by simp |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
27 |
|
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
28 |
instance proof |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
29 |
fix a b :: real and x y :: "'a \<times> 'b" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
30 |
show "scaleR a (x + y) = scaleR a x + scaleR a y" |
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
37678
diff
changeset
|
31 |
by (simp add: prod_eq_iff scaleR_right_distrib) |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
32 |
show "scaleR (a + b) x = scaleR a x + scaleR b x" |
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
37678
diff
changeset
|
33 |
by (simp add: prod_eq_iff scaleR_left_distrib) |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
34 |
show "scaleR a (scaleR b x) = scaleR (a * b) x" |
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
37678
diff
changeset
|
35 |
by (simp add: prod_eq_iff) |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
36 |
show "scaleR 1 x = x" |
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
37678
diff
changeset
|
37 |
by (simp add: prod_eq_iff) |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
38 |
qed |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
39 |
|
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
40 |
end |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
41 |
|
31415 | 42 |
subsection {* Product is a topological space *} |
43 |
||
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36661
diff
changeset
|
44 |
instantiation prod :: (topological_space, topological_space) topological_space |
31415 | 45 |
begin |
46 |
||
54779
d9edb711ef31
pragmatic executability of instance prod::{open,dist,norm}
immler
parents:
53930
diff
changeset
|
47 |
definition open_prod_def[code del]: |
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset
|
48 |
"open (S :: ('a \<times> 'b) set) \<longleftrightarrow> |
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset
|
49 |
(\<forall>x\<in>S. \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S)" |
31415 | 50 |
|
36332 | 51 |
lemma open_prod_elim: |
52 |
assumes "open S" and "x \<in> S" |
|
53 |
obtains A B where "open A" and "open B" and "x \<in> A \<times> B" and "A \<times> B \<subseteq> S" |
|
54 |
using assms unfolding open_prod_def by fast |
|
55 |
||
56 |
lemma open_prod_intro: |
|
57 |
assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S" |
|
58 |
shows "open S" |
|
59 |
using assms unfolding open_prod_def by fast |
|
60 |
||
31415 | 61 |
instance proof |
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset
|
62 |
show "open (UNIV :: ('a \<times> 'b) set)" |
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset
|
63 |
unfolding open_prod_def by auto |
31415 | 64 |
next |
65 |
fix S T :: "('a \<times> 'b) set" |
|
36332 | 66 |
assume "open S" "open T" |
67 |
show "open (S \<inter> T)" |
|
68 |
proof (rule open_prod_intro) |
|
69 |
fix x assume x: "x \<in> S \<inter> T" |
|
70 |
from x have "x \<in> S" by simp |
|
71 |
obtain Sa Sb where A: "open Sa" "open Sb" "x \<in> Sa \<times> Sb" "Sa \<times> Sb \<subseteq> S" |
|
72 |
using `open S` and `x \<in> S` by (rule open_prod_elim) |
|
73 |
from x have "x \<in> T" by simp |
|
74 |
obtain Ta Tb where B: "open Ta" "open Tb" "x \<in> Ta \<times> Tb" "Ta \<times> Tb \<subseteq> T" |
|
75 |
using `open T` and `x \<in> T` by (rule open_prod_elim) |
|
76 |
let ?A = "Sa \<inter> Ta" and ?B = "Sb \<inter> Tb" |
|
77 |
have "open ?A \<and> open ?B \<and> x \<in> ?A \<times> ?B \<and> ?A \<times> ?B \<subseteq> S \<inter> T" |
|
78 |
using A B by (auto simp add: open_Int) |
|
79 |
thus "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S \<inter> T" |
|
80 |
by fast |
|
81 |
qed |
|
31415 | 82 |
next |
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset
|
83 |
fix K :: "('a \<times> 'b) set set" |
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset
|
84 |
assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)" |
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset
|
85 |
unfolding open_prod_def by fast |
31415 | 86 |
qed |
87 |
||
88 |
end |
|
89 |
||
54890
cb892d835803
fundamental treatment of undefined vs. universally partial replaces code_abort
haftmann
parents:
54779
diff
changeset
|
90 |
declare [[code abort: "open::('a::topological_space*'b::topological_space) set \<Rightarrow> bool"]] |
54779
d9edb711ef31
pragmatic executability of instance prod::{open,dist,norm}
immler
parents:
53930
diff
changeset
|
91 |
|
31562 | 92 |
lemma open_Times: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<times> T)" |
93 |
unfolding open_prod_def by auto |
|
94 |
||
95 |
lemma fst_vimage_eq_Times: "fst -` S = S \<times> UNIV" |
|
96 |
by auto |
|
97 |
||
98 |
lemma snd_vimage_eq_Times: "snd -` S = UNIV \<times> S" |
|
99 |
by auto |
|
100 |
||
101 |
lemma open_vimage_fst: "open S \<Longrightarrow> open (fst -` S)" |
|
102 |
by (simp add: fst_vimage_eq_Times open_Times) |
|
103 |
||
104 |
lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)" |
|
105 |
by (simp add: snd_vimage_eq_Times open_Times) |
|
106 |
||
31568 | 107 |
lemma closed_vimage_fst: "closed S \<Longrightarrow> closed (fst -` S)" |
108 |
unfolding closed_open vimage_Compl [symmetric] |
|
109 |
by (rule open_vimage_fst) |
|
110 |
||
111 |
lemma closed_vimage_snd: "closed S \<Longrightarrow> closed (snd -` S)" |
|
112 |
unfolding closed_open vimage_Compl [symmetric] |
|
113 |
by (rule open_vimage_snd) |
|
114 |
||
115 |
lemma closed_Times: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)" |
|
116 |
proof - |
|
117 |
have "S \<times> T = (fst -` S) \<inter> (snd -` T)" by auto |
|
118 |
thus "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)" |
|
119 |
by (simp add: closed_vimage_fst closed_vimage_snd closed_Int) |
|
120 |
qed |
|
121 |
||
34110 | 122 |
lemma subset_fst_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> y \<in> B \<Longrightarrow> A \<subseteq> fst ` S" |
123 |
unfolding image_def subset_eq by force |
|
124 |
||
125 |
lemma subset_snd_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> x \<in> A \<Longrightarrow> B \<subseteq> snd ` S" |
|
126 |
unfolding image_def subset_eq by force |
|
127 |
||
128 |
lemma open_image_fst: assumes "open S" shows "open (fst ` S)" |
|
129 |
proof (rule openI) |
|
130 |
fix x assume "x \<in> fst ` S" |
|
131 |
then obtain y where "(x, y) \<in> S" by auto |
|
132 |
then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S" |
|
133 |
using `open S` unfolding open_prod_def by auto |
|
134 |
from `A \<times> B \<subseteq> S` `y \<in> B` have "A \<subseteq> fst ` S" by (rule subset_fst_imageI) |
|
135 |
with `open A` `x \<in> A` have "open A \<and> x \<in> A \<and> A \<subseteq> fst ` S" by simp |
|
136 |
then show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S" by - (rule exI) |
|
137 |
qed |
|
138 |
||
139 |
lemma open_image_snd: assumes "open S" shows "open (snd ` S)" |
|
140 |
proof (rule openI) |
|
141 |
fix y assume "y \<in> snd ` S" |
|
142 |
then obtain x where "(x, y) \<in> S" by auto |
|
143 |
then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S" |
|
144 |
using `open S` unfolding open_prod_def by auto |
|
145 |
from `A \<times> B \<subseteq> S` `x \<in> A` have "B \<subseteq> snd ` S" by (rule subset_snd_imageI) |
|
146 |
with `open B` `y \<in> B` have "open B \<and> y \<in> B \<and> B \<subseteq> snd ` S" by simp |
|
147 |
then show "\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> snd ` S" by - (rule exI) |
|
148 |
qed |
|
31568 | 149 |
|
44575 | 150 |
subsubsection {* Continuity of operations *} |
151 |
||
152 |
lemma tendsto_fst [tendsto_intros]: |
|
153 |
assumes "(f ---> a) F" |
|
154 |
shows "((\<lambda>x. fst (f x)) ---> fst a) F" |
|
155 |
proof (rule topological_tendstoI) |
|
156 |
fix S assume "open S" and "fst a \<in> S" |
|
157 |
then have "open (fst -` S)" and "a \<in> fst -` S" |
|
158 |
by (simp_all add: open_vimage_fst) |
|
159 |
with assms have "eventually (\<lambda>x. f x \<in> fst -` S) F" |
|
160 |
by (rule topological_tendstoD) |
|
161 |
then show "eventually (\<lambda>x. fst (f x) \<in> S) F" |
|
162 |
by simp |
|
163 |
qed |
|
164 |
||
165 |
lemma tendsto_snd [tendsto_intros]: |
|
166 |
assumes "(f ---> a) F" |
|
167 |
shows "((\<lambda>x. snd (f x)) ---> snd a) F" |
|
168 |
proof (rule topological_tendstoI) |
|
169 |
fix S assume "open S" and "snd a \<in> S" |
|
170 |
then have "open (snd -` S)" and "a \<in> snd -` S" |
|
171 |
by (simp_all add: open_vimage_snd) |
|
172 |
with assms have "eventually (\<lambda>x. f x \<in> snd -` S) F" |
|
173 |
by (rule topological_tendstoD) |
|
174 |
then show "eventually (\<lambda>x. snd (f x) \<in> S) F" |
|
175 |
by simp |
|
176 |
qed |
|
177 |
||
178 |
lemma tendsto_Pair [tendsto_intros]: |
|
179 |
assumes "(f ---> a) F" and "(g ---> b) F" |
|
180 |
shows "((\<lambda>x. (f x, g x)) ---> (a, b)) F" |
|
181 |
proof (rule topological_tendstoI) |
|
182 |
fix S assume "open S" and "(a, b) \<in> S" |
|
183 |
then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S" |
|
184 |
unfolding open_prod_def by fast |
|
185 |
have "eventually (\<lambda>x. f x \<in> A) F" |
|
186 |
using `(f ---> a) F` `open A` `a \<in> A` |
|
187 |
by (rule topological_tendstoD) |
|
188 |
moreover |
|
189 |
have "eventually (\<lambda>x. g x \<in> B) F" |
|
190 |
using `(g ---> b) F` `open B` `b \<in> B` |
|
191 |
by (rule topological_tendstoD) |
|
192 |
ultimately |
|
193 |
show "eventually (\<lambda>x. (f x, g x) \<in> S) F" |
|
194 |
by (rule eventually_elim2) |
|
195 |
(simp add: subsetD [OF `A \<times> B \<subseteq> S`]) |
|
196 |
qed |
|
197 |
||
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51002
diff
changeset
|
198 |
lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))" |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51002
diff
changeset
|
199 |
unfolding continuous_def by (rule tendsto_fst) |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51002
diff
changeset
|
200 |
|
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51002
diff
changeset
|
201 |
lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))" |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51002
diff
changeset
|
202 |
unfolding continuous_def by (rule tendsto_snd) |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51002
diff
changeset
|
203 |
|
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51002
diff
changeset
|
204 |
lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))" |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51002
diff
changeset
|
205 |
unfolding continuous_def by (rule tendsto_Pair) |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51002
diff
changeset
|
206 |
|
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56181
diff
changeset
|
207 |
lemma continuous_on_fst[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. fst (f x))" |
51644 | 208 |
unfolding continuous_on_def by (auto intro: tendsto_fst) |
209 |
||
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56181
diff
changeset
|
210 |
lemma continuous_on_snd[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. snd (f x))" |
51644 | 211 |
unfolding continuous_on_def by (auto intro: tendsto_snd) |
212 |
||
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56181
diff
changeset
|
213 |
lemma continuous_on_Pair[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. (f x, g x))" |
51644 | 214 |
unfolding continuous_on_def by (auto intro: tendsto_Pair) |
215 |
||
44575 | 216 |
lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a" |
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51002
diff
changeset
|
217 |
by (fact continuous_fst) |
44575 | 218 |
|
219 |
lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a" |
|
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51002
diff
changeset
|
220 |
by (fact continuous_snd) |
44575 | 221 |
|
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51002
diff
changeset
|
222 |
lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a" |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51002
diff
changeset
|
223 |
by (fact continuous_Pair) |
44575 | 224 |
|
225 |
subsubsection {* Separation axioms *} |
|
44214
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
226 |
|
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
227 |
lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B" |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
228 |
by (induct x) simp (* TODO: move elsewhere *) |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
229 |
|
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
230 |
instance prod :: (t0_space, t0_space) t0_space |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
231 |
proof |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
232 |
fix x y :: "'a \<times> 'b" assume "x \<noteq> y" |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
233 |
hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y" |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
234 |
by (simp add: prod_eq_iff) |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
235 |
thus "\<exists>U. open U \<and> (x \<in> U) \<noteq> (y \<in> U)" |
53930 | 236 |
by (fast dest: t0_space elim: open_vimage_fst open_vimage_snd) |
44214
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
237 |
qed |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
238 |
|
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
239 |
instance prod :: (t1_space, t1_space) t1_space |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
240 |
proof |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
241 |
fix x y :: "'a \<times> 'b" assume "x \<noteq> y" |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
242 |
hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y" |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
243 |
by (simp add: prod_eq_iff) |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
244 |
thus "\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U" |
53930 | 245 |
by (fast dest: t1_space elim: open_vimage_fst open_vimage_snd) |
44214
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
246 |
qed |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
247 |
|
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
248 |
instance prod :: (t2_space, t2_space) t2_space |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
249 |
proof |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
250 |
fix x y :: "'a \<times> 'b" assume "x \<noteq> y" |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
251 |
hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y" |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
252 |
by (simp add: prod_eq_iff) |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
253 |
thus "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}" |
53930 | 254 |
by (fast dest: hausdorff elim: open_vimage_fst open_vimage_snd) |
44214
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
255 |
qed |
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset
|
256 |
|
31339
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
257 |
subsection {* Product is a metric space *} |
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
258 |
|
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36661
diff
changeset
|
259 |
instantiation prod :: (metric_space, metric_space) metric_space |
31339
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
260 |
begin |
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
261 |
|
54779
d9edb711ef31
pragmatic executability of instance prod::{open,dist,norm}
immler
parents:
53930
diff
changeset
|
262 |
definition dist_prod_def[code del]: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51644
diff
changeset
|
263 |
"dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)" |
31339
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
264 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51644
diff
changeset
|
265 |
lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)" |
31339
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
266 |
unfolding dist_prod_def by simp |
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
267 |
|
36332 | 268 |
lemma dist_fst_le: "dist (fst x) (fst y) \<le> dist x y" |
53930 | 269 |
unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge1) |
36332 | 270 |
|
271 |
lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y" |
|
53930 | 272 |
unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2) |
36332 | 273 |
|
31339
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
274 |
instance proof |
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
275 |
fix x y :: "'a \<times> 'b" |
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
276 |
show "dist x y = 0 \<longleftrightarrow> x = y" |
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
37678
diff
changeset
|
277 |
unfolding dist_prod_def prod_eq_iff by simp |
31339
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
278 |
next |
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
279 |
fix x y z :: "'a \<times> 'b" |
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
280 |
show "dist x y \<le> dist x z + dist y z" |
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
281 |
unfolding dist_prod_def |
31563 | 282 |
by (intro order_trans [OF _ real_sqrt_sum_squares_triangle_ineq] |
283 |
real_sqrt_le_mono add_mono power_mono dist_triangle2 zero_le_dist) |
|
31415 | 284 |
next |
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset
|
285 |
fix S :: "('a \<times> 'b) set" |
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset
|
286 |
show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" |
31563 | 287 |
proof |
36332 | 288 |
assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" |
289 |
proof |
|
290 |
fix x assume "x \<in> S" |
|
291 |
obtain A B where "open A" "open B" "x \<in> A \<times> B" "A \<times> B \<subseteq> S" |
|
292 |
using `open S` and `x \<in> S` by (rule open_prod_elim) |
|
293 |
obtain r where r: "0 < r" "\<forall>y. dist y (fst x) < r \<longrightarrow> y \<in> A" |
|
294 |
using `open A` and `x \<in> A \<times> B` unfolding open_dist by auto |
|
295 |
obtain s where s: "0 < s" "\<forall>y. dist y (snd x) < s \<longrightarrow> y \<in> B" |
|
296 |
using `open B` and `x \<in> A \<times> B` unfolding open_dist by auto |
|
297 |
let ?e = "min r s" |
|
298 |
have "0 < ?e \<and> (\<forall>y. dist y x < ?e \<longrightarrow> y \<in> S)" |
|
299 |
proof (intro allI impI conjI) |
|
300 |
show "0 < min r s" by (simp add: r(1) s(1)) |
|
301 |
next |
|
302 |
fix y assume "dist y x < min r s" |
|
303 |
hence "dist y x < r" and "dist y x < s" |
|
304 |
by simp_all |
|
305 |
hence "dist (fst y) (fst x) < r" and "dist (snd y) (snd x) < s" |
|
306 |
by (auto intro: le_less_trans dist_fst_le dist_snd_le) |
|
307 |
hence "fst y \<in> A" and "snd y \<in> B" |
|
308 |
by (simp_all add: r(2) s(2)) |
|
309 |
hence "y \<in> A \<times> B" by (induct y, simp) |
|
310 |
with `A \<times> B \<subseteq> S` show "y \<in> S" .. |
|
311 |
qed |
|
312 |
thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" .. |
|
313 |
qed |
|
31563 | 314 |
next |
44575 | 315 |
assume *: "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" show "open S" |
316 |
proof (rule open_prod_intro) |
|
317 |
fix x assume "x \<in> S" |
|
318 |
then obtain e where "0 < e" and S: "\<forall>y. dist y x < e \<longrightarrow> y \<in> S" |
|
319 |
using * by fast |
|
320 |
def r \<equiv> "e / sqrt 2" and s \<equiv> "e / sqrt 2" |
|
321 |
from `0 < e` have "0 < r" and "0 < s" |
|
56541 | 322 |
unfolding r_def s_def by simp_all |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51644
diff
changeset
|
323 |
from `0 < e` have "e = sqrt (r\<^sup>2 + s\<^sup>2)" |
44575 | 324 |
unfolding r_def s_def by (simp add: power_divide) |
325 |
def A \<equiv> "{y. dist (fst x) y < r}" and B \<equiv> "{y. dist (snd x) y < s}" |
|
326 |
have "open A" and "open B" |
|
327 |
unfolding A_def B_def by (simp_all add: open_ball) |
|
328 |
moreover have "x \<in> A \<times> B" |
|
329 |
unfolding A_def B_def mem_Times_iff |
|
330 |
using `0 < r` and `0 < s` by simp |
|
331 |
moreover have "A \<times> B \<subseteq> S" |
|
332 |
proof (clarify) |
|
333 |
fix a b assume "a \<in> A" and "b \<in> B" |
|
334 |
hence "dist a (fst x) < r" and "dist b (snd x) < s" |
|
335 |
unfolding A_def B_def by (simp_all add: dist_commute) |
|
336 |
hence "dist (a, b) x < e" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51644
diff
changeset
|
337 |
unfolding dist_prod_def `e = sqrt (r\<^sup>2 + s\<^sup>2)` |
44575 | 338 |
by (simp add: add_strict_mono power_strict_mono) |
339 |
thus "(a, b) \<in> S" |
|
340 |
by (simp add: S) |
|
341 |
qed |
|
342 |
ultimately show "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S" by fast |
|
343 |
qed |
|
31563 | 344 |
qed |
31339
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
345 |
qed |
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
346 |
|
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
347 |
end |
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
348 |
|
54890
cb892d835803
fundamental treatment of undefined vs. universally partial replaces code_abort
haftmann
parents:
54779
diff
changeset
|
349 |
declare [[code abort: "dist::('a::metric_space*'b::metric_space)\<Rightarrow>('a*'b) \<Rightarrow> real"]] |
54779
d9edb711ef31
pragmatic executability of instance prod::{open,dist,norm}
immler
parents:
53930
diff
changeset
|
350 |
|
31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
351 |
lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))" |
53930 | 352 |
unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le]) |
31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
353 |
|
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
354 |
lemma Cauchy_snd: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. snd (X n))" |
53930 | 355 |
unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_snd_le]) |
31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
356 |
|
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
357 |
lemma Cauchy_Pair: |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
358 |
assumes "Cauchy X" and "Cauchy Y" |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
359 |
shows "Cauchy (\<lambda>n. (X n, Y n))" |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
360 |
proof (rule metric_CauchyI) |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
361 |
fix r :: real assume "0 < r" |
56541 | 362 |
hence "0 < r / sqrt 2" (is "0 < ?s") by simp |
31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
363 |
obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < ?s" |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
364 |
using metric_CauchyD [OF `Cauchy X` `0 < ?s`] .. |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
365 |
obtain N where N: "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (Y m) (Y n) < ?s" |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
366 |
using metric_CauchyD [OF `Cauchy Y` `0 < ?s`] .. |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
367 |
have "\<forall>m\<ge>max M N. \<forall>n\<ge>max M N. dist (X m, Y m) (X n, Y n) < r" |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
368 |
using M N by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair) |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
369 |
then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" .. |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
370 |
qed |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
371 |
|
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
372 |
subsection {* Product is a complete metric space *} |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
373 |
|
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36661
diff
changeset
|
374 |
instance prod :: (complete_space, complete_space) complete_space |
31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
375 |
proof |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
376 |
fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X" |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
377 |
have 1: "(\<lambda>n. fst (X n)) ----> lim (\<lambda>n. fst (X n))" |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
378 |
using Cauchy_fst [OF `Cauchy X`] |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
379 |
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
380 |
have 2: "(\<lambda>n. snd (X n)) ----> lim (\<lambda>n. snd (X n))" |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
381 |
using Cauchy_snd [OF `Cauchy X`] |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
382 |
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
383 |
have "X ----> (lim (\<lambda>n. fst (X n)), lim (\<lambda>n. snd (X n)))" |
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36332
diff
changeset
|
384 |
using tendsto_Pair [OF 1 2] by simp |
31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
385 |
then show "convergent X" |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
386 |
by (rule convergentI) |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
387 |
qed |
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
388 |
|
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
389 |
subsection {* Product is a normed vector space *} |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
390 |
|
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36661
diff
changeset
|
391 |
instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
392 |
begin |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
393 |
|
54779
d9edb711ef31
pragmatic executability of instance prod::{open,dist,norm}
immler
parents:
53930
diff
changeset
|
394 |
definition norm_prod_def[code del]: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51644
diff
changeset
|
395 |
"norm x = sqrt ((norm (fst x))\<^sup>2 + (norm (snd x))\<^sup>2)" |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
396 |
|
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
397 |
definition sgn_prod_def: |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
398 |
"sgn (x::'a \<times> 'b) = scaleR (inverse (norm x)) x" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
399 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51644
diff
changeset
|
400 |
lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<^sup>2 + (norm b)\<^sup>2)" |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
401 |
unfolding norm_prod_def by simp |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
402 |
|
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
403 |
instance proof |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
404 |
fix r :: real and x y :: "'a \<times> 'b" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
405 |
show "norm x = 0 \<longleftrightarrow> x = 0" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
406 |
unfolding norm_prod_def |
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
37678
diff
changeset
|
407 |
by (simp add: prod_eq_iff) |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
408 |
show "norm (x + y) \<le> norm x + norm y" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
409 |
unfolding norm_prod_def |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
410 |
apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq]) |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
411 |
apply (simp add: add_mono power_mono norm_triangle_ineq) |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
412 |
done |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
413 |
show "norm (scaleR r x) = \<bar>r\<bar> * norm x" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
414 |
unfolding norm_prod_def |
31587 | 415 |
apply (simp add: power_mult_distrib) |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44749
diff
changeset
|
416 |
apply (simp add: distrib_left [symmetric]) |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
417 |
apply (simp add: real_sqrt_mult_distrib) |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
418 |
done |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
419 |
show "sgn x = scaleR (inverse (norm x)) x" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
420 |
by (rule sgn_prod_def) |
31290 | 421 |
show "dist x y = norm (x - y)" |
31339
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
422 |
unfolding dist_prod_def norm_prod_def |
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset
|
423 |
by (simp add: dist_norm) |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
424 |
qed |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
425 |
|
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
426 |
end |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
427 |
|
54890
cb892d835803
fundamental treatment of undefined vs. universally partial replaces code_abort
haftmann
parents:
54779
diff
changeset
|
428 |
declare [[code abort: "norm::('a::real_normed_vector*'b::real_normed_vector) \<Rightarrow> real"]] |
54779
d9edb711ef31
pragmatic executability of instance prod::{open,dist,norm}
immler
parents:
53930
diff
changeset
|
429 |
|
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36661
diff
changeset
|
430 |
instance prod :: (banach, banach) banach .. |
31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset
|
431 |
|
44575 | 432 |
subsubsection {* Pair operations are linear *} |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
433 |
|
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset
|
434 |
lemma bounded_linear_fst: "bounded_linear fst" |
44127 | 435 |
using fst_add fst_scaleR |
436 |
by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def) |
|
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
437 |
|
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset
|
438 |
lemma bounded_linear_snd: "bounded_linear snd" |
44127 | 439 |
using snd_add snd_scaleR |
440 |
by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def) |
|
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
441 |
|
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
442 |
text {* TODO: move to NthRoot *} |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
443 |
lemma sqrt_add_le_add_sqrt: |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
444 |
assumes x: "0 \<le> x" and y: "0 \<le> y" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
445 |
shows "sqrt (x + y) \<le> sqrt x + sqrt y" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
446 |
apply (rule power2_le_imp_le) |
44749
5b1e1432c320
remove redundant lemma real_sum_squared_expand in favor of power2_sum
huffman
parents:
44575
diff
changeset
|
447 |
apply (simp add: power2_sum x y) |
44126 | 448 |
apply (simp add: x y) |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
449 |
done |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
450 |
|
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
451 |
lemma bounded_linear_Pair: |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
452 |
assumes f: "bounded_linear f" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
453 |
assumes g: "bounded_linear g" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
454 |
shows "bounded_linear (\<lambda>x. (f x, g x))" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
455 |
proof |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
456 |
interpret f: bounded_linear f by fact |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
457 |
interpret g: bounded_linear g by fact |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
458 |
fix x y and r :: real |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
459 |
show "(f (x + y), g (x + y)) = (f x, g x) + (f y, g y)" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
460 |
by (simp add: f.add g.add) |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
461 |
show "(f (r *\<^sub>R x), g (r *\<^sub>R x)) = r *\<^sub>R (f x, g x)" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
462 |
by (simp add: f.scaleR g.scaleR) |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
463 |
obtain Kf where "0 < Kf" and norm_f: "\<And>x. norm (f x) \<le> norm x * Kf" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
464 |
using f.pos_bounded by fast |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
465 |
obtain Kg where "0 < Kg" and norm_g: "\<And>x. norm (g x) \<le> norm x * Kg" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
466 |
using g.pos_bounded by fast |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
467 |
have "\<forall>x. norm (f x, g x) \<le> norm x * (Kf + Kg)" |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
468 |
apply (rule allI) |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
469 |
apply (simp add: norm_Pair) |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
470 |
apply (rule order_trans [OF sqrt_add_le_add_sqrt], simp, simp) |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44749
diff
changeset
|
471 |
apply (simp add: distrib_left) |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
472 |
apply (rule add_mono [OF norm_f norm_g]) |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
473 |
done |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
474 |
then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" .. |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
475 |
qed |
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
476 |
|
44575 | 477 |
subsubsection {* Frechet derivatives involving pairs *} |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
478 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
479 |
lemma has_derivative_Pair [derivative_intros]: |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
54890
diff
changeset
|
480 |
assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
54890
diff
changeset
|
481 |
shows "((\<lambda>x. (f x, g x)) has_derivative (\<lambda>h. (f' h, g' h))) (at x within s)" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
54890
diff
changeset
|
482 |
proof (rule has_derivativeI_sandwich[of 1]) |
44575 | 483 |
show "bounded_linear (\<lambda>h. (f' h, g' h))" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
54890
diff
changeset
|
484 |
using f g by (intro bounded_linear_Pair has_derivative_bounded_linear) |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51478
diff
changeset
|
485 |
let ?Rf = "\<lambda>y. f y - f x - f' (y - x)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51478
diff
changeset
|
486 |
let ?Rg = "\<lambda>y. g y - g x - g' (y - x)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51478
diff
changeset
|
487 |
let ?R = "\<lambda>y. ((f y, g y) - (f x, g x) - (f' (y - x), g' (y - x)))" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51478
diff
changeset
|
488 |
|
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51478
diff
changeset
|
489 |
show "((\<lambda>y. norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)) ---> 0) (at x within s)" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
54890
diff
changeset
|
490 |
using f g by (intro tendsto_add_zero) (auto simp: has_derivative_iff_norm) |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51478
diff
changeset
|
491 |
|
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51478
diff
changeset
|
492 |
fix y :: 'a assume "y \<noteq> x" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51478
diff
changeset
|
493 |
show "norm (?R y) / norm (y - x) \<le> norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51478
diff
changeset
|
494 |
unfolding add_divide_distrib [symmetric] |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51478
diff
changeset
|
495 |
by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt]) |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51478
diff
changeset
|
496 |
qed simp |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51478
diff
changeset
|
497 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
498 |
lemmas has_derivative_fst [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst] |
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
499 |
lemmas has_derivative_snd [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd] |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51478
diff
changeset
|
500 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
501 |
lemma has_derivative_split [derivative_intros]: |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51478
diff
changeset
|
502 |
"((\<lambda>p. f (fst p) (snd p)) has_derivative f') F \<Longrightarrow> ((\<lambda>(a, b). f a b) has_derivative f') F" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51478
diff
changeset
|
503 |
unfolding split_beta' . |
44575 | 504 |
|
505 |
subsection {* Product is an inner product space *} |
|
506 |
||
507 |
instantiation prod :: (real_inner, real_inner) real_inner |
|
508 |
begin |
|
509 |
||
510 |
definition inner_prod_def: |
|
511 |
"inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)" |
|
512 |
||
513 |
lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d" |
|
514 |
unfolding inner_prod_def by simp |
|
515 |
||
516 |
instance proof |
|
517 |
fix r :: real |
|
518 |
fix x y z :: "'a::real_inner \<times> 'b::real_inner" |
|
519 |
show "inner x y = inner y x" |
|
520 |
unfolding inner_prod_def |
|
521 |
by (simp add: inner_commute) |
|
522 |
show "inner (x + y) z = inner x z + inner y z" |
|
523 |
unfolding inner_prod_def |
|
524 |
by (simp add: inner_add_left) |
|
525 |
show "inner (scaleR r x) y = r * inner x y" |
|
526 |
unfolding inner_prod_def |
|
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44749
diff
changeset
|
527 |
by (simp add: distrib_left) |
44575 | 528 |
show "0 \<le> inner x x" |
529 |
unfolding inner_prod_def |
|
530 |
by (intro add_nonneg_nonneg inner_ge_zero) |
|
531 |
show "inner x x = 0 \<longleftrightarrow> x = 0" |
|
532 |
unfolding inner_prod_def prod_eq_iff |
|
533 |
by (simp add: add_nonneg_eq_0_iff) |
|
534 |
show "norm x = sqrt (inner x x)" |
|
535 |
unfolding norm_prod_def inner_prod_def |
|
536 |
by (simp add: power2_norm_eq_inner) |
|
537 |
qed |
|
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
538 |
|
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset
|
539 |
end |
44575 | 540 |
|
541 |
end |