author hoelzl Fri, 22 Apr 2016 15:18:46 +0200 changeset 63052 c968bce3921e parent 63051 e5e69206d52d child 63053 4a108f280dc2
Linear_Algebra: generalize linear_independent_extend to all real vector spaces
```--- 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 "\<exists>g. linear g \<and> (\<forall>x\<in>B. g x = f x) \<and> range g = span (f`B)"
+proof -
+  from maximal_independent_subset_extend[OF _ \<open>independent B\<close>, of UNIV]
+  obtain B' where "B \<subseteq> B'" "independent B'" "span B' = UNIV"
+    by (auto simp: top_unique)
+  have "\<forall>y. \<exists>X. {x. X x \<noteq> 0} \<subseteq> B' \<and> finite {x. X x \<noteq> 0} \<and> y = (\<Sum>x|X x \<noteq> 0. X x *\<^sub>R x)"
+    using \<open>span B' = UNIV\<close> unfolding span_alt by auto
+  then obtain X where X: "\<And>y. {x. X y x \<noteq> 0} \<subseteq> B'" "\<And>y. finite {x. X y x \<noteq> 0}"
+    "\<And>y. y = (\<Sum>x|X y x \<noteq> 0. X y x *\<^sub>R x)"
+    unfolding choice_iff by auto
+
+  have X_add: "X (x + y) = (\<lambda>z. X x z + X y z)" for x y
+    using \<open>independent B'\<close>
+  proof (rule independentD_unique)
+    have "(\<Sum>z | X x z + X y z \<noteq> 0. (X x z + X y z) *\<^sub>R z)
+      = (\<Sum>z\<in>{z. X x z \<noteq> 0} \<union> {z. X y z \<noteq> 0}. (X x z + X y z) *\<^sub>R z)"
+      by (intro setsum.mono_neutral_cong_left) (auto intro: X)
+    also have "\<dots> = (\<Sum>z\<in>{z. X x z \<noteq> 0}. X x z *\<^sub>R z) + (\<Sum>z\<in>{z. X y z \<noteq> 0}. X y z *\<^sub>R z)"
+               intro!: arg_cong2[where f="op +"]  setsum.mono_neutral_cong_right X)
+    also have "\<dots> = x + y"
+    also have "\<dots> = (\<Sum>z | X (x + y) z \<noteq> 0. X (x + y) z *\<^sub>R z)"
+      by (rule X(3))
+    finally show "(\<Sum>z | X (x + y) z \<noteq> 0. X (x + y) z *\<^sub>R z) = (\<Sum>z | X x z + X y z \<noteq> 0. (X x z + X y z) *\<^sub>R z)"
+      ..
+    have "{z. X x z + X y z \<noteq> 0} \<subseteq> {z. X x z \<noteq> 0} \<union> {z. X y z \<noteq> 0}"
+      by auto
+    then show "finite {z. X x z + X y z \<noteq> 0}" "{xa. X x xa + X y xa \<noteq> 0} \<subseteq> B'"
+        "finite {xa. X (x + y) xa \<noteq> 0}" "{xa. X (x + y) xa \<noteq> 0} \<subseteq> B'"
+      using X(1) by (auto dest: finite_subset intro: X)
+  qed
+
+  have X_cmult: "X (c *\<^sub>R x) = (\<lambda>z. c * X x z)" for x c
+    using \<open>independent B'\<close>
+  proof (rule independentD_unique)
+    show "finite {z. X (c *\<^sub>R x) z \<noteq> 0}" "{z. X (c *\<^sub>R x) z \<noteq> 0} \<subseteq> B'"
+      "finite {z. c * X x z \<noteq> 0}" "{z. c * X x z \<noteq> 0} \<subseteq> B' "
+      using X(1,2) by auto
+    show "(\<Sum>z | X (c *\<^sub>R x) z \<noteq> 0. X (c *\<^sub>R x) z *\<^sub>R z) = (\<Sum>z | c * X x z \<noteq> 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 \<in> B' \<Longrightarrow> X x = (\<lambda>z. if z = x then 1 else 0)" for x
+    using \<open>independent B'\<close>
+    by (rule independentD_unique[OF _ X(2) X(1)]) (auto intro: X simp: X(3)[symmetric])
+
+  def f' \<equiv> "\<lambda>y. if y \<in> B then f y else 0"
+  def g \<equiv> "\<lambda>y. \<Sum>x|X y x \<noteq> 0. X y x *\<^sub>R f' x"
+
+  have g_f': "x \<in> B' \<Longrightarrow> g x = f' x" for x
+    by (auto simp: g_def X_B')
+
+  have "linear g"
+  proof
+    fix x y
+    have *: "(\<Sum>z | X x z + X y z \<noteq> 0. (X x z + X y z) *\<^sub>R f' z)
+      = (\<Sum>z\<in>{z. X x z \<noteq> 0} \<union> {z. X y z \<noteq> 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"
+               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 "\<forall>x\<in>B. g x = f x"
+    using \<open>B \<subseteq> B'\<close> by (auto simp: g_f' f'_def)
+  moreover have "range g = span (f`B)"
+    unfolding \<open>span B' = UNIV\<close>[symmetric] span_linear_image[OF \<open>linear g\<close>, symmetric]
+  proof (rule span_subspace)
+    have "g ` B' \<subseteq> f`B \<union> {0}"
+      by (auto simp: g_f' f'_def)
+    also have "\<dots> \<subseteq> span (f`B)"
+      by (auto intro: span_superset span_0)
+    finally show "g ` B' \<subseteq> span (f`B)"
+      by auto
+    have "x \<in> B \<Longrightarrow> f x = g x" for x
+      using \<open>B \<subseteq> B'\<close> by (auto simp add: g_f' f'_def)
+    then show "span (f ` B) \<subseteq> span (g ` B')"
+      using \<open>B \<subseteq> B'\<close> by (intro span_mono) auto
+  qed (rule subspace_span)
+  ultimately show ?thesis
+    by auto
+qed
+
+lemma linear_independent_extend:
+  "independent B \<Longrightarrow> \<exists>g. linear g \<and> (\<forall>x\<in>B. g x = f x)"
+  using linear_independent_extend_subspace[of B f] by auto
+
text \<open>The degenerate case of the Exchange Lemma.\<close>

lemma spanning_subset_independent:
@@ -932,6 +1026,7 @@
and i: "independent s"
and sp: "s \<subseteq> span t"
shows "\<exists>t'. card t' = card t \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
+  thm maximal_independent_subset_extend[OF _ i, of "s \<union> 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 \<open>We can extend a linear mapping from basis.\<close>
-
-lemma linear_independent_extend_lemma:
-  fixes f :: "'a::real_vector \<Rightarrow> 'b::real_vector"
-  assumes fi: "finite B"
-    and ib: "independent B"
-  shows "\<exists>g.
-    (\<forall>x\<in> span B. \<forall>y\<in> span B. g (x + y) = g x + g y) \<and>
-    (\<forall>x\<in> span B. \<forall>c. g (c*\<^sub>R x) = c *\<^sub>R g x) \<and>
-    (\<forall>x\<in> 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"
-  from "2.hyps"(3)[OF ibf] obtain g where
-    g: "\<forall>x\<in>span b. \<forall>y\<in>span b. g (x + y) = g x + g y"
-    "\<forall>x\<in>span b. \<forall>c. g (c *\<^sub>R x) = c *\<^sub>R g x" "\<forall>x\<in>b. g x = f x" by blast
-  let ?h = "\<lambda>z. SOME k. (z - k *\<^sub>R a) \<in> span b"
-  {
-    fix z
-    assume z: "z \<in> span (insert a b)"
-    have th0: "z - ?h z *\<^sub>R a \<in> span b"
-      apply (rule someI_ex)
-      unfolding span_breakdown_eq[symmetric]
-      apply (rule z)
-      done
-    {
-      fix k
-      assume k: "z - k *\<^sub>R a \<in> 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 \<in> span b"
-      {
-        assume "k \<noteq> ?h z"
-        then have k0: "k - ?h z \<noteq> 0" by simp
-        from k0 span_mul[OF khz, of "1 /(k - ?h z)"]
-        have "a \<in> 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 \<in> span b \<and> (\<forall>k. z - k *\<^sub>R a \<in> span b \<longrightarrow> k = ?h z)"
-      by blast
-  }
-  note h = this
-  let ?g = "\<lambda>z. ?h z *\<^sub>R f a + g (z - ?h z *\<^sub>R a)"
-  {
-    fix x y
-    assume x: "x \<in> span (insert a b)"
-      and y: "y \<in> span (insert a b)"
-    have tha: "\<And>(x::'a) y a k l. (x + y) - (k + l) *\<^sub>R a = (x - k *\<^sub>R a) + (y - l *\<^sub>R a)"
-    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"
-      g(1)[rule_format,OF conjunct1[OF h, OF x] conjunct1[OF h, OF y]]
-  moreover
-  {
-    fix x :: "'a"
-    fix c :: real
-    assume x: "x \<in> span (insert a b)"
-    have tha: "\<And>(x::'a) c k a. c *\<^sub>R x - (c * k) *\<^sub>R a = c *\<^sub>R (x - k *\<^sub>R a)"
-    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]]
-  }
-  moreover
-  {
-    fix x
-    assume x: "x \<in> 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 \<in> 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 "\<exists>g. linear g \<and> (\<forall>x\<in>B. g x = f x)"
-proof -
-  from maximal_independent_subset_extend[of B UNIV] iB
-  obtain C where C: "B \<subseteq> C" "independent C" "\<And>x. x \<in> span C"
-    by auto
-
-  from C(2) independent_bound[of C] linear_independent_extend_lemma[of C f]
-  obtain g where g:
-    "(\<forall>x\<in> span C. \<forall>y\<in> span C. g (x + y) = g x + g y) \<and>
-     (\<forall>x\<in> span C. \<forall>c. g (c*\<^sub>R x) = c *\<^sub>R g x) \<and>
-     (\<forall>x\<in> C. g x = f x)" by blast
-  from g show ?thesis
-    unfolding linear_iff
-    using C
-    apply clarsimp
-    apply blast
-    done
-qed
-
text \<open>Can construct an isomorphism between spaces of same dimension.\<close>

lemma subspace_isomorphism:
@@ -2482,15 +2431,15 @@
assumes lf: "linear f"
and SB: "S \<subseteq> span B"
and f0: "\<forall>x\<in>B. f x = 0"
-  shows "\<forall>x \<in> S. f x = 0"
+  shows "\<forall>x\<in>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 \<subseteq> span B"
-    and fg: "\<forall> x\<in> B. f x = g x"
-  shows "\<forall>x\<in> S. f x = g x"
+    and fg: "\<forall>x\<in>B. f x = g x"
+  shows "\<forall>x\<in>S. f x = g x"
proof -
let ?h = "\<lambda>x. f x - g x"
from fg have fg': "\<forall>x\<in> B. ?h x = 0" by simp```