src/HOL/Multivariate_Analysis/Linear_Algebra.thy

 lemma subspace_sub: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
   using subspace_add [of S x "- y"] by (simp add: subspace_neg)
 
 lemma (in real_vector) subspace_setsum:
   assumes sA: "subspace A"
-    and f: "\<forall>x\<in>B. f x \<in> A"
+    and f: "\<And>x. x \<in> B \<Longrightarrow> f x \<in> A"
   shows "setsum f B \<in> A"
 proof (cases "finite B")
   case True
   then show ?thesis
     using f by induct (simp_all add: subspace_0 [OF sA] subspace_add [OF sA])
 qed (simp add: subspace_0 [OF sA])
 
-lemma subspace_trivial: "subspace {0}"
+lemma subspace_trivial [iff]: "subspace {0}"
   by (simp add: subspace_def)
 
 lemma (in real_vector) subspace_inter: "subspace A \<Longrightarrow> subspace B \<Longrightarrow> subspace (A \<inter> B)"
   by (simp add: subspace_def)
 
 lemma subspace_Times: "subspace A \<Longrightarrow> subspace B \<Longrightarrow> subspace (A \<times> B)"
   unfolding subspace_def zero_prod_def by simp
 
-text \<open>Properties of span.\<close>
+lemma subspace_sums: "\<lbrakk>subspace S; subspace T\<rbrakk> \<Longrightarrow> subspace {x + y|x y. x \<in> S \<and> y \<in> T}"
+apply (simp add: subspace_def)
+apply (intro conjI impI allI)
+  using add.right_neutral apply blast
+ apply clarify
+ apply (metis add.assoc add.left_commute)
+using scaleR_add_right by blast
+
+subsection \<open>Properties of span\<close>
 
 lemma (in real_vector) span_mono: "A \<subseteq> B \<Longrightarrow> span A \<subseteq> span B"
   by (metis span_def hull_mono)
 
 lemma (in real_vector) subspace_span: "subspace (span S)"

   unfolding span_def hull_hull ..
 
 lemma (in real_vector) span_superset: "x \<in> S \<Longrightarrow> x \<in> span S"
   by (metis span_clauses(1))
 
-lemma (in real_vector) span_0: "0 \<in> span S"
+lemma (in real_vector) span_0 [simp]: "0 \<in> span S"
   by (metis subspace_span subspace_0)
 
 lemma span_inc: "S \<subseteq> span S"
   by (metis subset_eq span_superset)
 

 lemma (in real_vector) dependent_0:
   assumes "0 \<in> A"
   shows "dependent A"
   unfolding dependent_def
   using assms span_0
-  by auto
+  by blast
 
 lemma (in real_vector) span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
   by (metis subspace_add subspace_span)
 
 lemma (in real_vector) span_mul: "x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S"

   by (metis subspace_neg subspace_span)
 
 lemma span_sub: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
   by (metis subspace_span subspace_sub)
 
-lemma (in real_vector) span_setsum: "\<forall>x\<in>A. f x \<in> span S \<Longrightarrow> setsum f A \<in> span S"
+lemma (in real_vector) span_setsum: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> span S) \<Longrightarrow> setsum f A \<in> span S"
   by (rule subspace_setsum [OF subspace_span])
 
 lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
   by (metis add_minus_cancel scaleR_minus1_left subspace_def subspace_span)
 

       apply (rule exI[where x= "?S"])
       apply (auto simp del: scaleR_minus_left)
       done
   }
   ultimately show ?thesis by blast
+qed
+
+lemma dependent_finite:
+  assumes "finite S"
+    shows "dependent S \<longleftrightarrow> (\<exists>u. (\<exists>v \<in> S. u v \<noteq> 0) \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = 0)"
+           (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then obtain T u v
+         where "finite T" "T \<subseteq> S" "v\<in>T" "u v \<noteq> 0" "(\<Sum>v\<in>T. u v *\<^sub>R v) = 0"
+    by (force simp: dependent_explicit)
+  with assms show ?rhs
+    apply (rule_tac x="\<lambda>v. if v \<in> T then u v else 0" in exI)
+    apply (auto simp: setsum.mono_neutral_right)
+    done
+next
+  assume ?rhs  with assms show ?lhs
+    by (fastforce simp add: dependent_explicit)
 qed
 
 lemma span_alt:
   "span B = {(\<Sum>x | f x \<noteq> 0. f x *\<^sub>R x) | f. {x. f x \<noteq> 0} \<subseteq> B \<and> finite {x. f x \<noteq> 0}}"
   unfolding span_explicit

   fixes S :: "'a::euclidean_space set"
   assumes "independent S"
   shows independent_imp_finite: "finite S" and independent_card_le:"card S \<le> DIM('a)"
 using assms independent_bound by auto
 
+lemma independent_explicit:
+  fixes B :: "'a::euclidean_space set"
+  shows "independent B \<longleftrightarrow>
+         finite B \<and> (\<forall>c. (\<Sum>v\<in>B. c v *\<^sub>R v) = 0 \<longrightarrow> (\<forall>v \<in> B. c v = 0))"
+apply (cases "finite B")
+ apply (force simp: dependent_finite)
+using independent_bound
+apply auto
+done
+
 lemma dependent_biggerset:
   fixes S :: "'a::euclidean_space set"
   shows "(finite S \<Longrightarrow> card S > DIM('a)) \<Longrightarrow> dependent S"
   by (metis independent_bound not_less)
 

     have "x - k *\<^sub>R (a - (\<Sum>x\<in>C. (x \<bullet> a / (x \<bullet> x)) *\<^sub>R x)) \<in> span C \<longleftrightarrow> x - k *\<^sub>R a \<in> span C"
       apply (simp only: scaleR_right_diff_distrib th0)
       apply (rule span_add_eq)
       apply (rule span_mul)
       apply (rule span_setsum)
-      apply clarify
       apply (rule span_mul)
       apply (rule span_superset)
       apply assumption
       done
   }

     by (simp add: span_span)
   let ?a = "a - setsum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B"
   have "setsum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B \<in> span S"
     unfolding sSB
     apply (rule span_setsum)
-    apply clarsimp
     apply (rule span_mul)
     apply (rule span_superset)
     apply assumption
     done
   with a have a0:"?a  \<noteq> 0"

   ultimately show ?thesis by blast
 qed
 
 lemma norm_cauchy_schwarz_equal: "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow> collinear {0, x, y}"
   unfolding norm_cauchy_schwarz_abs_eq
-  apply (cases "x=0", simp_all add: collinear_2)
-  apply (cases "y=0", simp_all add: collinear_2 insert_commute)
+  apply (cases "x=0", simp_all)
+  apply (cases "y=0", simp_all add: insert_commute)
   unfolding collinear_lemma
   apply simp
   apply (subgoal_tac "norm x \<noteq> 0")
   apply (subgoal_tac "norm y \<noteq> 0")
   apply (rule iffI)