src/HOL/Real/HahnBanach/NormedSpace.thy
author ballarin
Tue Jun 20 15:53:44 2006 +0200 (2006-06-20)
changeset 19931 fb32b43e7f80
parent 16417 9bc16273c2d4
child 19984 29bb4659f80a
permissions -rw-r--r--
Restructured locales with predicates: import is now an interpretation.
New method intro_locales.
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
haftmann@16417
     8
theory NormedSpace imports  Subspace begin
wenzelm@7535
     9
wenzelm@9035
    10
subsection {* Quasinorms *}
wenzelm@7808
    11
wenzelm@10687
    12
text {*
wenzelm@10687
    13
  A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
wenzelm@10687
    14
  into the reals that has the following properties: it is positive
wenzelm@10687
    15
  definite, absolute homogenous and subadditive.
wenzelm@10687
    16
*}
wenzelm@7535
    17
wenzelm@13515
    18
locale norm_syntax =
wenzelm@13515
    19
  fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
wenzelm@7535
    20
wenzelm@13515
    21
locale seminorm = var V + norm_syntax +
wenzelm@13515
    22
  assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
wenzelm@13515
    23
    and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
wenzelm@13515
    24
    and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
wenzelm@7535
    25
ballarin@14254
    26
declare seminorm.intro [intro?]
ballarin@14254
    27
wenzelm@13547
    28
lemma (in seminorm) diff_subadditive:
wenzelm@13547
    29
  includes vectorspace
wenzelm@13547
    30
  shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
wenzelm@9035
    31
proof -
wenzelm@13515
    32
  assume x: "x \<in> V" and y: "y \<in> V"
wenzelm@13515
    33
  hence "x - y = x + - 1 \<cdot> y"
wenzelm@13515
    34
    by (simp add: diff_eq2 negate_eq2a)
wenzelm@13515
    35
  also from x y have "\<parallel>\<dots>\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>- 1 \<cdot> y\<parallel>"
wenzelm@13515
    36
    by (simp add: subadditive)
wenzelm@13515
    37
  also from y have "\<parallel>- 1 \<cdot> y\<parallel> = \<bar>- 1\<bar> * \<parallel>y\<parallel>"
wenzelm@13515
    38
    by (rule abs_homogenous)
wenzelm@13515
    39
  also have "\<dots> = \<parallel>y\<parallel>" by simp
wenzelm@13515
    40
  finally show ?thesis .
wenzelm@9035
    41
qed
wenzelm@7535
    42
wenzelm@13547
    43
lemma (in seminorm) minus:
wenzelm@13547
    44
  includes vectorspace
wenzelm@13547
    45
  shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
wenzelm@9035
    46
proof -
wenzelm@13515
    47
  assume x: "x \<in> V"
wenzelm@13515
    48
  hence "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
wenzelm@13515
    49
  also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
wenzelm@13515
    50
    by (rule abs_homogenous)
wenzelm@13515
    51
  also have "\<dots> = \<parallel>x\<parallel>" by simp
wenzelm@13515
    52
  finally show ?thesis .
wenzelm@9035
    53
qed
wenzelm@7535
    54
wenzelm@7535
    55
wenzelm@9035
    56
subsection {* Norms *}
wenzelm@7808
    57
wenzelm@10687
    58
text {*
wenzelm@10687
    59
  A \emph{norm} @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
wenzelm@10687
    60
  @{text 0} vector to @{text 0}.
wenzelm@10687
    61
*}
wenzelm@7535
    62
wenzelm@13515
    63
locale norm = seminorm +
wenzelm@13515
    64
  assumes zero_iff [iff]: "x \<in> V \<Longrightarrow> (\<parallel>x\<parallel> = 0) = (x = 0)"
wenzelm@7535
    65
wenzelm@7535
    66
wenzelm@9035
    67
subsection {* Normed vector spaces *}
wenzelm@7808
    68
wenzelm@13515
    69
text {*
wenzelm@13515
    70
  A vector space together with a norm is called a \emph{normed
wenzelm@13515
    71
  space}.
wenzelm@13515
    72
*}
wenzelm@7535
    73
wenzelm@13547
    74
locale normed_vectorspace = vectorspace + norm
wenzelm@7535
    75
ballarin@14254
    76
declare normed_vectorspace.intro [intro?]
ballarin@14254
    77
wenzelm@13515
    78
lemma (in normed_vectorspace) gt_zero [intro?]:
wenzelm@13515
    79
  "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>"
wenzelm@13515
    80
proof -
wenzelm@13515
    81
  assume x: "x \<in> V" and neq: "x \<noteq> 0"
wenzelm@13515
    82
  from x have "0 \<le> \<parallel>x\<parallel>" ..
wenzelm@13515
    83
  also have [symmetric]: "\<dots> \<noteq> 0"
wenzelm@9035
    84
  proof
wenzelm@13515
    85
    assume "\<parallel>x\<parallel> = 0"
wenzelm@13515
    86
    with x have "x = 0" by simp
wenzelm@13515
    87
    with neq show False by contradiction
wenzelm@13515
    88
  qed
wenzelm@13515
    89
  finally show ?thesis .
wenzelm@9035
    90
qed
wenzelm@7535
    91
wenzelm@13515
    92
text {*
wenzelm@13515
    93
  Any subspace of a normed vector space is again a normed vectorspace.
wenzelm@13515
    94
*}
wenzelm@7917
    95
wenzelm@10687
    96
lemma subspace_normed_vs [intro?]:
wenzelm@13547
    97
  includes subspace F E + normed_vectorspace E
wenzelm@13515
    98
  shows "normed_vectorspace F norm"
wenzelm@13515
    99
proof
ballarin@19931
   100
  show "vectorspace F" by (rule vectorspace) intro_locales
ballarin@19931
   101
next
ballarin@19931
   102
  have "NormedSpace.norm E norm" by intro_locales
ballarin@19931
   103
  with subset show "NormedSpace.norm F norm"
ballarin@19931
   104
    by (simp add: norm_def seminorm_def norm_axioms_def)
wenzelm@9035
   105
qed
wenzelm@7535
   106
wenzelm@10687
   107
end