# Theory NormedSpace

Up to index of Isabelle/HOL/HOL-Complex/HahnBanach

theory NormedSpace
imports Subspace
begin

    (*  Title:      HOL/Real/HahnBanach/NormedSpace.thy
        ID:         $Id: NormedSpace.thy,v 1.21 2005/06/17 14:13:09 haftmann Exp $
        Author:     Gertrud Bauer, TU Munich
    *)

    header {* Normed vector spaces *}

    theory NormedSpace imports  Subspace begin

    subsection {* Quasinorms *}

    text {*
      A \emph{seminorm} @{text "\<parallel>·\<parallel>"} 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"    ("\<parallel>_\<parallel>")

    locale seminorm = var V + norm_syntax +
      assumes ge_zero [iff?]: "x ∈ V ==> 0 ≤ \<parallel>x\<parallel>"
        and abs_homogenous [iff?]: "x ∈ V ==> \<parallel>a · x\<parallel> = ¦a¦ * \<parallel>x\<parallel>"
        and subadditive [iff?]: "x ∈ V ==> y ∈ V ==> \<parallel>x + y\<parallel> ≤ \<parallel>x\<parallel> + \<parallel>y\<parallel>"

    declare seminorm.intro [intro?]

    lemma (in seminorm) diff_subadditive:
      includes vectorspace
      shows "x ∈ V ==> y ∈ V ==> \<parallel>x - y\<parallel> ≤ \<parallel>x\<parallel> + \<parallel>y\<parallel>"
    proof -
      assume x: "x ∈ V" and y: "y ∈ V"
      hence "x - y = x + - 1 · y"
        by (simp add: diff_eq2 negate_eq2a)
      also from x y have "\<parallel>…\<parallel> ≤ \<parallel>x\<parallel> + \<parallel>- 1 · y\<parallel>"
        by (simp add: subadditive)
      also from y have "\<parallel>- 1 · y\<parallel> = ¦- 1¦ * \<parallel>y\<parallel>"
        by (rule abs_homogenous)
      also have "… = \<parallel>y\<parallel>" by simp
      finally show ?thesis .
    qed

    lemma (in seminorm) minus:
      includes vectorspace
      shows "x ∈ V ==> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
    proof -
      assume x: "x ∈ V"
      hence "- x = - 1 · x" by (simp only: negate_eq1)
      also from x have "\<parallel>…\<parallel> = ¦- 1¦ * \<parallel>x\<parallel>"
        by (rule abs_homogenous)
      also have "… = \<parallel>x\<parallel>" by simp
      finally show ?thesis .
    qed

    subsection {* Norms *}

    text {*
      A \emph{norm} @{text "\<parallel>·\<parallel>"} is a seminorm that maps only the
      @{text 0} vector to @{text 0}.
    *}

    locale norm = seminorm +
      assumes zero_iff [iff]: "x ∈ V ==> (\<parallel>x\<parallel> = 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 < \<parallel>x\<parallel>"
    proof -
      assume x: "x ∈ V" and neq: "x ≠ 0"
      from x have "0 ≤ \<parallel>x\<parallel>" ..
      also have [symmetric]: "… ≠ 0"
      proof
        assume "\<parallel>x\<parallel> = 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?]:
      includes subspace F E + normed_vectorspace E
      shows "normed_vectorspace F norm"
    proof
      show "vectorspace F" by (rule vectorspace)
      have "seminorm E norm" . with subset show "seminorm F norm"
        by (simp add: seminorm_def)
      have "norm_axioms E norm" . with subset show "norm_axioms F norm"
        by (simp add: norm_axioms_def)
    qed

    end

### Quasinorms

lemma diff_subadditive:

      [| seminorm V norm; vectorspace V; x ∈ V; y ∈ V |]
      ==> norm (x - y) ≤ norm x + norm y

lemma minus:

      [| seminorm V norm; vectorspace V; x ∈ V |] ==> norm (- x) = norm x

### Norms

### Normed vector spaces

lemma gt_zero:

      [| normed_vectorspace V norm; x ∈ V; x ≠ (0::'a) |] ==> 0 < norm x

lemma subspace_normed_vs:

      [| normed_vectorspace E norm; subspace F E |] ==> normed_vectorspace F norm