src/HOL/Hahn_Banach/Function_Norm.thy
 author blanchet Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) changeset 58306 117ba6cbe414 parent 57512 cc97b347b301 child 58744 c434e37f290e permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
1 (*  Title:      HOL/Hahn_Banach/Function_Norm.thy
2     Author:     Gertrud Bauer, TU Munich
3 *)
5 header {* The norm of a function *}
7 theory Function_Norm
8 imports Normed_Space Function_Order
9 begin
11 subsection {* Continuous linear forms*}
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 *}
24 locale continuous = linearform +
25   fixes norm :: "_ \<Rightarrow> real"    ("\<parallel>_\<parallel>")
26   assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
28 declare continuous.intro [intro?] continuous_axioms.intro [intro?]
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 f norm"
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 f norm" ..
39 qed
42 subsection {* The norm of a linear form *}
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}.
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}
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"}.
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}
71   @{text fn_norm} is equal to the supremum of @{text B}, if the
72   supremum exists (otherwise it is undefined).
73 *}
75 locale fn_norm =
76   fixes norm :: "_ \<Rightarrow> real"    ("\<parallel>_\<parallel>")
77   fixes B defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
78   fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
79   defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
81 locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm
83 lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f"
84   by (simp add: B_def)
86 text {*
87   The following lemma states that every continuous linear form on a
88   normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
89 *}
91 lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
92   assumes "continuous V f norm"
93   shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
94 proof -
95   interpret continuous V f norm by fact
96   txt {* The existence of the supremum is shown using the
97     completeness of the reals. Completeness means, that every
98     non-empty bounded set of reals has a supremum. *}
99   have "\<exists>a. lub (B V f) a"
100   proof (rule real_complete)
101     txt {* First we have to show that @{text B} is non-empty: *}
102     have "0 \<in> B V f" ..
103     then show "\<exists>x. x \<in> B V f" ..
105     txt {* Then we have to show that @{text B} is bounded: *}
106     show "\<exists>c. \<forall>y \<in> B V f. y \<le> c"
107     proof -
108       txt {* We know that @{text f} is bounded by some value @{text c}. *}
109       from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
111       txt {* To prove the thesis, we have to show that there is some
112         @{text b}, such that @{text "y \<le> b"} for all @{text "y \<in>
113         B"}. Due to the definition of @{text B} there are two cases. *}
115       def b \<equiv> "max c 0"
116       have "\<forall>y \<in> B V f. y \<le> b"
117       proof
118         fix y assume y: "y \<in> B V f"
119         show "y \<le> b"
120         proof cases
121           assume "y = 0"
122           then show ?thesis unfolding b_def by arith
123         next
124           txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
125             @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
126           assume "y \<noteq> 0"
127           with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
128               and x: "x \<in> V" and neq: "x \<noteq> 0"
129             by (auto simp add: B_def divide_inverse)
130           from x neq have gt: "0 < \<parallel>x\<parallel>" ..
132           txt {* The thesis follows by a short calculation using the
133             fact that @{text f} is bounded. *}
135           note y_rep
136           also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
137           proof (rule mult_right_mono)
138             from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
139             from gt have "0 < inverse \<parallel>x\<parallel>"
140               by (rule positive_imp_inverse_positive)
141             then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
142           qed
143           also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)"
144             by (rule Groups.mult.assoc)
145           also
146           from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
147           then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp
148           also have "c * 1 \<le> b" by (simp add: b_def)
149           finally show "y \<le> b" .
150         qed
151       qed
152       then show ?thesis ..
153     qed
154   qed
155   then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex)
156 qed
158 lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:
159   assumes "continuous V f norm"
160   assumes b: "b \<in> B V f"
161   shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
162 proof -
163   interpret continuous V f norm by fact
164   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
165     using continuous V f norm by (rule fn_norm_works)
166   from this and b show ?thesis ..
167 qed
169 lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:
170   assumes "continuous V f norm"
171   assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
172   shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
173 proof -
174   interpret continuous V f norm by fact
175   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
176     using continuous V f norm by (rule fn_norm_works)
177   from this and b show ?thesis ..
178 qed
180 text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
182 lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
183   assumes "continuous V f norm"
184   shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
185 proof -
186   interpret continuous V f norm by fact
187   txt {* The function norm is defined as the supremum of @{text B}.
188     So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
189     0"}, provided the supremum exists and @{text B} is not empty. *}
190   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
191     using continuous V f norm by (rule fn_norm_works)
192   moreover have "0 \<in> B V f" ..
193   ultimately show ?thesis ..
194 qed
196 text {*
197   \medskip The fundamental property of function norms is:
198   \begin{center}
199   @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
200   \end{center}
201 *}
203 lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:
204   assumes "continuous V f norm" "linearform V f"
205   assumes x: "x \<in> V"
206   shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
207 proof -
208   interpret continuous V f norm by fact
209   interpret linearform V f by fact
210   show ?thesis
211   proof cases
212     assume "x = 0"
213     then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
214     also have "f 0 = 0" by rule unfold_locales
215     also have "\<bar>\<dots>\<bar> = 0" by simp
216     also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
217       using continuous V f norm by (rule fn_norm_ge_zero)
218     from x have "0 \<le> norm x" ..
219     with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
220     finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
221   next
222     assume "x \<noteq> 0"
223     with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp
224     then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp
225     also have "\<dots> \<le>  \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
226     proof (rule mult_right_mono)
227       from x show "0 \<le> \<parallel>x\<parallel>" ..
228       from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
229         by (auto simp add: B_def divide_inverse)
230       with continuous V f norm show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
231         by (rule fn_norm_ub)
232     qed
233     finally show ?thesis .
234   qed
235 qed
237 text {*
238   \medskip The function norm is the least positive real number for
239   which the following inequation holds:
240   \begin{center}
241     @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
242   \end{center}
243 *}
245 lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
246   assumes "continuous V f norm"
247   assumes ineq: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
248   shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
249 proof -
250   interpret continuous V f norm by fact
251   show ?thesis
252   proof (rule fn_norm_leastB [folded B_def fn_norm_def])
253     fix b assume b: "b \<in> B V f"
254     show "b \<le> c"
255     proof cases
256       assume "b = 0"
257       with ge show ?thesis by simp
258     next
259       assume "b \<noteq> 0"
260       with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
261         and x_neq: "x \<noteq> 0" and x: "x \<in> V"
262         by (auto simp add: B_def divide_inverse)
263       note b_rep
264       also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
265       proof (rule mult_right_mono)
266         have "0 < \<parallel>x\<parallel>" using x x_neq ..
267         then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
268         from x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by (rule ineq)
269       qed
270       also have "\<dots> = c"
271       proof -
272         from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp
273         then show ?thesis by simp
274       qed
275       finally show ?thesis .
276     qed
277   qed (insert continuous V f norm, simp_all add: continuous_def)
278 qed
280 end