Quelle Normed_Space.thy Sprache: Isabelle

(*  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 [intro?]: "x \ V \ 0 \ \x\"
    and abs_homogenous [intro?]: "x \ V \ \a \ x\ = \a\ * \x\"
    and subadditive [intro?]: "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
    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

quality95%

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.