wenzelm@7566
|
1 |
(* Title: HOL/Real/HahnBanach/NormedSpace.thy
|
wenzelm@7566
|
2 |
ID: $Id$
|
wenzelm@7566
|
3 |
Author: Gertrud Bauer, TU Munich
|
wenzelm@7566
|
4 |
*)
|
wenzelm@7535
|
5 |
|
wenzelm@9035
|
6 |
header {* Normed vector spaces *}
|
wenzelm@7808
|
7 |
|
wenzelm@9035
|
8 |
theory NormedSpace = Subspace:
|
wenzelm@7535
|
9 |
|
bauerg@9374
|
10 |
syntax
|
bauerg@9374
|
11 |
abs :: "real \<Rightarrow> real" ("|_|")
|
wenzelm@7535
|
12 |
|
wenzelm@9035
|
13 |
subsection {* Quasinorms *}
|
wenzelm@7808
|
14 |
|
wenzelm@7978
|
15 |
text{* A \emph{seminorm} $\norm{\cdot}$ is a function on a real vector
|
wenzelm@7978
|
16 |
space into the reals that has the following properties: It is positive
|
wenzelm@9035
|
17 |
definite, absolute homogenous and subadditive. *}
|
wenzelm@7535
|
18 |
|
wenzelm@7535
|
19 |
constdefs
|
bauerg@9374
|
20 |
is_seminorm :: "['a::{plus, minus, zero} set, 'a => real] => bool"
|
bauerg@9374
|
21 |
"is_seminorm V norm == \<forall>x \<in> V. \<forall>y \<in> V. \<forall>a.
|
wenzelm@9035
|
22 |
#0 <= norm x
|
bauerg@9374
|
23 |
\<and> norm (a \<cdot> x) = |a| * norm x
|
bauerg@9374
|
24 |
\<and> norm (x + y) <= norm x + norm y"
|
wenzelm@7535
|
25 |
|
wenzelm@7978
|
26 |
lemma is_seminormI [intro]:
|
bauerg@9374
|
27 |
"[| !! x y a. [| x \<in> V; y \<in> V|] ==> #0 <= norm x;
|
bauerg@9374
|
28 |
!! x a. x \<in> V ==> norm (a \<cdot> x) = |a| * norm x;
|
bauerg@9374
|
29 |
!! x y. [|x \<in> V; y \<in> V |] ==> norm (x + y) <= norm x + norm y |]
|
wenzelm@9035
|
30 |
==> is_seminorm V norm"
|
wenzelm@9035
|
31 |
by (unfold is_seminorm_def, force)
|
wenzelm@7535
|
32 |
|
wenzelm@9408
|
33 |
lemma seminorm_ge_zero [intro?]:
|
bauerg@9374
|
34 |
"[| is_seminorm V norm; x \<in> V |] ==> #0 <= norm x"
|
wenzelm@9035
|
35 |
by (unfold is_seminorm_def, force)
|
wenzelm@7535
|
36 |
|
wenzelm@8838
|
37 |
lemma seminorm_abs_homogenous:
|
bauerg@9374
|
38 |
"[| is_seminorm V norm; x \<in> V |]
|
bauerg@9374
|
39 |
==> norm (a \<cdot> x) = |a| * norm x"
|
wenzelm@9035
|
40 |
by (unfold is_seminorm_def, force)
|
wenzelm@7535
|
41 |
|
wenzelm@7978
|
42 |
lemma seminorm_subadditive:
|
bauerg@9374
|
43 |
"[| is_seminorm V norm; x \<in> V; y \<in> V |]
|
wenzelm@9035
|
44 |
==> norm (x + y) <= norm x + norm y"
|
wenzelm@9035
|
45 |
by (unfold is_seminorm_def, force)
|
wenzelm@7535
|
46 |
|
wenzelm@7978
|
47 |
lemma seminorm_diff_subadditive:
|
bauerg@9374
|
48 |
"[| is_seminorm V norm; x \<in> V; y \<in> V; is_vectorspace V |]
|
wenzelm@9035
|
49 |
==> norm (x - y) <= norm x + norm y"
|
wenzelm@9035
|
50 |
proof -
|
bauerg@9374
|
51 |
assume "is_seminorm V norm" "x \<in> V" "y \<in> V" "is_vectorspace V"
|
bauerg@9374
|
52 |
have "norm (x - y) = norm (x + - #1 \<cdot> y)"
|
wenzelm@9035
|
53 |
by (simp! add: diff_eq2 negate_eq2a)
|
bauerg@9374
|
54 |
also have "... <= norm x + norm (- #1 \<cdot> y)"
|
wenzelm@9035
|
55 |
by (simp! add: seminorm_subadditive)
|
bauerg@9374
|
56 |
also have "norm (- #1 \<cdot> y) = |- #1| * norm y"
|
wenzelm@9035
|
57 |
by (rule seminorm_abs_homogenous)
|
bauerg@9374
|
58 |
also have "|- #1| = (#1::real)" by (rule abs_minus_one)
|
wenzelm@9035
|
59 |
finally show "norm (x - y) <= norm x + norm y" by simp
|
wenzelm@9035
|
60 |
qed
|
wenzelm@7535
|
61 |
|
wenzelm@7978
|
62 |
lemma seminorm_minus:
|
bauerg@9374
|
63 |
"[| is_seminorm V norm; x \<in> V; is_vectorspace V |]
|
wenzelm@9035
|
64 |
==> norm (- x) = norm x"
|
wenzelm@9035
|
65 |
proof -
|
bauerg@9374
|
66 |
assume "is_seminorm V norm" "x \<in> V" "is_vectorspace V"
|
bauerg@9374
|
67 |
have "norm (- x) = norm (- #1 \<cdot> x)" by (simp! only: negate_eq1)
|
bauerg@9374
|
68 |
also have "... = |- #1| * norm x"
|
wenzelm@9035
|
69 |
by (rule seminorm_abs_homogenous)
|
bauerg@9374
|
70 |
also have "|- #1| = (#1::real)" by (rule abs_minus_one)
|
wenzelm@9035
|
71 |
finally show "norm (- x) = norm x" by simp
|
wenzelm@9035
|
72 |
qed
|
wenzelm@7535
|
73 |
|
wenzelm@7535
|
74 |
|
wenzelm@9035
|
75 |
subsection {* Norms *}
|
wenzelm@7808
|
76 |
|
wenzelm@7978
|
77 |
text{* A \emph{norm} $\norm{\cdot}$ is a seminorm that maps only the
|
wenzelm@9035
|
78 |
$\zero$ vector to $0$. *}
|
wenzelm@7535
|
79 |
|
wenzelm@7535
|
80 |
constdefs
|
bauerg@9374
|
81 |
is_norm :: "['a::{plus, minus, zero} set, 'a => real] => bool"
|
bauerg@9374
|
82 |
"is_norm V norm == \<forall>x \<in> V. is_seminorm V norm
|
bauerg@9374
|
83 |
\<and> (norm x = #0) = (x = 0)"
|
wenzelm@7535
|
84 |
|
wenzelm@7566
|
85 |
lemma is_normI [intro]:
|
bauerg@9374
|
86 |
"\<forall>x \<in> V. is_seminorm V norm \<and> (norm x = #0) = (x = 0)
|
wenzelm@9035
|
87 |
==> is_norm V norm" by (simp only: is_norm_def)
|
wenzelm@7535
|
88 |
|
wenzelm@9408
|
89 |
lemma norm_is_seminorm [intro?]:
|
bauerg@9374
|
90 |
"[| is_norm V norm; x \<in> V |] ==> is_seminorm V norm"
|
wenzelm@9035
|
91 |
by (unfold is_norm_def, force)
|
wenzelm@7535
|
92 |
|
wenzelm@7808
|
93 |
lemma norm_zero_iff:
|
bauerg@9374
|
94 |
"[| is_norm V norm; x \<in> V |] ==> (norm x = #0) = (x = 0)"
|
wenzelm@9035
|
95 |
by (unfold is_norm_def, force)
|
wenzelm@7535
|
96 |
|
wenzelm@9408
|
97 |
lemma norm_ge_zero [intro?]:
|
bauerg@9374
|
98 |
"[|is_norm V norm; x \<in> V |] ==> #0 <= norm x"
|
wenzelm@9035
|
99 |
by (unfold is_norm_def is_seminorm_def, force)
|
wenzelm@7535
|
100 |
|
wenzelm@7535
|
101 |
|
wenzelm@9035
|
102 |
subsection {* Normed vector spaces *}
|
wenzelm@7808
|
103 |
|
wenzelm@7917
|
104 |
text{* A vector space together with a norm is called
|
wenzelm@9035
|
105 |
a \emph{normed space}. *}
|
wenzelm@7535
|
106 |
|
wenzelm@7535
|
107 |
constdefs
|
wenzelm@7917
|
108 |
is_normed_vectorspace ::
|
bauerg@9374
|
109 |
"['a::{plus, minus, zero} set, 'a => real] => bool"
|
wenzelm@7535
|
110 |
"is_normed_vectorspace V norm ==
|
bauerg@9374
|
111 |
is_vectorspace V \<and> is_norm V norm"
|
wenzelm@7535
|
112 |
|
wenzelm@7566
|
113 |
lemma normed_vsI [intro]:
|
wenzelm@7808
|
114 |
"[| is_vectorspace V; is_norm V norm |]
|
wenzelm@9035
|
115 |
==> is_normed_vectorspace V norm"
|
wenzelm@9035
|
116 |
by (unfold is_normed_vectorspace_def) blast
|
wenzelm@7535
|
117 |
|
wenzelm@9408
|
118 |
lemma normed_vs_vs [intro?]:
|
wenzelm@9035
|
119 |
"is_normed_vectorspace V norm ==> is_vectorspace V"
|
wenzelm@9035
|
120 |
by (unfold is_normed_vectorspace_def) force
|
wenzelm@7535
|
121 |
|
wenzelm@9408
|
122 |
lemma normed_vs_norm [intro?]:
|
wenzelm@9035
|
123 |
"is_normed_vectorspace V norm ==> is_norm V norm"
|
wenzelm@9035
|
124 |
by (unfold is_normed_vectorspace_def, elim conjE)
|
wenzelm@7535
|
125 |
|
wenzelm@9408
|
126 |
lemma normed_vs_norm_ge_zero [intro?]:
|
bauerg@9374
|
127 |
"[| is_normed_vectorspace V norm; x \<in> V |] ==> #0 <= norm x"
|
wenzelm@9035
|
128 |
by (unfold is_normed_vectorspace_def, rule, elim conjE)
|
wenzelm@7535
|
129 |
|
wenzelm@9408
|
130 |
lemma normed_vs_norm_gt_zero [intro?]:
|
bauerg@9374
|
131 |
"[| is_normed_vectorspace V norm; x \<in> V; x \<noteq> 0 |] ==> #0 < norm x"
|
wenzelm@9035
|
132 |
proof (unfold is_normed_vectorspace_def, elim conjE)
|
bauerg@9374
|
133 |
assume "x \<in> V" "x \<noteq> 0" "is_vectorspace V" "is_norm V norm"
|
wenzelm@9035
|
134 |
have "#0 <= norm x" ..
|
bauerg@9374
|
135 |
also have "#0 \<noteq> norm x"
|
wenzelm@9035
|
136 |
proof
|
wenzelm@9035
|
137 |
presume "norm x = #0"
|
bauerg@9374
|
138 |
also have "?this = (x = 0)" by (rule norm_zero_iff)
|
bauerg@9374
|
139 |
finally have "x = 0" .
|
wenzelm@9035
|
140 |
thus "False" by contradiction
|
wenzelm@9035
|
141 |
qed (rule sym)
|
wenzelm@9035
|
142 |
finally show "#0 < norm x" .
|
wenzelm@9035
|
143 |
qed
|
wenzelm@7535
|
144 |
|
wenzelm@9408
|
145 |
lemma normed_vs_norm_abs_homogenous [intro?]:
|
bauerg@9374
|
146 |
"[| is_normed_vectorspace V norm; x \<in> V |]
|
bauerg@9374
|
147 |
==> norm (a \<cdot> x) = |a| * norm x"
|
wenzelm@8838
|
148 |
by (rule seminorm_abs_homogenous, rule norm_is_seminorm,
|
wenzelm@9035
|
149 |
rule normed_vs_norm)
|
wenzelm@7535
|
150 |
|
wenzelm@9408
|
151 |
lemma normed_vs_norm_subadditive [intro?]:
|
bauerg@9374
|
152 |
"[| is_normed_vectorspace V norm; x \<in> V; y \<in> V |]
|
wenzelm@9035
|
153 |
==> norm (x + y) <= norm x + norm y"
|
wenzelm@7978
|
154 |
by (rule seminorm_subadditive, rule norm_is_seminorm,
|
wenzelm@9035
|
155 |
rule normed_vs_norm)
|
wenzelm@7535
|
156 |
|
wenzelm@7917
|
157 |
text{* Any subspace of a normed vector space is again a
|
wenzelm@9035
|
158 |
normed vectorspace.*}
|
wenzelm@7917
|
159 |
|
wenzelm@9408
|
160 |
lemma subspace_normed_vs [intro?]:
|
bauerg@9374
|
161 |
"[| is_vectorspace E; is_subspace F E;
|
wenzelm@9035
|
162 |
is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm"
|
wenzelm@9035
|
163 |
proof (rule normed_vsI)
|
wenzelm@7808
|
164 |
assume "is_subspace F E" "is_vectorspace E"
|
wenzelm@9035
|
165 |
"is_normed_vectorspace E norm"
|
wenzelm@9035
|
166 |
show "is_vectorspace F" ..
|
wenzelm@9035
|
167 |
show "is_norm F norm"
|
wenzelm@9035
|
168 |
proof (intro is_normI ballI conjI)
|
wenzelm@9035
|
169 |
show "is_seminorm F norm"
|
wenzelm@9035
|
170 |
proof
|
bauerg@9374
|
171 |
fix x y a presume "x \<in> E"
|
wenzelm@9035
|
172 |
show "#0 <= norm x" ..
|
bauerg@9374
|
173 |
show "norm (a \<cdot> x) = |a| * norm x" ..
|
bauerg@9374
|
174 |
presume "y \<in> E"
|
wenzelm@9035
|
175 |
show "norm (x + y) <= norm x + norm y" ..
|
wenzelm@9035
|
176 |
qed (simp!)+
|
wenzelm@7535
|
177 |
|
bauerg@9374
|
178 |
fix x assume "x \<in> F"
|
bauerg@9374
|
179 |
show "(norm x = #0) = (x = 0)"
|
wenzelm@9035
|
180 |
proof (rule norm_zero_iff)
|
wenzelm@9035
|
181 |
show "is_norm E norm" ..
|
wenzelm@9035
|
182 |
qed (simp!)
|
wenzelm@9035
|
183 |
qed
|
wenzelm@9035
|
184 |
qed
|
wenzelm@7535
|
185 |
|
wenzelm@9035
|
186 |
end |