src/HOL/Hahn_Banach/Function_Norm.thy
 author nipkow Fri Aug 28 18:52:41 2009 +0200 (2009-08-28) changeset 32436 10cd49e0c067 parent 31795 be3e1cc5005c child 32960 69916a850301 permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
     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 real_divide_def)

   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 real_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 le_maxI1)

   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 real_divide_def)

   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 real_divide_def)

   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