src/HOL/Hahn_Banach/Normed_Space.thy
changeset 31795 be3e1cc5005c
parent 29252 ea97aa6aeba2
child 44887 7ca82df6e951
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,117 @@
+(*  Title:      HOL/Hahn_Banach/Normed_Space.thy
+    Author:     Gertrud Bauer, TU Munich
+*)
+
+header {* Normed vector spaces *}
+
+theory Normed_Space
+imports Subspace
+begin
+
+subsection {* Quasinorms *}
+
+text {*
+  A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
+  into the reals that has the following properties: it is positive
+  definite, absolute homogenous and subadditive.
+*}
+
+locale norm_syntax =
+  fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
+
+locale seminorm = var_V + norm_syntax +
+  constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
+  assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
+    and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
+    and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
+
+declare seminorm.intro [intro?]
+
+lemma (in seminorm) diff_subadditive:
+  assumes "vectorspace V"
+  shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
+proof -
+  interpret vectorspace V by fact
+  assume x: "x \<in> V" and y: "y \<in> V"
+  then have "x - y = x + - 1 \<cdot> y"
+    by (simp add: diff_eq2 negate_eq2a)
+  also from x y have "\<parallel>\<dots>\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>- 1 \<cdot> y\<parallel>"
+    by (simp add: subadditive)
+  also from y have "\<parallel>- 1 \<cdot> y\<parallel> = \<bar>- 1\<bar> * \<parallel>y\<parallel>"
+    by (rule abs_homogenous)
+  also have "\<dots> = \<parallel>y\<parallel>" by simp
+  finally show ?thesis .
+qed
+
+lemma (in seminorm) minus:
+  assumes "vectorspace V"
+  shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
+proof -
+  interpret vectorspace V by fact
+  assume x: "x \<in> V"
+  then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
+  also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
+    by (rule abs_homogenous)
+  also have "\<dots> = \<parallel>x\<parallel>" by simp
+  finally show ?thesis .
+qed
+
+
+subsection {* Norms *}
+
+text {*
+  A \emph{norm} @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
+  @{text 0} vector to @{text 0}.
+*}
+
+locale norm = seminorm +
+  assumes zero_iff [iff]: "x \<in> V \<Longrightarrow> (\<parallel>x\<parallel> = 0) = (x = 0)"
+
+
+subsection {* Normed vector spaces *}
+
+text {*
+  A vector space together with a norm is called a \emph{normed
+  space}.
+*}
+
+locale normed_vectorspace = vectorspace + norm
+
+declare normed_vectorspace.intro [intro?]
+
+lemma (in normed_vectorspace) gt_zero [intro?]:
+  "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>"
+proof -
+  assume x: "x \<in> V" and neq: "x \<noteq> 0"
+  from x have "0 \<le> \<parallel>x\<parallel>" ..
+  also have [symmetric]: "\<dots> \<noteq> 0"
+  proof
+    assume "\<parallel>x\<parallel> = 0"
+    with x have "x = 0" by simp
+    with neq show False by contradiction
+  qed
+  finally show ?thesis .
+qed
+
+text {*
+  Any subspace of a normed vector space is again a normed vectorspace.
+*}
+
+lemma subspace_normed_vs [intro?]:
+  fixes F E norm
+  assumes "subspace F E" "normed_vectorspace E norm"
+  shows "normed_vectorspace F norm"
+proof -
+  interpret subspace F E by fact
+  interpret normed_vectorspace E norm by fact
+  show ?thesis
+  proof
+    show "vectorspace F" by (rule vectorspace) unfold_locales
+  next
+    have "Normed_Space.norm E norm" ..
+    with subset show "Normed_Space.norm F norm"
+      by (simp add: norm_def seminorm_def norm_axioms_def)
+  qed
+qed
+
+end