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