src/HOL/Hahn_Banach/Normed_Space.thy
 author wenzelm Mon Apr 25 16:09:26 2016 +0200 (2016-04-25) changeset 63040 eb4ddd18d635 parent 61879 e4f9d8f094fe permissions -rw-r--r--
eliminated old 'def';
1 (*  Title:      HOL/Hahn_Banach/Normed_Space.thy
2     Author:     Gertrud Bauer, TU Munich
3 *)
5 section \<open>Normed vector spaces\<close>
7 theory Normed_Space
8 imports Subspace
9 begin
11 subsection \<open>Quasinorms\<close>
13 text \<open>
14   A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals that
15   has the following properties: it is positive definite, absolute homogeneous
17 \<close>
19 locale seminorm =
20   fixes V :: "'a::{minus, plus, zero, uminus} set"
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>"
26 declare seminorm.intro [intro?]
29   assumes "vectorspace V"
30   shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
31 proof -
32   interpret vectorspace V by fact
33   assume x: "x \<in> V" and y: "y \<in> V"
34   then have "x - y = x + - 1 \<cdot> y"
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>"
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 .
42 qed
44 lemma (in seminorm) minus:
45   assumes "vectorspace V"
46   shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
47 proof -
48   interpret vectorspace V by fact
49   assume x: "x \<in> V"
50   then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
51   also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>" by (rule abs_homogenous)
52   also have "\<dots> = \<parallel>x\<parallel>" by simp
53   finally show ?thesis .
54 qed
57 subsection \<open>Norms\<close>
59 text \<open>
60   A \<^emph>\<open>norm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a seminorm that maps only the \<open>0\<close> vector to \<open>0\<close>.
61 \<close>
63 locale norm = seminorm +
64   assumes zero_iff [iff]: "x \<in> V \<Longrightarrow> (\<parallel>x\<parallel> = 0) = (x = 0)"
67 subsection \<open>Normed vector spaces\<close>
69 text \<open>
70   A vector space together with a norm is called a \<^emph>\<open>normed space\<close>.
71 \<close>
73 locale normed_vectorspace = vectorspace + norm
75 declare normed_vectorspace.intro [intro?]
77 lemma (in normed_vectorspace) gt_zero [intro?]:
78   assumes x: "x \<in> V" and neq: "x \<noteq> 0"
79   shows "0 < \<parallel>x\<parallel>"
80 proof -
81   from x have "0 \<le> \<parallel>x\<parallel>" ..
82   also have "0 \<noteq> \<parallel>x\<parallel>"
83   proof
84     assume "0 = \<parallel>x\<parallel>"
85     with x have "x = 0" by simp
86     with neq show False by contradiction
87   qed
88   finally show ?thesis .
89 qed
91 text \<open>
92   Any subspace of a normed vector space is again a normed vectorspace.
93 \<close>
95 lemma subspace_normed_vs [intro?]:
96   fixes F E norm
97   assumes "subspace F E" "normed_vectorspace E norm"
98   shows "normed_vectorspace F norm"
99 proof -
100   interpret subspace F E by fact
101   interpret normed_vectorspace E norm by fact
102   show ?thesis
103   proof
104     show "vectorspace F" by (rule vectorspace) unfold_locales
105   next
106     have "Normed_Space.norm E norm" ..
107     with subset show "Normed_Space.norm F norm"
108       by (simp add: norm_def seminorm_def norm_axioms_def)
109   qed
110 qed
112 end