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