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