8 theory FunctionNorm = NormedSpace + FunctionOrder: |
8 theory FunctionNorm = NormedSpace + FunctionOrder: |
9 |
9 |
10 subsection {* Continuous linear forms*} |
10 subsection {* Continuous linear forms*} |
11 |
11 |
12 text {* |
12 text {* |
13 A linear form @{text f} on a normed vector space @{text "(V, \\<parallel>\\<cdot>\\<parallel>)"} |
13 A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"} |
14 is \emph{continuous}, iff it is bounded, i.~e. |
14 is \emph{continuous}, iff it is bounded, i.~e. |
15 \begin{center} |
15 \begin{center} |
16 @{text "\\<exists>c \\<in> R. \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c \\<cdot> \\<parallel>x\\<parallel>"} |
16 @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} |
17 \end{center} |
17 \end{center} |
18 In our application no other functions than linear forms are |
18 In our application no other functions than linear forms are |
19 considered, so we can define continuous linear forms as bounded |
19 considered, so we can define continuous linear forms as bounded |
20 linear forms: |
20 linear forms: |
21 *} |
21 *} |
22 |
22 |
23 constdefs |
23 constdefs |
24 is_continuous :: |
24 is_continuous :: |
25 "'a::{plus, minus, zero} set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> bool" |
25 "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool" |
26 "is_continuous V norm f \\<equiv> |
26 "is_continuous V norm f \<equiv> |
27 is_linearform V f \\<and> (\\<exists>c. \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x)" |
27 is_linearform V f \<and> (\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x)" |
28 |
28 |
29 lemma continuousI [intro]: |
29 lemma continuousI [intro]: |
30 "is_linearform V f \\<Longrightarrow> (\\<And>x. x \\<in> V \\<Longrightarrow> \\<bar>f x\\<bar> \\<le> c * norm x) |
30 "is_linearform V f \<Longrightarrow> (\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * norm x) |
31 \\<Longrightarrow> is_continuous V norm f" |
31 \<Longrightarrow> is_continuous V norm f" |
32 proof (unfold is_continuous_def, intro exI conjI ballI) |
32 by (unfold is_continuous_def) blast |
33 assume r: "\\<And>x. x \\<in> V \\<Longrightarrow> \\<bar>f x\\<bar> \\<le> c * norm x" |
|
34 fix x assume "x \\<in> V" show "\\<bar>f x\\<bar> \\<le> c * norm x" by (rule r) |
|
35 qed |
|
36 |
33 |
37 lemma continuous_linearform [intro?]: |
34 lemma continuous_linearform [intro?]: |
38 "is_continuous V norm f \\<Longrightarrow> is_linearform V f" |
35 "is_continuous V norm f \<Longrightarrow> is_linearform V f" |
39 by (unfold is_continuous_def) blast |
36 by (unfold is_continuous_def) blast |
40 |
37 |
41 lemma continuous_bounded [intro?]: |
38 lemma continuous_bounded [intro?]: |
42 "is_continuous V norm f |
39 "is_continuous V norm f |
43 \\<Longrightarrow> \\<exists>c. \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x" |
40 \<Longrightarrow> \<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x" |
44 by (unfold is_continuous_def) blast |
41 by (unfold is_continuous_def) blast |
45 |
42 |
|
43 |
46 subsection{* The norm of a linear form *} |
44 subsection{* The norm of a linear form *} |
47 |
45 |
48 |
|
49 text {* |
46 text {* |
50 The least real number @{text c} for which holds |
47 The least real number @{text c} for which holds |
51 \begin{center} |
48 \begin{center} |
52 @{text "\\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c \\<cdot> \\<parallel>x\\<parallel>"} |
49 @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} |
53 \end{center} |
50 \end{center} |
54 is called the \emph{norm} of @{text f}. |
51 is called the \emph{norm} of @{text f}. |
55 |
52 |
56 For non-trivial vector spaces @{text "V \\<noteq> {0}"} the norm can be |
53 For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be |
57 defined as |
54 defined as |
58 \begin{center} |
55 \begin{center} |
59 @{text "\\<parallel>f\\<parallel> = \<sup>x \\<noteq> 0. \\<bar>f x\\<bar> / \\<parallel>x\\<parallel>"} |
56 @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"} |
60 \end{center} |
57 \end{center} |
61 |
58 |
62 For the case @{text "V = {0}"} the supremum would be taken from an |
59 For the case @{text "V = {0}"} the supremum would be taken from an |
63 empty set. Since @{text \\<real>} is unbounded, there would be no supremum. |
60 empty set. Since @{text \<real>} is unbounded, there would be no supremum. |
64 To avoid this situation it must be guaranteed that there is an |
61 To avoid this situation it must be guaranteed that there is an |
65 element in this set. This element must be @{text "{} \\<ge> 0"} so that |
62 element in this set. This element must be @{text "{} \<ge> 0"} so that |
66 @{text function_norm} has the norm properties. Furthermore |
63 @{text function_norm} has the norm properties. Furthermore |
67 it does not have to change the norm in all other cases, so it must |
64 it does not have to change the norm in all other cases, so it must |
68 be @{text 0}, as all other elements of are @{text "{} \\<ge> 0"}. |
65 be @{text 0}, as all other elements of are @{text "{} \<ge> 0"}. |
69 |
66 |
70 Thus we define the set @{text B} the supremum is taken from as |
67 Thus we define the set @{text B} the supremum is taken from as |
71 \begin{center} |
68 \begin{center} |
72 @{text "{0} \\<union> {\\<bar>f x\\<bar> / \\<parallel>x\\<parallel>. x \\<noteq> 0 \\<and> x \\<in> F}"} |
69 @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"} |
73 \end{center} |
70 \end{center} |
74 *} |
71 *} |
75 |
72 |
76 constdefs |
73 constdefs |
77 B :: "'a set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> ('a::{plus, minus, zero} \\<Rightarrow> real) \\<Rightarrow> real set" |
74 B :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a::{plus, minus, zero} \<Rightarrow> real) \<Rightarrow> real set" |
78 "B V norm f \\<equiv> |
75 "B V norm f \<equiv> |
79 {#0} \\<union> {\\<bar>f x\\<bar> * inverse (norm x) | x. x \\<noteq> 0 \\<and> x \\<in> V}" |
76 {#0} \<union> {\<bar>f x\<bar> * inverse (norm x) | x. x \<noteq> 0 \<and> x \<in> V}" |
80 |
77 |
81 text {* |
78 text {* |
82 @{text n} is the function norm of @{text f}, iff @{text n} is the |
79 @{text n} is the function norm of @{text f}, iff @{text n} is the |
83 supremum of @{text B}. |
80 supremum of @{text B}. |
84 *} |
81 *} |
85 |
82 |
86 constdefs |
83 constdefs |
87 is_function_norm :: |
84 is_function_norm :: |
88 "('a::{minus,plus,zero} \\<Rightarrow> real) \\<Rightarrow> 'a set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> real \\<Rightarrow> bool" |
85 "('a::{minus,plus,zero} \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool" |
89 "is_function_norm f V norm fn \\<equiv> is_Sup UNIV (B V norm f) fn" |
86 "is_function_norm f V norm fn \<equiv> is_Sup UNIV (B V norm f) fn" |
90 |
87 |
91 text {* |
88 text {* |
92 @{text function_norm} is equal to the supremum of @{text B}, if the |
89 @{text function_norm} is equal to the supremum of @{text B}, if the |
93 supremum exists. Otherwise it is undefined. |
90 supremum exists. Otherwise it is undefined. |
94 *} |
91 *} |
95 |
92 |
96 constdefs |
93 constdefs |
97 function_norm :: "('a::{minus,plus,zero} \\<Rightarrow> real) \\<Rightarrow> 'a set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> real" |
94 function_norm :: "('a::{minus,plus,zero} \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real" |
98 "function_norm f V norm \\<equiv> Sup UNIV (B V norm f)" |
95 "function_norm f V norm \<equiv> Sup UNIV (B V norm f)" |
99 |
96 |
100 syntax |
97 syntax |
101 function_norm :: "('a \\<Rightarrow> real) \\<Rightarrow> 'a set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> real" ("\\<parallel>_\\<parallel>_,_") |
98 function_norm :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real" ("\<parallel>_\<parallel>_,_") |
102 |
99 |
103 lemma B_not_empty: "#0 \\<in> B V norm f" |
100 lemma B_not_empty: "#0 \<in> B V norm f" |
104 by (unfold B_def) blast |
101 by (unfold B_def) blast |
105 |
102 |
106 text {* |
103 text {* |
107 The following lemma states that every continuous linear form on a |
104 The following lemma states that every continuous linear form on a |
108 normed space @{text "(V, \\<parallel>\\<cdot>\\<parallel>)"} has a function norm. |
105 normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm. |
109 *} |
106 *} |
110 |
107 |
111 lemma ex_fnorm [intro?]: |
108 lemma ex_fnorm [intro?]: |
112 "is_normed_vectorspace V norm \\<Longrightarrow> is_continuous V norm f |
109 "is_normed_vectorspace V norm \<Longrightarrow> is_continuous V norm f |
113 \\<Longrightarrow> is_function_norm f V norm \\<parallel>f\\<parallel>V,norm" |
110 \<Longrightarrow> is_function_norm f V norm \<parallel>f\<parallel>V,norm" |
114 proof (unfold function_norm_def is_function_norm_def |
111 proof (unfold function_norm_def is_function_norm_def |
115 is_continuous_def Sup_def, elim conjE, rule someI2_ex) |
112 is_continuous_def Sup_def, elim conjE, rule someI2_ex) |
116 assume "is_normed_vectorspace V norm" |
113 assume "is_normed_vectorspace V norm" |
117 assume "is_linearform V f" |
114 assume "is_linearform V f" |
118 and e: "\\<exists>c. \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x" |
115 and e: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x" |
119 |
116 |
120 txt {* The existence of the supremum is shown using the |
117 txt {* The existence of the supremum is shown using the |
121 completeness of the reals. Completeness means, that |
118 completeness of the reals. Completeness means, that |
122 every non-empty bounded set of reals has a |
119 every non-empty bounded set of reals has a |
123 supremum. *} |
120 supremum. *} |
124 show "\\<exists>a. is_Sup UNIV (B V norm f) a" |
121 show "\<exists>a. is_Sup UNIV (B V norm f) a" |
125 proof (unfold is_Sup_def, rule reals_complete) |
122 proof (unfold is_Sup_def, rule reals_complete) |
126 |
123 |
127 txt {* First we have to show that @{text B} is non-empty: *} |
124 txt {* First we have to show that @{text B} is non-empty: *} |
128 |
125 |
129 show "\\<exists>X. X \\<in> B V norm f" |
126 show "\<exists>X. X \<in> B V norm f" |
130 proof |
127 proof |
131 show "#0 \\<in> (B V norm f)" by (unfold B_def) blast |
128 show "#0 \<in> (B V norm f)" by (unfold B_def) blast |
132 qed |
129 qed |
133 |
130 |
134 txt {* Then we have to show that @{text B} is bounded: *} |
131 txt {* Then we have to show that @{text B} is bounded: *} |
135 |
132 |
136 from e show "\\<exists>Y. isUb UNIV (B V norm f) Y" |
133 from e show "\<exists>Y. isUb UNIV (B V norm f) Y" |
137 proof |
134 proof |
138 |
135 |
139 txt {* We know that @{text f} is bounded by some value @{text c}. *} |
136 txt {* We know that @{text f} is bounded by some value @{text c}. *} |
140 |
137 |
141 fix c assume a: "\\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x" |
138 fix c assume a: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x" |
142 def b \\<equiv> "max c #0" |
139 def b \<equiv> "max c #0" |
143 |
140 |
144 show "?thesis" |
141 show "?thesis" |
145 proof (intro exI isUbI setleI ballI, unfold B_def, |
142 proof (intro exI isUbI setleI ballI, unfold B_def, |
146 elim UnE CollectE exE conjE singletonE) |
143 elim UnE CollectE exE conjE singletonE) |
147 |
144 |
148 txt {* To proof the thesis, we have to show that there is some |
145 txt {* To proof the thesis, we have to show that there is some |
149 constant @{text b}, such that @{text "y \\<le> b"} for all |
146 constant @{text b}, such that @{text "y \<le> b"} for all |
150 @{text "y \\<in> B"}. Due to the definition of @{text B} there are |
147 @{text "y \<in> B"}. Due to the definition of @{text B} there are |
151 two cases for @{text "y \\<in> B"}. If @{text "y = 0"} then |
148 two cases for @{text "y \<in> B"}. If @{text "y = 0"} then |
152 @{text "y \\<le> max c 0"}: *} |
149 @{text "y \<le> max c 0"}: *} |
153 |
150 |
154 fix y assume "y = (#0::real)" |
151 fix y assume "y = (#0::real)" |
155 show "y \\<le> b" by (simp! add: le_maxI2) |
152 show "y \<le> b" by (simp! add: le_maxI2) |
156 |
153 |
157 txt {* The second case is @{text "y = \\<bar>f x\\<bar> / \\<parallel>x\\<parallel>"} for some |
154 txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some |
158 @{text "x \\<in> V"} with @{text "x \\<noteq> 0"}. *} |
155 @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *} |
159 |
156 |
160 next |
157 next |
161 fix x y |
158 fix x y |
162 assume "x \\<in> V" "x \\<noteq> 0" |
159 assume "x \<in> V" "x \<noteq> 0" |
163 |
160 |
164 txt {* The thesis follows by a short calculation using the |
161 txt {* The thesis follows by a short calculation using the |
165 fact that @{text f} is bounded. *} |
162 fact that @{text f} is bounded. *} |
166 |
163 |
167 assume "y = \\<bar>f x\\<bar> * inverse (norm x)" |
164 assume "y = \<bar>f x\<bar> * inverse (norm x)" |
168 also have "... \\<le> c * norm x * inverse (norm x)" |
165 also have "... \<le> c * norm x * inverse (norm x)" |
169 proof (rule real_mult_le_le_mono2) |
166 proof (rule real_mult_le_le_mono2) |
170 show "#0 \\<le> inverse (norm x)" |
167 show "#0 \<le> inverse (norm x)" |
171 by (rule order_less_imp_le, rule real_inverse_gt_zero1, |
168 by (rule order_less_imp_le, rule real_inverse_gt_zero1, |
172 rule normed_vs_norm_gt_zero) |
169 rule normed_vs_norm_gt_zero) |
173 from a show "\\<bar>f x\\<bar> \\<le> c * norm x" .. |
170 from a show "\<bar>f x\<bar> \<le> c * norm x" .. |
174 qed |
171 qed |
175 also have "... = c * (norm x * inverse (norm x))" |
172 also have "... = c * (norm x * inverse (norm x))" |
176 by (rule real_mult_assoc) |
173 by (rule real_mult_assoc) |
177 also have "(norm x * inverse (norm x)) = (#1::real)" |
174 also have "(norm x * inverse (norm x)) = (#1::real)" |
178 proof (rule real_mult_inv_right1) |
175 proof (rule real_mult_inv_right1) |
179 show nz: "norm x \\<noteq> #0" |
176 show nz: "norm x \<noteq> #0" |
180 by (rule not_sym, rule lt_imp_not_eq, |
177 by (rule not_sym, rule lt_imp_not_eq, |
181 rule normed_vs_norm_gt_zero) |
178 rule normed_vs_norm_gt_zero) |
182 qed |
179 qed |
183 also have "c * ... \\<le> b " by (simp! add: le_maxI1) |
180 also have "c * ... \<le> b " by (simp! add: le_maxI1) |
184 finally show "y \\<le> b" . |
181 finally show "y \<le> b" . |
185 qed simp |
182 qed simp |
186 qed |
183 qed |
187 qed |
184 qed |
188 qed |
185 qed |
189 |
186 |
190 text {* The norm of a continuous function is always @{text "\\<ge> 0"}. *} |
187 text {* The norm of a continuous function is always @{text "\<ge> 0"}. *} |
191 |
188 |
192 lemma fnorm_ge_zero [intro?]: |
189 lemma fnorm_ge_zero [intro?]: |
193 "is_continuous V norm f \\<Longrightarrow> is_normed_vectorspace V norm |
190 "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm |
194 \\<Longrightarrow> #0 \\<le> \\<parallel>f\\<parallel>V,norm" |
191 \<Longrightarrow> #0 \<le> \<parallel>f\<parallel>V,norm" |
195 proof - |
192 proof - |
196 assume c: "is_continuous V norm f" |
193 assume c: "is_continuous V norm f" |
197 and n: "is_normed_vectorspace V norm" |
194 and n: "is_normed_vectorspace V norm" |
198 |
195 |
199 txt {* The function norm is defined as the supremum of @{text B}. |
196 txt {* The function norm is defined as the supremum of @{text B}. |
200 So it is @{text "\\<ge> 0"} if all elements in @{text B} are |
197 So it is @{text "\<ge> 0"} if all elements in @{text B} are |
201 @{text "\\<ge> 0"}, provided the supremum exists and @{text B} is not |
198 @{text "\<ge> 0"}, provided the supremum exists and @{text B} is not |
202 empty. *} |
199 empty. *} |
203 |
200 |
204 show ?thesis |
201 show ?thesis |
205 proof (unfold function_norm_def, rule sup_ub1) |
202 proof (unfold function_norm_def, rule sup_ub1) |
206 show "\\<forall>x \\<in> (B V norm f). #0 \\<le> x" |
203 show "\<forall>x \<in> (B V norm f). #0 \<le> x" |
207 proof (intro ballI, unfold B_def, |
204 proof (intro ballI, unfold B_def, |
208 elim UnE singletonE CollectE exE conjE) |
205 elim UnE singletonE CollectE exE conjE) |
209 fix x r |
206 fix x r |
210 assume "x \\<in> V" "x \\<noteq> 0" |
207 assume "x \<in> V" "x \<noteq> 0" |
211 and r: "r = \\<bar>f x\\<bar> * inverse (norm x)" |
208 and r: "r = \<bar>f x\<bar> * inverse (norm x)" |
212 |
209 |
213 have ge: "#0 \\<le> \\<bar>f x\\<bar>" by (simp! only: abs_ge_zero) |
210 have ge: "#0 \<le> \<bar>f x\<bar>" by (simp! only: abs_ge_zero) |
214 have "#0 \\<le> inverse (norm x)" |
211 have "#0 \<le> inverse (norm x)" |
215 by (rule order_less_imp_le, rule real_inverse_gt_zero1, rule)(*** |
212 by (rule order_less_imp_le, rule real_inverse_gt_zero1, rule)(*** |
216 proof (rule order_less_imp_le); |
213 proof (rule order_less_imp_le); |
217 show "#0 < inverse (norm x)"; |
214 show "#0 < inverse (norm x)"; |
218 proof (rule real_inverse_gt_zero); |
215 proof (rule real_inverse_gt_zero); |
219 show "#0 < norm x"; ..; |
216 show "#0 < norm x"; ..; |
220 qed; |
217 qed; |
221 qed; ***) |
218 qed; ***) |
222 with ge show "#0 \\<le> r" |
219 with ge show "#0 \<le> r" |
223 by (simp only: r, rule real_le_mult_order1a) |
220 by (simp only: r, rule real_le_mult_order1a) |
224 qed (simp!) |
221 qed (simp!) |
225 |
222 |
226 txt {* Since @{text f} is continuous the function norm exists: *} |
223 txt {* Since @{text f} is continuous the function norm exists: *} |
227 |
224 |
228 have "is_function_norm f V norm \\<parallel>f\\<parallel>V,norm" .. |
225 have "is_function_norm f V norm \<parallel>f\<parallel>V,norm" .. |
229 thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" |
226 thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" |
230 by (unfold is_function_norm_def function_norm_def) |
227 by (unfold is_function_norm_def function_norm_def) |
231 |
228 |
232 txt {* @{text B} is non-empty by construction: *} |
229 txt {* @{text B} is non-empty by construction: *} |
233 |
230 |
234 show "#0 \\<in> B V norm f" by (rule B_not_empty) |
231 show "#0 \<in> B V norm f" by (rule B_not_empty) |
235 qed |
232 qed |
236 qed |
233 qed |
237 |
234 |
238 text {* |
235 text {* |
239 \medskip The fundamental property of function norms is: |
236 \medskip The fundamental property of function norms is: |
240 \begin{center} |
237 \begin{center} |
241 @{text "\\<bar>f x\\<bar> \\<le> \\<parallel>f\\<parallel> \\<cdot> \\<parallel>x\\<parallel>"} |
238 @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} |
242 \end{center} |
239 \end{center} |
243 *} |
240 *} |
244 |
241 |
245 lemma norm_fx_le_norm_f_norm_x: |
242 lemma norm_fx_le_norm_f_norm_x: |
246 "is_continuous V norm f \\<Longrightarrow> is_normed_vectorspace V norm \\<Longrightarrow> x \\<in> V |
243 "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm \<Longrightarrow> x \<in> V |
247 \\<Longrightarrow> \\<bar>f x\\<bar> \\<le> \\<parallel>f\\<parallel>V,norm * norm x" |
244 \<Longrightarrow> \<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" |
248 proof - |
245 proof - |
249 assume "is_normed_vectorspace V norm" "x \\<in> V" |
246 assume "is_normed_vectorspace V norm" "x \<in> V" |
250 and c: "is_continuous V norm f" |
247 and c: "is_continuous V norm f" |
251 have v: "is_vectorspace V" .. |
248 have v: "is_vectorspace V" .. |
252 |
249 |
253 txt{* The proof is by case analysis on @{text x}. *} |
250 txt{* The proof is by case analysis on @{text x}. *} |
254 |
251 |
258 txt {* For the case @{text "x = 0"} the thesis follows from the |
255 txt {* For the case @{text "x = 0"} the thesis follows from the |
259 linearity of @{text f}: for every linear function holds |
256 linearity of @{text f}: for every linear function holds |
260 @{text "f 0 = 0"}. *} |
257 @{text "f 0 = 0"}. *} |
261 |
258 |
262 assume "x = 0" |
259 assume "x = 0" |
263 have "\\<bar>f x\\<bar> = \\<bar>f 0\\<bar>" by (simp!) |
260 have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by (simp!) |
264 also from v continuous_linearform have "f 0 = #0" .. |
261 also from v continuous_linearform have "f 0 = #0" .. |
265 also note abs_zero |
262 also note abs_zero |
266 also have "#0 \\<le> \\<parallel>f\\<parallel>V,norm * norm x" |
263 also have "#0 \<le> \<parallel>f\<parallel>V,norm * norm x" |
267 proof (rule real_le_mult_order1a) |
264 proof (rule real_le_mult_order1a) |
268 show "#0 \\<le> \\<parallel>f\\<parallel>V,norm" .. |
265 show "#0 \<le> \<parallel>f\<parallel>V,norm" .. |
269 show "#0 \\<le> norm x" .. |
266 show "#0 \<le> norm x" .. |
270 qed |
267 qed |
271 finally |
268 finally |
272 show "\\<bar>f x\\<bar> \\<le> \\<parallel>f\\<parallel>V,norm * norm x" . |
269 show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" . |
273 |
270 |
274 next |
271 next |
275 assume "x \\<noteq> 0" |
272 assume "x \<noteq> 0" |
276 have n: "#0 < norm x" .. |
273 have n: "#0 < norm x" .. |
277 hence nz: "norm x \\<noteq> #0" |
274 hence nz: "norm x \<noteq> #0" |
278 by (simp only: lt_imp_not_eq) |
275 by (simp only: lt_imp_not_eq) |
279 |
276 |
280 txt {* For the case @{text "x \\<noteq> 0"} we derive the following fact |
277 txt {* For the case @{text "x \<noteq> 0"} we derive the following fact |
281 from the definition of the function norm:*} |
278 from the definition of the function norm:*} |
282 |
279 |
283 have l: "\\<bar>f x\\<bar> * inverse (norm x) \\<le> \\<parallel>f\\<parallel>V,norm" |
280 have l: "\<bar>f x\<bar> * inverse (norm x) \<le> \<parallel>f\<parallel>V,norm" |
284 proof (unfold function_norm_def, rule sup_ub) |
281 proof (unfold function_norm_def, rule sup_ub) |
285 from ex_fnorm [OF _ c] |
282 from ex_fnorm [OF _ c] |
286 show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" |
283 show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" |
287 by (simp! add: is_function_norm_def function_norm_def) |
284 by (simp! add: is_function_norm_def function_norm_def) |
288 show "\\<bar>f x\\<bar> * inverse (norm x) \\<in> B V norm f" |
285 show "\<bar>f x\<bar> * inverse (norm x) \<in> B V norm f" |
289 by (unfold B_def, intro UnI2 CollectI exI [of _ x] |
286 by (unfold B_def, intro UnI2 CollectI exI [of _ x] |
290 conjI, simp) |
287 conjI, simp) |
291 qed |
288 qed |
292 |
289 |
293 txt {* The thesis now follows by a short calculation: *} |
290 txt {* The thesis now follows by a short calculation: *} |
294 |
291 |
295 have "\\<bar>f x\\<bar> = \\<bar>f x\\<bar> * #1" by (simp!) |
292 have "\<bar>f x\<bar> = \<bar>f x\<bar> * #1" by (simp!) |
296 also from nz have "#1 = inverse (norm x) * norm x" |
293 also from nz have "#1 = inverse (norm x) * norm x" |
297 by (simp add: real_mult_inv_left1) |
294 by (simp add: real_mult_inv_left1) |
298 also have "\\<bar>f x\\<bar> * ... = \\<bar>f x\\<bar> * inverse (norm x) * norm x" |
295 also have "\<bar>f x\<bar> * ... = \<bar>f x\<bar> * inverse (norm x) * norm x" |
299 by (simp! add: real_mult_assoc) |
296 by (simp! add: real_mult_assoc) |
300 also from n l have "... \\<le> \\<parallel>f\\<parallel>V,norm * norm x" |
297 also from n l have "... \<le> \<parallel>f\<parallel>V,norm * norm x" |
301 by (simp add: real_mult_le_le_mono2) |
298 by (simp add: real_mult_le_le_mono2) |
302 finally show "\\<bar>f x\\<bar> \\<le> \\<parallel>f\\<parallel>V,norm * norm x" . |
299 finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" . |
303 qed |
300 qed |
304 qed |
301 qed |
305 |
302 |
306 text {* |
303 text {* |
307 \medskip The function norm is the least positive real number for |
304 \medskip The function norm is the least positive real number for |
308 which the following inequation holds: |
305 which the following inequation holds: |
309 \begin{center} |
306 \begin{center} |
310 @{text "\\<bar>f x\\<bar> \\<le> c \\<cdot> \\<parallel>x\\<parallel>"} |
307 @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} |
311 \end{center} |
308 \end{center} |
312 *} |
309 *} |
313 |
310 |
314 lemma fnorm_le_ub: |
311 lemma fnorm_le_ub: |
315 "is_continuous V norm f \\<Longrightarrow> is_normed_vectorspace V norm \\<Longrightarrow> |
312 "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm \<Longrightarrow> |
316 \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x \\<Longrightarrow> #0 \\<le> c |
313 \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x \<Longrightarrow> #0 \<le> c |
317 \\<Longrightarrow> \\<parallel>f\\<parallel>V,norm \\<le> c" |
314 \<Longrightarrow> \<parallel>f\<parallel>V,norm \<le> c" |
318 proof (unfold function_norm_def) |
315 proof (unfold function_norm_def) |
319 assume "is_normed_vectorspace V norm" |
316 assume "is_normed_vectorspace V norm" |
320 assume c: "is_continuous V norm f" |
317 assume c: "is_continuous V norm f" |
321 assume fb: "\\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x" |
318 assume fb: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x" |
322 and "#0 \\<le> c" |
319 and "#0 \<le> c" |
323 |
320 |
324 txt {* Suppose the inequation holds for some @{text "c \\<ge> 0"}. If |
321 txt {* Suppose the inequation holds for some @{text "c \<ge> 0"}. If |
325 @{text c} is an upper bound of @{text B}, then @{text c} is greater |
322 @{text c} is an upper bound of @{text B}, then @{text c} is greater |
326 than the function norm since the function norm is the least upper |
323 than the function norm since the function norm is the least upper |
327 bound. *} |
324 bound. *} |
328 |
325 |
329 show "Sup UNIV (B V norm f) \\<le> c" |
326 show "Sup UNIV (B V norm f) \<le> c" |
330 proof (rule sup_le_ub) |
327 proof (rule sup_le_ub) |
331 from ex_fnorm [OF _ c] |
328 from ex_fnorm [OF _ c] |
332 show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" |
329 show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" |
333 by (simp! add: is_function_norm_def function_norm_def) |
330 by (simp! add: is_function_norm_def function_norm_def) |
334 |
331 |
335 txt {* @{text c} is an upper bound of @{text B}, i.e. every |
332 txt {* @{text c} is an upper bound of @{text B}, i.e. every |
336 @{text "y \\<in> B"} is less than @{text c}. *} |
333 @{text "y \<in> B"} is less than @{text c}. *} |
337 |
334 |
338 show "isUb UNIV (B V norm f) c" |
335 show "isUb UNIV (B V norm f) c" |
339 proof (intro isUbI setleI ballI) |
336 proof (intro isUbI setleI ballI) |
340 fix y assume "y \\<in> B V norm f" |
337 fix y assume "y \<in> B V norm f" |
341 thus le: "y \\<le> c" |
338 thus le: "y \<le> c" |
342 proof (unfold B_def, elim UnE CollectE exE conjE singletonE) |
339 proof (unfold B_def, elim UnE CollectE exE conjE singletonE) |
343 |
340 |
344 txt {* The first case for @{text "y \\<in> B"} is @{text "y = 0"}. *} |
341 txt {* The first case for @{text "y \<in> B"} is @{text "y = 0"}. *} |
345 |
342 |
346 assume "y = #0" |
343 assume "y = #0" |
347 show "y \\<le> c" by (blast!) |
344 show "y \<le> c" by (blast!) |
348 |
345 |
349 txt{* The second case is @{text "y = \\<bar>f x\\<bar> / \\<parallel>x\\<parallel>"} for some |
346 txt{* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some |
350 @{text "x \\<in> V"} with @{text "x \\<noteq> 0"}. *} |
347 @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *} |
351 |
348 |
352 next |
349 next |
353 fix x |
350 fix x |
354 assume "x \\<in> V" "x \\<noteq> 0" |
351 assume "x \<in> V" "x \<noteq> 0" |
355 |
352 |
356 have lz: "#0 < norm x" |
353 have lz: "#0 < norm x" |
357 by (simp! add: normed_vs_norm_gt_zero) |
354 by (simp! add: normed_vs_norm_gt_zero) |
358 |
355 |
359 have nz: "norm x \\<noteq> #0" |
356 have nz: "norm x \<noteq> #0" |
360 proof (rule not_sym) |
357 proof (rule not_sym) |
361 from lz show "#0 \\<noteq> norm x" |
358 from lz show "#0 \<noteq> norm x" |
362 by (simp! add: order_less_imp_not_eq) |
359 by (simp! add: order_less_imp_not_eq) |
363 qed |
360 qed |
364 |
361 |
365 from lz have "#0 < inverse (norm x)" |
362 from lz have "#0 < inverse (norm x)" |
366 by (simp! add: real_inverse_gt_zero1) |
363 by (simp! add: real_inverse_gt_zero1) |
367 hence inverse_gez: "#0 \\<le> inverse (norm x)" |
364 hence inverse_gez: "#0 \<le> inverse (norm x)" |
368 by (rule order_less_imp_le) |
365 by (rule order_less_imp_le) |
369 |
366 |
370 assume "y = \\<bar>f x\\<bar> * inverse (norm x)" |
367 assume "y = \<bar>f x\<bar> * inverse (norm x)" |
371 also from inverse_gez have "... \\<le> c * norm x * inverse (norm x)" |
368 also from inverse_gez have "... \<le> c * norm x * inverse (norm x)" |
372 proof (rule real_mult_le_le_mono2) |
369 proof (rule real_mult_le_le_mono2) |
373 show "\\<bar>f x\\<bar> \\<le> c * norm x" by (rule bspec) |
370 show "\<bar>f x\<bar> \<le> c * norm x" by (rule bspec) |
374 qed |
371 qed |
375 also have "... \\<le> c" by (simp add: nz real_mult_assoc) |
372 also have "... \<le> c" by (simp add: nz real_mult_assoc) |
376 finally show ?thesis . |
373 finally show ?thesis . |
377 qed |
374 qed |
378 qed blast |
375 qed blast |
379 qed |
376 qed |
380 qed |
377 qed |