(* Title: HOL/Hahn_Banach/Normed_Space.thy
Author: Gertrud Bauer, TU Munich
*)
header {* Normed vector spaces *}
theory Normed_Space
imports Subspace
begin
subsection {* Quasinorms *}
text {*
A \emph{seminorm} @{text "\\\"} is a function on a real vector space
into the reals that has the following properties: it is positive
definite, absolute homogenous and subadditive.
*}
locale norm_syntax =
fixes norm :: "'a \ real" ("\_\")
locale seminorm = var_V + norm_syntax +
constrains V :: "'a\{minus, plus, zero, uminus} set"
assumes ge_zero [iff?]: "x \ V \ 0 \ \x\"
and abs_homogenous [iff?]: "x \ V \ \a \ x\ = \a\ * \x\"
and subadditive [iff?]: "x \ V \ y \ V \ \x + y\ \ \x\ + \y\"
declare seminorm.intro [intro?]
lemma (in seminorm) diff_subadditive:
assumes "vectorspace V"
shows "x \ V \ y \ V \ \x - y\ \ \x\ + \y\"
proof -
interpret vectorspace V by fact
assume x: "x \ V" and y: "y \ V"
then have "x - y = x + - 1 \ y"
by (simp add: diff_eq2 negate_eq2a)
also from x y have "\\\ \ \x\ + \- 1 \ y\"
by (simp add: subadditive)
also from y have "\- 1 \ y\ = \- 1\ * \y\"
by (rule abs_homogenous)
also have "\ = \y\" by simp
finally show ?thesis .
qed
lemma (in seminorm) minus:
assumes "vectorspace V"
shows "x \ V \ \- x\ = \x\"
proof -
interpret vectorspace V by fact
assume x: "x \ V"
then have "- x = - 1 \ x" by (simp only: negate_eq1)
also from x have "\\\ = \- 1\ * \x\"
by (rule abs_homogenous)
also have "\ = \x\" by simp
finally show ?thesis .
qed
subsection {* Norms *}
text {*
A \emph{norm} @{text "\\\"} is a seminorm that maps only the
@{text 0} vector to @{text 0}.
*}
locale norm = seminorm +
assumes zero_iff [iff]: "x \ V \ (\x\ = 0) = (x = 0)"
subsection {* Normed vector spaces *}
text {*
A vector space together with a norm is called a \emph{normed
space}.
*}
locale normed_vectorspace = vectorspace + norm
declare normed_vectorspace.intro [intro?]
lemma (in normed_vectorspace) gt_zero [intro?]:
"x \ V \ x \ 0 \ 0 < \x\"
proof -
assume x: "x \ V" and neq: "x \ 0"
from x have "0 \ \x\" ..
also have [symmetric]: "\ \ 0"
proof
assume "\x\ = 0"
with x have "x = 0" by simp
with neq show False by contradiction
qed
finally show ?thesis .
qed
text {*
Any subspace of a normed vector space is again a normed vectorspace.
*}
lemma subspace_normed_vs [intro?]:
fixes F E norm
assumes "subspace F E" "normed_vectorspace E norm"
shows "normed_vectorspace F norm"
proof -
interpret subspace F E by fact
interpret normed_vectorspace E norm by fact
show ?thesis
proof
show "vectorspace F" by (rule vectorspace) unfold_locales
next
have "Normed_Space.norm E norm" ..
with subset show "Normed_Space.norm F norm"
by (simp add: norm_def seminorm_def norm_axioms_def)
qed
qed
end