src/HOL/Real/HahnBanach/FunctionNorm.thy

Updated files to remove 0r and 1r from theorems in descendant theories
of RealBin. Some new theorems added.

(*  Title:      HOL/Real/HahnBanach/FunctionNorm.thy
    ID:         $Id$
    Author:     Gertrud Bauer, TU Munich
*)

header {* The norm of a function *};

theory FunctionNorm = NormedSpace + FunctionOrder:;

subsection {* Continuous linear forms*};

text{* A linear form $f$ on a normed vector space $(V, \norm{\cdot})$
is \emph{continuous}, iff it is bounded, i.~e.
\[\Ex {c\in R}{\All {x\in V} {|f\ap x| \leq c \cdot \norm x}}\]
In our application no other functions than linear forms are considered,
so we can define continuous linear forms as bounded linear forms:
*};

constdefs
  is_continuous ::
  "['a::{minus, plus} set, 'a => real, 'a => real] => bool" 
  "is_continuous V norm f == 
    is_linearform V f & (EX c. ALL x:V. abs (f x) <= c * norm x)";

lemma continuousI [intro]: 
  "[| is_linearform V f; !! x. x:V ==> abs (f x) <= c * norm x |] 
  ==> is_continuous V norm f";
proof (unfold is_continuous_def, intro exI conjI ballI);
  assume r: "!! x. x:V ==> abs (f x) <= c * norm x"; 
  fix x; assume "x:V"; show "abs (f x) <= c * norm x"; by (rule r);
qed;
  
lemma continuous_linearform [intro??]: 
  "is_continuous V norm f ==> is_linearform V f";
  by (unfold is_continuous_def) force;

lemma continuous_bounded [intro??]:
  "is_continuous V norm f 
  ==> EX c. ALL x:V. abs (f x) <= c * norm x";
  by (unfold is_continuous_def) force;

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


text{* The least real number $c$ for which holds
\[\All {x\in V}{|f\ap x| \leq c \cdot \norm x}\]
is called the \emph{norm} of $f$.

For non-trivial vector spaces $V \neq \{\zero\}$ the norm can be defined as 
\[\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x} \] 

For the case $V = \{\zero\}$ the supremum would be taken from an
empty set. Since $\bbbR$ is unbounded, there would be no supremum.  To
avoid this situation it must be guaranteed that there is an element in
this set. This element must be ${} \ge 0$ so that
$\idt{function{\dsh}norm}$ has the norm properties. Furthermore it
does not have to change the norm in all other cases, so it must be
$0$, as all other elements of are ${} \ge 0$.

Thus we define the set $B$ the supremum is taken from as
\[
\{ 0 \} \Un \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}
 \]
*};

constdefs
  B :: "[ 'a set, 'a => real, 'a => real ] => real set"
  "B V norm f == 
  {(#0::real)} \Un {abs (f x) * rinv (norm x) | x. x ~= 00 & x:V}";

text{* $n$ is the function norm of $f$, iff 
$n$ is the supremum of $B$. 
*};

constdefs 
  is_function_norm :: 
  " ['a set, 'a => real, 'a => real] => real => bool"
  "is_function_norm V norm f fn == is_Sup UNIV (B V norm f) fn";

text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$, 
if the supremum exists. Otherwise it is undefined. *};

constdefs 
  function_norm :: " ['a set, 'a => real, 'a => real] => real"
  "function_norm V norm f == Sup UNIV (B V norm f)";

lemma B_not_empty: "(#0::real) : B V norm f";
  by (unfold B_def, force);

text {* The following lemma states that every continuous linear form
on a normed space $(V, \norm{\cdot})$ has a function norm. *};

lemma ex_fnorm [intro??]: 
  "[| is_normed_vectorspace V norm; is_continuous V norm f|]
     ==> is_function_norm V norm f (function_norm V norm f)"; 
proof (unfold function_norm_def is_function_norm_def 
  is_continuous_def Sup_def, elim conjE, rule selectI2EX);
  assume "is_normed_vectorspace V norm";
  assume "is_linearform V f" 
  and e: "EX c. ALL x:V. abs (f x) <= c * norm x";

  txt {* The existence of the supremum is shown using the 
  completeness of the reals. Completeness means, that
  every non-empty bounded set of reals has a 
  supremum. *};
  show  "EX a. is_Sup UNIV (B V norm f) a"; 
  proof (unfold is_Sup_def, rule reals_complete);

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

    show "EX X. X : B V norm f"; 
    proof (intro exI);
      show "(#0::real) : (B V norm f)"; by (unfold B_def, force);
    qed;

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

    from e; show "EX Y. isUb UNIV (B V norm f) Y";
    proof;

      txt {* We know that $f$ is bounded by some value $c$. *};  
  
      fix c; assume a: "ALL x:V. abs (f x) <= c * norm x";
      def b == "max c (#0::real)";

      show "?thesis";
      proof (intro exI isUbI setleI ballI, unfold B_def, 
	elim UnE CollectE exE conjE singletonE);

        txt{* To proof the thesis, we have to show that there is 
        some constant $b$, such that $y \leq b$ for all $y\in B$. 
        Due to the definition of $B$ there are two cases for
        $y\in B$. If $y = 0$ then $y \leq idt{max}\ap c\ap 0$: *};

	fix y; assume "y = (#0::real)";
        show "y <= b"; by (simp! add: le_max2);

        txt{* The second case is 
        $y = {|f\ap x|}/{\norm x}$ for some 
        $x\in V$ with $x \neq \zero$. *};

      next;
	fix x y;
        assume "x:V" "x ~= 00"; (***

         have ge: "(#0::real) <= rinv (norm x)";
          by (rule real_less_imp_le, rule real_rinv_gt_zero, 
                rule normed_vs_norm_gt_zero); (***
          proof (rule real_less_imp_le);
            show "(#0::real) < rinv (norm x)";
            proof (rule real_rinv_gt_zero);
              show "(#0::real) < norm x"; ..;
            qed;
          qed; ***)
        have nz: "norm x ~= (#0::real)"; 
          by (rule not_sym, rule lt_imp_not_eq, 
              rule normed_vs_norm_gt_zero); (***
          proof (rule not_sym);
            show "(#0::real) ~= norm x"; 
            proof (rule lt_imp_not_eq);
              show "(#0::real) < norm x"; ..;
            qed;
          qed; ***)***)

        txt {* The thesis follows by a short calculation using the 
        fact that $f$ is bounded. *};
    
        assume "y = abs (f x) * rinv (norm x)";
        also; have "... <= c * norm x * rinv (norm x)";
        proof (rule real_mult_le_le_mono2);
          show "(#0::real) <= rinv (norm x)";
            by (rule real_less_imp_le, rule real_rinv_gt_zero1, 
                rule normed_vs_norm_gt_zero);
          from a; show "abs (f x) <= c * norm x"; ..;
        qed;
        also; have "... = c * (norm x * rinv (norm x))"; 
          by (rule real_mult_assoc);
        also; have "(norm x * rinv (norm x)) = (#1::real)"; 
        proof (rule real_mult_inv_right1);
          show nz: "norm x ~= (#0::real)"; 
            by (rule not_sym, rule lt_imp_not_eq, 
              rule normed_vs_norm_gt_zero);
        qed;
        also; have "c * ... <= b "; by (simp! add: le_max1);
	finally; show "y <= b"; .;
      qed simp;
    qed;
  qed;
qed;

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

lemma fnorm_ge_zero [intro??]: 
  "[| is_continuous V norm f; is_normed_vectorspace V norm|]
   ==> (#0::real) <= function_norm V norm f";
proof -;
  assume c: "is_continuous V norm f" 
     and n: "is_normed_vectorspace V norm";

  txt {* The function norm is defined as the supremum of $B$. 
  So it is $\geq 0$ if all elements in $B$ are $\geq 0$, provided
  the supremum exists and $B$ is not empty. *};

  show ?thesis; 
  proof (unfold function_norm_def, rule sup_ub1);
    show "ALL x:(B V norm f). (#0::real) <= x"; 
    proof (intro ballI, unfold B_def,
           elim UnE singletonE CollectE exE conjE); 
      fix x r;
      assume "x : V" "x ~= 00" 
        and r: "r = abs (f x) * rinv (norm x)";

      have ge: "(#0::real) <= abs (f x)"; by (simp! only: abs_ge_zero);
      have "(#0::real) <= rinv (norm x)"; 
        by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule);(***
        proof (rule real_less_imp_le);
          show "(#0::real) < rinv (norm x)"; 
          proof (rule real_rinv_gt_zero);
            show "(#0::real) < norm x"; ..;
          qed;
        qed; ***)
      with ge; show "(#0::real) <= r";
       by (simp only: r, rule real_le_mult_order1a);
    qed (simp!);

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

    have "is_function_norm V norm f (function_norm V norm f)"; ..;
    thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
      by (unfold is_function_norm_def function_norm_def);

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

    show "(#0::real) : B V norm f"; by (rule B_not_empty);
  qed;
qed;
  
text{* \medskip The fundamental property of function norms is: 
\begin{matharray}{l}
| f\ap x | \leq {\fnorm {f}} \cdot {\norm x}  
\end{matharray}
*};

lemma norm_fx_le_norm_f_norm_x: 
  "[| is_normed_vectorspace V norm; x:V; is_continuous V norm f |] 
    ==> abs (f x) <= function_norm V norm f * norm x"; 
proof -; 
  assume "is_normed_vectorspace V norm" "x:V" 
  and c: "is_continuous V norm f";
  have v: "is_vectorspace V"; ..;
  assume "x:V";

 txt{* The proof is by case analysis on $x$. *};
 
  show ?thesis;
  proof cases;

    txt {* For the case $x = \zero$ the thesis follows
    from the linearity of $f$: for every linear function
    holds $f\ap \zero = 0$. *};

    assume "x = 00";
    have "abs (f x) = abs (f 00)"; by (simp!);
    also; from v continuous_linearform; have "f 00 = (#0::real)"; ..;
    also; note abs_zero;
    also; have "(#0::real) <= function_norm V norm f * norm x";
    proof (rule real_le_mult_order1a);
      show "(#0::real) <= function_norm V norm f"; ..;
      show "(#0::real) <= norm x"; ..;
    qed;
    finally; 
    show "abs (f x) <= function_norm V norm f * norm x"; .;

  next;
    assume "x ~= 00";
    have n: "(#0::real) <= norm x"; ..;
    have nz: "norm x ~= (#0::real)";
    proof (rule lt_imp_not_eq [RS not_sym]);
      show "(#0::real) < norm x"; ..;
    qed;

    txt {* For the case $x\neq \zero$ we derive the following
    fact from the definition of the function norm:*};

    have l: "abs (f x) * rinv (norm x) <= function_norm V norm f";
    proof (unfold function_norm_def, rule sup_ub);
      from ex_fnorm [OF _ c];
      show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
         by (simp! add: is_function_norm_def function_norm_def);
      show "abs (f x) * rinv (norm x) : B V norm f"; 
        by (unfold B_def, intro UnI2 CollectI exI [of _ x]
            conjI, simp);
    qed;

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

    have "abs (f x) = abs (f x) * (#1::real)"; by (simp!);
    also; from nz; have "(#1::real) = rinv (norm x) * norm x"; 
      by (rule real_mult_inv_left1 [RS sym]);
    also; 
    have "abs (f x) * ... = abs (f x) * rinv (norm x) * norm x";
      by (simp! add: real_mult_assoc [of "abs (f x)"]);
    also; have "... <= function_norm V norm f * norm x"; 
      by (rule real_mult_le_le_mono2 [OF n l]);
    finally; 
    show "abs (f x) <= function_norm V norm f * norm x"; .;
  qed;
qed;

text{* \medskip The function norm is the least positive real number for 
which the following inequation holds:
\begin{matharray}{l}
| f\ap x | \leq c \cdot {\norm x}  
\end{matharray} 
*};

lemma fnorm_le_ub: 
  "[| is_normed_vectorspace V norm; is_continuous V norm f;
     ALL x:V. abs (f x) <= c * norm x; (#0::real) <= c |]
  ==> function_norm V norm f <= c";
proof (unfold function_norm_def);
  assume "is_normed_vectorspace V norm"; 
  assume c: "is_continuous V norm f";
  assume fb: "ALL x:V. abs (f x) <= c * norm x"
         and "(#0::real) <= c";

  txt {* Suppose the inequation holds for some $c\geq 0$.
  If $c$ is an upper bound of $B$, then $c$ is greater 
  than the function norm since the function norm is the
  least upper bound.
  *};

  show "Sup UNIV (B V norm f) <= c"; 
  proof (rule sup_le_ub);
    from ex_fnorm [OF _ c]; 
    show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
      by (simp! add: is_function_norm_def function_norm_def); 
  
    txt {* $c$ is an upper bound of $B$, i.~e.~every
    $y\in B$ is less than $c$. *};

    show "isUb UNIV (B V norm f) c";  
    proof (intro isUbI setleI ballI);
      fix y; assume "y: B V norm f";
      thus le: "y <= c";
      proof (unfold B_def, elim UnE CollectE exE conjE singletonE);

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

        assume "y = (#0::real)";
        show "y <= c"; by (force!);

        txt{* The second case is 
        $y = {|f\ap x|}/{\norm x}$ for some 
        $x\in V$ with $x \neq \zero$. *};  

      next;
	fix x; 
        assume "x : V" "x ~= 00"; 

        have lz: "(#0::real) < norm x"; 
          by (simp! add: normed_vs_norm_gt_zero);
          
        have nz: "norm x ~= (#0::real)"; 
        proof (rule not_sym);
          from lz; show "(#0::real) ~= norm x";
            by (simp! add: order_less_imp_not_eq);
        qed;
            
	from lz; have "(#0::real) < rinv (norm x)";
	  by (simp! add: real_rinv_gt_zero1);
	hence rinv_gez: "(#0::real) <= rinv (norm x)";
          by (rule real_less_imp_le);

	assume "y = abs (f x) * rinv (norm x)"; 
	also; from rinv_gez; have "... <= c * norm x * rinv (norm x)";
	  proof (rule real_mult_le_le_mono2);
	    show "abs (f x) <= c * norm x"; by (rule bspec);
	  qed;
	also; have "... <= c"; by (simp add: nz real_mult_assoc);
	finally; show ?thesis; .;
      qed;
    qed force;
  qed;
qed;

end;