src/HOL/Hahn_Banach/Hahn_Banach.thy
 author wenzelm Mon Apr 25 16:09:26 2016 +0200 (2016-04-25) changeset 63040 eb4ddd18d635 parent 61879 e4f9d8f094fe child 65166 f8aafbf2b02e permissions -rw-r--r--
eliminated old 'def';
1 (*  Title:      HOL/Hahn_Banach/Hahn_Banach.thy
2     Author:     Gertrud Bauer, TU Munich
3 *)
5 section \<open>The Hahn-Banach Theorem\<close>
7 theory Hahn_Banach
8 imports Hahn_Banach_Lemmas
9 begin
11 text \<open>
12   We present the proof of two different versions of the Hahn-Banach Theorem,
13   closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
14 \<close>
17 subsection \<open>The Hahn-Banach Theorem for vector spaces\<close>
19 paragraph \<open>Hahn-Banach Theorem.\<close>
20 text \<open>
21   Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm on
22   \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded by
23   \<open>p\<close>, i.e. \<open>\<forall>x \<in> F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear form \<open>h\<close>
24   on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded by \<open>p\<close>.
25 \<close>
27 paragraph \<open>Proof Sketch.\<close>
28 text \<open>
29   \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces of
30   \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension.
32   \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper bound in \<open>M\<close>.
34   \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in \<open>M\<close>.
36   \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical
39     \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in a
40     norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>.
42     \<^item> Thus \<open>g\<close> can not be maximal. Contradiction!
43 \<close>
45 theorem Hahn_Banach:
46   assumes E: "vectorspace E" and "subspace F E"
47     and "seminorm E p" and "linearform F f"
48   assumes fp: "\<forall>x \<in> F. f x \<le> p x"
49   shows "\<exists>h. linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)"
50     \<comment> \<open>Let \<open>E\<close> be a vector space, \<open>F\<close> a subspace of \<open>E\<close>, \<open>p\<close> a seminorm on \<open>E\<close>,\<close>
51     \<comment> \<open>and \<open>f\<close> a linear form on \<open>F\<close> such that \<open>f\<close> is bounded by \<open>p\<close>,\<close>
52     \<comment> \<open>then \<open>f\<close> can be extended to a linear form \<open>h\<close> on \<open>E\<close> in a norm-preserving way. \<^smallskip>\<close>
53 proof -
54   interpret vectorspace E by fact
55   interpret subspace F E by fact
56   interpret seminorm E p by fact
57   interpret linearform F f by fact
58   define M where "M = norm_pres_extensions E p F f"
59   then have M: "M = \<dots>" by (simp only:)
60   from E have F: "vectorspace F" ..
61   note FE = \<open>F \<unlhd> E\<close>
62   {
63     fix c assume cM: "c \<in> chains M" and ex: "\<exists>x. x \<in> c"
64     have "\<Union>c \<in> M"
65       \<comment> \<open>Show that every non-empty chain \<open>c\<close> of \<open>M\<close> has an upper bound in \<open>M\<close>:\<close>
66       \<comment> \<open>\<open>\<Union>c\<close> is greater than any element of the chain \<open>c\<close>, so it suffices to show \<open>\<Union>c \<in> M\<close>.\<close>
67       unfolding M_def
68     proof (rule norm_pres_extensionI)
69       let ?H = "domain (\<Union>c)"
70       let ?h = "funct (\<Union>c)"
72       have a: "graph ?H ?h = \<Union>c"
73       proof (rule graph_domain_funct)
74         fix x y z assume "(x, y) \<in> \<Union>c" and "(x, z) \<in> \<Union>c"
75         with M_def cM show "z = y" by (rule sup_definite)
76       qed
77       moreover from M cM a have "linearform ?H ?h"
78         by (rule sup_lf)
79       moreover from a M cM ex FE E have "?H \<unlhd> E"
80         by (rule sup_subE)
81       moreover from a M cM ex FE have "F \<unlhd> ?H"
82         by (rule sup_supF)
83       moreover from a M cM ex have "graph F f \<subseteq> graph ?H ?h"
84         by (rule sup_ext)
85       moreover from a M cM have "\<forall>x \<in> ?H. ?h x \<le> p x"
86         by (rule sup_norm_pres)
87       ultimately show "\<exists>H h. \<Union>c = graph H h
88           \<and> linearform H h
89           \<and> H \<unlhd> E
90           \<and> F \<unlhd> H
91           \<and> graph F f \<subseteq> graph H h
92           \<and> (\<forall>x \<in> H. h x \<le> p x)" by blast
93     qed
94   }
95   then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> x = g"
96   \<comment> \<open>With Zorn's Lemma we can conclude that there is a maximal element in \<open>M\<close>. \<^smallskip>\<close>
97   proof (rule Zorn's_Lemma)
98       \<comment> \<open>We show that \<open>M\<close> is non-empty:\<close>
99     show "graph F f \<in> M"
100       unfolding M_def
101     proof (rule norm_pres_extensionI2)
102       show "linearform F f" by fact
103       show "F \<unlhd> E" by fact
104       from F show "F \<unlhd> F" by (rule vectorspace.subspace_refl)
105       show "graph F f \<subseteq> graph F f" ..
106       show "\<forall>x\<in>F. f x \<le> p x" by fact
107     qed
108   qed
109   then obtain g where gM: "g \<in> M" and gx: "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
110     by blast
111   from gM obtain H h where
112       g_rep: "g = graph H h"
113     and linearform: "linearform H h"
114     and HE: "H \<unlhd> E" and FH: "F \<unlhd> H"
115     and graphs: "graph F f \<subseteq> graph H h"
116     and hp: "\<forall>x \<in> H. h x \<le> p x" unfolding M_def ..
117       \<comment> \<open>\<open>g\<close> is a norm-preserving extension of \<open>f\<close>, in other words:\<close>
118       \<comment> \<open>\<open>g\<close> is the graph of some linear form \<open>h\<close> defined on a subspace \<open>H\<close> of \<open>E\<close>,\<close>
119       \<comment> \<open>and \<open>h\<close> is an extension of \<open>f\<close> that is again bounded by \<open>p\<close>. \<^smallskip>\<close>
120   from HE E have H: "vectorspace H"
121     by (rule subspace.vectorspace)
123   have HE_eq: "H = E"
124     \<comment> \<open>We show that \<open>h\<close> is defined on whole \<open>E\<close> by classical contradiction. \<^smallskip>\<close>
125   proof (rule classical)
126     assume neq: "H \<noteq> E"
127       \<comment> \<open>Assume \<open>h\<close> is not defined on whole \<open>E\<close>. Then show that \<open>h\<close> can be extended\<close>
128       \<comment> \<open>in a norm-preserving way to a function \<open>h'\<close> with the graph \<open>g'\<close>. \<^smallskip>\<close>
129     have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'"
130     proof -
131       from HE have "H \<subseteq> E" ..
132       with neq obtain x' where x'E: "x' \<in> E" and "x' \<notin> H" by blast
133       obtain x': "x' \<noteq> 0"
134       proof
135         show "x' \<noteq> 0"
136         proof
137           assume "x' = 0"
138           with H have "x' \<in> H" by (simp only: vectorspace.zero)
139           with \<open>x' \<notin> H\<close> show False by contradiction
140         qed
141       qed
143       define H' where "H' = H + lin x'"
144         \<comment> \<open>Define \<open>H'\<close> as the direct sum of \<open>H\<close> and the linear closure of \<open>x'\<close>. \<^smallskip>\<close>
145       have HH': "H \<unlhd> H'"
146       proof (unfold H'_def)
147         from x'E have "vectorspace (lin x')" ..
148         with H show "H \<unlhd> H + lin x'" ..
149       qed
151       obtain xi where
152         xi: "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
153           \<and> xi \<le> p (y + x') - h y"
154         \<comment> \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequality; this will\<close>
155         \<comment> \<open>be used to establish that \<open>h'\<close> is a norm-preserving extension of \<open>h\<close>.
156            \label{ex-xi-use}\<^smallskip>\<close>
157       proof -
158         from H have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y \<le> xi
159             \<and> xi \<le> p (y + x') - h y"
160         proof (rule ex_xi)
161           fix u v assume u: "u \<in> H" and v: "v \<in> H"
162           with HE have uE: "u \<in> E" and vE: "v \<in> E" by auto
163           from H u v linearform have "h v - h u = h (v - u)"
164             by (simp add: linearform.diff)
165           also from hp and H u v have "\<dots> \<le> p (v - u)"
166             by (simp only: vectorspace.diff_closed)
167           also from x'E uE vE have "v - u = x' + - x' + v + - u"
168             by (simp add: diff_eq1)
169           also from x'E uE vE have "\<dots> = v + x' + - (u + x')"
171           also from x'E uE vE have "\<dots> = (v + x') - (u + x')"
172             by (simp add: diff_eq1)
173           also from x'E uE vE E have "p \<dots> \<le> p (v + x') + p (u + x')"
175           finally have "h v - h u \<le> p (v + x') + p (u + x')" .
176           then show "- p (u + x') - h u \<le> p (v + x') - h v" by simp
177         qed
178         then show thesis by (blast intro: that)
179       qed
181       define h' where "h' x = (let (y, a) =
182           SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi)" for x
183         \<comment> \<open>Define the extension \<open>h'\<close> of \<open>h\<close> to \<open>H'\<close> using \<open>\<xi>\<close>. \<^smallskip>\<close>
185       have "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'"
186         \<comment> \<open>\<open>h'\<close> is an extension of \<open>h\<close> \dots \<^smallskip>\<close>
187       proof
188         show "g \<subseteq> graph H' h'"
189         proof -
190           have "graph H h \<subseteq> graph H' h'"
191           proof (rule graph_extI)
192             fix t assume t: "t \<in> H"
193             from E HE t have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
194               using \<open>x' \<notin> H\<close> \<open>x' \<in> E\<close> \<open>x' \<noteq> 0\<close> by (rule decomp_H'_H)
195             with h'_def show "h t = h' t" by (simp add: Let_def)
196           next
197             from HH' show "H \<subseteq> H'" ..
198           qed
199           with g_rep show ?thesis by (simp only:)
200         qed
202         show "g \<noteq> graph H' h'"
203         proof -
204           have "graph H h \<noteq> graph H' h'"
205           proof
206             assume eq: "graph H h = graph H' h'"
207             have "x' \<in> H'"
208               unfolding H'_def
209             proof
210               from H show "0 \<in> H" by (rule vectorspace.zero)
211               from x'E show "x' \<in> lin x'" by (rule x_lin_x)
212               from x'E show "x' = 0 + x'" by simp
213             qed
214             then have "(x', h' x') \<in> graph H' h'" ..
215             with eq have "(x', h' x') \<in> graph H h" by (simp only:)
216             then have "x' \<in> H" ..
217             with \<open>x' \<notin> H\<close> show False by contradiction
218           qed
219           with g_rep show ?thesis by simp
220         qed
221       qed
222       moreover have "graph H' h' \<in> M"
223         \<comment> \<open>and \<open>h'\<close> is norm-preserving. \<^smallskip>\<close>
224       proof (unfold M_def)
225         show "graph H' h' \<in> norm_pres_extensions E p F f"
226         proof (rule norm_pres_extensionI2)
227           show "linearform H' h'"
228             using h'_def H'_def HE linearform \<open>x' \<notin> H\<close> \<open>x' \<in> E\<close> \<open>x' \<noteq> 0\<close> E
229             by (rule h'_lf)
230           show "H' \<unlhd> E"
231           unfolding H'_def
232           proof
233             show "H \<unlhd> E" by fact
234             show "vectorspace E" by fact
235             from x'E show "lin x' \<unlhd> E" ..
236           qed
237           from H \<open>F \<unlhd> H\<close> HH' show FH': "F \<unlhd> H'"
238             by (rule vectorspace.subspace_trans)
239           show "graph F f \<subseteq> graph H' h'"
240           proof (rule graph_extI)
241             fix x assume x: "x \<in> F"
242             with graphs have "f x = h x" ..
243             also have "\<dots> = h x + 0 * xi" by simp
244             also have "\<dots> = (let (y, a) = (x, 0) in h y + a * xi)"
245               by (simp add: Let_def)
246             also have "(x, 0) =
247                 (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)"
248               using E HE
249             proof (rule decomp_H'_H [symmetric])
250               from FH x show "x \<in> H" ..
251               from x' show "x' \<noteq> 0" .
252               show "x' \<notin> H" by fact
253               show "x' \<in> E" by fact
254             qed
255             also have
256               "(let (y, a) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)
257               in h y + a * xi) = h' x" by (simp only: h'_def)
258             finally show "f x = h' x" .
259           next
260             from FH' show "F \<subseteq> H'" ..
261           qed
262           show "\<forall>x \<in> H'. h' x \<le> p x"
263             using h'_def H'_def \<open>x' \<notin> H\<close> \<open>x' \<in> E\<close> \<open>x' \<noteq> 0\<close> E HE
264               \<open>seminorm E p\<close> linearform and hp xi
265             by (rule h'_norm_pres)
266         qed
267       qed
268       ultimately show ?thesis ..
269     qed
270     then have "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp
271       \<comment> \<open>So the graph \<open>g\<close> of \<open>h\<close> cannot be maximal. Contradiction! \<^smallskip>\<close>
272     with gx show "H = E" by contradiction
273   qed
275   from HE_eq and linearform have "linearform E h"
276     by (simp only:)
277   moreover have "\<forall>x \<in> F. h x = f x"
278   proof
279     fix x assume "x \<in> F"
280     with graphs have "f x = h x" ..
281     then show "h x = f x" ..
282   qed
283   moreover from HE_eq and hp have "\<forall>x \<in> E. h x \<le> p x"
284     by (simp only:)
285   ultimately show ?thesis by blast
286 qed
289 subsection \<open>Alternative formulation\<close>
291 text \<open>
292   The following alternative formulation of the Hahn-Banach
293   Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form \<open>f\<close>
294   and a seminorm \<open>p\<close> the following inequality are equivalent:\footnote{This
295   was shown in lemma @{thm [source] abs_ineq_iff} (see page
296   \pageref{abs-ineq-iff}).}
297   \begin{center}
298   \begin{tabular}{lll}
299   \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and & \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\
300   \end{tabular}
301   \end{center}
302 \<close>
304 theorem abs_Hahn_Banach:
305   assumes E: "vectorspace E" and FE: "subspace F E"
306     and lf: "linearform F f" and sn: "seminorm E p"
307   assumes fp: "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
308   shows "\<exists>g. linearform E g
309     \<and> (\<forall>x \<in> F. g x = f x)
310     \<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x)"
311 proof -
312   interpret vectorspace E by fact
313   interpret subspace F E by fact
314   interpret linearform F f by fact
315   interpret seminorm E p by fact
316   have "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x) \<and> (\<forall>x \<in> E. g x \<le> p x)"
317     using E FE sn lf
318   proof (rule Hahn_Banach)
319     show "\<forall>x \<in> F. f x \<le> p x"
320       using FE E sn lf and fp by (rule abs_ineq_iff [THEN iffD1])
321   qed
322   then obtain g where lg: "linearform E g" and *: "\<forall>x \<in> F. g x = f x"
323       and **: "\<forall>x \<in> E. g x \<le> p x" by blast
324   have "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
325     using _ E sn lg **
326   proof (rule abs_ineq_iff [THEN iffD2])
327     show "E \<unlhd> E" ..
328   qed
329   with lg * show ?thesis by blast
330 qed
333 subsection \<open>The Hahn-Banach Theorem for normed spaces\<close>
335 text \<open>
336   Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>, can
337   be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> = \<parallel>g\<parallel>\<close>.
338 \<close>
340 theorem norm_Hahn_Banach:
341   fixes V and norm ("\<parallel>_\<parallel>")
342   fixes B defines "\<And>V f. B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
343   fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
344   defines "\<And>V f. \<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
345   assumes E_norm: "normed_vectorspace E norm" and FE: "subspace F E"
346     and linearform: "linearform F f" and "continuous F f norm"
347   shows "\<exists>g. linearform E g
348      \<and> continuous E g norm
349      \<and> (\<forall>x \<in> F. g x = f x)
350      \<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
351 proof -
352   interpret normed_vectorspace E norm by fact
353   interpret normed_vectorspace_with_fn_norm E norm B fn_norm
354     by (auto simp: B_def fn_norm_def) intro_locales
355   interpret subspace F E by fact
356   interpret linearform F f by fact
357   interpret continuous F f norm by fact
358   have E: "vectorspace E" by intro_locales
359   have F: "vectorspace F" by rule intro_locales
360   have F_norm: "normed_vectorspace F norm"
361     using FE E_norm by (rule subspace_normed_vs)
362   have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
363     by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero
364       [OF normed_vectorspace_with_fn_norm.intro,
365        OF F_norm \<open>continuous F f norm\<close> , folded B_def fn_norm_def])
366   txt \<open>We define a function \<open>p\<close> on \<open>E\<close> as follows:
367     \<open>p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>\<close>
368   define p where "p x = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>" for x
370   txt \<open>\<open>p\<close> is a seminorm on \<open>E\<close>:\<close>
371   have q: "seminorm E p"
372   proof
373     fix x y a assume x: "x \<in> E" and y: "y \<in> E"
375     txt \<open>\<open>p\<close> is positive definite:\<close>
376     have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
377     moreover from x have "0 \<le> \<parallel>x\<parallel>" ..
378     ultimately show "0 \<le> p x"
379       by (simp add: p_def zero_le_mult_iff)
381     txt \<open>\<open>p\<close> is absolutely homogeneous:\<close>
383     show "p (a \<cdot> x) = \<bar>a\<bar> * p x"
384     proof -
385       have "p (a \<cdot> x) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>a \<cdot> x\<parallel>" by (simp only: p_def)
386       also from x have "\<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>" by (rule abs_homogenous)
387       also have "\<parallel>f\<parallel>\<hyphen>F * (\<bar>a\<bar> * \<parallel>x\<parallel>) = \<bar>a\<bar> * (\<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>)" by simp
388       also have "\<dots> = \<bar>a\<bar> * p x" by (simp only: p_def)
389       finally show ?thesis .
390     qed
392     txt \<open>Furthermore, \<open>p\<close> is subadditive:\<close>
394     show "p (x + y) \<le> p x + p y"
395     proof -
396       have "p (x + y) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel>" by (simp only: p_def)
397       also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
398       from x y have "\<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" ..
399       with a have " \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>F * (\<parallel>x\<parallel> + \<parallel>y\<parallel>)"
400         by (simp add: mult_left_mono)
401       also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>" by (simp only: distrib_left)
402       also have "\<dots> = p x + p y" by (simp only: p_def)
403       finally show ?thesis .
404     qed
405   qed
407   txt \<open>\<open>f\<close> is bounded by \<open>p\<close>.\<close>
409   have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
410   proof
411     fix x assume "x \<in> F"
412     with \<open>continuous F f norm\<close> and linearform
413     show "\<bar>f x\<bar> \<le> p x"
414       unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
415         [OF normed_vectorspace_with_fn_norm.intro,
416          OF F_norm, folded B_def fn_norm_def])
417   qed
419   txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we can
420     apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be
421     extended in a norm-preserving way to some function \<open>g\<close> on the whole vector
422     space \<open>E\<close>.\<close>
424   with E FE linearform q obtain g where
425       linearformE: "linearform E g"
426     and a: "\<forall>x \<in> F. g x = f x"
427     and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
428     by (rule abs_Hahn_Banach [elim_format]) iprover
430   txt \<open>We furthermore have to show that \<open>g\<close> is also continuous:\<close>
432   have g_cont: "continuous E g norm" using linearformE
433   proof
434     fix x assume "x \<in> E"
435     with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
436       by (simp only: p_def)
437   qed
439   txt \<open>To complete the proof, we show that \<open>\<parallel>g\<parallel> = \<parallel>f\<parallel>\<close>.\<close>
441   have "\<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
442   proof (rule order_antisym)
443     txt \<open>
444       First we show \<open>\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>\<close>. The function norm \<open>\<parallel>g\<parallel>\<close> is defined as the
445       smallest \<open>c \<in> \<real>\<close> such that
446       \begin{center}
447       \begin{tabular}{l}
448       \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
449       \end{tabular}
450       \end{center}
451       \<^noindent> Furthermore holds
452       \begin{center}
453       \begin{tabular}{l}
454       \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>
455       \end{tabular}
456       \end{center}
457     \<close>
459     from g_cont _ ge_zero
460     show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
461     proof
462       fix x assume "x \<in> E"
463       with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
464         by (simp only: p_def)
465     qed
467     txt \<open>The other direction is achieved by a similar argument.\<close>
469     show "\<parallel>f\<parallel>\<hyphen>F \<le> \<parallel>g\<parallel>\<hyphen>E"
470     proof (rule normed_vectorspace_with_fn_norm.fn_norm_least
471         [OF normed_vectorspace_with_fn_norm.intro,
472          OF F_norm, folded B_def fn_norm_def])
473       fix x assume x: "x \<in> F"
474       show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
475       proof -
476         from a x have "g x = f x" ..
477         then have "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
478         also from g_cont
479         have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
480         proof (rule fn_norm_le_cong [OF _ linearformE, folded B_def fn_norm_def])
481           from FE x show "x \<in> E" ..
482         qed
483         finally show ?thesis .
484       qed
485     next
486       show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
487         using g_cont
488         by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
489       show "continuous F f norm" by fact
490     qed
491   qed
492   with linearformE a g_cont show ?thesis by blast
493 qed
495 end