28 !! x a. x \<in> V ==> norm (a \<cdot> x) = |a| * norm x; |
28 !! x a. x \<in> V ==> norm (a \<cdot> x) = |a| * norm x; |
29 !! x y. [|x \<in> V; y \<in> V |] ==> norm (x + y) <= norm x + norm y |] |
29 !! x y. [|x \<in> V; y \<in> V |] ==> norm (x + y) <= norm x + norm y |] |
30 ==> is_seminorm V norm" |
30 ==> is_seminorm V norm" |
31 by (unfold is_seminorm_def, force) |
31 by (unfold is_seminorm_def, force) |
32 |
32 |
33 lemma seminorm_ge_zero [intro??]: |
33 lemma seminorm_ge_zero [intro?]: |
34 "[| is_seminorm V norm; x \<in> V |] ==> #0 <= norm x" |
34 "[| is_seminorm V norm; x \<in> V |] ==> #0 <= norm x" |
35 by (unfold is_seminorm_def, force) |
35 by (unfold is_seminorm_def, force) |
36 |
36 |
37 lemma seminorm_abs_homogenous: |
37 lemma seminorm_abs_homogenous: |
38 "[| is_seminorm V norm; x \<in> V |] |
38 "[| is_seminorm V norm; x \<in> V |] |
84 |
84 |
85 lemma is_normI [intro]: |
85 lemma is_normI [intro]: |
86 "\<forall>x \<in> V. is_seminorm V norm \<and> (norm x = #0) = (x = 0) |
86 "\<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) |
87 ==> is_norm V norm" by (simp only: is_norm_def) |
88 |
88 |
89 lemma norm_is_seminorm [intro??]: |
89 lemma norm_is_seminorm [intro?]: |
90 "[| is_norm V norm; x \<in> V |] ==> is_seminorm V norm" |
90 "[| is_norm V norm; x \<in> V |] ==> is_seminorm V norm" |
91 by (unfold is_norm_def, force) |
91 by (unfold is_norm_def, force) |
92 |
92 |
93 lemma norm_zero_iff: |
93 lemma norm_zero_iff: |
94 "[| is_norm V norm; x \<in> V |] ==> (norm x = #0) = (x = 0)" |
94 "[| is_norm V norm; x \<in> V |] ==> (norm x = #0) = (x = 0)" |
95 by (unfold is_norm_def, force) |
95 by (unfold is_norm_def, force) |
96 |
96 |
97 lemma norm_ge_zero [intro??]: |
97 lemma norm_ge_zero [intro?]: |
98 "[|is_norm V norm; x \<in> V |] ==> #0 <= norm x" |
98 "[|is_norm V norm; x \<in> V |] ==> #0 <= norm x" |
99 by (unfold is_norm_def is_seminorm_def, force) |
99 by (unfold is_norm_def is_seminorm_def, force) |
100 |
100 |
101 |
101 |
102 subsection {* Normed vector spaces *} |
102 subsection {* Normed vector spaces *} |
113 lemma normed_vsI [intro]: |
113 lemma normed_vsI [intro]: |
114 "[| is_vectorspace V; is_norm V norm |] |
114 "[| is_vectorspace V; is_norm V norm |] |
115 ==> is_normed_vectorspace V norm" |
115 ==> is_normed_vectorspace V norm" |
116 by (unfold is_normed_vectorspace_def) blast |
116 by (unfold is_normed_vectorspace_def) blast |
117 |
117 |
118 lemma normed_vs_vs [intro??]: |
118 lemma normed_vs_vs [intro?]: |
119 "is_normed_vectorspace V norm ==> is_vectorspace V" |
119 "is_normed_vectorspace V norm ==> is_vectorspace V" |
120 by (unfold is_normed_vectorspace_def) force |
120 by (unfold is_normed_vectorspace_def) force |
121 |
121 |
122 lemma normed_vs_norm [intro??]: |
122 lemma normed_vs_norm [intro?]: |
123 "is_normed_vectorspace V norm ==> is_norm V norm" |
123 "is_normed_vectorspace V norm ==> is_norm V norm" |
124 by (unfold is_normed_vectorspace_def, elim conjE) |
124 by (unfold is_normed_vectorspace_def, elim conjE) |
125 |
125 |
126 lemma normed_vs_norm_ge_zero [intro??]: |
126 lemma normed_vs_norm_ge_zero [intro?]: |
127 "[| is_normed_vectorspace V norm; x \<in> V |] ==> #0 <= norm x" |
127 "[| is_normed_vectorspace V norm; x \<in> V |] ==> #0 <= norm x" |
128 by (unfold is_normed_vectorspace_def, rule, elim conjE) |
128 by (unfold is_normed_vectorspace_def, rule, elim conjE) |
129 |
129 |
130 lemma normed_vs_norm_gt_zero [intro??]: |
130 lemma normed_vs_norm_gt_zero [intro?]: |
131 "[| is_normed_vectorspace V norm; x \<in> V; x \<noteq> 0 |] ==> #0 < norm x" |
131 "[| is_normed_vectorspace V norm; x \<in> V; x \<noteq> 0 |] ==> #0 < norm x" |
132 proof (unfold is_normed_vectorspace_def, elim conjE) |
132 proof (unfold is_normed_vectorspace_def, elim conjE) |
133 assume "x \<in> V" "x \<noteq> 0" "is_vectorspace V" "is_norm V norm" |
133 assume "x \<in> V" "x \<noteq> 0" "is_vectorspace V" "is_norm V norm" |
134 have "#0 <= norm x" .. |
134 have "#0 <= norm x" .. |
135 also have "#0 \<noteq> norm x" |
135 also have "#0 \<noteq> norm x" |
140 thus "False" by contradiction |
140 thus "False" by contradiction |
141 qed (rule sym) |
141 qed (rule sym) |
142 finally show "#0 < norm x" . |
142 finally show "#0 < norm x" . |
143 qed |
143 qed |
144 |
144 |
145 lemma normed_vs_norm_abs_homogenous [intro??]: |
145 lemma normed_vs_norm_abs_homogenous [intro?]: |
146 "[| is_normed_vectorspace V norm; x \<in> V |] |
146 "[| is_normed_vectorspace V norm; x \<in> V |] |
147 ==> norm (a \<cdot> x) = |a| * norm x" |
147 ==> norm (a \<cdot> x) = |a| * norm x" |
148 by (rule seminorm_abs_homogenous, rule norm_is_seminorm, |
148 by (rule seminorm_abs_homogenous, rule norm_is_seminorm, |
149 rule normed_vs_norm) |
149 rule normed_vs_norm) |
150 |
150 |
151 lemma normed_vs_norm_subadditive [intro??]: |
151 lemma normed_vs_norm_subadditive [intro?]: |
152 "[| is_normed_vectorspace V norm; x \<in> V; y \<in> V |] |
152 "[| is_normed_vectorspace V norm; x \<in> V; y \<in> V |] |
153 ==> norm (x + y) <= norm x + norm y" |
153 ==> norm (x + y) <= norm x + norm y" |
154 by (rule seminorm_subadditive, rule norm_is_seminorm, |
154 by (rule seminorm_subadditive, rule norm_is_seminorm, |
155 rule normed_vs_norm) |
155 rule normed_vs_norm) |
156 |
156 |
157 text{* Any subspace of a normed vector space is again a |
157 text{* Any subspace of a normed vector space is again a |
158 normed vectorspace.*} |
158 normed vectorspace.*} |
159 |
159 |
160 lemma subspace_normed_vs [intro??]: |
160 lemma subspace_normed_vs [intro?]: |
161 "[| is_vectorspace E; is_subspace F E; |
161 "[| is_vectorspace E; is_subspace F E; |
162 is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm" |
162 is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm" |
163 proof (rule normed_vsI) |
163 proof (rule normed_vsI) |
164 assume "is_subspace F E" "is_vectorspace E" |
164 assume "is_subspace F E" "is_vectorspace E" |
165 "is_normed_vectorspace E norm" |
165 "is_normed_vectorspace E norm" |