Quelle Subspace.thy Sprache: Isabelle

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

section \<open>Subspaces\<close>

theory Subspace
imports Vector_Space "HOL-Library.Set_Algebras"
begin

subsection \<open>Definition\<close>

text \<open>
  A non-empty subset \<open>U\<close> of a vector space \<open>V\<close> is a \<^emph>\<open>subspace\<close> of \<open>V\<close>, iff
  \<open>U\<close> is closed under addition and scalar multiplication.
\<close>

locale subspace =
  fixes U :: "'a::{minus, plus, zero, uminus} set" and V
  assumes non_empty [iff, intro]: "U \ {}"
    and subset [iff]: "U \ V"
    and add_closed [iff]: "x \ U \ y \ U \ x + y \ U"
    and mult_closed [iff]: "x \ U \ a \ x \ U"

notation (symbols)
  subspace  (infix \<open>\<unlhd>\<close> 50)

declare vectorspace.intro [intro?] subspace.intro [intro?]

lemma subspace_subset [elim]: "U \ V \ U \ V"
  by (rule subspace.subset)

lemma (in subspace) subsetD [iff]: "x \ U \ x \ V"
  using subset by blast

lemma subspaceD [elim]: "U \ V \ x \ U \ x \ V"
  by (rule subspace.subsetD)

lemma rev_subspaceD [elim?]: "x \ U \ U \ V \ x \ V"
  by (rule subspace.subsetD)

lemma (in subspace) diff_closed [iff]:
  assumes "vectorspace V"
  assumes x: "x \ U" and y: "y \ U"
  shows "x - y \ U"
proof -
  interpret vectorspace V by fact
  from x y show ?thesis by (simp add: diff_eq1 negate_eq1)
qed

text \<open>
  \<^medskip>
  Similar as for linear spaces, the existence of the zero element in every
  subspace follows from the non-emptiness of the carrier set and by vector
  space laws.
\<close>

lemma (in subspace) zero [intro]:
  assumes "vectorspace V"
  shows "0 \ U"
proof -
  interpret V: vectorspace V by fact
  have "U \ {}" by (rule non_empty)
  then obtain x where x: "x \ U" by blast
  then have "x \ V" .. then have "0 = x - x" by simp
  also from \<open>vectorspace V\<close> x x have "\<dots> \<in> U" by (rule diff_closed)
  finally show ?thesis .
qed

lemma (in subspace) neg_closed [iff]:
  assumes "vectorspace V"
  assumes x: "x \ U"
  shows "- x \ U"
proof -
  interpret vectorspace V by fact
  from x show ?thesis by (simp add: negate_eq1)
qed

text \<open>\<^medskip> Further derived laws: every subspace is a vector space.\<close>

lemma (in subspace) vectorspace [iff]:
  assumes "vectorspace V"
  shows "vectorspace U"
proof -
  interpret vectorspace V by fact
  show ?thesis
  proof
    show "U \ {}" ..
    fix x y z assume x: "x \ U" and y: "y \ U" and z: "z \ U"
    fix a b :: real
    from x y show "x + y \ U" by simp
    from x show "a \ x \ U" by simp
    from x y z show "(x + y) + z = x + (y + z)" by (simp add: add_ac)
    from x y show "x + y = y + x" by (simp add: add_ac)
    from x show "x - x = 0" by simp
    from x show "0 + x = x" by simp
    from x y show "a \ (x + y) = a \ x + a \ y" by (simp add: distrib)
    from x show "(a + b) \ x = a \ x + b \ x" by (simp add: distrib)
    from x show "(a * b) \ x = a \ b \ x" by (simp add: mult_assoc)
    from x show "1 \ x = x" by simp
    from x show "- x = - 1 \ x" by (simp add: negate_eq1)
    from x y show "x - y = x + - y" by (simp add: diff_eq1)
  qed
qed

text \<open>The subspace relation is reflexive.\<close>

lemma (in vectorspace) subspace_refl [intro]: "V \ V"
proof
  show "V \ {}" ..
  show "V \ V" ..
  fix a :: real and x y assume x: "x \ V" and y: "y \ V"
  from x y show "x + y \ V" by simp
  from x show "a \ x \ V" by simp
qed

text \<open>The subspace relation is transitive.\<close>

lemma (in vectorspace) subspace_trans [trans]:
  "U \ V \ V \ W \ U \ W"
proof
  assume uv: "U \ V" and vw: "V \ W"
  from uv show "U \ {}" by (rule subspace.non_empty)
  show "U \ W"
  proof -
    from uv have "U \ V" by (rule subspace.subset)
    also from vw have "V \ W" by (rule subspace.subset)
    finally show ?thesis .
  qed
  fix x y assume x: "x \ U" and y: "y \ U"
  from uv and x y show "x + y \ U" by (rule subspace.add_closed)
  from uv and x show "a \ x \ U" for a by (rule subspace.mult_closed)
qed

subsection \<open>Linear closure\<close>

text \<open>
  The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all scalar multiples of
  \<open>x\<close>.
\<close>

definition lin :: "('a::{minus,plus,zero}) \ 'a set"
  where "lin x = {a \ x | a. True}"

lemma linI [intro]: "y = a \ x \ y \ lin x"
  unfolding lin_def by blast

lemma linI' [iff]: "a \ x \ lin x"
  unfolding lin_def by blast

lemma linE [elim]:
  assumes "x \ lin v"
  obtains a :: real where "x = a \ v"
  using assms unfolding lin_def by blast

text \<open>Every vector is contained in its linear closure.\<close>

lemma (in vectorspace) x_lin_x [iff]: "x \ V \ x \ lin x"
proof -
  assume "x \ V"
  then have "x = 1 \ x" by simp
  also have "\ \ lin x" ..
  finally show ?thesis .
qed

lemma (in vectorspace) "0_lin_x" [iff]: "x \ V \ 0 \ lin x"
proof
  assume "x \ V"
  then show "0 = 0 \ x" by simp
qed

text \<open>Any linear closure is a subspace.\<close>

lemma (in vectorspace) lin_subspace [intro]:
  assumes x: "x \ V"
  shows "lin x \ V"
proof
  from x show "lin x \ {}" by auto
  show "lin x \ V"
  proof
    fix x' assume "x' \<in> lin x"
    then obtain a where "x' = a \ x" ..
    with x show "x' \ V" by simp
  qed

  fix x' x'' assume x': "x' \ lin x" and x'': "x'' \ lin x"
  show "x' + x'' \ lin x"
  proof -
    from x' obtain a' where "x' = a' \ x" ..
    moreover from x'' obtain a'' where "x'' = a'' \ x" ..
    ultimately have "x' + x'' = (a' + a'') \ x"
      using x by (simp add: distrib)
    also have "\ \ lin x" ..
    finally show ?thesis .
  qed
  show "a \ x' \ lin x" for a :: real
  proof -
    from x' obtain a' where "x' = a' \ x" ..
    with x have "a \ x' = (a * a') \ x" by (simp add: mult_assoc)
    also have "\ \ lin x" ..
    finally show ?thesis .
  qed
qed

text \<open>Any linear closure is a vector space.\<close>

lemma (in vectorspace) lin_vectorspace [intro]:
  assumes "x \ V"
  shows "vectorspace (lin x)"
proof -
  from \<open>x \<in> V\<close> have "subspace (lin x) V"
    by (rule lin_subspace)
  from this and vectorspace_axioms show ?thesis
    by (rule subspace.vectorspace)
qed

subsection \<open>Sum of two vectorspaces\<close>

text \<open>
  The \<^emph>\<open>sum\<close> of two vectorspaces \<open>U\<close> and \<open>V\<close> is the set of all sums of
  elements from \<open>U\<close> and \<open>V\<close>.
\<close>

lemma sum_def: "U + V = {u + v | u v. u \ U \ v \ V}"
  unfolding set_plus_def by auto

lemma sumE [elim]:
    "x \ U + V \ (\u v. x = u + v \ u \ U \ v \ V \ C) \ C"
  unfolding sum_def by blast

lemma sumI [intro]:
    "u \ U \ v \ V \ x = u + v \ x \ U + V"
  unfolding sum_def by blast

lemma sumI' [intro]:
    "u \ U \ v \ V \ u + v \ U + V"
  unfolding sum_def by blast

text \<open>\<open>U\<close> is a subspace of \<open>U + V\<close>.\<close>

lemma subspace_sum1 [iff]:
  assumes "vectorspace U" "vectorspace V"
  shows "U \ U + V"
proof -
  interpret vectorspace U by fact
  interpret vectorspace V by fact
  show ?thesis
  proof
    show "U \ {}" ..
    show "U \ U + V"
    proof
      fix x assume x: "x \ U"
      moreover have "0 \ V" ..
      ultimately have "x + 0 \ U + V" ..
      with x show "x \ U + V" by simp
    qed
    fix x y assume x: "x \ U" and "y \ U"
    then show "x + y \ U" by simp
    from x show "a \ x \ U" for a by simp
  qed
qed

text \<open>The sum of two subspaces is again a subspace.\<close>

lemma sum_subspace [intro?]:
  assumes "subspace U E" "vectorspace E" "subspace V E"
  shows "U + V \ E"
proof -
  interpret subspace U E by fact
  interpret vectorspace E by fact
  interpret subspace V E by fact
  show ?thesis
  proof
    have "0 \ U + V"
    proof
      show "0 \ U" using \vectorspace E\ ..
      show "0 \ V" using \vectorspace E\ ..
      show "(0::'a) = 0 + 0" by simp
    qed
    then show "U + V \ {}" by blast
    show "U + V \ E"
    proof
      fix x assume "x \ U + V"
      then obtain u v where "x = u + v" and
        "u \ U" and "v \ V" ..
      then show "x \ E" by simp
    qed

    fix x y assume x: "x \ U + V" and y: "y \ U + V"
    show "x + y \ U + V"
    proof -
      from x obtain ux vx where "x = ux + vx" and "ux \ U" and "vx \ V" ..
      moreover
      from y obtain uy vy where "y = uy + vy" and "uy \ U" and "vy \ V" ..
      ultimately
      have "ux + uy \ U"
        and "vx + vy \ V"
        and "x + y = (ux + uy) + (vx + vy)"
        using x y by (simp_all add: add_ac)
      then show ?thesis ..
    qed
    show "a \ x \ U + V" for a
    proof -
      from x obtain u v where "x = u + v" and "u \ U" and "v \ V" ..
      then have "a \ u \ U" and "a \ v \ V"
        and "a \ x = (a \ u) + (a \ v)" by (simp_all add: distrib)
      then show ?thesis ..
    qed
  qed
qed

text \<open>The sum of two subspaces is a vectorspace.\<close>

lemma sum_vs [intro?]:
    "U \ E \ V \ E \ vectorspace E \ vectorspace (U + V)"
  by (rule subspace.vectorspace) (rule sum_subspace)

subsection \<open>Direct sums\<close>

text \<open>
  The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the zero element is the only
  common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct sum of
  \<open>U\<close> and \<open>V\<close> the decomposition in \<open>x = u + v\<close> with \<open>u \<in> U\<close> and \<open>v \<in> V\<close> is
  unique.
\<close>

lemma decomp:
  assumes "vectorspace E" "subspace U E" "subspace V E"
  assumes direct: "U \ V = {0}"
    and u1: "u1 \ U" and u2: "u2 \ U"
    and v1: "v1 \ V" and v2: "v2 \ V"
    and sum: "u1 + v1 = u2 + v2"
  shows "u1 = u2 \ v1 = v2"
proof -
  interpret vectorspace E by fact
  interpret subspace U E by fact
  interpret subspace V E by fact
  show ?thesis
  proof
    have U: "vectorspace U"  (* FIXME: use interpret *)
      using \<open>subspace U E\<close> \<open>vectorspace E\<close> by (rule subspace.vectorspace)
    have V: "vectorspace V"
      using \<open>subspace V E\<close> \<open>vectorspace E\<close> by (rule subspace.vectorspace)
    from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1"
      by (simp add: add_diff_swap)
    from u1 u2 have u: "u1 - u2 \ U"
      by (rule vectorspace.diff_closed [OF U])
    with eq have v': "v2 - v1 \ U" by (simp only:)
    from v2 v1 have v: "v2 - v1 \ V"
      by (rule vectorspace.diff_closed [OF V])
    with eq have u': " u1 - u2 \ V" by (simp only:)

    show "u1 = u2"
    proof (rule add_minus_eq)
      from u1 show "u1 \ E" ..
      from u2 show "u2 \ E" ..
      from u u' and direct show "u1 - u2 = 0" by blast
    qed
    show "v1 = v2"
    proof (rule add_minus_eq [symmetric])
      from v1 show "v1 \ E" ..
      from v2 show "v2 \ E" ..
      from v v' and direct show "v2 - v1 = 0" by blast
    qed
  qed
qed

text \<open>
  An application of the previous lemma will be used in the proof of the
  Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any element
  \<open>y + a \<cdot> x\<^sub>0\<close> of the direct sum of a vectorspace \<open>H\<close> and the linear closure
  of \<open>x\<^sub>0\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are uniquely determined.
\<close>

lemma decomp_H':
  assumes "vectorspace E" "subspace H E"
  assumes y1: "y1 \ H" and y2: "y2 \ H"
    and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
    and eq: "y1 + a1 \ x' = y2 + a2 \ x'"
  shows "y1 = y2 \ a1 = a2"
proof -
  interpret vectorspace E by fact
  interpret subspace H E by fact
  show ?thesis
  proof
    have c: "y1 = y2 \ a1 \ x' = a2 \ x'"
    proof (rule decomp)
      show "a1 \ x' \ lin x'" ..
      show "a2 \ x' \ lin x'" ..
      show "H \ lin x' = {0}"
      proof
        show "H \ lin x' \ {0}"
        proof
          fix x assume x: "x \ H \ lin x'"
          then obtain a where xx': "x = a \ x'"
            by blast
          have "x = 0"
          proof (cases "a = 0")
            case True
            with xx' and x' show ?thesis by simp
          next
            case False
            from x have "x \ H" ..
            with xx' have "inverse a \ a \ x' \ H" by simp
            with False and x' have "x' \<in> H" by (simp add: mult_assoc2)
            with \<open>x' \<notin> H\<close> show ?thesis by contradiction
          qed
          then show "x \ {0}" ..
        qed
        show "{0} \ H \ lin x'"
        proof -
          have "0 \ H" using \vectorspace E\ ..
          moreover have "0 \ lin x'" using \x' \ E\ ..
          ultimately show ?thesis by blast
        qed
      qed
      show "lin x' \ E" using \x' \ E\ ..
    qed (rule \<open>vectorspace E\<close>, rule \<open>subspace H E\<close>, rule y1, rule y2, rule eq)
    then show "y1 = y2" ..
    from c have "a1 \ x' = a2 \ x'" ..
    with x' show "a1 = a2" by (simp add: mult_right_cancel)
  qed
qed

text \<open>
  Since for any element \<open>y + a \<cdot> x'\<close> of the direct sum of a vectorspace \<open>H\<close>
  and the linear closure of \<open>x'\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are unique, it
  follows from \<open>y \<in> H\<close> that \<open>a = 0\<close>.
\<close>

lemma decomp_H'_H:
  assumes "vectorspace E" "subspace H E"
  assumes t: "t \ H"
    and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
  shows "(SOME (y, a). t = y + a \ x' \ y \ H) = (t, 0)"
proof -
  interpret vectorspace E by fact
  interpret subspace H E by fact
  show ?thesis
  proof (rule, simp_all only: split_paired_all split_conv)
    from t x' show "t = t + 0 \ x' \ t \ H" by simp
    fix y and a assume ya: "t = y + a \ x' \ y \ H"
    have "y = t \ a = 0"
    proof (rule decomp_H')
      from ya x' show "y + a \ x' = t + 0 \ x'" by simp
      from ya show "y \ H" ..
    qed (rule \<open>vectorspace E\<close>, rule \<open>subspace H E\<close>, rule t, (rule x')+)
    with t x' show "(y, a) = (y + a \ x', 0)" by simp
  qed
qed

text \<open>
  The components \<open>y \<in> H\<close> and \<open>a\<close> in \<open>y + a \<cdot> x'\<close> are unique, so the function
  \<open>h'\<close> defined by \<open>h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>\<close> is definite.
\<close>

lemma h'_definite:
  fixes H
  assumes h'_def:
    "\x. h' x =
      (let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
       in (h y) + a * xi)"
    and x: "x = y + a \ x'"
  assumes "vectorspace E" "subspace H E"
  assumes y: "y \ H"
    and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
  shows "h' x = h y + a * xi"
proof -
  interpret vectorspace E by fact
  interpret subspace H E by fact
  from x y x' have "x \ H + lin x'" by auto
  have "\!(y, a). x = y + a \ x' \ y \ H" (is "\!p. ?P p")
  proof (rule ex_ex1I)
    from x y show "\p. ?P p" by blast
    fix p q assume p: "?P p" and q: "?P q"
    show "p = q"
    proof -
      from p have xp: "x = fst p + snd p \ x' \ fst p \ H"
        by (cases p) simp
      from q have xq: "x = fst q + snd q \ x' \ fst q \ H"
        by (cases q) simp
      have "fst p = fst q \ snd p = snd q"
      proof (rule decomp_H')
        from xp show "fst p \ H" ..
        from xq show "fst q \ H" ..
        from xp and xq show "fst p + snd p \ x' = fst q + snd q \ x'"
          by simp
      qed (rule \<open>vectorspace E\<close>, rule \<open>subspace H E\<close>, (rule x')+)
      then show ?thesis by (cases p, cases q) simp
    qed
  qed
  then have eq: "(SOME (y, a). x = y + a \ x' \ y \ H) = (y, a)"
    by (rule some1_equality) (simp add: x y)
  with h'_def show "h' x = h y + a * xi" by (simp add: Let_def)
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.13 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.