# HG changeset patch # User hoelzl # Date 1461331126 -7200 # Node ID c968bce3921e5d8860f7a77a15296998ecaabe2c # Parent e5e69206d52d17da49e736500b47e2fce56f7732 Linear_Algebra: generalize linear_independent_extend to all real vector spaces diff -r e5e69206d52d -r c968bce3921e src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Apr 22 11:57:03 2016 +0200 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Apr 22 15:18:46 2016 +0200 @@ -886,6 +886,100 @@ ultimately show ?thesis by blast qed +lemma linear_independent_extend_subspace: + assumes "independent B" + shows "\g. linear g \ (\x\B. g x = f x) \ range g = span (f`B)" +proof - + from maximal_independent_subset_extend[OF _ \independent B\, of UNIV] + obtain B' where "B \ B'" "independent B'" "span B' = UNIV" + by (auto simp: top_unique) + have "\y. \X. {x. X x \ 0} \ B' \ finite {x. X x \ 0} \ y = (\x|X x \ 0. X x *\<^sub>R x)" + using \span B' = UNIV\ unfolding span_alt by auto + then obtain X where X: "\y. {x. X y x \ 0} \ B'" "\y. finite {x. X y x \ 0}" + "\y. y = (\x|X y x \ 0. X y x *\<^sub>R x)" + unfolding choice_iff by auto + + have X_add: "X (x + y) = (\z. X x z + X y z)" for x y + using \independent B'\ + proof (rule independentD_unique) + have "(\z | X x z + X y z \ 0. (X x z + X y z) *\<^sub>R z) + = (\z\{z. X x z \ 0} \ {z. X y z \ 0}. (X x z + X y z) *\<^sub>R z)" + by (intro setsum.mono_neutral_cong_left) (auto intro: X) + also have "\ = (\z\{z. X x z \ 0}. X x z *\<^sub>R z) + (\z\{z. X y z \ 0}. X y z *\<^sub>R z)" + by (auto simp add: scaleR_add_left setsum.distrib + intro!: arg_cong2[where f="op +"] setsum.mono_neutral_cong_right X) + also have "\ = x + y" + by (simp add: X(3)[symmetric]) + also have "\ = (\z | X (x + y) z \ 0. X (x + y) z *\<^sub>R z)" + by (rule X(3)) + finally show "(\z | X (x + y) z \ 0. X (x + y) z *\<^sub>R z) = (\z | X x z + X y z \ 0. (X x z + X y z) *\<^sub>R z)" + .. + have "{z. X x z + X y z \ 0} \ {z. X x z \ 0} \ {z. X y z \ 0}" + by auto + then show "finite {z. X x z + X y z \ 0}" "{xa. X x xa + X y xa \ 0} \ B'" + "finite {xa. X (x + y) xa \ 0}" "{xa. X (x + y) xa \ 0} \ B'" + using X(1) by (auto dest: finite_subset intro: X) + qed + + have X_cmult: "X (c *\<^sub>R x) = (\z. c * X x z)" for x c + using \independent B'\ + proof (rule independentD_unique) + show "finite {z. X (c *\<^sub>R x) z \ 0}" "{z. X (c *\<^sub>R x) z \ 0} \ B'" + "finite {z. c * X x z \ 0}" "{z. c * X x z \ 0} \ B' " + using X(1,2) by auto + show "(\z | X (c *\<^sub>R x) z \ 0. X (c *\<^sub>R x) z *\<^sub>R z) = (\z | c * X x z \ 0. (c * X x z) *\<^sub>R z)" + unfolding scaleR_scaleR[symmetric] scaleR_setsum_right[symmetric] + by (cases "c = 0") (auto simp: X(3)[symmetric]) + qed + + have X_B': "x \ B' \ X x = (\z. if z = x then 1 else 0)" for x + using \independent B'\ + by (rule independentD_unique[OF _ X(2) X(1)]) (auto intro: X simp: X(3)[symmetric]) + + def f' \ "\y. if y \ B then f y else 0" + def g \ "\y. \x|X y x \ 0. X y x *\<^sub>R f' x" + + have g_f': "x \ B' \ g x = f' x" for x + by (auto simp: g_def X_B') + + have "linear g" + proof + fix x y + have *: "(\z | X x z + X y z \ 0. (X x z + X y z) *\<^sub>R f' z) + = (\z\{z. X x z \ 0} \ {z. X y z \ 0}. (X x z + X y z) *\<^sub>R f' z)" + by (intro setsum.mono_neutral_cong_left) (auto intro: X) + show "g (x + y) = g x + g y" + unfolding g_def X_add * + by (auto simp add: scaleR_add_left setsum.distrib + intro!: arg_cong2[where f="op +"] setsum.mono_neutral_cong_right X) + next + show "g (r *\<^sub>R x) = r *\<^sub>R g x" for r x + by (auto simp add: g_def X_cmult scaleR_setsum_right intro!: setsum.mono_neutral_cong_left X) + qed + moreover have "\x\B. g x = f x" + using \B \ B'\ by (auto simp: g_f' f'_def) + moreover have "range g = span (f`B)" + unfolding \span B' = UNIV\[symmetric] span_linear_image[OF \linear g\, symmetric] + proof (rule span_subspace) + have "g ` B' \ f`B \ {0}" + by (auto simp: g_f' f'_def) + also have "\ \ span (f`B)" + by (auto intro: span_superset span_0) + finally show "g ` B' \ span (f`B)" + by auto + have "x \ B \ f x = g x" for x + using \B \ B'\ by (auto simp add: g_f' f'_def) + then show "span (f ` B) \ span (g ` B')" + using \B \ B'\ by (intro span_mono) auto + qed (rule subspace_span) + ultimately show ?thesis + by auto +qed + +lemma linear_independent_extend: + "independent B \ \g. linear g \ (\x\B. g x = f x)" + using linear_independent_extend_subspace[of B f] by auto + text \The degenerate case of the Exchange Lemma.\ lemma spanning_subset_independent: @@ -932,6 +1026,7 @@ and i: "independent s" and sp: "s \ span t" shows "\t'. card t' = card t \ finite t' \ s \ t' \ t' \ s \ t \ s \ span t'" + thm maximal_independent_subset_extend[OF _ i, of "s \ t"] using f i sp proof (induct "card (t - s)" arbitrary: s t rule: less_induct) case less @@ -2261,152 +2356,6 @@ from "2.hyps"(3)[OF fb ifb fib xsb "2.prems"(5)] show "x = 0" . qed -text \We can extend a linear mapping from basis.\ - -lemma linear_independent_extend_lemma: - fixes f :: "'a::real_vector \ 'b::real_vector" - assumes fi: "finite B" - and ib: "independent B" - shows "\g. - (\x\ span B. \y\ span B. g (x + y) = g x + g y) \ - (\x\ span B. \c. g (c*\<^sub>R x) = c *\<^sub>R g x) \ - (\x\ B. g x = f x)" - using ib fi -proof (induct rule: finite_induct[OF fi]) - case 1 - then show ?case by auto -next - case (2 a b) - from "2.prems" "2.hyps" have ibf: "independent b" "finite b" - by (simp_all add: independent_insert) - from "2.hyps"(3)[OF ibf] obtain g where - g: "\x\span b. \y\span b. g (x + y) = g x + g y" - "\x\span b. \c. g (c *\<^sub>R x) = c *\<^sub>R g x" "\x\b. g x = f x" by blast - let ?h = "\z. SOME k. (z - k *\<^sub>R a) \ span b" - { - fix z - assume z: "z \ span (insert a b)" - have th0: "z - ?h z *\<^sub>R a \ span b" - apply (rule someI_ex) - unfolding span_breakdown_eq[symmetric] - apply (rule z) - done - { - fix k - assume k: "z - k *\<^sub>R a \ span b" - have eq: "z - ?h z *\<^sub>R a - (z - k*\<^sub>R a) = (k - ?h z) *\<^sub>R a" - by (simp add: field_simps scaleR_left_distrib [symmetric]) - from span_sub[OF th0 k] have khz: "(k - ?h z) *\<^sub>R a \ span b" - by (simp add: eq) - { - assume "k \ ?h z" - then have k0: "k - ?h z \ 0" by simp - from k0 span_mul[OF khz, of "1 /(k - ?h z)"] - have "a \ span b" by simp - with "2.prems"(1) "2.hyps"(2) have False - by (auto simp add: dependent_def) - } - then have "k = ?h z" by blast - } - with th0 have "z - ?h z *\<^sub>R a \ span b \ (\k. z - k *\<^sub>R a \ span b \ k = ?h z)" - by blast - } - note h = this - let ?g = "\z. ?h z *\<^sub>R f a + g (z - ?h z *\<^sub>R a)" - { - fix x y - assume x: "x \ span (insert a b)" - and y: "y \ span (insert a b)" - have tha: "\(x::'a) y a k l. (x + y) - (k + l) *\<^sub>R a = (x - k *\<^sub>R a) + (y - l *\<^sub>R a)" - by (simp add: algebra_simps) - have addh: "?h (x + y) = ?h x + ?h y" - apply (rule conjunct2[OF h, rule_format, symmetric]) - apply (rule span_add[OF x y]) - unfolding tha - apply (metis span_add x y conjunct1[OF h, rule_format]) - done - have "?g (x + y) = ?g x + ?g y" - unfolding addh tha - g(1)[rule_format,OF conjunct1[OF h, OF x] conjunct1[OF h, OF y]] - by (simp add: scaleR_left_distrib)} - moreover - { - fix x :: "'a" - fix c :: real - assume x: "x \ span (insert a b)" - have tha: "\(x::'a) c k a. c *\<^sub>R x - (c * k) *\<^sub>R a = c *\<^sub>R (x - k *\<^sub>R a)" - by (simp add: algebra_simps) - have hc: "?h (c *\<^sub>R x) = c * ?h x" - apply (rule conjunct2[OF h, rule_format, symmetric]) - apply (metis span_mul x) - apply (metis tha span_mul x conjunct1[OF h]) - done - have "?g (c *\<^sub>R x) = c*\<^sub>R ?g x" - unfolding hc tha g(2)[rule_format, OF conjunct1[OF h, OF x]] - by (simp add: algebra_simps) - } - moreover - { - fix x - assume x: "x \ insert a b" - { - assume xa: "x = a" - have ha1: "1 = ?h a" - apply (rule conjunct2[OF h, rule_format]) - apply (metis span_superset insertI1) - using conjunct1[OF h, OF span_superset, OF insertI1] - apply (auto simp add: span_0) - done - from xa ha1[symmetric] have "?g x = f x" - apply simp - using g(2)[rule_format, OF span_0, of 0] - apply simp - done - } - moreover - { - assume xb: "x \ b" - have h0: "0 = ?h x" - apply (rule conjunct2[OF h, rule_format]) - apply (metis span_superset x) - apply simp - apply (metis span_superset xb) - done - have "?g x = f x" - by (simp add: h0[symmetric] g(3)[rule_format, OF xb]) - } - ultimately have "?g x = f x" - using x by blast - } - ultimately show ?case - apply - - apply (rule exI[where x="?g"]) - apply blast - done -qed - -lemma linear_independent_extend: - fixes B :: "'a::euclidean_space set" - assumes iB: "independent B" - shows "\g. linear g \ (\x\B. g x = f x)" -proof - - from maximal_independent_subset_extend[of B UNIV] iB - obtain C where C: "B \ C" "independent C" "\x. x \ span C" - by auto - - from C(2) independent_bound[of C] linear_independent_extend_lemma[of C f] - obtain g where g: - "(\x\ span C. \y\ span C. g (x + y) = g x + g y) \ - (\x\ span C. \c. g (c*\<^sub>R x) = c *\<^sub>R g x) \ - (\x\ C. g x = f x)" by blast - from g show ?thesis - unfolding linear_iff - using C - apply clarsimp - apply blast - done -qed - text \Can construct an isomorphism between spaces of same dimension.\ lemma subspace_isomorphism: @@ -2482,15 +2431,15 @@ assumes lf: "linear f" and SB: "S \ span B" and f0: "\x\B. f x = 0" - shows "\x \ S. f x = 0" + shows "\x\S. f x = 0" by (metis linear_eq_0_span[OF lf] subset_eq SB f0) lemma linear_eq: assumes lf: "linear f" and lg: "linear g" and S: "S \ span B" - and fg: "\ x\ B. f x = g x" - shows "\x\ S. f x = g x" + and fg: "\x\B. f x = g x" + shows "\x\S. f x = g x" proof - let ?h = "\x. f x - g x" from fg have fg': "\x\ B. ?h x = 0" by simp