1 (* Title: HOL/Real/HahnBanach/NormedSpace.thy |
|
2 ID: $Id$ |
|
3 Author: Gertrud Bauer, TU Munich |
|
4 *) |
|
5 |
|
6 header {* Normed vector spaces *} |
|
7 |
|
8 theory NormedSpace |
|
9 imports Subspace |
|
10 begin |
|
11 |
|
12 subsection {* Quasinorms *} |
|
13 |
|
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 *} |
|
19 |
|
20 locale norm_syntax = |
|
21 fixes norm :: "'a \<Rightarrow> real" ("\<parallel>_\<parallel>") |
|
22 |
|
23 locale seminorm = var V + norm_syntax + |
|
24 constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set" |
|
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>" |
|
28 |
|
29 declare seminorm.intro [intro?] |
|
30 |
|
31 lemma (in seminorm) diff_subadditive: |
|
32 assumes "vectorspace V" |
|
33 shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" |
|
34 proof - |
|
35 interpret vectorspace [V] by fact |
|
36 assume x: "x \<in> V" and y: "y \<in> V" |
|
37 then have "x - y = x + - 1 \<cdot> y" |
|
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 . |
|
45 qed |
|
46 |
|
47 lemma (in seminorm) minus: |
|
48 assumes "vectorspace V" |
|
49 shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>" |
|
50 proof - |
|
51 interpret vectorspace [V] by fact |
|
52 assume x: "x \<in> V" |
|
53 then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1) |
|
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 . |
|
58 qed |
|
59 |
|
60 |
|
61 subsection {* Norms *} |
|
62 |
|
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 *} |
|
67 |
|
68 locale norm = seminorm + |
|
69 assumes zero_iff [iff]: "x \<in> V \<Longrightarrow> (\<parallel>x\<parallel> = 0) = (x = 0)" |
|
70 |
|
71 |
|
72 subsection {* Normed vector spaces *} |
|
73 |
|
74 text {* |
|
75 A vector space together with a norm is called a \emph{normed |
|
76 space}. |
|
77 *} |
|
78 |
|
79 locale normed_vectorspace = vectorspace + norm |
|
80 |
|
81 declare normed_vectorspace.intro [intro?] |
|
82 |
|
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" |
|
89 proof |
|
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 . |
|
95 qed |
|
96 |
|
97 text {* |
|
98 Any subspace of a normed vector space is again a normed vectorspace. |
|
99 *} |
|
100 |
|
101 lemma subspace_normed_vs [intro?]: |
|
102 fixes F E norm |
|
103 assumes "subspace F E" "normed_vectorspace E norm" |
|
104 shows "normed_vectorspace F norm" |
|
105 proof - |
|
106 interpret subspace [F E] by fact |
|
107 interpret normed_vectorspace [E norm] by fact |
|
108 show ?thesis |
|
109 proof |
|
110 show "vectorspace F" by (rule vectorspace) unfold_locales |
|
111 next |
|
112 have "NormedSpace.norm E norm" .. |
|
113 with subset show "NormedSpace.norm F norm" |
|
114 by (simp add: norm_def seminorm_def norm_axioms_def) |
|
115 qed |
|
116 qed |
|
117 |
|
118 end |
|