author | haftmann |
Mon, 17 Nov 2008 17:00:55 +0100 | |
changeset 28823 | dcbef866c9e2 |
parent 27612 | d3eb431db035 |
child 29234 | 60f7fb56f8cd |
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 |
|
27612 | 8 |
theory NormedSpace |
9 |
imports Subspace |
|
10 |
begin |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
11 |
|
9035 | 12 |
subsection {* Quasinorms *} |
7808 | 13 |
|
10687 | 14 |
text {* |
15 |
A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space |
|
16 |
into the reals that has the following properties: it is positive |
|
17 |
definite, absolute homogenous and subadditive. |
|
18 |
*} |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
19 |
|
13515 | 20 |
locale norm_syntax = |
21 |
fixes norm :: "'a \<Rightarrow> real" ("\<parallel>_\<parallel>") |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
22 |
|
13515 | 23 |
locale seminorm = var V + norm_syntax + |
25762 | 24 |
constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set" |
13515 | 25 |
assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>" |
26 |
and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>" |
|
27 |
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
|
28 |
|
14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13547
diff
changeset
|
29 |
declare seminorm.intro [intro?] |
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13547
diff
changeset
|
30 |
|
13547 | 31 |
lemma (in seminorm) diff_subadditive: |
27611 | 32 |
assumes "vectorspace V" |
13547 | 33 |
shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" |
9035 | 34 |
proof - |
27611 | 35 |
interpret vectorspace [V] by fact |
13515 | 36 |
assume x: "x \<in> V" and y: "y \<in> V" |
27612 | 37 |
then have "x - y = x + - 1 \<cdot> y" |
13515 | 38 |
by (simp add: diff_eq2 negate_eq2a) |
39 |
also from x y have "\<parallel>\<dots>\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>- 1 \<cdot> y\<parallel>" |
|
40 |
by (simp add: subadditive) |
|
41 |
also from y have "\<parallel>- 1 \<cdot> y\<parallel> = \<bar>- 1\<bar> * \<parallel>y\<parallel>" |
|
42 |
by (rule abs_homogenous) |
|
43 |
also have "\<dots> = \<parallel>y\<parallel>" by simp |
|
44 |
finally show ?thesis . |
|
9035 | 45 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
46 |
|
13547 | 47 |
lemma (in seminorm) minus: |
27611 | 48 |
assumes "vectorspace V" |
13547 | 49 |
shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>" |
9035 | 50 |
proof - |
27611 | 51 |
interpret vectorspace [V] by fact |
13515 | 52 |
assume x: "x \<in> V" |
27612 | 53 |
then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1) |
13515 | 54 |
also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>" |
55 |
by (rule abs_homogenous) |
|
56 |
also have "\<dots> = \<parallel>x\<parallel>" by simp |
|
57 |
finally show ?thesis . |
|
9035 | 58 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
59 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
60 |
|
9035 | 61 |
subsection {* Norms *} |
7808 | 62 |
|
10687 | 63 |
text {* |
64 |
A \emph{norm} @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the |
|
65 |
@{text 0} vector to @{text 0}. |
|
66 |
*} |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
67 |
|
13515 | 68 |
locale norm = seminorm + |
69 |
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
|
70 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
71 |
|
9035 | 72 |
subsection {* Normed vector spaces *} |
7808 | 73 |
|
13515 | 74 |
text {* |
75 |
A vector space together with a norm is called a \emph{normed |
|
76 |
space}. |
|
77 |
*} |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
78 |
|
13547 | 79 |
locale normed_vectorspace = vectorspace + norm |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
80 |
|
14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13547
diff
changeset
|
81 |
declare normed_vectorspace.intro [intro?] |
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13547
diff
changeset
|
82 |
|
13515 | 83 |
lemma (in normed_vectorspace) gt_zero [intro?]: |
84 |
"x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>" |
|
85 |
proof - |
|
86 |
assume x: "x \<in> V" and neq: "x \<noteq> 0" |
|
87 |
from x have "0 \<le> \<parallel>x\<parallel>" .. |
|
88 |
also have [symmetric]: "\<dots> \<noteq> 0" |
|
9035 | 89 |
proof |
13515 | 90 |
assume "\<parallel>x\<parallel> = 0" |
91 |
with x have "x = 0" by simp |
|
92 |
with neq show False by contradiction |
|
93 |
qed |
|
94 |
finally show ?thesis . |
|
9035 | 95 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
96 |
|
13515 | 97 |
text {* |
98 |
Any subspace of a normed vector space is again a normed vectorspace. |
|
99 |
*} |
|
7917 | 100 |
|
10687 | 101 |
lemma subspace_normed_vs [intro?]: |
27611 | 102 |
fixes F E norm |
103 |
assumes "subspace F E" "normed_vectorspace E norm" |
|
13515 | 104 |
shows "normed_vectorspace F norm" |
27611 | 105 |
proof - |
106 |
interpret subspace [F E] by fact |
|
107 |
interpret normed_vectorspace [E norm] by fact |
|
27612 | 108 |
show ?thesis |
109 |
proof |
|
27611 | 110 |
show "vectorspace F" by (rule vectorspace) unfold_locales |
111 |
next |
|
28823 | 112 |
have "NormedSpace.norm E norm" .. |
27611 | 113 |
with subset show "NormedSpace.norm F norm" |
114 |
by (simp add: norm_def seminorm_def norm_axioms_def) |
|
115 |
qed |
|
9035 | 116 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
117 |
|
10687 | 118 |
end |