src/HOL/Real/HahnBanach/NormedSpace.thy
author wenzelm
Tue Jul 15 19:39:37 2008 +0200 (2008-07-15)
changeset 27612 d3eb431db035
parent 27611 2c01c0bdb385
child 28823 dcbef866c9e2
permissions -rw-r--r--
modernized specifications and proofs;
tuned document;
     1 (*  Title:      HOL/Real/HahnBanach/NormedSpace.thy
     2     ID:         $Id$
     3     Author:     Gertrud Bauer, TU Munich
     4 *)
     5 
     6 header {* Normed vector spaces *}
     7 
     8 theory NormedSpace
     9 imports Subspace
    10 begin
    11 
    12 subsection {* Quasinorms *}
    13 
    14 text {*
    15   A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
    16   into the reals that has the following properties: it is positive
    17   definite, absolute homogenous and subadditive.
    18 *}
    19 
    20 locale norm_syntax =
    21   fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
    22 
    23 locale seminorm = var V + norm_syntax +
    24   constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
    25   assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
    26     and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
    27     and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
    28 
    29 declare seminorm.intro [intro?]
    30 
    31 lemma (in seminorm) diff_subadditive:
    32   assumes "vectorspace V"
    33   shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
    34 proof -
    35   interpret vectorspace [V] by fact
    36   assume x: "x \<in> V" and y: "y \<in> V"
    37   then have "x - y = x + - 1 \<cdot> y"
    38     by (simp add: diff_eq2 negate_eq2a)
    39   also from x y have "\<parallel>\<dots>\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>- 1 \<cdot> y\<parallel>"
    40     by (simp add: subadditive)
    41   also from y have "\<parallel>- 1 \<cdot> y\<parallel> = \<bar>- 1\<bar> * \<parallel>y\<parallel>"
    42     by (rule abs_homogenous)
    43   also have "\<dots> = \<parallel>y\<parallel>" by simp
    44   finally show ?thesis .
    45 qed
    46 
    47 lemma (in seminorm) minus:
    48   assumes "vectorspace V"
    49   shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
    50 proof -
    51   interpret vectorspace [V] by fact
    52   assume x: "x \<in> V"
    53   then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
    54   also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
    55     by (rule abs_homogenous)
    56   also have "\<dots> = \<parallel>x\<parallel>" by simp
    57   finally show ?thesis .
    58 qed
    59 
    60 
    61 subsection {* Norms *}
    62 
    63 text {*
    64   A \emph{norm} @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
    65   @{text 0} vector to @{text 0}.
    66 *}
    67 
    68 locale norm = seminorm +
    69   assumes zero_iff [iff]: "x \<in> V \<Longrightarrow> (\<parallel>x\<parallel> = 0) = (x = 0)"
    70 
    71 
    72 subsection {* Normed vector spaces *}
    73 
    74 text {*
    75   A vector space together with a norm is called a \emph{normed
    76   space}.
    77 *}
    78 
    79 locale normed_vectorspace = vectorspace + norm
    80 
    81 declare normed_vectorspace.intro [intro?]
    82 
    83 lemma (in normed_vectorspace) gt_zero [intro?]:
    84   "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>"
    85 proof -
    86   assume x: "x \<in> V" and neq: "x \<noteq> 0"
    87   from x have "0 \<le> \<parallel>x\<parallel>" ..
    88   also have [symmetric]: "\<dots> \<noteq> 0"
    89   proof
    90     assume "\<parallel>x\<parallel> = 0"
    91     with x have "x = 0" by simp
    92     with neq show False by contradiction
    93   qed
    94   finally show ?thesis .
    95 qed
    96 
    97 text {*
    98   Any subspace of a normed vector space is again a normed vectorspace.
    99 *}
   100 
   101 lemma subspace_normed_vs [intro?]:
   102   fixes F E norm
   103   assumes "subspace F E" "normed_vectorspace E norm"
   104   shows "normed_vectorspace F norm"
   105 proof -
   106   interpret subspace [F E] by fact
   107   interpret normed_vectorspace [E norm] by fact
   108   show ?thesis
   109   proof
   110     show "vectorspace F" by (rule vectorspace) unfold_locales
   111   next
   112     have "NormedSpace.norm E norm" by unfold_locales
   113     with subset show "NormedSpace.norm F norm"
   114       by (simp add: norm_def seminorm_def norm_axioms_def)
   115   qed
   116 qed
   117 
   118 end