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