author | wenzelm |
Mon, 02 Nov 2015 11:10:28 +0100 | |
changeset 61539 | a29295dac1ca |
parent 61486 | 3590367b0ce9 |
child 61540 | f92bf6674699 |
permissions | -rw-r--r-- |
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset
|
1 |
(* Title: HOL/Hahn_Banach/Normed_Space.thy |
7566 | 2 |
Author: Gertrud Bauer, TU Munich |
3 |
*) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
4 |
|
58889 | 5 |
section \<open>Normed vector spaces\<close> |
7808 | 6 |
|
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset
|
7 |
theory Normed_Space |
27612 | 8 |
imports Subspace |
9 |
begin |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
10 |
|
58744 | 11 |
subsection \<open>Quasinorms\<close> |
7808 | 12 |
|
58744 | 13 |
text \<open> |
61539 | 14 |
A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space |
10687 | 15 |
into the reals that has the following properties: it is positive |
56749 | 16 |
definite, absolute homogeneous and subadditive. |
58744 | 17 |
\<close> |
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 = |
61076 | 20 |
fixes V :: "'a::{minus, plus, zero, uminus} set" |
13515 | 21 |
fixes norm :: "'a \<Rightarrow> real" ("\<parallel>_\<parallel>") |
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: |
27611 | 29 |
assumes "vectorspace V" |
13547 | 30 |
shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" |
9035 | 31 |
proof - |
29234 | 32 |
interpret vectorspace V by fact |
13515 | 33 |
assume x: "x \<in> V" and y: "y \<in> V" |
27612 | 34 |
then have "x - y = x + - 1 \<cdot> y" |
13515 | 35 |
by (simp add: diff_eq2 negate_eq2a) |
36 |
also from x y have "\<parallel>\<dots>\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>- 1 \<cdot> y\<parallel>" |
|
37 |
by (simp add: subadditive) |
|
38 |
also from y have "\<parallel>- 1 \<cdot> y\<parallel> = \<bar>- 1\<bar> * \<parallel>y\<parallel>" |
|
39 |
by (rule abs_homogenous) |
|
40 |
also have "\<dots> = \<parallel>y\<parallel>" by simp |
|
41 |
finally show ?thesis . |
|
9035 | 42 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
43 |
|
13547 | 44 |
lemma (in seminorm) minus: |
27611 | 45 |
assumes "vectorspace V" |
13547 | 46 |
shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>" |
9035 | 47 |
proof - |
29234 | 48 |
interpret vectorspace V by fact |
13515 | 49 |
assume x: "x \<in> V" |
27612 | 50 |
then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1) |
44887 | 51 |
also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>" by (rule abs_homogenous) |
13515 | 52 |
also have "\<dots> = \<parallel>x\<parallel>" by simp |
53 |
finally show ?thesis . |
|
9035 | 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 |
|
58744 | 57 |
subsection \<open>Norms\<close> |
7808 | 58 |
|
58744 | 59 |
text \<open> |
61539 | 60 |
A \<^emph>\<open>norm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a seminorm that maps only the |
61 |
\<open>0\<close> vector to \<open>0\<close>. |
|
58744 | 62 |
\<close> |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
63 |
|
13515 | 64 |
locale norm = seminorm + |
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 |
|
58744 | 68 |
subsection \<open>Normed vector spaces\<close> |
7808 | 69 |
|
58744 | 70 |
text \<open> |
61486 | 71 |
A vector space together with a norm is called a \<^emph>\<open>normed |
72 |
space\<close>. |
|
58744 | 73 |
\<close> |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
74 |
|
13547 | 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 | 79 |
lemma (in normed_vectorspace) gt_zero [intro?]: |
44887 | 80 |
assumes x: "x \<in> V" and neq: "x \<noteq> 0" |
81 |
shows "0 < \<parallel>x\<parallel>" |
|
13515 | 82 |
proof - |
83 |
from x have "0 \<le> \<parallel>x\<parallel>" .. |
|
44887 | 84 |
also have "0 \<noteq> \<parallel>x\<parallel>" |
9035 | 85 |
proof |
44887 | 86 |
assume "0 = \<parallel>x\<parallel>" |
13515 | 87 |
with x have "x = 0" by simp |
88 |
with neq show False by contradiction |
|
89 |
qed |
|
90 |
finally show ?thesis . |
|
9035 | 91 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
92 |
|
58744 | 93 |
text \<open> |
13515 | 94 |
Any subspace of a normed vector space is again a normed vectorspace. |
58744 | 95 |
\<close> |
7917 | 96 |
|
10687 | 97 |
lemma subspace_normed_vs [intro?]: |
27611 | 98 |
fixes F E norm |
99 |
assumes "subspace F E" "normed_vectorspace E norm" |
|
13515 | 100 |
shows "normed_vectorspace F norm" |
27611 | 101 |
proof - |
29234 | 102 |
interpret subspace F E by fact |
103 |
interpret normed_vectorspace E norm by fact |
|
27612 | 104 |
show ?thesis |
105 |
proof |
|
27611 | 106 |
show "vectorspace F" by (rule vectorspace) unfold_locales |
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 | 110 |
by (simp add: norm_def seminorm_def norm_axioms_def) |
111 |
qed |
|
9035 | 112 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
113 |
|
10687 | 114 |
end |