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;
```     1 (*  Title:      HOL/Hahn_Banach/Normed_Space.thy
```
```     2     Author:     Gertrud Bauer, TU Munich
```
```     3 *)
```
```     4
```
```     5 section \<open>Normed vector spaces\<close>
```
```     6
```
```     7 theory Normed_Space
```
```     8 imports Subspace
```
```     9 begin
```
```    10
```
```    11 subsection \<open>Quasinorms\<close>
```
```    12
```
```    13 text \<open>
```
```    14   A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals that
```
```    15   has the following properties: it is positive definite, absolute homogeneous
```
```    16   and subadditive.
```
```    17 \<close>
```
```    18
```
```    19 locale seminorm =
```
```    20   fixes V :: "'a::{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 \<open>Norms\<close>
```
```    58
```
```    59 text \<open>
```
```    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>.
```
```    61 \<close>
```
```    62
```
```    63 locale norm = seminorm +
```
```    64   assumes zero_iff [iff]: "x \<in> V \<Longrightarrow> (\<parallel>x\<parallel> = 0) = (x = 0)"
```
```    65
```
```    66
```
```    67 subsection \<open>Normed vector spaces\<close>
```
```    68
```
```    69 text \<open>
```
```    70   A vector space together with a norm is called a \<^emph>\<open>normed space\<close>.
```
```    71 \<close>
```
```    72
```
```    73 locale normed_vectorspace = vectorspace + norm
```
```    74
```
```    75 declare normed_vectorspace.intro [intro?]
```
```    76
```
```    77 lemma (in normed_vectorspace) gt_zero [intro?]:
```
```    78   assumes x: "x \<in> V" and neq: "x \<noteq> 0"
```
```    79   shows "0 < \<parallel>x\<parallel>"
```
```    80 proof -
```
```    81   from x have "0 \<le> \<parallel>x\<parallel>" ..
```
```    82   also have "0 \<noteq> \<parallel>x\<parallel>"
```
```    83   proof
```
```    84     assume "0 = \<parallel>x\<parallel>"
```
```    85     with x have "x = 0" by simp
```
```    86     with neq show False by contradiction
```
```    87   qed
```
```    88   finally show ?thesis .
```
```    89 qed
```
```    90
```
```    91 text \<open>
```
```    92   Any subspace of a normed vector space is again a normed vectorspace.
```
```    93 \<close>
```
```    94
```
```    95 lemma subspace_normed_vs [intro?]:
```
```    96   fixes F E norm
```
```    97   assumes "subspace F E" "normed_vectorspace E norm"
```
```    98   shows "normed_vectorspace F norm"
```
```    99 proof -
```
```   100   interpret subspace F E by fact
```
```   101   interpret normed_vectorspace E norm by fact
```
```   102   show ?thesis
```
```   103   proof
```
```   104     show "vectorspace F" by (rule vectorspace) unfold_locales
```
```   105   next
```
```   106     have "Normed_Space.norm E norm" ..
```
```   107     with subset show "Normed_Space.norm F norm"
```
```   108       by (simp add: norm_def seminorm_def norm_axioms_def)
```
```   109   qed
```
```   110 qed
```
```   111
```
```   112 end
```