1(*  Title:      HOL/Hahn_Banach/Normed_Space.thy
2    Author:     Gertrud Bauer, TU Munich
3*)
4
5section \<open>Normed vector spaces\<close>
6
7theory Normed_Space
8imports Subspace
9begin
10
11subsection \<open>Quasinorms\<close>
12
13text \<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
16  and subadditive.
17\<close>
18
19locale 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>"
25
26declare seminorm.intro [intro?]
27
28lemma (in seminorm) diff_subadditive:
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>"
31proof -
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>"
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 .
42qed
43
44lemma (in seminorm) minus:
45  assumes "vectorspace V"
46  shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
47proof -
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 .
54qed
55
56
57subsection \<open>Norms\<close>
58
59text \<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>
62
63locale norm = seminorm +
64  assumes zero_iff [iff]: "x \<in> V \<Longrightarrow> (\<parallel>x\<parallel> = 0) = (x = 0)"
65
66
67subsection \<open>Normed vector spaces\<close>
68
69text \<open>
70  A vector space together with a norm is called a \<^emph>\<open>normed space\<close>.
71\<close>
72
73locale normed_vectorspace = vectorspace + norm
74
75declare normed_vectorspace.intro [intro?]
76
77lemma (in normed_vectorspace) gt_zero [intro?]:
78  assumes x: "x \<in> V" and neq: "x \<noteq> 0"
79  shows "0 < \<parallel>x\<parallel>"
80proof -
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 .
89qed
90
91text \<open>
92  Any subspace of a normed vector space is again a normed vectorspace.
93\<close>
94
95lemma subspace_normed_vs [intro?]:
96  fixes F E norm
97  assumes "subspace F E" "normed_vectorspace E norm"
98  shows "normed_vectorspace F norm"
99proof -
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
110qed
111
112end
113