src/HOL/Real/HahnBanach/NormedSpace.thy
author wenzelm
Sun Jul 23 12:01:05 2000 +0200 (2000-07-23)
changeset 9408 d3d56e1d2ec1
parent 9374 153853af318b
child 10687 c186279eecea
permissions -rw-r--r--
classical atts now intro! / intro / intro?;
wenzelm@7566
     1
(*  Title:      HOL/Real/HahnBanach/NormedSpace.thy
wenzelm@7566
     2
    ID:         $Id$
wenzelm@7566
     3
    Author:     Gertrud Bauer, TU Munich
wenzelm@7566
     4
*)
wenzelm@7535
     5
wenzelm@9035
     6
header {* Normed vector spaces *}
wenzelm@7808
     7
wenzelm@9035
     8
theory NormedSpace =  Subspace:
wenzelm@7535
     9
bauerg@9374
    10
syntax 
bauerg@9374
    11
  abs :: "real \<Rightarrow> real" ("|_|")
wenzelm@7535
    12
wenzelm@9035
    13
subsection {* Quasinorms *}
wenzelm@7808
    14
wenzelm@7978
    15
text{* A \emph{seminorm} $\norm{\cdot}$ is a function on a real vector
wenzelm@7978
    16
space into the reals that has the following properties: It is positive
wenzelm@9035
    17
definite, absolute homogenous and subadditive.  *}
wenzelm@7535
    18
wenzelm@7535
    19
constdefs
bauerg@9374
    20
  is_seminorm :: "['a::{plus, minus, zero} set, 'a => real] => bool"
bauerg@9374
    21
  "is_seminorm V norm == \<forall>x \<in>  V. \<forall>y \<in> V. \<forall>a. 
wenzelm@9035
    22
        #0 <= norm x 
bauerg@9374
    23
      \<and> norm (a \<cdot> x) = |a| * norm x
bauerg@9374
    24
      \<and> norm (x + y) <= norm x + norm y"
wenzelm@7535
    25
wenzelm@7978
    26
lemma is_seminormI [intro]: 
bauerg@9374
    27
  "[| !! x y a. [| x \<in> V; y \<in> V|] ==> #0 <= norm x;
bauerg@9374
    28
  !! x a. x \<in> V ==> norm (a \<cdot> x) = |a| * norm x;
bauerg@9374
    29
  !! x y. [|x \<in> V; y \<in> V |] ==> norm (x + y) <= norm x + norm y |] 
wenzelm@9035
    30
  ==> is_seminorm V norm"
wenzelm@9035
    31
  by (unfold is_seminorm_def, force)
wenzelm@7535
    32
wenzelm@9408
    33
lemma seminorm_ge_zero [intro?]:
bauerg@9374
    34
  "[| is_seminorm V norm; x \<in> V |] ==> #0 <= norm x"
wenzelm@9035
    35
  by (unfold is_seminorm_def, force)
wenzelm@7535
    36
wenzelm@8838
    37
lemma seminorm_abs_homogenous: 
bauerg@9374
    38
  "[| is_seminorm V norm; x \<in> V |] 
bauerg@9374
    39
  ==> norm (a \<cdot> x) = |a| * norm x"
wenzelm@9035
    40
  by (unfold is_seminorm_def, force)
wenzelm@7535
    41
wenzelm@7978
    42
lemma seminorm_subadditive: 
bauerg@9374
    43
  "[| is_seminorm V norm; x \<in> V; y \<in> V |] 
wenzelm@9035
    44
  ==> norm (x + y) <= norm x + norm y"
wenzelm@9035
    45
  by (unfold is_seminorm_def, force)
wenzelm@7535
    46
wenzelm@7978
    47
lemma seminorm_diff_subadditive: 
bauerg@9374
    48
  "[| is_seminorm V norm; x \<in> V; y \<in> V; is_vectorspace V |] 
wenzelm@9035
    49
  ==> norm (x - y) <= norm x + norm y"
wenzelm@9035
    50
proof -
bauerg@9374
    51
  assume "is_seminorm V norm" "x \<in> V" "y \<in> V" "is_vectorspace V"
bauerg@9374
    52
  have "norm (x - y) = norm (x + - #1 \<cdot> y)"  
wenzelm@9035
    53
    by (simp! add: diff_eq2 negate_eq2a)
bauerg@9374
    54
  also have "... <= norm x + norm  (- #1 \<cdot> y)" 
wenzelm@9035
    55
    by (simp! add: seminorm_subadditive)
bauerg@9374
    56
  also have "norm (- #1 \<cdot> y) = |- #1| * norm y" 
wenzelm@9035
    57
    by (rule seminorm_abs_homogenous)
bauerg@9374
    58
  also have "|- #1| = (#1::real)" by (rule abs_minus_one)
wenzelm@9035
    59
  finally show "norm (x - y) <= norm x + norm y" by simp
wenzelm@9035
    60
qed
wenzelm@7535
    61
wenzelm@7978
    62
lemma seminorm_minus: 
bauerg@9374
    63
  "[| is_seminorm V norm; x \<in> V; is_vectorspace V |] 
wenzelm@9035
    64
  ==> norm (- x) = norm x"
wenzelm@9035
    65
proof -
bauerg@9374
    66
  assume "is_seminorm V norm" "x \<in> V" "is_vectorspace V"
bauerg@9374
    67
  have "norm (- x) = norm (- #1 \<cdot> x)" by (simp! only: negate_eq1)
bauerg@9374
    68
  also have "... = |- #1| * norm x" 
wenzelm@9035
    69
    by (rule seminorm_abs_homogenous)
bauerg@9374
    70
  also have "|- #1| = (#1::real)" by (rule abs_minus_one)
wenzelm@9035
    71
  finally show "norm (- x) = norm x" by simp
wenzelm@9035
    72
qed
wenzelm@7535
    73
wenzelm@7535
    74
wenzelm@9035
    75
subsection {* Norms *}
wenzelm@7808
    76
wenzelm@7978
    77
text{* A \emph{norm} $\norm{\cdot}$ is a seminorm that maps only the
wenzelm@9035
    78
$\zero$ vector to $0$. *}
wenzelm@7535
    79
wenzelm@7535
    80
constdefs
bauerg@9374
    81
  is_norm :: "['a::{plus, minus, zero} set, 'a => real] => bool"
bauerg@9374
    82
  "is_norm V norm == \<forall>x \<in> V.  is_seminorm V norm 
bauerg@9374
    83
      \<and> (norm x = #0) = (x = 0)"
wenzelm@7535
    84
wenzelm@7566
    85
lemma is_normI [intro]: 
bauerg@9374
    86
  "\<forall>x \<in> V.  is_seminorm V norm  \<and> (norm x = #0) = (x = 0) 
wenzelm@9035
    87
  ==> is_norm V norm" by (simp only: is_norm_def)
wenzelm@7535
    88
wenzelm@9408
    89
lemma norm_is_seminorm [intro?]: 
bauerg@9374
    90
  "[| is_norm V norm; x \<in> V |] ==> is_seminorm V norm"
wenzelm@9035
    91
  by (unfold is_norm_def, force)
wenzelm@7535
    92
wenzelm@7808
    93
lemma norm_zero_iff: 
bauerg@9374
    94
  "[| is_norm V norm; x \<in> V |] ==> (norm x = #0) = (x = 0)"
wenzelm@9035
    95
  by (unfold is_norm_def, force)
wenzelm@7535
    96
wenzelm@9408
    97
lemma norm_ge_zero [intro?]:
bauerg@9374
    98
  "[|is_norm V norm; x \<in> V |] ==> #0 <= norm x"
wenzelm@9035
    99
  by (unfold is_norm_def is_seminorm_def, force)
wenzelm@7535
   100
wenzelm@7535
   101
wenzelm@9035
   102
subsection {* Normed vector spaces *}
wenzelm@7808
   103
wenzelm@7917
   104
text{* A vector space together with a norm is called
wenzelm@9035
   105
a \emph{normed space}. *}
wenzelm@7535
   106
wenzelm@7535
   107
constdefs
wenzelm@7917
   108
  is_normed_vectorspace :: 
bauerg@9374
   109
  "['a::{plus, minus, zero} set, 'a => real] => bool"
wenzelm@7535
   110
  "is_normed_vectorspace V norm ==
bauerg@9374
   111
      is_vectorspace V \<and> is_norm V norm"
wenzelm@7535
   112
wenzelm@7566
   113
lemma normed_vsI [intro]: 
wenzelm@7808
   114
  "[| is_vectorspace V; is_norm V norm |] 
wenzelm@9035
   115
  ==> is_normed_vectorspace V norm"
wenzelm@9035
   116
  by (unfold is_normed_vectorspace_def) blast 
wenzelm@7535
   117
wenzelm@9408
   118
lemma normed_vs_vs [intro?]: 
wenzelm@9035
   119
  "is_normed_vectorspace V norm ==> is_vectorspace V"
wenzelm@9035
   120
  by (unfold is_normed_vectorspace_def) force
wenzelm@7535
   121
wenzelm@9408
   122
lemma normed_vs_norm [intro?]: 
wenzelm@9035
   123
  "is_normed_vectorspace V norm ==> is_norm V norm"
wenzelm@9035
   124
  by (unfold is_normed_vectorspace_def, elim conjE)
wenzelm@7535
   125
wenzelm@9408
   126
lemma normed_vs_norm_ge_zero [intro?]: 
bauerg@9374
   127
  "[| is_normed_vectorspace V norm; x \<in> V |] ==> #0 <= norm x"
wenzelm@9035
   128
  by (unfold is_normed_vectorspace_def, rule, elim conjE)
wenzelm@7535
   129
wenzelm@9408
   130
lemma normed_vs_norm_gt_zero [intro?]: 
bauerg@9374
   131
  "[| is_normed_vectorspace V norm; x \<in> V; x \<noteq> 0 |] ==> #0 < norm x"
wenzelm@9035
   132
proof (unfold is_normed_vectorspace_def, elim conjE)
bauerg@9374
   133
  assume "x \<in> V" "x \<noteq> 0" "is_vectorspace V" "is_norm V norm"
wenzelm@9035
   134
  have "#0 <= norm x" ..
bauerg@9374
   135
  also have "#0 \<noteq> norm x"
wenzelm@9035
   136
  proof
wenzelm@9035
   137
    presume "norm x = #0"
bauerg@9374
   138
    also have "?this = (x = 0)" by (rule norm_zero_iff)
bauerg@9374
   139
    finally have "x = 0" .
wenzelm@9035
   140
    thus "False" by contradiction
wenzelm@9035
   141
  qed (rule sym)
wenzelm@9035
   142
  finally show "#0 < norm x" .
wenzelm@9035
   143
qed
wenzelm@7535
   144
wenzelm@9408
   145
lemma normed_vs_norm_abs_homogenous [intro?]: 
bauerg@9374
   146
  "[| is_normed_vectorspace V norm; x \<in> V |] 
bauerg@9374
   147
  ==> norm (a \<cdot> x) = |a| * norm x"
wenzelm@8838
   148
  by (rule seminorm_abs_homogenous, rule norm_is_seminorm, 
wenzelm@9035
   149
      rule normed_vs_norm)
wenzelm@7535
   150
wenzelm@9408
   151
lemma normed_vs_norm_subadditive [intro?]: 
bauerg@9374
   152
  "[| is_normed_vectorspace V norm; x \<in> V; y \<in> V |] 
wenzelm@9035
   153
  ==> norm (x + y) <= norm x + norm y"
wenzelm@7978
   154
  by (rule seminorm_subadditive, rule norm_is_seminorm, 
wenzelm@9035
   155
     rule normed_vs_norm)
wenzelm@7535
   156
wenzelm@7917
   157
text{* Any subspace of a normed vector space is again a 
wenzelm@9035
   158
normed vectorspace.*}
wenzelm@7917
   159
wenzelm@9408
   160
lemma subspace_normed_vs [intro?]: 
bauerg@9374
   161
  "[| is_vectorspace E; is_subspace F E;
wenzelm@9035
   162
  is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm"
wenzelm@9035
   163
proof (rule normed_vsI)
wenzelm@7808
   164
  assume "is_subspace F E" "is_vectorspace E" 
wenzelm@9035
   165
         "is_normed_vectorspace E norm"
wenzelm@9035
   166
  show "is_vectorspace F" ..
wenzelm@9035
   167
  show "is_norm F norm" 
wenzelm@9035
   168
  proof (intro is_normI ballI conjI)
wenzelm@9035
   169
    show "is_seminorm F norm" 
wenzelm@9035
   170
    proof
bauerg@9374
   171
      fix x y a presume "x \<in> E"
wenzelm@9035
   172
      show "#0 <= norm x" ..
bauerg@9374
   173
      show "norm (a \<cdot> x) = |a| * norm x" ..
bauerg@9374
   174
      presume "y \<in> E"
wenzelm@9035
   175
      show "norm (x + y) <= norm x + norm y" ..
wenzelm@9035
   176
    qed (simp!)+
wenzelm@7535
   177
bauerg@9374
   178
    fix x assume "x \<in> F"
bauerg@9374
   179
    show "(norm x = #0) = (x = 0)" 
wenzelm@9035
   180
    proof (rule norm_zero_iff)
wenzelm@9035
   181
      show "is_norm E norm" ..
wenzelm@9035
   182
    qed (simp!)
wenzelm@9035
   183
  qed
wenzelm@9035
   184
qed
wenzelm@7535
   185
wenzelm@9035
   186
end