author  wenzelm 
Wed, 24 Jun 2009 21:46:54 +0200  
changeset 31795  be3e1cc5005c 
parent 29252  src/HOL/HahnBanach/NormedSpace.thy@ea97aa6aeba2 
child 44887  7ca82df6e951 
permissions  rwrr 
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 HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

4 

9035  5 
header {* Normed vector spaces *} 
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 HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

10 

9035  11 
subsection {* Quasinorms *} 
7808  12 

10687  13 
text {* 
14 
A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space 

15 
into the reals that has the following properties: it is positive 

16 
definite, absolute homogenous and subadditive. 

17 
*} 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

18 

13515  19 
locale norm_syntax = 
20 
fixes norm :: "'a \<Rightarrow> real" ("\<parallel>_\<parallel>") 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

21 

29234  22 
locale seminorm = var_V + norm_syntax + 
25762  23 
constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set" 
13515  24 
assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>" 
25 
and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>" 

26 
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 HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

27 

14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13547
diff
changeset

28 
declare seminorm.intro [intro?] 
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13547
diff
changeset

29 

13547  30 
lemma (in seminorm) diff_subadditive: 
27611  31 
assumes "vectorspace V" 
13547  32 
shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x  y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" 
9035  33 
proof  
29234  34 
interpret vectorspace V by fact 
13515  35 
assume x: "x \<in> V" and y: "y \<in> V" 
27612  36 
then have "x  y = x +  1 \<cdot> y" 
13515  37 
by (simp add: diff_eq2 negate_eq2a) 
38 
also from x y have "\<parallel>\<dots>\<parallel> \<le> \<parallel>x\<parallel> + \<parallel> 1 \<cdot> y\<parallel>" 

39 
by (simp add: subadditive) 

40 
also from y have "\<parallel> 1 \<cdot> y\<parallel> = \<bar> 1\<bar> * \<parallel>y\<parallel>" 

41 
by (rule abs_homogenous) 

42 
also have "\<dots> = \<parallel>y\<parallel>" by simp 

43 
finally show ?thesis . 

9035  44 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

45 

13547  46 
lemma (in seminorm) minus: 
27611  47 
assumes "vectorspace V" 
13547  48 
shows "x \<in> V \<Longrightarrow> \<parallel> x\<parallel> = \<parallel>x\<parallel>" 
9035  49 
proof  
29234  50 
interpret vectorspace V by fact 
13515  51 
assume x: "x \<in> V" 
27612  52 
then have " x =  1 \<cdot> x" by (simp only: negate_eq1) 
13515  53 
also from x have "\<parallel>\<dots>\<parallel> = \<bar> 1\<bar> * \<parallel>x\<parallel>" 
54 
by (rule abs_homogenous) 

55 
also have "\<dots> = \<parallel>x\<parallel>" by simp 

56 
finally show ?thesis . 

9035  57 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

58 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

59 

9035  60 
subsection {* Norms *} 
7808  61 

10687  62 
text {* 
63 
A \emph{norm} @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the 

64 
@{text 0} vector to @{text 0}. 

65 
*} 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

66 

13515  67 
locale norm = seminorm + 
68 
assumes zero_iff [iff]: "x \<in> V \<Longrightarrow> (\<parallel>x\<parallel> = 0) = (x = 0)" 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

69 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

70 

9035  71 
subsection {* Normed vector spaces *} 
7808  72 

13515  73 
text {* 
74 
A vector space together with a norm is called a \emph{normed 

75 
space}. 

76 
*} 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

77 

13547  78 
locale normed_vectorspace = vectorspace + norm 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

79 

14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13547
diff
changeset

80 
declare normed_vectorspace.intro [intro?] 
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13547
diff
changeset

81 

13515  82 
lemma (in normed_vectorspace) gt_zero [intro?]: 
83 
"x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>" 

84 
proof  

85 
assume x: "x \<in> V" and neq: "x \<noteq> 0" 

86 
from x have "0 \<le> \<parallel>x\<parallel>" .. 

87 
also have [symmetric]: "\<dots> \<noteq> 0" 

9035  88 
proof 
13515  89 
assume "\<parallel>x\<parallel> = 0" 
90 
with x have "x = 0" by simp 

91 
with neq show False by contradiction 

92 
qed 

93 
finally show ?thesis . 

9035  94 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

95 

13515  96 
text {* 
97 
Any subspace of a normed vector space is again a normed vectorspace. 

98 
*} 

7917  99 

10687  100 
lemma subspace_normed_vs [intro?]: 
27611  101 
fixes F E norm 
102 
assumes "subspace F E" "normed_vectorspace E norm" 

13515  103 
shows "normed_vectorspace F norm" 
27611  104 
proof  
29234  105 
interpret subspace F E by fact 
106 
interpret normed_vectorspace E norm by fact 

27612  107 
show ?thesis 
108 
proof 

27611  109 
show "vectorspace F" by (rule vectorspace) unfold_locales 
110 
next 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset

111 
have "Normed_Space.norm E norm" .. 
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset

112 
with subset show "Normed_Space.norm F norm" 
27611  113 
by (simp add: norm_def seminorm_def norm_axioms_def) 
114 
qed 

9035  115 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

116 

10687  117 
end 