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