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