src/HOL/Hahn_Banach/Normed_Space.thy
author wenzelm
Wed, 24 Jun 2009 21:46:54 +0200
changeset 31795 be3e1cc5005c
parent 29252 src/HOL/HahnBanach/NormedSpace.thy@ea97aa6aeba2
child 44887 7ca82df6e951
permissions -rw-r--r--
standard naming conventions for session and theories;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29252
diff changeset
     1
(*  Title:      HOL/Hahn_Banach/Normed_Space.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 {* Normed vector spaces *}
7808
fd019ac3485f update from Gertrud;
wenzelm
parents: 7566
diff changeset
     6
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29252
diff changeset
     7
theory Normed_Space
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
     8
imports Subspace
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 {* Quasinorms *}
7808
fd019ac3485f update from Gertrud;
wenzelm
parents: 7566
diff changeset
    12
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    13
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    14
  A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    15
  into the reals that has the following properties: it is positive
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    16
  definite, absolute homogenous and subadditive.
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    17
*}
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    18
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    19
locale norm_syntax =
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    20
  fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    21
29234
60f7fb56f8cd More porting to new locales.
ballarin
parents: 28823
diff changeset
    22
locale seminorm = var_V + norm_syntax +
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 20538
diff changeset
    23
  constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    24
  assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    25
    and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    26
    and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<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: 13547
diff changeset
    28
declare seminorm.intro [intro?]
342634f38451 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents: 13547
diff changeset
    29
13547
wenzelm
parents: 13515
diff changeset
    30
lemma (in seminorm) diff_subadditive:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
    31
  assumes "vectorspace V"
13547
wenzelm
parents: 13515
diff changeset
    32
  shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    33
proof -
29234
60f7fb56f8cd More porting to new locales.
ballarin
parents: 28823
diff changeset
    34
  interpret vectorspace V by fact
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    35
  assume x: "x \<in> V" and y: "y \<in> V"
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
    36
  then have "x - y = x + - 1 \<cdot> y"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    37
    by (simp add: diff_eq2 negate_eq2a)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    38
  also from x y have "\<parallel>\<dots>\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>- 1 \<cdot> y\<parallel>"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    39
    by (simp add: subadditive)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    40
  also from y have "\<parallel>- 1 \<cdot> y\<parallel> = \<bar>- 1\<bar> * \<parallel>y\<parallel>"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    41
    by (rule abs_homogenous)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    42
  also have "\<dots> = \<parallel>y\<parallel>" by simp
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    43
  finally show ?thesis .
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    44
qed
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    45
13547
wenzelm
parents: 13515
diff changeset
    46
lemma (in seminorm) minus:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
    47
  assumes "vectorspace V"
13547
wenzelm
parents: 13515
diff changeset
    48
  shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    49
proof -
29234
60f7fb56f8cd More porting to new locales.
ballarin
parents: 28823
diff changeset
    50
  interpret vectorspace V by fact
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    51
  assume x: "x \<in> V"
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
    52
  then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    53
  also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    54
    by (rule abs_homogenous)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    55
  also have "\<dots> = \<parallel>x\<parallel>" by simp
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    56
  finally show ?thesis .
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    57
qed
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    58
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    59
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    60
subsection {* Norms *}
7808
fd019ac3485f update from Gertrud;
wenzelm
parents: 7566
diff changeset
    61
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    62
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    63
  A \emph{norm} @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    64
  @{text 0} vector to @{text 0}.
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    65
*}
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    66
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    67
locale norm = seminorm +
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    68
  assumes zero_iff [iff]: "x \<in> V \<Longrightarrow> (\<parallel>x\<parallel> = 0) = (x = 0)"
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    69
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    70
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    71
subsection {* Normed vector spaces *}
7808
fd019ac3485f update from Gertrud;
wenzelm
parents: 7566
diff changeset
    72
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    73
text {*
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    74
  A vector space together with a norm is called a \emph{normed
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    75
  space}.
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    76
*}
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    77
13547
wenzelm
parents: 13515
diff changeset
    78
locale normed_vectorspace = vectorspace + norm
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    79
14254
342634f38451 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents: 13547
diff changeset
    80
declare normed_vectorspace.intro [intro?]
342634f38451 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents: 13547
diff changeset
    81
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    82
lemma (in normed_vectorspace) gt_zero [intro?]:
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    83
  "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    84
proof -
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    85
  assume x: "x \<in> V" and neq: "x \<noteq> 0"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    86
  from x have "0 \<le> \<parallel>x\<parallel>" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    87
  also have [symmetric]: "\<dots> \<noteq> 0"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    88
  proof
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    89
    assume "\<parallel>x\<parallel> = 0"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    90
    with x have "x = 0" by simp
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    91
    with neq show False by contradiction
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    92
  qed
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    93
  finally show ?thesis .
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    94
qed
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    95
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    96
text {*
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    97
  Any subspace of a normed vector space is again a normed vectorspace.
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    98
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    99
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
   100
lemma subspace_normed_vs [intro?]:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
   101
  fixes F E norm
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
   102
  assumes "subspace F E" "normed_vectorspace E norm"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   103
  shows "normed_vectorspace F norm"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
   104
proof -
29234
60f7fb56f8cd More porting to new locales.
ballarin
parents: 28823
diff changeset
   105
  interpret subspace F E by fact
60f7fb56f8cd More porting to new locales.
ballarin
parents: 28823
diff changeset
   106
  interpret normed_vectorspace E norm by fact
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   107
  show ?thesis
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   108
  proof
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
   109
    show "vectorspace F" by (rule vectorspace) unfold_locales
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
   110
  next
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29252
diff changeset
   111
    have "Normed_Space.norm E norm" ..
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29252
diff changeset
   112
    with subset show "Normed_Space.norm F norm"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
   113
      by (simp add: norm_def seminorm_def norm_axioms_def)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
   114
  qed
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   115
qed
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   116
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
   117
end