1 (* Title: HOL/Real/HahnBanach/FunctionNorm.thy |
|
2 ID: $Id$ |
|
3 Author: Gertrud Bauer, TU Munich |
|
4 *) |
|
5 |
|
6 header {* The norm of a function *} |
|
7 |
|
8 theory FunctionNorm |
|
9 imports NormedSpace FunctionOrder |
|
10 begin |
|
11 |
|
12 subsection {* Continuous linear forms*} |
|
13 |
|
14 text {* |
|
15 A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"} |
|
16 is \emph{continuous}, iff it is bounded, i.e. |
|
17 \begin{center} |
|
18 @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} |
|
19 \end{center} |
|
20 In our application no other functions than linear forms are |
|
21 considered, so we can define continuous linear forms as bounded |
|
22 linear forms: |
|
23 *} |
|
24 |
|
25 locale continuous = var V + norm_syntax + linearform + |
|
26 assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" |
|
27 |
|
28 declare continuous.intro [intro?] continuous_axioms.intro [intro?] |
|
29 |
|
30 lemma continuousI [intro]: |
|
31 fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>") |
|
32 assumes "linearform V f" |
|
33 assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" |
|
34 shows "continuous V norm f" |
|
35 proof |
|
36 show "linearform V f" by fact |
|
37 from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast |
|
38 then show "continuous_axioms V norm f" .. |
|
39 qed |
|
40 |
|
41 |
|
42 subsection {* The norm of a linear form *} |
|
43 |
|
44 text {* |
|
45 The least real number @{text c} for which holds |
|
46 \begin{center} |
|
47 @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} |
|
48 \end{center} |
|
49 is called the \emph{norm} of @{text f}. |
|
50 |
|
51 For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be |
|
52 defined as |
|
53 \begin{center} |
|
54 @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"} |
|
55 \end{center} |
|
56 |
|
57 For the case @{text "V = {0}"} the supremum would be taken from an |
|
58 empty set. Since @{text \<real>} is unbounded, there would be no supremum. |
|
59 To avoid this situation it must be guaranteed that there is an |
|
60 element in this set. This element must be @{text "{} \<ge> 0"} so that |
|
61 @{text fn_norm} has the norm properties. Furthermore it does not |
|
62 have to change the norm in all other cases, so it must be @{text 0}, |
|
63 as all other elements are @{text "{} \<ge> 0"}. |
|
64 |
|
65 Thus we define the set @{text B} where the supremum is taken from as |
|
66 follows: |
|
67 \begin{center} |
|
68 @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"} |
|
69 \end{center} |
|
70 |
|
71 @{text fn_norm} is equal to the supremum of @{text B}, if the |
|
72 supremum exists (otherwise it is undefined). |
|
73 *} |
|
74 |
|
75 locale fn_norm = norm_syntax + |
|
76 fixes B defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}" |
|
77 fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999) |
|
78 defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)" |
|
79 |
|
80 locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm |
|
81 |
|
82 lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f" |
|
83 by (simp add: B_def) |
|
84 |
|
85 text {* |
|
86 The following lemma states that every continuous linear form on a |
|
87 normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm. |
|
88 *} |
|
89 |
|
90 lemma (in normed_vectorspace_with_fn_norm) fn_norm_works: |
|
91 assumes "continuous V norm f" |
|
92 shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
|
93 proof - |
|
94 interpret continuous [V norm f] by fact |
|
95 txt {* The existence of the supremum is shown using the |
|
96 completeness of the reals. Completeness means, that every |
|
97 non-empty bounded set of reals has a supremum. *} |
|
98 have "\<exists>a. lub (B V f) a" |
|
99 proof (rule real_complete) |
|
100 txt {* First we have to show that @{text B} is non-empty: *} |
|
101 have "0 \<in> B V f" .. |
|
102 then show "\<exists>x. x \<in> B V f" .. |
|
103 |
|
104 txt {* Then we have to show that @{text B} is bounded: *} |
|
105 show "\<exists>c. \<forall>y \<in> B V f. y \<le> c" |
|
106 proof - |
|
107 txt {* We know that @{text f} is bounded by some value @{text c}. *} |
|
108 from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. |
|
109 |
|
110 txt {* To prove the thesis, we have to show that there is some |
|
111 @{text b}, such that @{text "y \<le> b"} for all @{text "y \<in> |
|
112 B"}. Due to the definition of @{text B} there are two cases. *} |
|
113 |
|
114 def b \<equiv> "max c 0" |
|
115 have "\<forall>y \<in> B V f. y \<le> b" |
|
116 proof |
|
117 fix y assume y: "y \<in> B V f" |
|
118 show "y \<le> b" |
|
119 proof cases |
|
120 assume "y = 0" |
|
121 then show ?thesis unfolding b_def by arith |
|
122 next |
|
123 txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some |
|
124 @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *} |
|
125 assume "y \<noteq> 0" |
|
126 with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>" |
|
127 and x: "x \<in> V" and neq: "x \<noteq> 0" |
|
128 by (auto simp add: B_def real_divide_def) |
|
129 from x neq have gt: "0 < \<parallel>x\<parallel>" .. |
|
130 |
|
131 txt {* The thesis follows by a short calculation using the |
|
132 fact that @{text f} is bounded. *} |
|
133 |
|
134 note y_rep |
|
135 also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" |
|
136 proof (rule mult_right_mono) |
|
137 from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. |
|
138 from gt have "0 < inverse \<parallel>x\<parallel>" |
|
139 by (rule positive_imp_inverse_positive) |
|
140 then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le) |
|
141 qed |
|
142 also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)" |
|
143 by (rule real_mult_assoc) |
|
144 also |
|
145 from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp |
|
146 then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp |
|
147 also have "c * 1 \<le> b" by (simp add: b_def le_maxI1) |
|
148 finally show "y \<le> b" . |
|
149 qed |
|
150 qed |
|
151 then show ?thesis .. |
|
152 qed |
|
153 qed |
|
154 then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex) |
|
155 qed |
|
156 |
|
157 lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]: |
|
158 assumes "continuous V norm f" |
|
159 assumes b: "b \<in> B V f" |
|
160 shows "b \<le> \<parallel>f\<parallel>\<hyphen>V" |
|
161 proof - |
|
162 interpret continuous [V norm f] by fact |
|
163 have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
|
164 using `continuous V norm f` by (rule fn_norm_works) |
|
165 from this and b show ?thesis .. |
|
166 qed |
|
167 |
|
168 lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB: |
|
169 assumes "continuous V norm f" |
|
170 assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y" |
|
171 shows "\<parallel>f\<parallel>\<hyphen>V \<le> y" |
|
172 proof - |
|
173 interpret continuous [V norm f] by fact |
|
174 have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
|
175 using `continuous V norm f` by (rule fn_norm_works) |
|
176 from this and b show ?thesis .. |
|
177 qed |
|
178 |
|
179 text {* The norm of a continuous function is always @{text "\<ge> 0"}. *} |
|
180 |
|
181 lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]: |
|
182 assumes "continuous V norm f" |
|
183 shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V" |
|
184 proof - |
|
185 interpret continuous [V norm f] by fact |
|
186 txt {* The function norm is defined as the supremum of @{text B}. |
|
187 So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge> |
|
188 0"}, provided the supremum exists and @{text B} is not empty. *} |
|
189 have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
|
190 using `continuous V norm f` by (rule fn_norm_works) |
|
191 moreover have "0 \<in> B V f" .. |
|
192 ultimately show ?thesis .. |
|
193 qed |
|
194 |
|
195 text {* |
|
196 \medskip The fundamental property of function norms is: |
|
197 \begin{center} |
|
198 @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} |
|
199 \end{center} |
|
200 *} |
|
201 |
|
202 lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong: |
|
203 assumes "continuous V norm f" "linearform V f" |
|
204 assumes x: "x \<in> V" |
|
205 shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" |
|
206 proof - |
|
207 interpret continuous [V norm f] by fact |
|
208 interpret linearform [V f] . |
|
209 show ?thesis |
|
210 proof cases |
|
211 assume "x = 0" |
|
212 then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp |
|
213 also have "f 0 = 0" by rule unfold_locales |
|
214 also have "\<bar>\<dots>\<bar> = 0" by simp |
|
215 also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V" |
|
216 using `continuous V norm f` by (rule fn_norm_ge_zero) |
|
217 from x have "0 \<le> norm x" .. |
|
218 with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff) |
|
219 finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" . |
|
220 next |
|
221 assume "x \<noteq> 0" |
|
222 with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp |
|
223 then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp |
|
224 also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" |
|
225 proof (rule mult_right_mono) |
|
226 from x show "0 \<le> \<parallel>x\<parallel>" .. |
|
227 from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f" |
|
228 by (auto simp add: B_def real_divide_def) |
|
229 with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V" |
|
230 by (rule fn_norm_ub) |
|
231 qed |
|
232 finally show ?thesis . |
|
233 qed |
|
234 qed |
|
235 |
|
236 text {* |
|
237 \medskip The function norm is the least positive real number for |
|
238 which the following inequation holds: |
|
239 \begin{center} |
|
240 @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} |
|
241 \end{center} |
|
242 *} |
|
243 |
|
244 lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]: |
|
245 assumes "continuous V norm f" |
|
246 assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c" |
|
247 shows "\<parallel>f\<parallel>\<hyphen>V \<le> c" |
|
248 proof - |
|
249 interpret continuous [V norm f] by fact |
|
250 show ?thesis |
|
251 proof (rule fn_norm_leastB [folded B_def fn_norm_def]) |
|
252 fix b assume b: "b \<in> B V f" |
|
253 show "b \<le> c" |
|
254 proof cases |
|
255 assume "b = 0" |
|
256 with ge show ?thesis by simp |
|
257 next |
|
258 assume "b \<noteq> 0" |
|
259 with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>" |
|
260 and x_neq: "x \<noteq> 0" and x: "x \<in> V" |
|
261 by (auto simp add: B_def real_divide_def) |
|
262 note b_rep |
|
263 also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" |
|
264 proof (rule mult_right_mono) |
|
265 have "0 < \<parallel>x\<parallel>" using x x_neq .. |
|
266 then show "0 \<le> inverse \<parallel>x\<parallel>" by simp |
|
267 from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. |
|
268 qed |
|
269 also have "\<dots> = c" |
|
270 proof - |
|
271 from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp |
|
272 then show ?thesis by simp |
|
273 qed |
|
274 finally show ?thesis . |
|
275 qed |
|
276 qed (insert `continuous V norm f`, simp_all add: continuous_def) |
|
277 qed |
|
278 |
|
279 end |
|