1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HahnBanach/NormedSpace.thy	Tue Dec 30 11:10:01 2008 +0100
     1.3 @@ -0,0 +1,117 @@
     1.4 +(*  Title:      HOL/Real/HahnBanach/NormedSpace.thy
     1.5 +    Author:     Gertrud Bauer, TU Munich
     1.6 +*)
     1.7 +
     1.8 +header {* Normed vector spaces *}
     1.9 +
    1.10 +theory NormedSpace
    1.11 +imports Subspace
    1.12 +begin
    1.13 +
    1.14 +subsection {* Quasinorms *}
    1.15 +
    1.16 +text {*
    1.17 +  A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
    1.18 +  into the reals that has the following properties: it is positive
    1.19 +  definite, absolute homogenous and subadditive.
    1.20 +*}
    1.21 +
    1.22 +locale norm_syntax =
    1.23 +  fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
    1.24 +
    1.25 +locale seminorm = var_V + norm_syntax +
    1.26 +  constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
    1.27 +  assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
    1.28 +    and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
    1.29 +    and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
    1.30 +
    1.31 +declare seminorm.intro [intro?]
    1.32 +
    1.33 +lemma (in seminorm) diff_subadditive:
    1.34 +  assumes "vectorspace V"
    1.35 +  shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
    1.36 +proof -
    1.37 +  interpret vectorspace V by fact
    1.38 +  assume x: "x \<in> V" and y: "y \<in> V"
    1.39 +  then have "x - y = x + - 1 \<cdot> y"
    1.40 +    by (simp add: diff_eq2 negate_eq2a)
    1.41 +  also from x y have "\<parallel>\<dots>\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>- 1 \<cdot> y\<parallel>"
    1.42 +    by (simp add: subadditive)
    1.43 +  also from y have "\<parallel>- 1 \<cdot> y\<parallel> = \<bar>- 1\<bar> * \<parallel>y\<parallel>"
    1.44 +    by (rule abs_homogenous)
    1.45 +  also have "\<dots> = \<parallel>y\<parallel>" by simp
    1.46 +  finally show ?thesis .
    1.47 +qed
    1.48 +
    1.49 +lemma (in seminorm) minus:
    1.50 +  assumes "vectorspace V"
    1.51 +  shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
    1.52 +proof -
    1.53 +  interpret vectorspace V by fact
    1.54 +  assume x: "x \<in> V"
    1.55 +  then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
    1.56 +  also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
    1.57 +    by (rule abs_homogenous)
    1.58 +  also have "\<dots> = \<parallel>x\<parallel>" by simp
    1.59 +  finally show ?thesis .
    1.60 +qed
    1.61 +
    1.62 +
    1.63 +subsection {* Norms *}
    1.64 +
    1.65 +text {*
    1.66 +  A \emph{norm} @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
    1.67 +  @{text 0} vector to @{text 0}.
    1.68 +*}
    1.69 +
    1.70 +locale norm = seminorm +
    1.71 +  assumes zero_iff [iff]: "x \<in> V \<Longrightarrow> (\<parallel>x\<parallel> = 0) = (x = 0)"
    1.72 +
    1.73 +
    1.74 +subsection {* Normed vector spaces *}
    1.75 +
    1.76 +text {*
    1.77 +  A vector space together with a norm is called a \emph{normed
    1.78 +  space}.
    1.79 +*}
    1.80 +
    1.81 +locale normed_vectorspace = vectorspace + norm
    1.82 +
    1.83 +declare normed_vectorspace.intro [intro?]
    1.84 +
    1.85 +lemma (in normed_vectorspace) gt_zero [intro?]:
    1.86 +  "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>"
    1.87 +proof -
    1.88 +  assume x: "x \<in> V" and neq: "x \<noteq> 0"
    1.89 +  from x have "0 \<le> \<parallel>x\<parallel>" ..
    1.90 +  also have [symmetric]: "\<dots> \<noteq> 0"
    1.91 +  proof
    1.92 +    assume "\<parallel>x\<parallel> = 0"
    1.93 +    with x have "x = 0" by simp
    1.94 +    with neq show False by contradiction
    1.95 +  qed
    1.96 +  finally show ?thesis .
    1.97 +qed
    1.98 +
    1.99 +text {*
   1.100 +  Any subspace of a normed vector space is again a normed vectorspace.
   1.101 +*}
   1.102 +
   1.103 +lemma subspace_normed_vs [intro?]:
   1.104 +  fixes F E norm
   1.105 +  assumes "subspace F E" "normed_vectorspace E norm"
   1.106 +  shows "normed_vectorspace F norm"
   1.107 +proof -
   1.108 +  interpret subspace F E by fact
   1.109 +  interpret normed_vectorspace E norm by fact
   1.110 +  show ?thesis
   1.111 +  proof
   1.112 +    show "vectorspace F" by (rule vectorspace) unfold_locales
   1.113 +  next
   1.114 +    have "NormedSpace.norm E norm" ..
   1.115 +    with subset show "NormedSpace.norm F norm"
   1.116 +      by (simp add: norm_def seminorm_def norm_axioms_def)
   1.117 +  qed
   1.118 +qed
   1.119 +
   1.120 +end