src/HOL/Hahn_Banach/Function_Norm.thy
 author wenzelm Mon Apr 25 16:09:26 2016 +0200 (2016-04-25) changeset 63040 eb4ddd18d635 parent 61879 e4f9d8f094fe permissions -rw-r--r--
eliminated old 'def';
tuned comments;
     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