(*  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::{plus, minus, zero} set, 'a => real, 'a => real] => bool" 

   "is_continuous V norm f == 

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

 lemma continuousI [intro]: 

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

   ==> is_continuous V norm f"

 proof (unfold is_continuous_def, intro exI conjI ballI)

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

   fix x assume "x \\<in> V" show "|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 

   ==> \\<exists>c. \\<forall>x \\<in> V. |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 \} \Union \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}

  \]

 *}

 constdefs

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

   "B V norm f == 

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

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

 $n$ is the supremum of $B$. 

 *}

 constdefs 

   is_function_norm :: 

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

   "is_function_norm f V norm 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::{minus,plus,zero} => real, 'a set, 'a => real] => real"

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

 syntax   

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

 lemma B_not_empty: "#0 \\<in> 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 f V norm \\<parallel>f\\<parallel>V,norm" 

 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: "\\<exists>c. \\<forall>x \\<in> V. |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  "\\<exists>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 "\\<exists>X. X \\<in> B V norm f" 

     proof (intro exI)

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

     qed

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

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

     proof

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

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

       def b == "max c #0"

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

         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 \\<in> V" "x \\<noteq> 0" (***

          have ge: "#0 <= 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 < rinv (norm x)";

             proof (rule real_rinv_gt_zero);

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

             qed;

           qed; *** )

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

           by (rule not_sym, rule lt_imp_not_eq, 

               rule normed_vs_norm_gt_zero) (***

           proof (rule not_sym);

             show "#0 \\<noteq> norm x"; 

             proof (rule lt_imp_not_eq);

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

             qed;

           qed; ***)***)

         txt {* The thesis follows by a short calculation using the 

         fact that $f$ is bounded. *}

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

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

         proof (rule real_mult_le_le_mono2)

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

             by (rule real_less_imp_le, rule real_rinv_gt_zero1, 

                 rule normed_vs_norm_gt_zero)

           from a show "|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 \\<noteq> #0" 

             by (rule not_sym, rule lt_imp_not_eq, 

               rule normed_vs_norm_gt_zero)

         qed

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

 	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 <= \\<parallel>f\\<parallel>V,norm"

 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 "\\<forall>x \\<in> (B V norm f). #0 <= x" 

     proof (intro ballI, unfold B_def,

            elim UnE singletonE CollectE exE conjE) 

       fix x r

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

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

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

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

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

         proof (rule real_less_imp_le);

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

           proof (rule real_rinv_gt_zero);

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

           qed;

         qed; ***)

       with ge show "#0 <= 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 f V norm \\<parallel>f\\<parallel>V,norm" ..

     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 \\<in> 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_continuous V norm f; is_normed_vectorspace V norm; x \\<in> V |] 

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

 proof - 

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

   and c: "is_continuous V norm f"

   have v: "is_vectorspace 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 = 0"

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

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

     also note abs_zero

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

     proof (rule real_le_mult_order1a)

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

       show "#0 <= norm x" ..

     qed

     finally 

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

   next

     assume "x \\<noteq> 0"

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

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

       by (simp only: lt_imp_not_eq)

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

     fact from the definition of the function norm:*}

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

     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 "|f x| * rinv (norm x) \\<in> 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 "|f x| = |f x| * #1" by (simp!)

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

       by (simp add: real_mult_inv_left1)

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

       by (simp! add: real_mult_assoc)

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

       by (simp add: real_mult_le_le_mono2)

     finally show "|f x| <= \\<parallel>f\\<parallel>V,norm * 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_continuous V norm f; is_normed_vectorspace V norm; 

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

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

 proof (unfold function_norm_def)

   assume "is_normed_vectorspace V norm" 

   assume c: "is_continuous V norm f"

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

     and "#0 <= 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 \\<in> 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"

         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 \\<in> V" "x \\<noteq> 0" 

         have lz: "#0 < norm x" 

           by (simp! add: normed_vs_norm_gt_zero)

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

         proof (rule not_sym)

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

             by (simp! add: order_less_imp_not_eq)

         qed

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

 	  by (simp! add: real_rinv_gt_zero1)

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

           by (rule real_less_imp_le)

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

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

 	  proof (rule real_mult_le_le_mono2)

 	    show "|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