summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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';

tuned comments;

tuned comments;

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

16 and subadditive.

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?]

28 lemma (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>"

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>"

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 .

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