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