src/HOL/Hahn_Banach/Normed_Space.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46867 0883804b67bb
child 56749 e96d6b38649e
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: 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
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
    19
locale seminorm =
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
    20
  fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    21
  fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    22
  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
    23
    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
    24
    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
    25
14254
342634f38451 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents: 13547
diff changeset
    26
declare seminorm.intro [intro?]
342634f38451 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents: 13547
diff changeset
    27
13547
wenzelm
parents: 13515
diff changeset
    28
lemma (in seminorm) diff_subadditive:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
    29
  assumes "vectorspace V"
13547
wenzelm
parents: 13515
diff changeset
    30
  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
    31
proof -
29234
60f7fb56f8cd More porting to new locales.
ballarin
parents: 28823
diff changeset
    32
  interpret vectorspace V by fact
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    33
  assume x: "x \<in> V" and y: "y \<in> V"
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
    34
  then have "x - y = x + - 1 \<cdot> y"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    35
    by (simp add: diff_eq2 negate_eq2a)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    36
  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
    37
    by (simp add: subadditive)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    38
  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
    39
    by (rule abs_homogenous)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    40
  also have "\<dots> = \<parallel>y\<parallel>" by simp
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    41
  finally show ?thesis .
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    42
qed
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    43
13547
wenzelm
parents: 13515
diff changeset
    44
lemma (in seminorm) minus:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
    45
  assumes "vectorspace V"
13547
wenzelm
parents: 13515
diff changeset
    46
  shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    47
proof -
29234
60f7fb56f8cd More porting to new locales.
ballarin
parents: 28823
diff changeset
    48
  interpret vectorspace V by fact
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    49
  assume x: "x \<in> V"
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
    50
  then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 31795
diff changeset
    51
  also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>" by (rule abs_homogenous)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    52
  also have "\<dots> = \<parallel>x\<parallel>" by simp
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    53
  finally show ?thesis .
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    54
qed
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    55
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    56
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    57
subsection {* Norms *}
7808
fd019ac3485f update from Gertrud;
wenzelm
parents: 7566
diff changeset
    58
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    59
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    60
  A \emph{norm} @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    61
  @{text 0} vector to @{text 0}.
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    62
*}
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    63
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    64
locale norm = seminorm +
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    65
  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
    66
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    67
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    68
subsection {* Normed vector spaces *}
7808
fd019ac3485f update from Gertrud;
wenzelm
parents: 7566
diff changeset
    69
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    70
text {*
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    71
  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
    72
  space}.
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    73
*}
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    74
13547
wenzelm
parents: 13515
diff changeset
    75
locale normed_vectorspace = vectorspace + norm
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    76
14254
342634f38451 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents: 13547
diff changeset
    77
declare normed_vectorspace.intro [intro?]
342634f38451 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents: 13547
diff changeset
    78
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    79
lemma (in normed_vectorspace) gt_zero [intro?]:
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 31795
diff changeset
    80
  assumes x: "x \<in> V" and neq: "x \<noteq> 0"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 31795
diff changeset
    81
  shows "0 < \<parallel>x\<parallel>"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    82
proof -
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    83
  from x have "0 \<le> \<parallel>x\<parallel>" ..
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 31795
diff changeset
    84
  also have "0 \<noteq> \<parallel>x\<parallel>"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    85
  proof
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 31795
diff changeset
    86
    assume "0 = \<parallel>x\<parallel>"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    87
    with x have "x = 0" by simp
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    88
    with neq show False by contradiction
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    89
  qed
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    90
  finally show ?thesis .
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    91
qed
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    92
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    93
text {*
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    94
  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
    95
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    96
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    97
lemma subspace_normed_vs [intro?]:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
    98
  fixes F E norm
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
    99
  assumes "subspace F E" "normed_vectorspace E norm"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
   100
  shows "normed_vectorspace F norm"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
   101
proof -
29234
60f7fb56f8cd More porting to new locales.
ballarin
parents: 28823
diff changeset
   102
  interpret subspace F E by fact
60f7fb56f8cd More porting to new locales.
ballarin
parents: 28823
diff changeset
   103
  interpret normed_vectorspace E norm by fact
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   104
  show ?thesis
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   105
  proof
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
   106
    show "vectorspace F" by (rule vectorspace) unfold_locales
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
   107
  next
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29252
diff changeset
   108
    have "Normed_Space.norm E norm" ..
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29252
diff changeset
   109
    with subset show "Normed_Space.norm F norm"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
   110
      by (simp add: norm_def seminorm_def norm_axioms_def)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
   111
  qed
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   112
qed
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   113
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
   114
end