src/HOL/Hahn_Banach/Normed_Space.thy
 author haftmann Fri Nov 01 18:51:14 2013 +0100 (2013-11-01) changeset 54230 b1d955791529 parent 46867 0883804b67bb child 56749 e96d6b38649e permissions -rw-r--r--
more simplification rules on unary and binary minus
     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 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