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