src/HOL/Hahn_Banach/Function_Norm.thy
 author haftmann Fri Nov 01 18:51:14 2013 +0100 (2013-11-01) changeset 54230 b1d955791529 parent 50918 3b6417e9f73e child 57512 cc97b347b301 permissions -rw-r--r--
more simplification rules on unary and binary minus
     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 = linearform +

    25   fixes norm :: "_ \<Rightarrow> real"    ("\<parallel>_\<parallel>")

    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 f norm"

    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 f norm" ..

    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 =

    76   fixes norm :: "_ \<Rightarrow> real"    ("\<parallel>_\<parallel>")

    77   fixes B defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"

    78   fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)

    79   defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"

    80

    81 locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm

    82

    83 lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f"

    84   by (simp add: B_def)

    85

    86 text {*

    87   The following lemma states that every continuous linear form on a

    88   normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.

    89 *}

    90

    91 lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:

    92   assumes "continuous V f norm"

    93   shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"

    94 proof -

    95   interpret continuous V f norm by fact

    96   txt {* The existence of the supremum is shown using the

    97     completeness of the reals. Completeness means, that every

    98     non-empty bounded set of reals has a supremum. *}

    99   have "\<exists>a. lub (B V f) a"

   100   proof (rule real_complete)

   101     txt {* First we have to show that @{text B} is non-empty: *}

   102     have "0 \<in> B V f" ..

   103     then show "\<exists>x. x \<in> B V f" ..

   104

   105     txt {* Then we have to show that @{text B} is bounded: *}

   106     show "\<exists>c. \<forall>y \<in> B V f. y \<le> c"

   107     proof -

   108       txt {* We know that @{text f} is bounded by some value @{text c}. *}

   109       from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..

   110

   111       txt {* To prove the thesis, we have to show that there is some

   112         @{text b}, such that @{text "y \<le> b"} for all @{text "y \<in>

   113         B"}. Due to the definition of @{text B} there are two cases. *}

   114

   115       def b \<equiv> "max c 0"

   116       have "\<forall>y \<in> B V f. y \<le> b"

   117       proof

   118         fix y assume y: "y \<in> B V f"

   119         show "y \<le> b"

   120         proof cases

   121           assume "y = 0"

   122           then show ?thesis unfolding b_def by arith

   123         next

   124           txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some

   125             @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}

   126           assume "y \<noteq> 0"

   127           with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"

   128               and x: "x \<in> V" and neq: "x \<noteq> 0"

   129             by (auto simp add: B_def divide_inverse)

   130           from x neq have gt: "0 < \<parallel>x\<parallel>" ..

   131

   132           txt {* The thesis follows by a short calculation using the

   133             fact that @{text f} is bounded. *}

   134

   135           note y_rep

   136           also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"

   137           proof (rule mult_right_mono)

   138             from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..

   139             from gt have "0 < inverse \<parallel>x\<parallel>"

   140               by (rule positive_imp_inverse_positive)

   141             then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)

   142           qed

   143           also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)"

   144             by (rule Groups.mult_assoc)

   145           also

   146           from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp

   147           then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp

   148           also have "c * 1 \<le> b" by (simp add: b_def)

   149           finally show "y \<le> b" .

   150         qed

   151       qed

   152       then show ?thesis ..

   153     qed

   154   qed

   155   then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex)

   156 qed

   157

   158 lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:

   159   assumes "continuous V f norm"

   160   assumes b: "b \<in> B V f"

   161   shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"

   162 proof -

   163   interpret continuous V f norm by fact

   164   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"

   165     using continuous V f norm by (rule fn_norm_works)

   166   from this and b show ?thesis ..

   167 qed

   168

   169 lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:

   170   assumes "continuous V f norm"

   171   assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"

   172   shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"

   173 proof -

   174   interpret continuous V f norm by fact

   175   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"

   176     using continuous V f norm by (rule fn_norm_works)

   177   from this and b show ?thesis ..

   178 qed

   179

   180 text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}

   181

   182 lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:

   183   assumes "continuous V f norm"

   184   shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"

   185 proof -

   186   interpret continuous V f norm by fact

   187   txt {* The function norm is defined as the supremum of @{text B}.

   188     So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>

   189     0"}, provided the supremum exists and @{text B} is not empty. *}

   190   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"

   191     using continuous V f norm by (rule fn_norm_works)

   192   moreover have "0 \<in> B V f" ..

   193   ultimately show ?thesis ..

   194 qed

   195

   196 text {*

   197   \medskip The fundamental property of function norms is:

   198   \begin{center}

   199   @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}

   200   \end{center}

   201 *}

   202

   203 lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:

   204   assumes "continuous V f norm" "linearform V f"

   205   assumes x: "x \<in> V"

   206   shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"

   207 proof -

   208   interpret continuous V f norm by fact

   209   interpret linearform V f by fact

   210   show ?thesis

   211   proof cases

   212     assume "x = 0"

   213     then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp

   214     also have "f 0 = 0" by rule unfold_locales

   215     also have "\<bar>\<dots>\<bar> = 0" by simp

   216     also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"

   217       using continuous V f norm by (rule fn_norm_ge_zero)

   218     from x have "0 \<le> norm x" ..

   219     with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)

   220     finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .

   221   next

   222     assume "x \<noteq> 0"

   223     with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp

   224     then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp

   225     also have "\<dots> \<le>  \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"

   226     proof (rule mult_right_mono)

   227       from x show "0 \<le> \<parallel>x\<parallel>" ..

   228       from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"

   229         by (auto simp add: B_def divide_inverse)

   230       with continuous V f norm show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"

   231         by (rule fn_norm_ub)

   232     qed

   233     finally show ?thesis .

   234   qed

   235 qed

   236

   237 text {*

   238   \medskip The function norm is the least positive real number for

   239   which the following inequation holds:

   240   \begin{center}

   241     @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}

   242   \end{center}

   243 *}

   244

   245 lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:

   246   assumes "continuous V f norm"

   247   assumes ineq: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"

   248   shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"

   249 proof -

   250   interpret continuous V f norm by fact

   251   show ?thesis

   252   proof (rule fn_norm_leastB [folded B_def fn_norm_def])

   253     fix b assume b: "b \<in> B V f"

   254     show "b \<le> c"

   255     proof cases

   256       assume "b = 0"

   257       with ge show ?thesis by simp

   258     next

   259       assume "b \<noteq> 0"

   260       with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"

   261         and x_neq: "x \<noteq> 0" and x: "x \<in> V"

   262         by (auto simp add: B_def divide_inverse)

   263       note b_rep

   264       also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"

   265       proof (rule mult_right_mono)

   266         have "0 < \<parallel>x\<parallel>" using x x_neq ..

   267         then show "0 \<le> inverse \<parallel>x\<parallel>" by simp

   268         from x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by (rule ineq)

   269       qed

   270       also have "\<dots> = c"

   271       proof -

   272         from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp

   273         then show ?thesis by simp

   274       qed

   275       finally show ?thesis .

   276     qed

   277   qed (insert continuous V f norm, simp_all add: continuous_def)

   278 qed

   279

   280 end