(* 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 and subadditive. › 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?] 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 ∗‹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