src/HOL/Real/HahnBanach/FunctionNorm.thy
 author wenzelm Sun Jul 23 12:01:05 2000 +0200 (2000-07-23) changeset 9408 d3d56e1d2ec1 parent 9394 1ff8a6234c6a child 9503 3324cbbecef8 permissions -rw-r--r--
classical atts now intro! / intro / intro?;
     1 (*  Title:      HOL/Real/HahnBanach/FunctionNorm.thy

     2     ID:         $Id$

     3     Author:     Gertrud Bauer, TU Munich

     4 *)

     5

     6 header {* The norm of a function *}

     7

     8 theory FunctionNorm = NormedSpace + FunctionOrder:

     9

    10 subsection {* Continuous linear forms*}

    11

    12 text{* A linear form $f$ on a normed vector space $(V, \norm{\cdot})$

    13 is \emph{continuous}, iff it is bounded, i.~e.

    14 $\Ex {c\in R}{\All {x\in V} {|f\ap x| \leq c \cdot \norm x}}$

    15 In our application no other functions than linear forms are considered,

    16 so we can define continuous linear forms as bounded linear forms:

    17 *}

    18

    19 constdefs

    20   is_continuous ::

    21   "['a::{plus, minus, zero} set, 'a => real, 'a => real] => bool"

    22   "is_continuous V norm f ==

    23     is_linearform V f \\<and> (\\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x)"

    24

    25 lemma continuousI [intro]:

    26   "[| is_linearform V f; !! x. x \\<in> V ==> |f x| <= c * norm x |]

    27   ==> is_continuous V norm f"

    28 proof (unfold is_continuous_def, intro exI conjI ballI)

    29   assume r: "!! x. x \\<in> V ==> |f x| <= c * norm x"

    30   fix x assume "x \\<in> V" show "|f x| <= c * norm x" by (rule r)

    31 qed

    32

    33 lemma continuous_linearform [intro?]:

    34   "is_continuous V norm f ==> is_linearform V f"

    35   by (unfold is_continuous_def) force

    36

    37 lemma continuous_bounded [intro?]:

    38   "is_continuous V norm f

    39   ==> \\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x"

    40   by (unfold is_continuous_def) force

    41

    42 subsection{* The norm of a linear form *}

    43

    44

    45 text{* The least real number $c$ for which holds

    46 $\All {x\in V}{|f\ap x| \leq c \cdot \norm x}$

    47 is called the \emph{norm} of $f$.

    48

    49 For non-trivial vector spaces $V \neq \{\zero\}$ the norm can be defined as

    50 $\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x}$

    51

    52 For the case $V = \{\zero\}$ the supremum would be taken from an

    53 empty set. Since $\bbbR$ is unbounded, there would be no supremum.  To

    54 avoid this situation it must be guaranteed that there is an element in

    55 this set. This element must be ${} \ge 0$ so that

    56 $\idt{function{\dsh}norm}$ has the norm properties. Furthermore it

    57 does not have to change the norm in all other cases, so it must be

    58 $0$, as all other elements of are ${} \ge 0$.

    59

    60 Thus we define the set $B$ the supremum is taken from as

    61 $  62 \{ 0 \} \Union \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}   63$

    64 *}

    65

    66 constdefs

    67   B :: "[ 'a set, 'a => real, 'a::{plus, minus, zero} => real ] => real set"

    68   "B V norm f ==

    69   {#0} \\<union> {|f x| * rinv (norm x) | x. x \\<noteq> 0 \\<and> x \\<in> V}"

    70

    71 text{* $n$ is the function norm of $f$, iff

    72 $n$ is the supremum of $B$.

    73 *}

    74

    75 constdefs

    76   is_function_norm ::

    77   " ['a::{minus,plus,zero}  => real, 'a set, 'a => real] => real => bool"

    78   "is_function_norm f V norm fn == is_Sup UNIV (B V norm f) fn"

    79

    80 text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$,

    81 if the supremum exists. Otherwise it is undefined. *}

    82

    83 constdefs

    84   function_norm :: " ['a::{minus,plus,zero} => real, 'a set, 'a => real] => real"

    85   "function_norm f V norm == Sup UNIV (B V norm f)"

    86

    87 syntax

    88   function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\\<parallel>_\\<parallel>_,_")

    89

    90 lemma B_not_empty: "#0 \\<in> B V norm f"

    91   by (unfold B_def, force)

    92

    93 text {* The following lemma states that every continuous linear form

    94 on a normed space $(V, \norm{\cdot})$ has a function norm. *}

    95

    96 lemma ex_fnorm [intro?]:

    97   "[| is_normed_vectorspace V norm; is_continuous V norm f|]

    98      ==> is_function_norm f V norm \\<parallel>f\\<parallel>V,norm"

    99 proof (unfold function_norm_def is_function_norm_def

   100   is_continuous_def Sup_def, elim conjE, rule selectI2EX)

   101   assume "is_normed_vectorspace V norm"

   102   assume "is_linearform V f"

   103   and e: "\\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x"

   104

   105   txt {* The existence of the supremum is shown using the

   106   completeness of the reals. Completeness means, that

   107   every non-empty bounded set of reals has a

   108   supremum. *}

   109   show  "\\<exists>a. is_Sup UNIV (B V norm f) a"

   110   proof (unfold is_Sup_def, rule reals_complete)

   111

   112     txt {* First we have to show that $B$ is non-empty: *}

   113

   114     show "\\<exists>X. X \\<in> B V norm f"

   115     proof (intro exI)

   116       show "#0 \\<in> (B V norm f)" by (unfold B_def, force)

   117     qed

   118

   119     txt {* Then we have to show that $B$ is bounded: *}

   120

   121     from e show "\\<exists>Y. isUb UNIV (B V norm f) Y"

   122     proof

   123

   124       txt {* We know that $f$ is bounded by some value $c$. *}

   125

   126       fix c assume a: "\\<forall>x \\<in> V. |f x| <= c * norm x"

   127       def b == "max c #0"

   128

   129       show "?thesis"

   130       proof (intro exI isUbI setleI ballI, unfold B_def,

   131 	elim UnE CollectE exE conjE singletonE)

   132

   133         txt{* To proof the thesis, we have to show that there is

   134         some constant $b$, such that $y \leq b$ for all $y\in B$.

   135         Due to the definition of $B$ there are two cases for

   136         $y\in B$. If $y = 0$ then $y \leq \idt{max}\ap c\ap 0$: *}

   137

   138 	fix y assume "y = (#0::real)"

   139         show "y <= b" by (simp! add: le_maxI2)

   140

   141         txt{* The second case is

   142         $y = {|f\ap x|}/{\norm x}$ for some

   143         $x\in V$ with $x \neq \zero$. *}

   144

   145       next

   146 	fix x y

   147         assume "x \\<in> V" "x \\<noteq> 0" (***

   148

   149          have ge: "#0 <= rinv (norm x)";

   150           by (rule real_less_imp_le, rule real_rinv_gt_zero,

   151                 rule normed_vs_norm_gt_zero); ( ***

   152           proof (rule real_less_imp_le);

   153             show "#0 < rinv (norm x)";

   154             proof (rule real_rinv_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| * rinv (norm x)"

   172         also have "... <= c * norm x * rinv (norm x)"

   173         proof (rule real_mult_le_le_mono2)

   174           show "#0 <= rinv (norm x)"

   175             by (rule real_less_imp_le, rule real_rinv_gt_zero1,

   176                 rule normed_vs_norm_gt_zero)

   177           from a show "|f x| <= c * norm x" ..

   178         qed

   179         also have "... = c * (norm x * rinv (norm x))"

   180           by (rule real_mult_assoc)

   181         also have "(norm x * rinv (norm x)) = (#1::real)"

   182         proof (rule real_mult_inv_right1)

   183           show nz: "norm x \\<noteq> #0"

   184             by (rule not_sym, rule lt_imp_not_eq,

   185               rule normed_vs_norm_gt_zero)

   186         qed

   187         also have "c * ... <= b " by (simp! add: le_maxI1)

   188 	finally show "y <= b" .

   189       qed simp

   190     qed

   191   qed

   192 qed

   193

   194 text {* The norm of a continuous function is always $\geq 0$. *}

   195

   196 lemma fnorm_ge_zero [intro?]:

   197   "[| is_continuous V norm f; is_normed_vectorspace V norm |]

   198    ==> #0 <= \\<parallel>f\\<parallel>V,norm"

   199 proof -

   200   assume c: "is_continuous V norm f"

   201      and n: "is_normed_vectorspace V norm"

   202

   203   txt {* The function norm is defined as the supremum of $B$.

   204   So it is $\geq 0$ if all elements in $B$ are $\geq 0$, provided

   205   the supremum exists and $B$ is not empty. *}

   206

   207   show ?thesis

   208   proof (unfold function_norm_def, rule sup_ub1)

   209     show "\\<forall>x \\<in> (B V norm f). #0 <= x"

   210     proof (intro ballI, unfold B_def,

   211            elim UnE singletonE CollectE exE conjE)

   212       fix x r

   213       assume "x \\<in> V" "x \\<noteq> 0"

   214         and r: "r = |f x| * rinv (norm x)"

   215

   216       have ge: "#0 <= |f x|" by (simp! only: abs_ge_zero)

   217       have "#0 <= rinv (norm x)"

   218         by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule)(***

   219         proof (rule real_less_imp_le);

   220           show "#0 < rinv (norm x)";

   221           proof (rule real_rinv_gt_zero);

   222             show "#0 < norm x"; ..;

   223           qed;

   224         qed; ***)

   225       with ge show "#0 <= r"

   226        by (simp only: r, rule real_le_mult_order1a)

   227     qed (simp!)

   228

   229     txt {* Since $f$ is continuous the function norm exists: *}

   230

   231     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))"

   233       by (unfold is_function_norm_def function_norm_def)

   234

   235     txt {* $B$ is non-empty by construction: *}

   236

   237     show "#0 \\<in> B V norm f" by (rule B_not_empty)

   238   qed

   239 qed

   240

   241 text{* \medskip The fundamental property of function norms is:

   242 \begin{matharray}{l}

   243 | f\ap x | \leq {\fnorm {f}} \cdot {\norm x}

   244 \end{matharray}

   245 *}

   246

   247 lemma norm_fx_le_norm_f_norm_x:

   248   "[| is_continuous V norm f; is_normed_vectorspace V norm; x \\<in> V |]

   249     ==> |f x| <= \\<parallel>f\\<parallel>V,norm * norm x"

   250 proof -

   251   assume "is_normed_vectorspace V norm" "x \\<in> V"

   252   and c: "is_continuous V norm f"

   253   have v: "is_vectorspace V" ..

   254

   255  txt{* The proof is by case analysis on $x$. *}

   256

   257   show ?thesis

   258   proof cases

   259

   260     txt {* For the case $x = \zero$ the thesis follows

   261     from the linearity of $f$: for every linear function

   262     holds $f\ap \zero = 0$. *}

   263

   264     assume "x = 0"

   265     have "|f x| = |f 0|" by (simp!)

   266     also from v continuous_linearform have "f 0 = #0" ..

   267     also note abs_zero

   268     also have "#0 <= \\<parallel>f\\<parallel>V,norm * norm x"

   269     proof (rule real_le_mult_order1a)

   270       show "#0 <= \\<parallel>f\\<parallel>V,norm" ..

   271       show "#0 <= norm x" ..

   272     qed

   273     finally

   274     show "|f x| <= \\<parallel>f\\<parallel>V,norm * norm x" .

   275

   276   next

   277     assume "x \\<noteq> 0"

   278     have n: "#0 < norm x" ..

   279     hence nz: "norm x \\<noteq> #0"

   280       by (simp only: lt_imp_not_eq)

   281

   282     txt {* For the case $x\neq \zero$ we derive the following

   283     fact from the definition of the function norm:*}

   284

   285     have l: "|f x| * rinv (norm x) <= \\<parallel>f\\<parallel>V,norm"

   286     proof (unfold function_norm_def, rule sup_ub)

   287       from ex_fnorm [OF _ c]

   288       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)

   290       show "|f x| * rinv (norm x) \\<in> B V norm f"

   291         by (unfold B_def, intro UnI2 CollectI exI [of _ x]

   292             conjI, simp)

   293     qed

   294

   295     txt {* The thesis now follows by a short calculation: *}

   296

   297     have "|f x| = |f x| * #1" by (simp!)

   298     also from nz have "#1 = rinv (norm x) * norm x"

   299       by (simp add: real_mult_inv_left1)

   300     also have "|f x| * ... = |f x| * rinv (norm x) * norm x"

   301       by (simp! add: real_mult_assoc)

   302     also from n l have "... <= \\<parallel>f\\<parallel>V,norm * norm x"

   303       by (simp add: real_mult_le_le_mono2)

   304     finally show "|f x| <= \\<parallel>f\\<parallel>V,norm * norm x" .

   305   qed

   306 qed

   307

   308 text{* \medskip The function norm is the least positive real number for

   309 which the following inequation holds:

   310 \begin{matharray}{l}

   311 | f\ap x | \leq c \cdot {\norm x}

   312 \end{matharray}

   313 *}

   314

   315 lemma fnorm_le_ub:

   316   "[| is_continuous V norm f; is_normed_vectorspace V norm;

   317      \\<forall>x \\<in> V. |f x| <= c * norm x; #0 <= c |]

   318   ==> \\<parallel>f\\<parallel>V,norm <= c"

   319 proof (unfold function_norm_def)

   320   assume "is_normed_vectorspace V norm"

   321   assume c: "is_continuous V norm f"

   322   assume fb: "\\<forall>x \\<in> V. |f x| <= c * norm x"

   323     and "#0 <= c"

   324

   325   txt {* Suppose the inequation holds for some $c\geq 0$.

   326   If $c$ is an upper bound of $B$, then $c$ is greater

   327   than the function norm since the function norm is the

   328   least upper bound.

   329   *}

   330

   331   show "Sup UNIV (B V norm f) <= c"

   332   proof (rule sup_le_ub)

   333     from ex_fnorm [OF _ c]

   334     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)

   336

   337     txt {* $c$ is an upper bound of $B$, i.e. every

   338     $y\in B$ is less than $c$. *}

   339

   340     show "isUb UNIV (B V norm f) c"

   341     proof (intro isUbI setleI ballI)

   342       fix y assume "y \\<in> B V norm f"

   343       thus le: "y <= c"

   344       proof (unfold B_def, elim UnE CollectE exE conjE singletonE)

   345

   346        txt {* The first case for $y\in B$ is $y=0$. *}

   347

   348         assume "y = #0"

   349         show "y <= c" by (force!)

   350

   351         txt{* The second case is

   352         $y = {|f\ap x|}/{\norm x}$ for some

   353         $x\in V$ with $x \neq \zero$. *}

   354

   355       next

   356 	fix x

   357         assume "x \\<in> V" "x \\<noteq> 0"

   358

   359         have lz: "#0 < norm x"

   360           by (simp! add: normed_vs_norm_gt_zero)

   361

   362         have nz: "norm x \\<noteq> #0"

   363         proof (rule not_sym)

   364           from lz show "#0 \\<noteq> norm x"

   365             by (simp! add: order_less_imp_not_eq)

   366         qed

   367

   368 	from lz have "#0 < rinv (norm x)"

   369 	  by (simp! add: real_rinv_gt_zero1)

   370 	hence rinv_gez: "#0 <= rinv (norm x)"

   371           by (rule real_less_imp_le)

   372

   373 	assume "y = |f x| * rinv (norm x)"

   374 	also from rinv_gez have "... <= c * norm x * rinv (norm x)"

   375 	  proof (rule real_mult_le_le_mono2)

   376 	    show "|f x| <= c * norm x" by (rule bspec)

   377 	  qed

   378 	also have "... <= c" by (simp add: nz real_mult_assoc)

   379 	finally show ?thesis .

   380       qed

   381     qed force

   382   qed

   383 qed

   384

   385 end