src/HOL/HahnBanach/Subspace.thy
 author ballarin Tue Dec 30 11:10:01 2008 +0100 (2008-12-30) changeset 29252 ea97aa6aeba2 parent 29234 src/HOL/Real/HahnBanach/Subspace.thy@60f7fb56f8cd parent 29197 src/HOL/Real/HahnBanach/Subspace.thy@6d4cb27ed19c child 30729 461ee3e49ad3 permissions -rw-r--r--
Merged.
     1 (*  Title:      HOL/Real/HahnBanach/Subspace.thy

     2     Author:     Gertrud Bauer, TU Munich

     3 *)

     4

     5 header {* Subspaces *}

     6

     7 theory Subspace

     8 imports VectorSpace

     9 begin

    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 =

    20   fixes U :: "'a\<Colon>{minus, plus, zero, uminus} set" and V

    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   assumes "vectorspace V"

    45   assumes x: "x \<in> U" and y: "y \<in> U"

    46   shows "x - y \<in> U"

    47 proof -

    48   interpret vectorspace V by fact

    49   from x y show ?thesis by (simp add: diff_eq1 negate_eq1)

    50 qed

    51

    52 text {*

    53   \medskip Similar as for linear spaces, the existence of the zero

    54   element in every subspace follows from the non-emptiness of the

    55   carrier set and by vector space laws.

    56 *}

    57

    58 lemma (in subspace) zero [intro]:

    59   assumes "vectorspace V"

    60   shows "0 \<in> U"

    61 proof -

    62   interpret V!: vectorspace V by fact

    63   have "U \<noteq> {}" by (rule non_empty)

    64   then obtain x where x: "x \<in> U" by blast

    65   then have "x \<in> V" .. then have "0 = x - x" by simp

    66   also from vectorspace V x x have "\<dots> \<in> U" by (rule diff_closed)

    67   finally show ?thesis .

    68 qed

    69

    70 lemma (in subspace) neg_closed [iff]:

    71   assumes "vectorspace V"

    72   assumes x: "x \<in> U"

    73   shows "- x \<in> U"

    74 proof -

    75   interpret vectorspace V by fact

    76   from x show ?thesis by (simp add: negate_eq1)

    77 qed

    78

    79 text {* \medskip Further derived laws: every subspace is a vector space. *}

    80

    81 lemma (in subspace) vectorspace [iff]:

    82   assumes "vectorspace V"

    83   shows "vectorspace U"

    84 proof -

    85   interpret vectorspace V by fact

    86   show ?thesis

    87   proof

    88     show "U \<noteq> {}" ..

    89     fix x y z assume x: "x \<in> U" and y: "y \<in> U" and z: "z \<in> U"

    90     fix a b :: real

    91     from x y show "x + y \<in> U" by simp

    92     from x show "a \<cdot> x \<in> U" by simp

    93     from x y z show "(x + y) + z = x + (y + z)" by (simp add: add_ac)

    94     from x y show "x + y = y + x" by (simp add: add_ac)

    95     from x show "x - x = 0" by simp

    96     from x show "0 + x = x" by simp

    97     from x y show "a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y" by (simp add: distrib)

    98     from x show "(a + b) \<cdot> x = a \<cdot> x + b \<cdot> x" by (simp add: distrib)

    99     from x show "(a * b) \<cdot> x = a \<cdot> b \<cdot> x" by (simp add: mult_assoc)

   100     from x show "1 \<cdot> x = x" by simp

   101     from x show "- x = - 1 \<cdot> x" by (simp add: negate_eq1)

   102     from x y show "x - y = x + - y" by (simp add: diff_eq1)

   103   qed

   104 qed

   105

   106

   107 text {* The subspace relation is reflexive. *}

   108

   109 lemma (in vectorspace) subspace_refl [intro]: "V \<unlhd> V"

   110 proof

   111   show "V \<noteq> {}" ..

   112   show "V \<subseteq> V" ..

   113   fix x y assume x: "x \<in> V" and y: "y \<in> V"

   114   fix a :: real

   115   from x y show "x + y \<in> V" by simp

   116   from x show "a \<cdot> x \<in> V" by simp

   117 qed

   118

   119 text {* The subspace relation is transitive. *}

   120

   121 lemma (in vectorspace) subspace_trans [trans]:

   122   "U \<unlhd> V \<Longrightarrow> V \<unlhd> W \<Longrightarrow> U \<unlhd> W"

   123 proof

   124   assume uv: "U \<unlhd> V" and vw: "V \<unlhd> W"

   125   from uv show "U \<noteq> {}" by (rule subspace.non_empty)

   126   show "U \<subseteq> W"

   127   proof -

   128     from uv have "U \<subseteq> V" by (rule subspace.subset)

   129     also from vw have "V \<subseteq> W" by (rule subspace.subset)

   130     finally show ?thesis .

   131   qed

   132   fix x y assume x: "x \<in> U" and y: "y \<in> U"

   133   from uv and x y show "x + y \<in> U" by (rule subspace.add_closed)

   134   from uv and x show "\<And>a. a \<cdot> x \<in> U" by (rule subspace.mult_closed)

   135 qed

   136

   137

   138 subsection {* Linear closure *}

   139

   140 text {*

   141   The \emph{linear closure} of a vector @{text x} is the set of all

   142   scalar multiples of @{text x}.

   143 *}

   144

   145 definition

   146   lin :: "('a::{minus, plus, zero}) \<Rightarrow> 'a set" where

   147   "lin x = {a \<cdot> x | a. True}"

   148

   149 lemma linI [intro]: "y = a \<cdot> x \<Longrightarrow> y \<in> lin x"

   150   unfolding lin_def by blast

   151

   152 lemma linI' [iff]: "a \<cdot> x \<in> lin x"

   153   unfolding lin_def by blast

   154

   155 lemma linE [elim]: "x \<in> lin v \<Longrightarrow> (\<And>a::real. x = a \<cdot> v \<Longrightarrow> C) \<Longrightarrow> C"

   156   unfolding lin_def by blast

   157

   158

   159 text {* Every vector is contained in its linear closure. *}

   160

   161 lemma (in vectorspace) x_lin_x [iff]: "x \<in> V \<Longrightarrow> x \<in> lin x"

   162 proof -

   163   assume "x \<in> V"

   164   then have "x = 1 \<cdot> x" by simp

   165   also have "\<dots> \<in> lin x" ..

   166   finally show ?thesis .

   167 qed

   168

   169 lemma (in vectorspace) "0_lin_x" [iff]: "x \<in> V \<Longrightarrow> 0 \<in> lin x"

   170 proof

   171   assume "x \<in> V"

   172   then show "0 = 0 \<cdot> x" by simp

   173 qed

   174

   175 text {* Any linear closure is a subspace. *}

   176

   177 lemma (in vectorspace) lin_subspace [intro]:

   178   "x \<in> V \<Longrightarrow> lin x \<unlhd> V"

   179 proof

   180   assume x: "x \<in> V"

   181   then show "lin x \<noteq> {}" by (auto simp add: x_lin_x)

   182   show "lin x \<subseteq> V"

   183   proof

   184     fix x' assume "x' \<in> lin x"

   185     then obtain a where "x' = a \<cdot> x" ..

   186     with x show "x' \<in> V" by simp

   187   qed

   188   fix x' x'' assume x': "x' \<in> lin x" and x'': "x'' \<in> lin x"

   189   show "x' + x'' \<in> lin x"

   190   proof -

   191     from x' obtain a' where "x' = a' \<cdot> x" ..

   192     moreover from x'' obtain a'' where "x'' = a'' \<cdot> x" ..

   193     ultimately have "x' + x'' = (a' + a'') \<cdot> x"

   194       using x by (simp add: distrib)

   195     also have "\<dots> \<in> lin x" ..

   196     finally show ?thesis .

   197   qed

   198   fix a :: real

   199   show "a \<cdot> x' \<in> lin x"

   200   proof -

   201     from x' obtain a' where "x' = a' \<cdot> x" ..

   202     with x have "a \<cdot> x' = (a * a') \<cdot> x" by (simp add: mult_assoc)

   203     also have "\<dots> \<in> lin x" ..

   204     finally show ?thesis .

   205   qed

   206 qed

   207

   208

   209 text {* Any linear closure is a vector space. *}

   210

   211 lemma (in vectorspace) lin_vectorspace [intro]:

   212   assumes "x \<in> V"

   213   shows "vectorspace (lin x)"

   214 proof -

   215   from x \<in> V have "subspace (lin x) V"

   216     by (rule lin_subspace)

   217   from this and vectorspace_axioms show ?thesis

   218     by (rule subspace.vectorspace)

   219 qed

   220

   221

   222 subsection {* Sum of two vectorspaces *}

   223

   224 text {*

   225   The \emph{sum} of two vectorspaces @{text U} and @{text V} is the

   226   set of all sums of elements from @{text U} and @{text V}.

   227 *}

   228

   229 instantiation "fun" :: (type, type) plus

   230 begin

   231

   232 definition

   233   sum_def: "plus_fun U V = {u + v | u v. u \<in> U \<and> v \<in> V}"  (* FIXME not fully general!? *)

   234

   235 instance ..

   236

   237 end

   238

   239 lemma sumE [elim]:

   240     "x \<in> U + V \<Longrightarrow> (\<And>u v. x = u + v \<Longrightarrow> u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> C) \<Longrightarrow> C"

   241   unfolding sum_def by blast

   242

   243 lemma sumI [intro]:

   244     "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> x = u + v \<Longrightarrow> x \<in> U + V"

   245   unfolding sum_def by blast

   246

   247 lemma sumI' [intro]:

   248     "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V"

   249   unfolding sum_def by blast

   250

   251 text {* @{text U} is a subspace of @{text "U + V"}. *}

   252

   253 lemma subspace_sum1 [iff]:

   254   assumes "vectorspace U" "vectorspace V"

   255   shows "U \<unlhd> U + V"

   256 proof -

   257   interpret vectorspace U by fact

   258   interpret vectorspace V by fact

   259   show ?thesis

   260   proof

   261     show "U \<noteq> {}" ..

   262     show "U \<subseteq> U + V"

   263     proof

   264       fix x assume x: "x \<in> U"

   265       moreover have "0 \<in> V" ..

   266       ultimately have "x + 0 \<in> U + V" ..

   267       with x show "x \<in> U + V" by simp

   268     qed

   269     fix x y assume x: "x \<in> U" and "y \<in> U"

   270     then show "x + y \<in> U" by simp

   271     from x show "\<And>a. a \<cdot> x \<in> U" by simp

   272   qed

   273 qed

   274

   275 text {* The sum of two subspaces is again a subspace. *}

   276

   277 lemma sum_subspace [intro?]:

   278   assumes "subspace U E" "vectorspace E" "subspace V E"

   279   shows "U + V \<unlhd> E"

   280 proof -

   281   interpret subspace U E by fact

   282   interpret vectorspace E by fact

   283   interpret subspace V E by fact

   284   show ?thesis

   285   proof

   286     have "0 \<in> U + V"

   287     proof

   288       show "0 \<in> U" using vectorspace E ..

   289       show "0 \<in> V" using vectorspace E ..

   290       show "(0::'a) = 0 + 0" by simp

   291     qed

   292     then show "U + V \<noteq> {}" by blast

   293     show "U + V \<subseteq> E"

   294     proof

   295       fix x assume "x \<in> U + V"

   296       then obtain u v where "x = u + v" and

   297 	"u \<in> U" and "v \<in> V" ..

   298       then show "x \<in> E" by simp

   299     qed

   300     fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V"

   301     show "x + y \<in> U + V"

   302     proof -

   303       from x obtain ux vx where "x = ux + vx" and "ux \<in> U" and "vx \<in> V" ..

   304       moreover

   305       from y obtain uy vy where "y = uy + vy" and "uy \<in> U" and "vy \<in> V" ..

   306       ultimately

   307       have "ux + uy \<in> U"

   308 	and "vx + vy \<in> V"

   309 	and "x + y = (ux + uy) + (vx + vy)"

   310 	using x y by (simp_all add: add_ac)

   311       then show ?thesis ..

   312     qed

   313     fix a show "a \<cdot> x \<in> U + V"

   314     proof -

   315       from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" ..

   316       then have "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V"

   317 	and "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" by (simp_all add: distrib)

   318       then show ?thesis ..

   319     qed

   320   qed

   321 qed

   322

   323 text{* The sum of two subspaces is a vectorspace. *}

   324

   325 lemma sum_vs [intro?]:

   326     "U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U + V)"

   327   by (rule subspace.vectorspace) (rule sum_subspace)

   328

   329

   330 subsection {* Direct sums *}

   331

   332 text {*

   333   The sum of @{text U} and @{text V} is called \emph{direct}, iff the

   334   zero element is the only common element of @{text U} and @{text

   335   V}. For every element @{text x} of the direct sum of @{text U} and

   336   @{text V} the decomposition in @{text "x = u + v"} with

   337   @{text "u \<in> U"} and @{text "v \<in> V"} is unique.

   338 *}

   339

   340 lemma decomp:

   341   assumes "vectorspace E" "subspace U E" "subspace V E"

   342   assumes direct: "U \<inter> V = {0}"

   343     and u1: "u1 \<in> U" and u2: "u2 \<in> U"

   344     and v1: "v1 \<in> V" and v2: "v2 \<in> V"

   345     and sum: "u1 + v1 = u2 + v2"

   346   shows "u1 = u2 \<and> v1 = v2"

   347 proof -

   348   interpret vectorspace E by fact

   349   interpret subspace U E by fact

   350   interpret subspace V E by fact

   351   show ?thesis

   352   proof

   353     have U: "vectorspace U"  (* FIXME: use interpret *)

   354       using subspace U E vectorspace E by (rule subspace.vectorspace)

   355     have V: "vectorspace V"

   356       using subspace V E vectorspace E by (rule subspace.vectorspace)

   357     from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1"

   358       by (simp add: add_diff_swap)

   359     from u1 u2 have u: "u1 - u2 \<in> U"

   360       by (rule vectorspace.diff_closed [OF U])

   361     with eq have v': "v2 - v1 \<in> U" by (simp only:)

   362     from v2 v1 have v: "v2 - v1 \<in> V"

   363       by (rule vectorspace.diff_closed [OF V])

   364     with eq have u': " u1 - u2 \<in> V" by (simp only:)

   365

   366     show "u1 = u2"

   367     proof (rule add_minus_eq)

   368       from u1 show "u1 \<in> E" ..

   369       from u2 show "u2 \<in> E" ..

   370       from u u' and direct show "u1 - u2 = 0" by blast

   371     qed

   372     show "v1 = v2"

   373     proof (rule add_minus_eq [symmetric])

   374       from v1 show "v1 \<in> E" ..

   375       from v2 show "v2 \<in> E" ..

   376       from v v' and direct show "v2 - v1 = 0" by blast

   377     qed

   378   qed

   379 qed

   380

   381 text {*

   382   An application of the previous lemma will be used in the proof of

   383   the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any

   384   element @{text "y + a \<cdot> x\<^sub>0"} of the direct sum of a

   385   vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"}

   386   the components @{text "y \<in> H"} and @{text a} are uniquely

   387   determined.

   388 *}

   389

   390 lemma decomp_H':

   391   assumes "vectorspace E" "subspace H E"

   392   assumes y1: "y1 \<in> H" and y2: "y2 \<in> H"

   393     and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"

   394     and eq: "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"

   395   shows "y1 = y2 \<and> a1 = a2"

   396 proof -

   397   interpret vectorspace E by fact

   398   interpret subspace H E by fact

   399   show ?thesis

   400   proof

   401     have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"

   402     proof (rule decomp)

   403       show "a1 \<cdot> x' \<in> lin x'" ..

   404       show "a2 \<cdot> x' \<in> lin x'" ..

   405       show "H \<inter> lin x' = {0}"

   406       proof

   407 	show "H \<inter> lin x' \<subseteq> {0}"

   408 	proof

   409           fix x assume x: "x \<in> H \<inter> lin x'"

   410           then obtain a where xx': "x = a \<cdot> x'"

   411             by blast

   412           have "x = 0"

   413           proof cases

   414             assume "a = 0"

   415             with xx' and x' show ?thesis by simp

   416           next

   417             assume a: "a \<noteq> 0"

   418             from x have "x \<in> H" ..

   419             with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp

   420             with a and x' have "x' \<in> H" by (simp add: mult_assoc2)

   421             with x' \<notin> H show ?thesis by contradiction

   422           qed

   423           then show "x \<in> {0}" ..

   424 	qed

   425 	show "{0} \<subseteq> H \<inter> lin x'"

   426 	proof -

   427           have "0 \<in> H" using vectorspace E ..

   428           moreover have "0 \<in> lin x'" using x' \<in> E ..

   429           ultimately show ?thesis by blast

   430 	qed

   431       qed

   432       show "lin x' \<unlhd> E" using x' \<in> E ..

   433     qed (rule vectorspace E, rule subspace H E, rule y1, rule y2, rule eq)

   434     then show "y1 = y2" ..

   435     from c have "a1 \<cdot> x' = a2 \<cdot> x'" ..

   436     with x' show "a1 = a2" by (simp add: mult_right_cancel)

   437   qed

   438 qed

   439

   440 text {*

   441   Since for any element @{text "y + a \<cdot> x'"} of the direct sum of a

   442   vectorspace @{text H} and the linear closure of @{text x'} the

   443   components @{text "y \<in> H"} and @{text a} are unique, it follows from

   444   @{text "y \<in> H"} that @{text "a = 0"}.

   445 *}

   446

   447 lemma decomp_H'_H:

   448   assumes "vectorspace E" "subspace H E"

   449   assumes t: "t \<in> H"

   450     and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"

   451   shows "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"

   452 proof -

   453   interpret vectorspace E by fact

   454   interpret subspace H E by fact

   455   show ?thesis

   456   proof (rule, simp_all only: split_paired_all split_conv)

   457     from t x' show "t = t + 0 \<cdot> x' \<and> t \<in> H" by simp

   458     fix y and a assume ya: "t = y + a \<cdot> x' \<and> y \<in> H"

   459     have "y = t \<and> a = 0"

   460     proof (rule decomp_H')

   461       from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp

   462       from ya show "y \<in> H" ..

   463     qed (rule vectorspace E, rule subspace H E, rule t, (rule x')+)

   464     with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp

   465   qed

   466 qed

   467

   468 text {*

   469   The components @{text "y \<in> H"} and @{text a} in @{text "y + a \<cdot> x'"}

   470   are unique, so the function @{text h'} defined by

   471   @{text "h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>"} is definite.

   472 *}

   473

   474 lemma h'_definite:

   475   fixes H

   476   assumes h'_def:

   477     "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)

   478                 in (h y) + a * xi)"

   479     and x: "x = y + a \<cdot> x'"

   480   assumes "vectorspace E" "subspace H E"

   481   assumes y: "y \<in> H"

   482     and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"

   483   shows "h' x = h y + a * xi"

   484 proof -

   485   interpret vectorspace E by fact

   486   interpret subspace H E by fact

   487   from x y x' have "x \<in> H + lin x'" by auto

   488   have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p")

   489   proof (rule ex_ex1I)

   490     from x y show "\<exists>p. ?P p" by blast

   491     fix p q assume p: "?P p" and q: "?P q"

   492     show "p = q"

   493     proof -

   494       from p have xp: "x = fst p + snd p \<cdot> x' \<and> fst p \<in> H"

   495         by (cases p) simp

   496       from q have xq: "x = fst q + snd q \<cdot> x' \<and> fst q \<in> H"

   497         by (cases q) simp

   498       have "fst p = fst q \<and> snd p = snd q"

   499       proof (rule decomp_H')

   500         from xp show "fst p \<in> H" ..

   501         from xq show "fst q \<in> H" ..

   502         from xp and xq show "fst p + snd p \<cdot> x' = fst q + snd q \<cdot> x'"

   503           by simp

   504       qed (rule vectorspace E, rule subspace H E, (rule x')+)

   505       then show ?thesis by (cases p, cases q) simp

   506     qed

   507   qed

   508   then have eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)"

   509     by (rule some1_equality) (simp add: x y)

   510   with h'_def show "h' x = h y + a * xi" by (simp add: Let_def)

   511 qed

   512

   513 end