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