author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46867  0883804b67bb 
child 56749  e96d6b38649e 
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 

46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

19 
locale seminorm = 
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

20 
fixes V :: "'a\<Colon>{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 HahnBanach 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 HahnBanach 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 HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

55 

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

56 

9035  57 
subsection {* Norms *} 
7808  58 

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

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

62 
*} 

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

66 

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

67 

9035  68 
subsection {* Normed vector spaces *} 
7808  69 

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

72 
space}. 

73 
*} 

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

74 

13547  75 
locale normed_vectorspace = vectorspace + norm 
7535
599d3414b51d
The HahnBanach 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 HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

92 

13515  93 
text {* 
94 
Any subspace of a normed vector space is again a normed vectorspace. 

95 
*} 

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

113 

10687  114 
end 