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