src/HOL/Real/HahnBanach/FunctionNorm.thy
author wenzelm
Tue Aug 27 11:03:05 2002 +0200 (2002-08-27)
changeset 13524 604d0f3622d6
parent 13515 a6a7025fd7e8
child 13547 bf399f3bd7dc
permissions -rw-r--r--
*** empty log message ***
     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 {*
    13   A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"}
    14   is \emph{continuous}, iff it is bounded, i.e.
    15   \begin{center}
    16   @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
    17   \end{center}
    18   In our application no other functions than linear forms are
    19   considered, so we can define continuous linear forms as bounded
    20   linear forms:
    21 *}
    22 
    23 locale continuous = var V + norm_syntax + linearform +
    24   assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
    25 
    26 lemma continuousI [intro]:
    27   includes norm_syntax + linearform
    28   assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
    29   shows "continuous V norm f"
    30 proof
    31   show "linearform V f" .
    32   from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast
    33   then show "continuous_axioms V norm f" ..
    34 qed
    35 
    36 
    37 subsection {* The norm of a linear form *}
    38 
    39 text {*
    40   The least real number @{text c} for which holds
    41   \begin{center}
    42   @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
    43   \end{center}
    44   is called the \emph{norm} of @{text f}.
    45 
    46   For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
    47   defined as
    48   \begin{center}
    49   @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"}
    50   \end{center}
    51 
    52   For the case @{text "V = {0}"} the supremum would be taken from an
    53   empty set. Since @{text \<real>} is unbounded, there would be no supremum.
    54   To avoid this situation it must be guaranteed that there is an
    55   element in this set. This element must be @{text "{} \<ge> 0"} so that
    56   @{text function_norm} has the norm properties. Furthermore
    57   it does not have to change the norm in all other cases, so it must
    58   be @{text 0}, as all other elements are @{text "{} \<ge> 0"}.
    59 
    60   Thus we define the set @{text B} where the supremum is taken from as
    61   follows:
    62   \begin{center}
    63   @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"}
    64   \end{center}
    65 
    66   @{text function_norm} is equal to the supremum of @{text B}, if the
    67   supremum exists (otherwise it is undefined).
    68 *}
    69 
    70 locale function_norm = norm_syntax +
    71   fixes B
    72   defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
    73   fixes function_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
    74   defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
    75 
    76 lemma (in function_norm) B_not_empty [intro]: "0 \<in> B V f"
    77   by (unfold B_def) simp
    78 
    79 locale (open) functional_vectorspace =
    80     normed_vectorspace + function_norm +
    81   fixes cont
    82   defines "cont f \<equiv> continuous V norm f"
    83 
    84 text {*
    85   The following lemma states that every continuous linear form on a
    86   normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
    87 *}
    88 
    89 lemma (in functional_vectorspace) function_norm_works:
    90   includes continuous
    91   shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    92 proof -
    93   txt {* The existence of the supremum is shown using the
    94     completeness of the reals. Completeness means, that every
    95     non-empty bounded set of reals has a supremum. *}
    96   have "\<exists>a. lub (B V f) a"
    97   proof (rule real_complete)
    98     txt {* First we have to show that @{text B} is non-empty: *}
    99     have "0 \<in> B V f" ..
   100     thus "\<exists>x. x \<in> B V f" ..
   101 
   102     txt {* Then we have to show that @{text B} is bounded: *}
   103     show "\<exists>c. \<forall>y \<in> B V f. y \<le> c"
   104     proof -
   105       txt {* We know that @{text f} is bounded by some value @{text c}. *}
   106       from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
   107 
   108       txt {* To prove the thesis, we have to show that there is some
   109         @{text b}, such that @{text "y \<le> b"} for all @{text "y \<in>
   110         B"}. Due to the definition of @{text B} there are two cases. *}
   111 
   112       def b \<equiv> "max c 0"
   113       have "\<forall>y \<in> B V f. y \<le> b"
   114       proof
   115         fix y assume y: "y \<in> B V f"
   116         show "y \<le> b"
   117         proof cases
   118           assume "y = 0"
   119           thus ?thesis by (unfold b_def) arith
   120         next
   121           txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
   122             @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
   123           assume "y \<noteq> 0"
   124           with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
   125               and x: "x \<in> V" and neq: "x \<noteq> 0"
   126             by (auto simp add: B_def real_divide_def)
   127           from x neq have gt: "0 < \<parallel>x\<parallel>" ..
   128 
   129           txt {* The thesis follows by a short calculation using the
   130             fact that @{text f} is bounded. *}
   131 
   132           note y_rep
   133           also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
   134           proof (rule real_mult_le_le_mono2)
   135             from c show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
   136             from gt have "0 < inverse \<parallel>x\<parallel>" by (rule real_inverse_gt_0)
   137             thus "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
   138           qed
   139           also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)"
   140             by (rule real_mult_assoc)
   141           also
   142           from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
   143           hence "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by (simp add: real_mult_inv_right1)
   144           also have "c * 1 \<le> b" by (simp add: b_def le_maxI1)
   145           finally show "y \<le> b" .
   146         qed
   147       qed
   148       thus ?thesis ..
   149     qed
   150   qed
   151   then show ?thesis
   152     by (unfold function_norm_def) (rule the_lubI_ex)
   153 qed
   154 
   155 lemma (in functional_vectorspace) function_norm_ub [intro?]:
   156   includes continuous
   157   assumes b: "b \<in> B V f"
   158   shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
   159 proof -
   160   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
   161   from this and b show ?thesis ..
   162 qed
   163 
   164 lemma (in functional_vectorspace) function_norm_least' [intro?]:
   165   includes continuous
   166   assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
   167   shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
   168 proof -
   169   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
   170   from this and b show ?thesis ..
   171 qed
   172 
   173 text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
   174 
   175 lemma (in functional_vectorspace) function_norm_ge_zero [iff]:
   176   includes continuous
   177   shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
   178 proof -
   179   txt {* The function norm is defined as the supremum of @{text B}.
   180     So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
   181     0"}, provided the supremum exists and @{text B} is not empty. *}
   182   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
   183   moreover have "0 \<in> B V f" ..
   184   ultimately show ?thesis ..
   185 qed
   186 
   187 text {*
   188   \medskip The fundamental property of function norms is:
   189   \begin{center}
   190   @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
   191   \end{center}
   192 *}
   193 
   194 lemma (in functional_vectorspace) function_norm_le_cong:
   195   includes continuous + vectorspace_linearform
   196   assumes x: "x \<in> V"
   197   shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
   198 proof cases
   199   assume "x = 0"
   200   then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
   201   also have "f 0 = 0" ..
   202   also have "\<bar>\<dots>\<bar> = 0" by simp
   203   also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
   204   proof (rule real_le_mult_order1a)
   205     show "0 \<le> \<parallel>f\<parallel>\<hyphen>V" ..
   206     show "0 \<le> norm x" ..
   207   qed
   208   finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
   209 next
   210   assume "x \<noteq> 0"
   211   with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp
   212   then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp
   213   also have "\<dots> \<le>  \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
   214   proof (rule real_mult_le_le_mono2)
   215     from x show "0 \<le> \<parallel>x\<parallel>" ..
   216     show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
   217     proof
   218       from x and neq show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
   219         by (auto simp add: B_def real_divide_def)
   220     qed
   221   qed
   222   finally show ?thesis .
   223 qed
   224 
   225 text {*
   226   \medskip The function norm is the least positive real number for
   227   which the following inequation holds:
   228   \begin{center}
   229     @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
   230   \end{center}
   231 *}
   232 
   233 lemma (in functional_vectorspace) function_norm_least [intro?]:
   234   includes continuous
   235   assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
   236   shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
   237 proof (rule function_norm_least')
   238   fix b assume b: "b \<in> B V f"
   239   show "b \<le> c"
   240   proof cases
   241     assume "b = 0"
   242     with ge show ?thesis by simp
   243   next
   244     assume "b \<noteq> 0"
   245     with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
   246         and x_neq: "x \<noteq> 0" and x: "x \<in> V"
   247       by (auto simp add: B_def real_divide_def)
   248     note b_rep
   249     also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
   250     proof (rule real_mult_le_le_mono2)
   251       have "0 < \<parallel>x\<parallel>" ..
   252       then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
   253       from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
   254     qed
   255     also have "\<dots> = c"
   256     proof -
   257       from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp
   258       then show ?thesis by simp
   259     qed
   260     finally show ?thesis .
   261   qed
   262 qed
   263 
   264 lemmas [iff?] =
   265   functional_vectorspace.function_norm_ge_zero
   266   functional_vectorspace.function_norm_le_cong
   267   functional_vectorspace.function_norm_least
   268 
   269 end