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