products/sources/formale sprachen/Delphi/Agenda 1.1/Auslieferung/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: tptp.yacc   Sprache: Unknown

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

section \<open>Normed vector spaces\<close>

theory Normed_Space
imports Subspace
begin

subsection \<open>Quasinorms\<close>

text \<open>
  A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals that
  has the following properties: it is positive definite, absolute homogeneous
  and subadditive.
\<close>

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 \<open>Norms\<close>

text \<open>
  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>.
\<close>

locale norm = seminorm +
  assumes zero_iff [iff]: "x \ V \ (\x\ = 0) = (x = 0)"


subsection \<open>Normed vector spaces\<close>

text \<open>
  A vector space together with a norm is called a \<^emph>\<open>normed space\<close>.
\<close>

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 \<open>
  Any subspace of a normed vector space is again a normed vectorspace.
\<close>

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

[ Verzeichnis aufwärts0.17unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]