author | ballarin |
Thu, 06 Nov 2003 14:18:05 +0100 | |
changeset 14254 | 342634f38451 |
parent 13547 | bf399f3bd7dc |
child 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
7566 | 1 |
(* Title: HOL/Real/HahnBanach/NormedSpace.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gertrud Bauer, TU Munich |
|
4 |
*) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
5 |
|
9035 | 6 |
header {* Normed vector spaces *} |
7808 | 7 |
|
9035 | 8 |
theory NormedSpace = Subspace: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
9 |
|
9035 | 10 |
subsection {* Quasinorms *} |
7808 | 11 |
|
10687 | 12 |
text {* |
13 |
A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space |
|
14 |
into the reals that has the following properties: it is positive |
|
15 |
definite, absolute homogenous and subadditive. |
|
16 |
*} |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
17 |
|
13515 | 18 |
locale norm_syntax = |
19 |
fixes norm :: "'a \<Rightarrow> real" ("\<parallel>_\<parallel>") |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
20 |
|
13515 | 21 |
locale seminorm = var V + norm_syntax + |
22 |
assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>" |
|
23 |
and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>" |
|
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 | 28 |
lemma (in seminorm) diff_subadditive: |
29 |
includes vectorspace |
|
30 |
shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" |
|
9035 | 31 |
proof - |
13515 | 32 |
assume x: "x \<in> V" and y: "y \<in> V" |
33 |
hence "x - y = x + - 1 \<cdot> y" |
|
34 |
by (simp add: diff_eq2 negate_eq2a) |
|
35 |
also from x y have "\<parallel>\<dots>\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>- 1 \<cdot> y\<parallel>" |
|
36 |
by (simp add: subadditive) |
|
37 |
also from y have "\<parallel>- 1 \<cdot> y\<parallel> = \<bar>- 1\<bar> * \<parallel>y\<parallel>" |
|
38 |
by (rule abs_homogenous) |
|
39 |
also have "\<dots> = \<parallel>y\<parallel>" by simp |
|
40 |
finally show ?thesis . |
|
9035 | 41 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
42 |
|
13547 | 43 |
lemma (in seminorm) minus: |
44 |
includes vectorspace |
|
45 |
shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>" |
|
9035 | 46 |
proof - |
13515 | 47 |
assume x: "x \<in> V" |
48 |
hence "- x = - 1 \<cdot> x" by (simp only: negate_eq1) |
|
49 |
also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>" |
|
50 |
by (rule abs_homogenous) |
|
51 |
also have "\<dots> = \<parallel>x\<parallel>" by simp |
|
52 |
finally show ?thesis . |
|
9035 | 53 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
54 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
55 |
|
9035 | 56 |
subsection {* Norms *} |
7808 | 57 |
|
10687 | 58 |
text {* |
59 |
A \emph{norm} @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the |
|
60 |
@{text 0} vector to @{text 0}. |
|
61 |
*} |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
62 |
|
13515 | 63 |
locale norm = seminorm + |
64 |
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
|
65 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
66 |
|
9035 | 67 |
subsection {* Normed vector spaces *} |
7808 | 68 |
|
13515 | 69 |
text {* |
70 |
A vector space together with a norm is called a \emph{normed |
|
71 |
space}. |
|
72 |
*} |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
73 |
|
13547 | 74 |
locale normed_vectorspace = vectorspace + norm |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
75 |
|
14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13547
diff
changeset
|
76 |
declare normed_vectorspace.intro [intro?] |
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13547
diff
changeset
|
77 |
|
13515 | 78 |
lemma (in normed_vectorspace) gt_zero [intro?]: |
79 |
"x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>" |
|
80 |
proof - |
|
81 |
assume x: "x \<in> V" and neq: "x \<noteq> 0" |
|
82 |
from x have "0 \<le> \<parallel>x\<parallel>" .. |
|
83 |
also have [symmetric]: "\<dots> \<noteq> 0" |
|
9035 | 84 |
proof |
13515 | 85 |
assume "\<parallel>x\<parallel> = 0" |
86 |
with x have "x = 0" by simp |
|
87 |
with neq show False by contradiction |
|
88 |
qed |
|
89 |
finally show ?thesis . |
|
9035 | 90 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
91 |
|
13515 | 92 |
text {* |
93 |
Any subspace of a normed vector space is again a normed vectorspace. |
|
94 |
*} |
|
7917 | 95 |
|
10687 | 96 |
lemma subspace_normed_vs [intro?]: |
13547 | 97 |
includes subspace F E + normed_vectorspace E |
13515 | 98 |
shows "normed_vectorspace F norm" |
99 |
proof |
|
100 |
show "vectorspace F" by (rule vectorspace) |
|
101 |
have "seminorm E norm" . with subset show "seminorm F norm" |
|
102 |
by (simp add: seminorm_def) |
|
103 |
have "norm_axioms E norm" . with subset show "norm_axioms F norm" |
|
104 |
by (simp add: norm_axioms_def) |
|
9035 | 105 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
106 |
|
10687 | 107 |
end |