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