9 begin |
9 begin |
10 |
10 |
11 subsection \<open>Continuous linear forms\<close> |
11 subsection \<open>Continuous linear forms\<close> |
12 |
12 |
13 text \<open> |
13 text \<open> |
14 A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> is \<^emph>\<open>continuous\<close>, |
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 iff it is bounded, i.e. |
15 it is bounded, i.e. |
16 \begin{center} |
16 \begin{center} |
17 \<open>\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close> |
17 \<open>\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close> |
18 \end{center} |
18 \end{center} |
19 In our application no other functions than linear forms are considered, so |
19 In our application no other functions than linear forms are considered, so |
20 we can define continuous linear forms as bounded linear forms: |
20 we can define continuous linear forms as bounded linear forms: |
50 For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be defined as |
50 For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be defined as |
51 \begin{center} |
51 \begin{center} |
52 \<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> |
52 \<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> |
53 \end{center} |
53 \end{center} |
54 |
54 |
55 For the case \<open>V = {0}\<close> the supremum would be taken from an empty set. |
55 For the case \<open>V = {0}\<close> the supremum would be taken from an empty set. Since |
56 Since \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this |
56 \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this situation it |
57 situation it must be guaranteed that there is an element in this set. This |
57 must be guaranteed that there is an element in this set. This element must |
58 element must be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties. |
58 be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties. Furthermore it does |
59 Furthermore it does not have to change the norm in all other cases, so it |
59 not have to change the norm in all other cases, so it must be \<open>0\<close>, as all |
60 must be \<open>0\<close>, as all other elements are \<open>{} \<ge> 0\<close>. |
60 other elements are \<open>{} \<ge> 0\<close>. |
61 |
61 |
62 Thus we define the set \<open>B\<close> where the supremum is taken from as follows: |
62 Thus we define the set \<open>B\<close> where the supremum is taken from as follows: |
63 \begin{center} |
63 \begin{center} |
64 \<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close> |
64 \<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close> |
65 \end{center} |
65 \end{center} |
66 |
66 |
67 \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists |
67 \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists (otherwise |
68 (otherwise it is undefined). |
68 it is undefined). |
69 \<close> |
69 \<close> |
70 |
70 |
71 locale fn_norm = |
71 locale fn_norm = |
72 fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>") |
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}" |
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}" |