src/HOL/Hahn_Banach/Function_Norm.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46867 0883804b67bb
child 50918 3b6417e9f73e
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29291
diff changeset
     1
(*  Title:      HOL/Hahn_Banach/Function_Norm.thy
7566
c5a3f980a7af accomodate refined facts handling;
wenzelm
parents: 7535
diff changeset
     2
    Author:     Gertrud Bauer, TU Munich
c5a3f980a7af accomodate refined facts handling;
wenzelm
parents: 7535
diff changeset
     3
*)
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
     4
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
     5
header {* The norm of a function *}
7808
fd019ac3485f update from Gertrud;
wenzelm
parents: 7656
diff changeset
     6
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29291
diff changeset
     7
theory Function_Norm
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29291
diff changeset
     8
imports Normed_Space Function_Order
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
     9
begin
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    10
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    11
subsection {* Continuous linear forms*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    12
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    13
text {*
11472
wenzelm
parents: 10752
diff changeset
    14
  A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"}
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    15
  is \emph{continuous}, iff it is bounded, i.e.
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    16
  \begin{center}
11472
wenzelm
parents: 10752
diff changeset
    17
  @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    18
  \end{center}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    19
  In our application no other functions than linear forms are
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    20
  considered, so we can define continuous linear forms as bounded
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    21
  linear forms:
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    22
*}
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    23
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
    24
locale continuous = linearform +
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
    25
  fixes norm :: "_ \<Rightarrow> real"    ("\<parallel>_\<parallel>")
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    26
  assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    27
14254
342634f38451 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents: 14214
diff changeset
    28
declare continuous.intro [intro?] continuous_axioms.intro [intro?]
342634f38451 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents: 14214
diff changeset
    29
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    30
lemma continuousI [intro]:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
    31
  fixes norm :: "_ \<Rightarrow> real"  ("\<parallel>_\<parallel>")
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
    32
  assumes "linearform V f"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    33
  assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
    34
  shows "continuous V f norm"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    35
proof
23378
1d138d6bb461 tuned proofs: avoid implicit prems;
wenzelm
parents: 22931
diff changeset
    36
  show "linearform V f" by fact
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    37
  from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
    38
  then show "continuous_axioms V f norm" ..
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    39
qed
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    40
11472
wenzelm
parents: 10752
diff changeset
    41
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    42
subsection {* The norm of a linear form *}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    43
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    44
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    45
  The least real number @{text c} for which holds
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    46
  \begin{center}
11472
wenzelm
parents: 10752
diff changeset
    47
  @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    48
  \end{center}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    49
  is called the \emph{norm} of @{text f}.
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    50
11472
wenzelm
parents: 10752
diff changeset
    51
  For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    52
  defined as
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    53
  \begin{center}
11472
wenzelm
parents: 10752
diff changeset
    54
  @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"}
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    55
  \end{center}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    56
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    57
  For the case @{text "V = {0}"} the supremum would be taken from an
11472
wenzelm
parents: 10752
diff changeset
    58
  empty set. Since @{text \<real>} is unbounded, there would be no supremum.
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    59
  To avoid this situation it must be guaranteed that there is an
11472
wenzelm
parents: 10752
diff changeset
    60
  element in this set. This element must be @{text "{} \<ge> 0"} so that
13547
wenzelm
parents: 13524
diff changeset
    61
  @{text fn_norm} has the norm properties. Furthermore it does not
wenzelm
parents: 13524
diff changeset
    62
  have to change the norm in all other cases, so it must be @{text 0},
wenzelm
parents: 13524
diff changeset
    63
  as all other elements are @{text "{} \<ge> 0"}.
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    64
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    65
  Thus we define the set @{text B} where the supremum is taken from as
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    66
  follows:
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    67
  \begin{center}
11472
wenzelm
parents: 10752
diff changeset
    68
  @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"}
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    69
  \end{center}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    70
13547
wenzelm
parents: 13524
diff changeset
    71
  @{text fn_norm} is equal to the supremum of @{text B}, if the
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    72
  supremum exists (otherwise it is undefined).
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    73
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    74
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
    75
locale fn_norm =
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
    76
  fixes norm :: "_ \<Rightarrow> real"    ("\<parallel>_\<parallel>")
13547
wenzelm
parents: 13524
diff changeset
    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}"
wenzelm
parents: 13524
diff changeset
    78
  fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    79
  defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    80
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
    81
locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
    82
13547
wenzelm
parents: 13524
diff changeset
    83
lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f"
wenzelm
parents: 13524
diff changeset
    84
  by (simp add: B_def)
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    85
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    86
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    87
  The following lemma states that every continuous linear form on a
11472
wenzelm
parents: 10752
diff changeset
    88
  normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    89
*}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    90
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
    91
lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
    92
  assumes "continuous V f norm"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    93
  shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    94
proof -
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
    95
  interpret continuous V f norm by fact
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
    96
  txt {* The existence of the supremum is shown using the
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    97
    completeness of the reals. Completeness means, that every
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    98
    non-empty bounded set of reals has a supremum. *}
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    99
  have "\<exists>a. lub (B V f) a"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   100
  proof (rule real_complete)
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   101
    txt {* First we have to show that @{text B} is non-empty: *}
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   102
    have "0 \<in> B V f" ..
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   103
    then show "\<exists>x. x \<in> B V f" ..
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   104
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   105
    txt {* Then we have to show that @{text B} is bounded: *}
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   106
    show "\<exists>c. \<forall>y \<in> B V f. y \<le> c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   107
    proof -
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   108
      txt {* We know that @{text f} is bounded by some value @{text c}. *}
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   109
      from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   110
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   111
      txt {* To prove the thesis, we have to show that there is some
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   112
        @{text b}, such that @{text "y \<le> b"} for all @{text "y \<in>
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   113
        B"}. Due to the definition of @{text B} there are two cases. *}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
   114
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   115
      def b \<equiv> "max c 0"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   116
      have "\<forall>y \<in> B V f. y \<le> b"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   117
      proof
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   118
        fix y assume y: "y \<in> B V f"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   119
        show "y \<le> b"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   120
        proof cases
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   121
          assume "y = 0"
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   122
          then show ?thesis unfolding b_def by arith
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   123
        next
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   124
          txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   125
            @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   126
          assume "y \<noteq> 0"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   127
          with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   128
              and x: "x \<in> V" and neq: "x \<noteq> 0"
36778
739a9379e29b avoid using real-specific versions of generic lemmas
huffman
parents: 32960
diff changeset
   129
            by (auto simp add: B_def divide_inverse)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   130
          from x neq have gt: "0 < \<parallel>x\<parallel>" ..
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
   131
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   132
          txt {* The thesis follows by a short calculation using the
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   133
            fact that @{text f} is bounded. *}
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   134
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   135
          note y_rep
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   136
          also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14254
diff changeset
   137
          proof (rule mult_right_mono)
23378
1d138d6bb461 tuned proofs: avoid implicit prems;
wenzelm
parents: 22931
diff changeset
   138
            from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14254
diff changeset
   139
            from gt have "0 < inverse \<parallel>x\<parallel>" 
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14254
diff changeset
   140
              by (rule positive_imp_inverse_positive)
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   141
            then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   142
          qed
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   143
          also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)"
36778
739a9379e29b avoid using real-specific versions of generic lemmas
huffman
parents: 32960
diff changeset
   144
            by (rule Groups.mult_assoc)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   145
          also
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   146
          from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   147
          then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp 
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 36778
diff changeset
   148
          also have "c * 1 \<le> b" by (simp add: b_def)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   149
          finally show "y \<le> b" .
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   150
        qed
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   151
      qed
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   152
      then show ?thesis ..
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   153
    qed
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   154
  qed
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   155
  then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   156
qed
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   157
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   158
lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
   159
  assumes "continuous V f norm"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   160
  assumes b: "b \<in> B V f"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   161
  shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   162
proof -
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
   163
  interpret continuous V f norm by fact
13547
wenzelm
parents: 13524
diff changeset
   164
  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
   165
    using `continuous V f norm` by (rule fn_norm_works)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   166
  from this and b show ?thesis ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   167
qed
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   168
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   169
lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
   170
  assumes "continuous V f norm"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   171
  assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   172
  shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   173
proof -
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
   174
  interpret continuous V f norm by fact
13547
wenzelm
parents: 13524
diff changeset
   175
  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
   176
    using `continuous V f norm` by (rule fn_norm_works)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   177
  from this and b show ?thesis ..
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   178
qed
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   179
11472
wenzelm
parents: 10752
diff changeset
   180
text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
   181
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   182
lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
   183
  assumes "continuous V f norm"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   184
  shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   185
proof -
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
   186
  interpret continuous V f norm by fact
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   187
  txt {* The function norm is defined as the supremum of @{text B}.
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   188
    So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   189
    0"}, provided the supremum exists and @{text B} is not empty. *}
13547
wenzelm
parents: 13524
diff changeset
   190
  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
   191
    using `continuous V f norm` by (rule fn_norm_works)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   192
  moreover have "0 \<in> B V f" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   193
  ultimately show ?thesis ..
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   194
qed
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   195
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   196
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   197
  \medskip The fundamental property of function norms is:
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   198
  \begin{center}
11472
wenzelm
parents: 10752
diff changeset
   199
  @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   200
  \end{center}
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   201
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
   202
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   203
lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
   204
  assumes "continuous V f norm" "linearform V f"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   205
  assumes x: "x \<in> V"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   206
  shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   207
proof -
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
   208
  interpret continuous V f norm by fact
29291
d3cc5398bad5 avoid implicit use of prems;
wenzelm
parents: 29252
diff changeset
   209
  interpret linearform V f by fact
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   210
  show ?thesis
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   211
  proof cases
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   212
    assume "x = 0"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   213
    then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   214
    also have "f 0 = 0" by rule unfold_locales
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   215
    also have "\<bar>\<dots>\<bar> = 0" by simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   216
    also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
   217
      using `continuous V f norm` by (rule fn_norm_ge_zero)
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   218
    from x have "0 \<le> norm x" ..
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   219
    with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   220
    finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   221
  next
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   222
    assume "x \<noteq> 0"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   223
    with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   224
    then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   225
    also have "\<dots> \<le>  \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   226
    proof (rule mult_right_mono)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   227
      from x show "0 \<le> \<parallel>x\<parallel>" ..
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   228
      from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
36778
739a9379e29b avoid using real-specific versions of generic lemmas
huffman
parents: 32960
diff changeset
   229
        by (auto simp add: B_def divide_inverse)
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
   230
      with `continuous V f norm` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31795
diff changeset
   231
        by (rule fn_norm_ub)
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   232
    qed
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   233
    finally show ?thesis .
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   234
  qed
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   235
qed
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   236
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   237
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   238
  \medskip The function norm is the least positive real number for
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   239
  which the following inequation holds:
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   240
  \begin{center}
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   241
    @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   242
  \end{center}
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   243
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
   244
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   245
lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
   246
  assumes "continuous V f norm"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   247
  assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   248
  shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   249
proof -
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
   250
  interpret continuous V f norm by fact
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   251
  show ?thesis
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   252
  proof (rule fn_norm_leastB [folded B_def fn_norm_def])
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   253
    fix b assume b: "b \<in> B V f"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   254
    show "b \<le> c"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   255
    proof cases
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   256
      assume "b = 0"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   257
      with ge show ?thesis by simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   258
    next
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   259
      assume "b \<noteq> 0"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   260
      with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   261
        and x_neq: "x \<noteq> 0" and x: "x \<in> V"
36778
739a9379e29b avoid using real-specific versions of generic lemmas
huffman
parents: 32960
diff changeset
   262
        by (auto simp add: B_def divide_inverse)
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   263
      note b_rep
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   264
      also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   265
      proof (rule mult_right_mono)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31795
diff changeset
   266
        have "0 < \<parallel>x\<parallel>" using x x_neq ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31795
diff changeset
   267
        then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31795
diff changeset
   268
        from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   269
      qed
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   270
      also have "\<dots> = c"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   271
      proof -
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31795
diff changeset
   272
        from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31795
diff changeset
   273
        then show ?thesis by simp
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   274
      qed
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   275
      finally show ?thesis .
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   276
    qed
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
   277
  qed (insert `continuous V f norm`, simp_all add: continuous_def)
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   278
qed
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   279
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10606
diff changeset
   280
end