# Theory Normed_Space

theory Normed_Space
imports Subspace
```(*  Title:      HOL/Hahn_Banach/Normed_Space.thy
Author:     Gertrud Bauer, TU Munich
*)

section ‹Normed vector spaces›

theory Normed_Space
imports Subspace
begin

subsection ‹Quasinorms›

text ‹
A ∗‹seminorm› ‹∥⋅∥› is a function on a real vector space into the reals that
has the following properties: it is positive definite, absolute homogeneous
›

locale seminorm =
fixes V :: "'a::{minus, plus, zero, uminus} set"
fixes norm :: "'a ⇒ real"    ("∥_∥")
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?]

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"
also from x y have "∥…∥ ≤ ∥x∥ + ∥- 1 ⋅ y∥"
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 ∗‹norm› ‹∥⋅∥› is a seminorm that maps only the ‹0› vector to ‹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 ∗‹normed space›.
›

locale normed_vectorspace = vectorspace + norm

declare normed_vectorspace.intro [intro?]

lemma (in normed_vectorspace) gt_zero [intro?]:
assumes x: "x ∈ V" and neq: "x ≠ 0"
shows "0 < ∥x∥"
proof -
from x have "0 ≤ ∥x∥" ..
also have "0 ≠ ∥x∥"
proof
assume "0 = ∥x∥"
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
```