src/HOL/Real/HahnBanach/NormedSpace.thy

removed explicit terminator (";");

(*  Title:      HOL/Real/HahnBanach/NormedSpace.thy
    ID:         $Id$
    Author:     Gertrud Bauer, TU Munich
*)

header {* Normed vector spaces *}

theory NormedSpace =  Subspace:


subsection {* Quasinorms *}

text{* A \emph{seminorm} $\norm{\cdot}$ is a function on a real vector
space into the reals that has the following properties: It is positive
definite, absolute homogenous and subadditive.  *}

constdefs
  is_seminorm :: "['a::{plus, minus} set, 'a => real] => bool"
  "is_seminorm V norm == ALL x: V. ALL y:V. ALL a. 
        #0 <= norm x 
      & norm (a (*) x) = (abs a) * (norm x)
      & norm (x + y) <= norm x + norm y"

lemma is_seminormI [intro]: 
  "[| !! x y a. [| x:V; y:V|] ==> #0 <= norm x;
  !! x a. x:V ==> norm (a (*) x) = (abs a) * (norm x);
  !! x y. [|x:V; y:V |] ==> norm (x + y) <= norm x + norm y |] 
  ==> is_seminorm V norm"
  by (unfold is_seminorm_def, force)

lemma seminorm_ge_zero [intro??]:
  "[| is_seminorm V norm; x:V |] ==> #0 <= norm x"
  by (unfold is_seminorm_def, force)

lemma seminorm_abs_homogenous: 
  "[| is_seminorm V norm; x:V |] 
  ==> norm (a (*) x) = (abs a) * (norm x)"
  by (unfold is_seminorm_def, force)

lemma seminorm_subadditive: 
  "[| is_seminorm V norm; x:V; y:V |] 
  ==> norm (x + y) <= norm x + norm y"
  by (unfold is_seminorm_def, force)

lemma seminorm_diff_subadditive: 
  "[| is_seminorm V norm; x:V; y:V; is_vectorspace V |] 
  ==> norm (x - y) <= norm x + norm y"
proof -
  assume "is_seminorm V norm" "x:V" "y:V" "is_vectorspace V"
  have "norm (x - y) = norm (x + - #1 (*) y)"  
    by (simp! add: diff_eq2 negate_eq2a)
  also have "... <= norm x + norm  (- #1 (*) y)" 
    by (simp! add: seminorm_subadditive)
  also have "norm (- #1 (*) y) = abs (- #1) * norm y" 
    by (rule seminorm_abs_homogenous)
  also have "abs (- #1) = (#1::real)" by (rule abs_minus_one)
  finally show "norm (x - y) <= norm x + norm y" by simp
qed

lemma seminorm_minus: 
  "[| is_seminorm V norm; x:V; is_vectorspace V |] 
  ==> norm (- x) = norm x"
proof -
  assume "is_seminorm V norm" "x:V" "is_vectorspace V"
  have "norm (- x) = norm (- #1 (*) x)" by (simp! only: negate_eq1)
  also have "... = abs (- #1) * norm x" 
    by (rule seminorm_abs_homogenous)
  also have "abs (- #1) = (#1::real)" by (rule abs_minus_one)
  finally show "norm (- x) = norm x" by simp
qed


subsection {* Norms *}

text{* A \emph{norm} $\norm{\cdot}$ is a seminorm that maps only the
$\zero$ vector to $0$. *}

constdefs
  is_norm :: "['a::{minus, plus} set, 'a => real] => bool"
  "is_norm V norm == ALL x: V.  is_seminorm V norm 
      & (norm x = #0) = (x = 00)"

lemma is_normI [intro]: 
  "ALL x: V.  is_seminorm V norm  & (norm x = #0) = (x = 00) 
  ==> is_norm V norm" by (simp only: is_norm_def)

lemma norm_is_seminorm [intro??]: 
  "[| is_norm V norm; x:V |] ==> is_seminorm V norm"
  by (unfold is_norm_def, force)

lemma norm_zero_iff: 
  "[| is_norm V norm; x:V |] ==> (norm x = #0) = (x = 00)"
  by (unfold is_norm_def, force)

lemma norm_ge_zero [intro??]:
  "[|is_norm V norm; x:V |] ==> #0 <= norm x"
  by (unfold is_norm_def is_seminorm_def, force)


subsection {* Normed vector spaces *}

text{* A vector space together with a norm is called
a \emph{normed space}. *}

constdefs
  is_normed_vectorspace :: 
  "['a::{plus, minus} set, 'a => real] => bool"
  "is_normed_vectorspace V norm ==
      is_vectorspace V &
      is_norm V norm"

lemma normed_vsI [intro]: 
  "[| is_vectorspace V; is_norm V norm |] 
  ==> is_normed_vectorspace V norm"
  by (unfold is_normed_vectorspace_def) blast 

lemma normed_vs_vs [intro??]: 
  "is_normed_vectorspace V norm ==> is_vectorspace V"
  by (unfold is_normed_vectorspace_def) force

lemma normed_vs_norm [intro??]: 
  "is_normed_vectorspace V norm ==> is_norm V norm"
  by (unfold is_normed_vectorspace_def, elim conjE)

lemma normed_vs_norm_ge_zero [intro??]: 
  "[| is_normed_vectorspace V norm; x:V |] ==> #0 <= norm x"
  by (unfold is_normed_vectorspace_def, rule, elim conjE)

lemma normed_vs_norm_gt_zero [intro??]: 
  "[| is_normed_vectorspace V norm; x:V; x ~= 00 |] ==> #0 < norm x"
proof (unfold is_normed_vectorspace_def, elim conjE)
  assume "x : V" "x ~= 00" "is_vectorspace V" "is_norm V norm"
  have "#0 <= norm x" ..
  also have "#0 ~= norm x"
  proof
    presume "norm x = #0"
    also have "?this = (x = 00)" by (rule norm_zero_iff)
    finally have "x = 00" .
    thus "False" by contradiction
  qed (rule sym)
  finally show "#0 < norm x" .
qed

lemma normed_vs_norm_abs_homogenous [intro??]: 
  "[| is_normed_vectorspace V norm; x:V |] 
  ==> norm (a (*) x) = (abs a) * (norm x)"
  by (rule seminorm_abs_homogenous, rule norm_is_seminorm, 
      rule normed_vs_norm)

lemma normed_vs_norm_subadditive [intro??]: 
  "[| is_normed_vectorspace V norm; x:V; y:V |] 
  ==> norm (x + y) <= norm x + norm y"
  by (rule seminorm_subadditive, rule norm_is_seminorm, 
     rule normed_vs_norm)

text{* Any subspace of a normed vector space is again a 
normed vectorspace.*}

lemma subspace_normed_vs [intro??]: 
  "[| is_subspace F E; is_vectorspace E; 
  is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm"
proof (rule normed_vsI)
  assume "is_subspace F E" "is_vectorspace E" 
         "is_normed_vectorspace E norm"
  show "is_vectorspace F" ..
  show "is_norm F norm" 
  proof (intro is_normI ballI conjI)
    show "is_seminorm F norm" 
    proof
      fix x y a presume "x : E"
      show "#0 <= norm x" ..
      show "norm (a (*) x) = abs a * norm x" ..
      presume "y : E"
      show "norm (x + y) <= norm x + norm y" ..
    qed (simp!)+

    fix x assume "x : F"
    show "(norm x = #0) = (x = 00)" 
    proof (rule norm_zero_iff)
      show "is_norm E norm" ..
    qed (simp!)
  qed
qed

end