1(* Title: HOL/Hahn_Banach/Normed_Space.thy 2 Author: Gertrud Bauer, TU Munich 3*) 4 5section \<open>Normed vector spaces\<close> 6 7theory Normed_Space 8imports Subspace 9begin 10 11subsection \<open>Quasinorms\<close> 12 13text \<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 19locale 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 26declare seminorm.intro [intro?] 27 28lemma (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>" 31proof - 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 . 42qed 43 44lemma (in seminorm) minus: 45 assumes "vectorspace V" 46 shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>" 47proof - 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 . 54qed 55 56 57subsection \<open>Norms\<close> 58 59text \<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 63locale norm = seminorm + 64 assumes zero_iff [iff]: "x \<in> V \<Longrightarrow> (\<parallel>x\<parallel> = 0) = (x = 0)" 65 66 67subsection \<open>Normed vector spaces\<close> 68 69text \<open> 70 A vector space together with a norm is called a \<^emph>\<open>normed space\<close>. 71\<close> 72 73locale normed_vectorspace = vectorspace + norm 74 75declare normed_vectorspace.intro [intro?] 76 77lemma (in normed_vectorspace) gt_zero [intro?]: 78 assumes x: "x \<in> V" and neq: "x \<noteq> 0" 79 shows "0 < \<parallel>x\<parallel>" 80proof - 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 . 89qed 90 91text \<open> 92 Any subspace of a normed vector space is again a normed vectorspace. 93\<close> 94 95lemma subspace_normed_vs [intro?]: 96 fixes F E norm 97 assumes "subspace F E" "normed_vectorspace E norm" 98 shows "normed_vectorspace F norm" 99proof - 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 110qed 111 112end 113