src/HOL/Real/HahnBanach/Subspace.thy
author haftmann
Wed Jan 02 15:14:02 2008 +0100 (2008-01-02)
changeset 25762 c03e9d04b3e4
parent 23378 1d138d6bb461
child 26199 04817a8802f2
permissions -rw-r--r--
splitted class uminus from class minus
     1 (*  Title:      HOL/Real/HahnBanach/Subspace.thy
     2     ID:         $Id$
     3     Author:     Gertrud Bauer, TU Munich
     4 *)
     5 
     6 header {* Subspaces *}
     7 
     8 theory Subspace imports VectorSpace begin
     9 
    10 
    11 subsection {* Definition *}
    12 
    13 text {*
    14   A non-empty subset @{text U} of a vector space @{text V} is a
    15   \emph{subspace} of @{text V}, iff @{text U} is closed under addition
    16   and scalar multiplication.
    17 *}
    18 
    19 locale subspace = var U + var V +
    20   constrains U :: "'a\<Colon>{minus, plus, zero, uminus} set"
    21   assumes non_empty [iff, intro]: "U \<noteq> {}"
    22     and subset [iff]: "U \<subseteq> V"
    23     and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
    24     and mult_closed [iff]: "x \<in> U \<Longrightarrow> a \<cdot> x \<in> U"
    25 
    26 notation (symbols)
    27   subspace  (infix "\<unlhd>" 50)
    28 
    29 declare vectorspace.intro [intro?] subspace.intro [intro?]
    30 
    31 lemma subspace_subset [elim]: "U \<unlhd> V \<Longrightarrow> U \<subseteq> V"
    32   by (rule subspace.subset)
    33 
    34 lemma (in subspace) subsetD [iff]: "x \<in> U \<Longrightarrow> x \<in> V"
    35   using subset by blast
    36 
    37 lemma subspaceD [elim]: "U \<unlhd> V \<Longrightarrow> x \<in> U \<Longrightarrow> x \<in> V"
    38   by (rule subspace.subsetD)
    39 
    40 lemma rev_subspaceD [elim?]: "x \<in> U \<Longrightarrow> U \<unlhd> V \<Longrightarrow> x \<in> V"
    41   by (rule subspace.subsetD)
    42 
    43 lemma (in subspace) diff_closed [iff]:
    44   includes vectorspace
    45   shows "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x - y \<in> U"
    46   by (simp add: diff_eq1 negate_eq1)
    47 
    48 
    49 text {*
    50   \medskip Similar as for linear spaces, the existence of the zero
    51   element in every subspace follows from the non-emptiness of the
    52   carrier set and by vector space laws.
    53 *}
    54 
    55 lemma (in subspace) zero [intro]:
    56   includes vectorspace
    57   shows "0 \<in> U"
    58 proof -
    59   have "U \<noteq> {}" by (rule U_V.non_empty)
    60   then obtain x where x: "x \<in> U" by blast
    61   hence "x \<in> V" .. hence "0 = x - x" by simp
    62   also from `vectorspace V` x x have "... \<in> U" by (rule U_V.diff_closed)
    63   finally show ?thesis .
    64 qed
    65 
    66 lemma (in subspace) neg_closed [iff]:
    67   includes vectorspace
    68   shows "x \<in> U \<Longrightarrow> - x \<in> U"
    69   by (simp add: negate_eq1)
    70 
    71 
    72 text {* \medskip Further derived laws: every subspace is a vector space. *}
    73 
    74 lemma (in subspace) vectorspace [iff]:
    75   includes vectorspace
    76   shows "vectorspace U"
    77 proof
    78   show "U \<noteq> {}" ..
    79   fix x y z assume x: "x \<in> U" and y: "y \<in> U" and z: "z \<in> U"
    80   fix a b :: real
    81   from x y show "x + y \<in> U" by simp
    82   from x show "a \<cdot> x \<in> U" by simp
    83   from x y z show "(x + y) + z = x + (y + z)" by (simp add: add_ac)
    84   from x y show "x + y = y + x" by (simp add: add_ac)
    85   from x show "x - x = 0" by simp
    86   from x show "0 + x = x" by simp
    87   from x y show "a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y" by (simp add: distrib)
    88   from x show "(a + b) \<cdot> x = a \<cdot> x + b \<cdot> x" by (simp add: distrib)
    89   from x show "(a * b) \<cdot> x = a \<cdot> b \<cdot> x" by (simp add: mult_assoc)
    90   from x show "1 \<cdot> x = x" by simp
    91   from x show "- x = - 1 \<cdot> x" by (simp add: negate_eq1)
    92   from x y show "x - y = x + - y" by (simp add: diff_eq1)
    93 qed
    94 
    95 
    96 text {* The subspace relation is reflexive. *}
    97 
    98 lemma (in vectorspace) subspace_refl [intro]: "V \<unlhd> V"
    99 proof
   100   show "V \<noteq> {}" ..
   101   show "V \<subseteq> V" ..
   102   fix x y assume x: "x \<in> V" and y: "y \<in> V"
   103   fix a :: real
   104   from x y show "x + y \<in> V" by simp
   105   from x show "a \<cdot> x \<in> V" by simp
   106 qed
   107 
   108 text {* The subspace relation is transitive. *}
   109 
   110 lemma (in vectorspace) subspace_trans [trans]:
   111   "U \<unlhd> V \<Longrightarrow> V \<unlhd> W \<Longrightarrow> U \<unlhd> W"
   112 proof
   113   assume uv: "U \<unlhd> V" and vw: "V \<unlhd> W"
   114   from uv show "U \<noteq> {}" by (rule subspace.non_empty)
   115   show "U \<subseteq> W"
   116   proof -
   117     from uv have "U \<subseteq> V" by (rule subspace.subset)
   118     also from vw have "V \<subseteq> W" by (rule subspace.subset)
   119     finally show ?thesis .
   120   qed
   121   fix x y assume x: "x \<in> U" and y: "y \<in> U"
   122   from uv and x y show "x + y \<in> U" by (rule subspace.add_closed)
   123   from uv and x show "\<And>a. a \<cdot> x \<in> U" by (rule subspace.mult_closed)
   124 qed
   125 
   126 
   127 subsection {* Linear closure *}
   128 
   129 text {*
   130   The \emph{linear closure} of a vector @{text x} is the set of all
   131   scalar multiples of @{text x}.
   132 *}
   133 
   134 definition
   135   lin :: "('a::{minus, plus, zero}) \<Rightarrow> 'a set" where
   136   "lin x = {a \<cdot> x | a. True}"
   137 
   138 lemma linI [intro]: "y = a \<cdot> x \<Longrightarrow> y \<in> lin x"
   139   by (unfold lin_def) blast
   140 
   141 lemma linI' [iff]: "a \<cdot> x \<in> lin x"
   142   by (unfold lin_def) blast
   143 
   144 lemma linE [elim]:
   145     "x \<in> lin v \<Longrightarrow> (\<And>a::real. x = a \<cdot> v \<Longrightarrow> C) \<Longrightarrow> C"
   146   by (unfold lin_def) blast
   147 
   148 
   149 text {* Every vector is contained in its linear closure. *}
   150 
   151 lemma (in vectorspace) x_lin_x [iff]: "x \<in> V \<Longrightarrow> x \<in> lin x"
   152 proof -
   153   assume "x \<in> V"
   154   hence "x = 1 \<cdot> x" by simp
   155   also have "\<dots> \<in> lin x" ..
   156   finally show ?thesis .
   157 qed
   158 
   159 lemma (in vectorspace) "0_lin_x" [iff]: "x \<in> V \<Longrightarrow> 0 \<in> lin x"
   160 proof
   161   assume "x \<in> V"
   162   thus "0 = 0 \<cdot> x" by simp
   163 qed
   164 
   165 text {* Any linear closure is a subspace. *}
   166 
   167 lemma (in vectorspace) lin_subspace [intro]:
   168   "x \<in> V \<Longrightarrow> lin x \<unlhd> V"
   169 proof
   170   assume x: "x \<in> V"
   171   thus "lin x \<noteq> {}" by (auto simp add: x_lin_x)
   172   show "lin x \<subseteq> V"
   173   proof
   174     fix x' assume "x' \<in> lin x"
   175     then obtain a where "x' = a \<cdot> x" ..
   176     with x show "x' \<in> V" by simp
   177   qed
   178   fix x' x'' assume x': "x' \<in> lin x" and x'': "x'' \<in> lin x"
   179   show "x' + x'' \<in> lin x"
   180   proof -
   181     from x' obtain a' where "x' = a' \<cdot> x" ..
   182     moreover from x'' obtain a'' where "x'' = a'' \<cdot> x" ..
   183     ultimately have "x' + x'' = (a' + a'') \<cdot> x"
   184       using x by (simp add: distrib)
   185     also have "\<dots> \<in> lin x" ..
   186     finally show ?thesis .
   187   qed
   188   fix a :: real
   189   show "a \<cdot> x' \<in> lin x"
   190   proof -
   191     from x' obtain a' where "x' = a' \<cdot> x" ..
   192     with x have "a \<cdot> x' = (a * a') \<cdot> x" by (simp add: mult_assoc)
   193     also have "\<dots> \<in> lin x" ..
   194     finally show ?thesis .
   195   qed
   196 qed
   197 
   198 
   199 text {* Any linear closure is a vector space. *}
   200 
   201 lemma (in vectorspace) lin_vectorspace [intro]:
   202   assumes "x \<in> V"
   203   shows "vectorspace (lin x)"
   204 proof -
   205   from `x \<in> V` have "subspace (lin x) V"
   206     by (rule lin_subspace)
   207   from this and `vectorspace V` show ?thesis
   208     by (rule subspace.vectorspace)
   209 qed
   210 
   211 
   212 subsection {* Sum of two vectorspaces *}
   213 
   214 text {*
   215   The \emph{sum} of two vectorspaces @{text U} and @{text V} is the
   216   set of all sums of elements from @{text U} and @{text V}.
   217 *}
   218 
   219 instance set :: (plus) plus ..
   220 
   221 defs (overloaded)
   222   sum_def: "U + V \<equiv> {u + v | u v. u \<in> U \<and> v \<in> V}"
   223 
   224 lemma sumE [elim]:
   225     "x \<in> U + V \<Longrightarrow> (\<And>u v. x = u + v \<Longrightarrow> u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> C) \<Longrightarrow> C"
   226   by (unfold sum_def) blast
   227 
   228 lemma sumI [intro]:
   229     "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> x = u + v \<Longrightarrow> x \<in> U + V"
   230   by (unfold sum_def) blast
   231 
   232 lemma sumI' [intro]:
   233     "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V"
   234   by (unfold sum_def) blast
   235 
   236 text {* @{text U} is a subspace of @{text "U + V"}. *}
   237 
   238 lemma subspace_sum1 [iff]:
   239   includes vectorspace U + vectorspace V
   240   shows "U \<unlhd> U + V"
   241 proof
   242   show "U \<noteq> {}" ..
   243   show "U \<subseteq> U + V"
   244   proof
   245     fix x assume x: "x \<in> U"
   246     moreover have "0 \<in> V" ..
   247     ultimately have "x + 0 \<in> U + V" ..
   248     with x show "x \<in> U + V" by simp
   249   qed
   250   fix x y assume x: "x \<in> U" and "y \<in> U"
   251   thus "x + y \<in> U" by simp
   252   from x show "\<And>a. a \<cdot> x \<in> U" by simp
   253 qed
   254 
   255 text {* The sum of two subspaces is again a subspace. *}
   256 
   257 lemma sum_subspace [intro?]:
   258   includes subspace U E + vectorspace E + subspace V E
   259   shows "U + V \<unlhd> E"
   260 proof
   261   have "0 \<in> U + V"
   262   proof
   263     show "0 \<in> U" using `vectorspace E` ..
   264     show "0 \<in> V" using `vectorspace E` ..
   265     show "(0::'a) = 0 + 0" by simp
   266   qed
   267   thus "U + V \<noteq> {}" by blast
   268   show "U + V \<subseteq> E"
   269   proof
   270     fix x assume "x \<in> U + V"
   271     then obtain u v where "x = u + v" and
   272       "u \<in> U" and "v \<in> V" ..
   273     then show "x \<in> E" by simp
   274   qed
   275   fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V"
   276   show "x + y \<in> U + V"
   277   proof -
   278     from x obtain ux vx where "x = ux + vx" and "ux \<in> U" and "vx \<in> V" ..
   279     moreover
   280     from y obtain uy vy where "y = uy + vy" and "uy \<in> U" and "vy \<in> V" ..
   281     ultimately
   282     have "ux + uy \<in> U"
   283       and "vx + vy \<in> V"
   284       and "x + y = (ux + uy) + (vx + vy)"
   285       using x y by (simp_all add: add_ac)
   286     thus ?thesis ..
   287   qed
   288   fix a show "a \<cdot> x \<in> U + V"
   289   proof -
   290     from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" ..
   291     hence "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V"
   292       and "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" by (simp_all add: distrib)
   293     thus ?thesis ..
   294   qed
   295 qed
   296 
   297 text{* The sum of two subspaces is a vectorspace. *}
   298 
   299 lemma sum_vs [intro?]:
   300     "U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U + V)"
   301   by (rule subspace.vectorspace) (rule sum_subspace)
   302 
   303 
   304 subsection {* Direct sums *}
   305 
   306 text {*
   307   The sum of @{text U} and @{text V} is called \emph{direct}, iff the
   308   zero element is the only common element of @{text U} and @{text
   309   V}. For every element @{text x} of the direct sum of @{text U} and
   310   @{text V} the decomposition in @{text "x = u + v"} with
   311   @{text "u \<in> U"} and @{text "v \<in> V"} is unique.
   312 *}
   313 
   314 lemma decomp:
   315   includes vectorspace E + subspace U E + subspace V E
   316   assumes direct: "U \<inter> V = {0}"
   317     and u1: "u1 \<in> U" and u2: "u2 \<in> U"
   318     and v1: "v1 \<in> V" and v2: "v2 \<in> V"
   319     and sum: "u1 + v1 = u2 + v2"
   320   shows "u1 = u2 \<and> v1 = v2"
   321 proof
   322   have U: "vectorspace U"
   323     using `subspace U E` `vectorspace E` by (rule subspace.vectorspace)
   324   have V: "vectorspace V"
   325     using `subspace V E` `vectorspace E` by (rule subspace.vectorspace)
   326   from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1"
   327     by (simp add: add_diff_swap)
   328   from u1 u2 have u: "u1 - u2 \<in> U"
   329     by (rule vectorspace.diff_closed [OF U])
   330   with eq have v': "v2 - v1 \<in> U" by (simp only:)
   331   from v2 v1 have v: "v2 - v1 \<in> V"
   332     by (rule vectorspace.diff_closed [OF V])
   333   with eq have u': " u1 - u2 \<in> V" by (simp only:)
   334 
   335   show "u1 = u2"
   336   proof (rule add_minus_eq)
   337     from u1 show "u1 \<in> E" ..
   338     from u2 show "u2 \<in> E" ..
   339     from u u' and direct show "u1 - u2 = 0" by blast
   340   qed
   341   show "v1 = v2"
   342   proof (rule add_minus_eq [symmetric])
   343     from v1 show "v1 \<in> E" ..
   344     from v2 show "v2 \<in> E" ..
   345     from v v' and direct show "v2 - v1 = 0" by blast
   346   qed
   347 qed
   348 
   349 text {*
   350   An application of the previous lemma will be used in the proof of
   351   the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any
   352   element @{text "y + a \<cdot> x\<^sub>0"} of the direct sum of a
   353   vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"}
   354   the components @{text "y \<in> H"} and @{text a} are uniquely
   355   determined.
   356 *}
   357 
   358 lemma decomp_H':
   359   includes vectorspace E + subspace H E
   360   assumes y1: "y1 \<in> H" and y2: "y2 \<in> H"
   361     and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
   362     and eq: "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
   363   shows "y1 = y2 \<and> a1 = a2"
   364 proof
   365   have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
   366   proof (rule decomp)
   367     show "a1 \<cdot> x' \<in> lin x'" ..
   368     show "a2 \<cdot> x' \<in> lin x'" ..
   369     show "H \<inter> lin x' = {0}"
   370     proof
   371       show "H \<inter> lin x' \<subseteq> {0}"
   372       proof
   373         fix x assume x: "x \<in> H \<inter> lin x'"
   374         then obtain a where xx': "x = a \<cdot> x'"
   375           by blast
   376         have "x = 0"
   377         proof cases
   378           assume "a = 0"
   379           with xx' and x' show ?thesis by simp
   380         next
   381           assume a: "a \<noteq> 0"
   382           from x have "x \<in> H" ..
   383           with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp
   384           with a and x' have "x' \<in> H" by (simp add: mult_assoc2)
   385           with `x' \<notin> H` show ?thesis by contradiction
   386         qed
   387         thus "x \<in> {0}" ..
   388       qed
   389       show "{0} \<subseteq> H \<inter> lin x'"
   390       proof -
   391         have "0 \<in> H" using `vectorspace E` ..
   392         moreover have "0 \<in> lin x'" using `x' \<in> E` ..
   393         ultimately show ?thesis by blast
   394       qed
   395     qed
   396     show "lin x' \<unlhd> E" using `x' \<in> E` ..
   397   qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq)
   398   thus "y1 = y2" ..
   399   from c have "a1 \<cdot> x' = a2 \<cdot> x'" ..
   400   with x' show "a1 = a2" by (simp add: mult_right_cancel)
   401 qed
   402 
   403 text {*
   404   Since for any element @{text "y + a \<cdot> x'"} of the direct sum of a
   405   vectorspace @{text H} and the linear closure of @{text x'} the
   406   components @{text "y \<in> H"} and @{text a} are unique, it follows from
   407   @{text "y \<in> H"} that @{text "a = 0"}.
   408 *}
   409 
   410 lemma decomp_H'_H:
   411   includes vectorspace E + subspace H E
   412   assumes t: "t \<in> H"
   413     and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
   414   shows "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
   415 proof (rule, simp_all only: split_paired_all split_conv)
   416   from t x' show "t = t + 0 \<cdot> x' \<and> t \<in> H" by simp
   417   fix y and a assume ya: "t = y + a \<cdot> x' \<and> y \<in> H"
   418   have "y = t \<and> a = 0"
   419   proof (rule decomp_H')
   420     from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp
   421     from ya show "y \<in> H" ..
   422   qed (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+)
   423   with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp
   424 qed
   425 
   426 text {*
   427   The components @{text "y \<in> H"} and @{text a} in @{text "y + a \<cdot> x'"}
   428   are unique, so the function @{text h'} defined by
   429   @{text "h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>"} is definite.
   430 *}
   431 
   432 lemma h'_definite:
   433   includes var H
   434   assumes h'_def:
   435     "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
   436                 in (h y) + a * xi)"
   437     and x: "x = y + a \<cdot> x'"
   438   includes vectorspace E + subspace H E
   439   assumes y: "y \<in> H"
   440     and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
   441   shows "h' x = h y + a * xi"
   442 proof -
   443   from x y x' have "x \<in> H + lin x'" by auto
   444   have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p")
   445   proof (rule ex_ex1I)
   446     from x y show "\<exists>p. ?P p" by blast
   447     fix p q assume p: "?P p" and q: "?P q"
   448     show "p = q"
   449     proof -
   450       from p have xp: "x = fst p + snd p \<cdot> x' \<and> fst p \<in> H"
   451         by (cases p) simp
   452       from q have xq: "x = fst q + snd q \<cdot> x' \<and> fst q \<in> H"
   453         by (cases q) simp
   454       have "fst p = fst q \<and> snd p = snd q"
   455       proof (rule decomp_H')
   456         from xp show "fst p \<in> H" ..
   457         from xq show "fst q \<in> H" ..
   458         from xp and xq show "fst p + snd p \<cdot> x' = fst q + snd q \<cdot> x'"
   459           by simp
   460       qed (rule `vectorspace E`, rule `subspace H E`, (rule x')+)
   461       thus ?thesis by (cases p, cases q) simp
   462     qed
   463   qed
   464   hence eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)"
   465     by (rule some1_equality) (simp add: x y)
   466   with h'_def show "h' x = h y + a * xi" by (simp add: Let_def)
   467 qed
   468 
   469 end