src/HOL/Hahn_Banach/Normed_Space.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 56749 e96d6b38649e
child 58744 c434e37f290e
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     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 homogeneous and subadditive.
    17 *}
    18 
    19 locale seminorm =
    20   fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set"
    21   fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
    22   assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
    23     and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
    24     and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
    25 
    26 declare seminorm.intro [intro?]
    27 
    28 lemma (in seminorm) diff_subadditive:
    29   assumes "vectorspace V"
    30   shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
    31 proof -
    32   interpret vectorspace V by fact
    33   assume x: "x \<in> V" and y: "y \<in> V"
    34   then have "x - y = x + - 1 \<cdot> y"
    35     by (simp add: diff_eq2 negate_eq2a)
    36   also from x y have "\<parallel>\<dots>\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>- 1 \<cdot> y\<parallel>"
    37     by (simp add: subadditive)
    38   also from y have "\<parallel>- 1 \<cdot> y\<parallel> = \<bar>- 1\<bar> * \<parallel>y\<parallel>"
    39     by (rule abs_homogenous)
    40   also have "\<dots> = \<parallel>y\<parallel>" by simp
    41   finally show ?thesis .
    42 qed
    43 
    44 lemma (in seminorm) minus:
    45   assumes "vectorspace V"
    46   shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
    47 proof -
    48   interpret vectorspace V by fact
    49   assume x: "x \<in> V"
    50   then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
    51   also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>" by (rule abs_homogenous)
    52   also have "\<dots> = \<parallel>x\<parallel>" by simp
    53   finally show ?thesis .
    54 qed
    55 
    56 
    57 subsection {* Norms *}
    58 
    59 text {*
    60   A \emph{norm} @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
    61   @{text 0} vector to @{text 0}.
    62 *}
    63 
    64 locale norm = seminorm +
    65   assumes zero_iff [iff]: "x \<in> V \<Longrightarrow> (\<parallel>x\<parallel> = 0) = (x = 0)"
    66 
    67 
    68 subsection {* Normed vector spaces *}
    69 
    70 text {*
    71   A vector space together with a norm is called a \emph{normed
    72   space}.
    73 *}
    74 
    75 locale normed_vectorspace = vectorspace + norm
    76 
    77 declare normed_vectorspace.intro [intro?]
    78 
    79 lemma (in normed_vectorspace) gt_zero [intro?]:
    80   assumes x: "x \<in> V" and neq: "x \<noteq> 0"
    81   shows "0 < \<parallel>x\<parallel>"
    82 proof -
    83   from x have "0 \<le> \<parallel>x\<parallel>" ..
    84   also have "0 \<noteq> \<parallel>x\<parallel>"
    85   proof
    86     assume "0 = \<parallel>x\<parallel>"
    87     with x have "x = 0" by simp
    88     with neq show False by contradiction
    89   qed
    90   finally show ?thesis .
    91 qed
    92 
    93 text {*
    94   Any subspace of a normed vector space is again a normed vectorspace.
    95 *}
    96 
    97 lemma subspace_normed_vs [intro?]:
    98   fixes F E norm
    99   assumes "subspace F E" "normed_vectorspace E norm"
   100   shows "normed_vectorspace F norm"
   101 proof -
   102   interpret subspace F E by fact
   103   interpret normed_vectorspace E norm by fact
   104   show ?thesis
   105   proof
   106     show "vectorspace F" by (rule vectorspace) unfold_locales
   107   next
   108     have "Normed_Space.norm E norm" ..
   109     with subset show "Normed_Space.norm F norm"
   110       by (simp add: norm_def seminorm_def norm_axioms_def)
   111   qed
   112 qed
   113 
   114 end