src/HOL/Hahn_Banach/Normed_Space.thy
 author hoelzl Tue Jan 18 21:37:23 2011 +0100 (2011-01-18) changeset 41654 32fe42892983 parent 31795 be3e1cc5005c child 44887 7ca82df6e951 permissions -rw-r--r--
Gauge measure removed
     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