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