src/HOL/Hahn_Banach/Normed_Space.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 61879 e4f9d8f094fe
permissions -rw-r--r--
more robust sorted_entries;
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@58889
     5
section \<open>Normed vector spaces\<close>
wenzelm@7808
     6
wenzelm@31795
     7
theory Normed_Space
wenzelm@27612
     8
imports Subspace
wenzelm@27612
     9
begin
wenzelm@7535
    10
wenzelm@58744
    11
subsection \<open>Quasinorms\<close>
wenzelm@7808
    12
wenzelm@58744
    13
text \<open>
wenzelm@61879
    14
  A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals that
wenzelm@61879
    15
  has the following properties: it is positive definite, absolute homogeneous
wenzelm@61879
    16
  and subadditive.
wenzelm@58744
    17
\<close>
wenzelm@7535
    18
wenzelm@46867
    19
locale seminorm =
wenzelm@61076
    20
  fixes V :: "'a::{minus, plus, zero, uminus} set"
wenzelm@13515
    21
  fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
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:
ballarin@27611
    29
  assumes "vectorspace V"
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 -
ballarin@29234
    32
  interpret vectorspace V by fact
wenzelm@13515
    33
  assume x: "x \<in> V" and y: "y \<in> V"
wenzelm@27612
    34
  then have "x - y = x + - 1 \<cdot> y"
wenzelm@13515
    35
    by (simp add: diff_eq2 negate_eq2a)
wenzelm@13515
    36
  also from x y have "\<parallel>\<dots>\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>- 1 \<cdot> y\<parallel>"
wenzelm@13515
    37
    by (simp add: subadditive)
wenzelm@13515
    38
  also from y have "\<parallel>- 1 \<cdot> y\<parallel> = \<bar>- 1\<bar> * \<parallel>y\<parallel>"
wenzelm@13515
    39
    by (rule abs_homogenous)
wenzelm@13515
    40
  also have "\<dots> = \<parallel>y\<parallel>" by simp
wenzelm@13515
    41
  finally show ?thesis .
wenzelm@9035
    42
qed
wenzelm@7535
    43
wenzelm@13547
    44
lemma (in seminorm) minus:
ballarin@27611
    45
  assumes "vectorspace V"
wenzelm@13547
    46
  shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
wenzelm@9035
    47
proof -
ballarin@29234
    48
  interpret vectorspace V by fact
wenzelm@13515
    49
  assume x: "x \<in> V"
wenzelm@27612
    50
  then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
wenzelm@44887
    51
  also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>" by (rule abs_homogenous)
wenzelm@13515
    52
  also have "\<dots> = \<parallel>x\<parallel>" by simp
wenzelm@13515
    53
  finally show ?thesis .
wenzelm@9035
    54
qed
wenzelm@7535
    55
wenzelm@7535
    56
wenzelm@58744
    57
subsection \<open>Norms\<close>
wenzelm@7808
    58
wenzelm@58744
    59
text \<open>
wenzelm@61879
    60
  A \<^emph>\<open>norm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a seminorm that maps only the \<open>0\<close> vector to \<open>0\<close>.
wenzelm@58744
    61
\<close>
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@58744
    67
subsection \<open>Normed vector spaces\<close>
wenzelm@7808
    68
wenzelm@58744
    69
text \<open>
wenzelm@61879
    70
  A vector space together with a norm is called a \<^emph>\<open>normed space\<close>.
wenzelm@58744
    71
\<close>
wenzelm@7535
    72
wenzelm@13547
    73
locale normed_vectorspace = vectorspace + norm
wenzelm@7535
    74
ballarin@14254
    75
declare normed_vectorspace.intro [intro?]
ballarin@14254
    76
wenzelm@13515
    77
lemma (in normed_vectorspace) gt_zero [intro?]:
wenzelm@44887
    78
  assumes x: "x \<in> V" and neq: "x \<noteq> 0"
wenzelm@44887
    79
  shows "0 < \<parallel>x\<parallel>"
wenzelm@13515
    80
proof -
wenzelm@13515
    81
  from x have "0 \<le> \<parallel>x\<parallel>" ..
wenzelm@44887
    82
  also have "0 \<noteq> \<parallel>x\<parallel>"
wenzelm@9035
    83
  proof
wenzelm@44887
    84
    assume "0 = \<parallel>x\<parallel>"
wenzelm@13515
    85
    with x have "x = 0" by simp
wenzelm@13515
    86
    with neq show False by contradiction
wenzelm@13515
    87
  qed
wenzelm@13515
    88
  finally show ?thesis .
wenzelm@9035
    89
qed
wenzelm@7535
    90
wenzelm@58744
    91
text \<open>
wenzelm@13515
    92
  Any subspace of a normed vector space is again a normed vectorspace.
wenzelm@58744
    93
\<close>
wenzelm@7917
    94
wenzelm@10687
    95
lemma subspace_normed_vs [intro?]:
ballarin@27611
    96
  fixes F E norm
ballarin@27611
    97
  assumes "subspace F E" "normed_vectorspace E norm"
wenzelm@13515
    98
  shows "normed_vectorspace F norm"
ballarin@27611
    99
proof -
ballarin@29234
   100
  interpret subspace F E by fact
ballarin@29234
   101
  interpret normed_vectorspace E norm by fact
wenzelm@27612
   102
  show ?thesis
wenzelm@27612
   103
  proof
ballarin@27611
   104
    show "vectorspace F" by (rule vectorspace) unfold_locales
ballarin@27611
   105
  next
wenzelm@31795
   106
    have "Normed_Space.norm E norm" ..
wenzelm@31795
   107
    with subset show "Normed_Space.norm F norm"
ballarin@27611
   108
      by (simp add: norm_def seminorm_def norm_axioms_def)
ballarin@27611
   109
  qed
wenzelm@9035
   110
qed
wenzelm@7535
   111
wenzelm@10687
   112
end