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