(* Title: HOL/Hahn_Banach/Subspace.thy Author: Gertrud Bauer, TU Munich *) section ‹Subspaces› theory Subspace imports Vector_Space "HOL-Library.Set_Algebras" begin subsection ‹Definition› text ‹ A non-empty subset ‹U› of a vector space ‹V› is a ∗‹subspace› of ‹V›, iff ‹U› is closed under addition and scalar multiplication. › 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 "⊴" 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 ‹ ┉ 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. › 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 ‹vectorspace V› x x have "… ∈ 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 ‹┉ Further derived laws: every subspace is a vector space.› 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 ‹The subspace relation is reflexive.› lemma (in vectorspace) subspace_refl [intro]: "V ⊴ V" proof show "V ≠ {}" .. show "V ⊆ V" .. next fix x y assume x: "x ∈ V" and y: "y ∈ V" fix a :: real from x y show "x + y ∈ V" by simp from x show "a ⋅ x ∈ V" by simp qed text ‹The subspace relation is transitive.› 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 ‹Linear closure› text ‹ The ∗‹linear closure› of a vector ‹x› is the set of all scalar multiples of ‹x›. › 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 ‹Every vector is contained in its linear closure.› 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 ‹Any linear closure is a subspace.› lemma (in vectorspace) lin_subspace [intro]: assumes x: "x ∈ V" shows "lin x ⊴ V" proof from x show "lin x ≠ {}" by auto next show "lin x ⊆ V" proof fix x' assume "x' ∈ lin x" then obtain a where "x' = a ⋅ x" .. with x show "x' ∈ V" by simp qed next 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 fix a :: real show "a ⋅ x' ∈ lin x" 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 ‹Any linear closure is a vector space.› lemma (in vectorspace) lin_vectorspace [intro]: assumes "x ∈ V" shows "vectorspace (lin x)" proof - from ‹x ∈ V› have "subspace (lin x) V" by (rule lin_subspace) from this and vectorspace_axioms show ?thesis by (rule subspace.vectorspace) qed subsection ‹Sum of two vectorspaces› text ‹ The ∗‹sum› of two vectorspaces ‹U› and ‹V› is the set of all sums of elements from ‹U› and ‹V›. › 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 ‹‹U› is a subspace of ‹U + V›.› 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 ‹The sum of two subspaces is again a subspace.› 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 next 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 fix a show "a ⋅ x ∈ U + V" 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 ‹The sum of two subspaces is a vectorspace.› lemma sum_vs [intro?]: "U ⊴ E ⟹ V ⊴ E ⟹ vectorspace E ⟹ vectorspace (U + V)" by (rule subspace.vectorspace) (rule sum_subspace) subsection ‹Direct sums› text ‹ The sum of ‹U› and ‹V› is called ∗‹direct›, iff the zero element is the only common element of ‹U› and ‹V›. For every element ‹x› of the direct sum of ‹U› and ‹V› the decomposition in ‹x = u + v› with ‹u ∈ U› and ‹v ∈ V› is unique. › 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 ‹subspace U E› ‹vectorspace E› by (rule subspace.vectorspace) have V: "vectorspace V" using ‹subspace V E› ‹vectorspace E› 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 ‹ 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 ‹y + a ⋅ x⇩_{0}› of the direct sum of a vectorspace ‹H› and the linear closure of ‹x⇩_{0}› the components ‹y ∈ H› and ‹a› are uniquely determined. › lemma decomp_H': assumes "vectorspace E" "subspace H E" assumes y1: "y1 ∈ H" and y2: "y2 ∈ H" and x': "x' ∉ H" "x' ∈ E" "x' ≠ 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 assume "a = 0" with xx' and x' show ?thesis by simp next assume a: "a ≠ 0" from x have "x ∈ H" .. with xx' have "inverse a ⋅ a ⋅ x' ∈ H" by simp with a and x' have "x' ∈ H" by (simp add: mult_assoc2) with ‹x' ∉ H› 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 ‹vectorspace E›, rule ‹subspace H E›, 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 ‹ Since for any element ‹y + a ⋅ x'› of the direct sum of a vectorspace ‹H› and the linear closure of ‹x'› the components ‹y ∈ H› and ‹a› are unique, it follows from ‹y ∈ H› that ‹a = 0›. › lemma decomp_H'_H: assumes "vectorspace E" "subspace H E" assumes t: "t ∈ H" and x': "x' ∉ H" "x' ∈ E" "x' ≠ 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 ‹vectorspace E›, rule ‹subspace H E›, rule t, (rule x')+) with t x' show "(y, a) = (y + a ⋅ x', 0)" by simp qed qed text ‹ The components ‹y ∈ H› and ‹a› in ‹y + a ⋅ x'› are unique, so the function ‹h'› defined by ‹h' (y + a ⋅ x') = h y + a ⋅ ξ› is definite. › lemma h'_definite: fixes H assumes h'_def: "⋀x. h' x = (let (y, a) = SOME (y, a). (x = y + a ⋅ x' ∧ y ∈ 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' ∉ H" "x' ∈ E" "x' ≠ 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 ‹vectorspace E›, rule ‹subspace H E›, (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