# HG changeset patch
# User wenzelm
# Date 1461704365 -7200
# Node ID 60406bf310f8e9598bb08638d941a97036f5ecf3
# Parent  4a108f280dc25e292927fd32086b4d8b913f824d# Parent  21ebc2f5c571d9a2086ccdbb27af4cfb067cd778
merged

diff -r 21ebc2f5c571 -r 60406bf310f8 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Apr 26 22:59:03 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -10,194 +10,71 @@
   "~~/src/HOL/Library/Infinite_Set"
 begin
 
-lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
-  by auto
-
-notation inner (infix "\<bullet>" 70)
-
-lemma square_bound_lemma:
-  fixes x :: real
-  shows "x < (1 + x) * (1 + x)"
-proof -
-  have "(x + 1/2)\<^sup>2 + 3/4 > 0"
-    using zero_le_power2[of "x+1/2"] by arith
-  then show ?thesis
-    by (simp add: field_simps power2_eq_square)
-qed
-
-lemma square_continuous:
-  fixes e :: real
-  shows "e > 0 \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> \<bar>y * y - x * x\<bar> < e)"
-  using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
-  by (force simp add: power2_eq_square)
-
-text\<open>Hence derive more interesting properties of the norm.\<close>
-
-lemma norm_eq_0_dot: "norm x = 0 \<longleftrightarrow> x \<bullet> x = (0::real)"
-  by simp (* TODO: delete *)
-
-lemma norm_triangle_sub:
-  fixes x y :: "'a::real_normed_vector"
-  shows "norm x \<le> norm y + norm (x - y)"
-  using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
-
-lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> x \<bullet> x \<le> y \<bullet> y"
-  by (simp add: norm_eq_sqrt_inner)
-
-lemma norm_lt: "norm x < norm y \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
-  by (simp add: norm_eq_sqrt_inner)
-
-lemma norm_eq: "norm x = norm y \<longleftrightarrow> x \<bullet> x = y \<bullet> y"
-  apply (subst order_eq_iff)
-  apply (auto simp: norm_le)
-  done
-
-lemma norm_eq_1: "norm x = 1 \<longleftrightarrow> x \<bullet> x = 1"
-  by (simp add: norm_eq_sqrt_inner)
-
-text\<open>Squaring equations and inequalities involving norms.\<close>
-
-lemma dot_square_norm: "x \<bullet> x = (norm x)\<^sup>2"
-  by (simp only: power2_norm_eq_inner) (* TODO: move? *)
-
-lemma norm_eq_square: "norm x = a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x = a\<^sup>2"
-  by (auto simp add: norm_eq_sqrt_inner)
-
-lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x \<le> a\<^sup>2"
-  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
-  using norm_ge_zero[of x]
-  apply arith
-  done
-
-lemma norm_ge_square: "norm x \<ge> a \<longleftrightarrow> a \<le> 0 \<or> x \<bullet> x \<ge> a\<^sup>2"
-  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
-  using norm_ge_zero[of x]
-  apply arith
+subsection \<open>A generic notion of "hull" (convex, affine, conic hull and closure).\<close>
+
+definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
+  where "S hull s = \<Inter>{t. S t \<and> s \<subseteq> t}"
+
+lemma hull_same: "S s \<Longrightarrow> S hull s = s"
+  unfolding hull_def by auto
+
+lemma hull_in: "(\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)) \<Longrightarrow> S (S hull s)"
+  unfolding hull_def Ball_def by auto
+
+lemma hull_eq: "(\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)) \<Longrightarrow> (S hull s) = s \<longleftrightarrow> S s"
+  using hull_same[of S s] hull_in[of S s] by metis
+
+lemma hull_hull [simp]: "S hull (S hull s) = S hull s"
+  unfolding hull_def by blast
+
+lemma hull_subset[intro]: "s \<subseteq> (S hull s)"
+  unfolding hull_def by blast
+
+lemma hull_mono: "s \<subseteq> t \<Longrightarrow> (S hull s) \<subseteq> (S hull t)"
+  unfolding hull_def by blast
+
+lemma hull_antimono: "\<forall>x. S x \<longrightarrow> T x \<Longrightarrow> (T hull s) \<subseteq> (S hull s)"
+  unfolding hull_def by blast
+
+lemma hull_minimal: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (S hull s) \<subseteq> t"
+  unfolding hull_def by blast
+
+lemma subset_hull: "S t \<Longrightarrow> S hull s \<subseteq> t \<longleftrightarrow> s \<subseteq> t"
+  unfolding hull_def by blast
+
+lemma hull_UNIV [simp]: "S hull UNIV = UNIV"
+  unfolding hull_def by auto
+
+lemma hull_unique: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> S t' \<Longrightarrow> t \<subseteq> t') \<Longrightarrow> (S hull s = t)"
+  unfolding hull_def by auto
+
+lemma hull_induct: "(\<And>x. x\<in> S \<Longrightarrow> P x) \<Longrightarrow> Q {x. P x} \<Longrightarrow> \<forall>x\<in> Q hull S. P x"
+  using hull_minimal[of S "{x. P x}" Q]
+  by (auto simp add: subset_eq)
+
+lemma hull_inc: "x \<in> S \<Longrightarrow> x \<in> P hull S"
+  by (metis hull_subset subset_eq)
+
+lemma hull_union_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))"
+  unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2)
+
+lemma hull_union:
+  assumes T: "\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)"
+  shows "S hull (s \<union> t) = S hull (S hull s \<union> S hull t)"
+  apply rule
+  apply (rule hull_mono)
+  unfolding Un_subset_iff
+  apply (metis hull_subset Un_upper1 Un_upper2 subset_trans)
+  apply (rule hull_minimal)
+  apply (metis hull_union_subset)
+  apply (metis hull_in T)
   done
 
-lemma norm_lt_square: "norm x < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a\<^sup>2"
-  by (metis not_le norm_ge_square)
-
-lemma norm_gt_square: "norm x > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a\<^sup>2"
-  by (metis norm_le_square not_less)
-
-text\<open>Dot product in terms of the norm rather than conversely.\<close>
-
-lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left
-  inner_scaleR_left inner_scaleR_right
-
-lemma dot_norm: "x \<bullet> y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
-  unfolding power2_norm_eq_inner inner_simps inner_commute by auto
-
-lemma dot_norm_neg: "x \<bullet> y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
-  unfolding power2_norm_eq_inner inner_simps inner_commute
-  by (auto simp add: algebra_simps)
-
-text\<open>Equality of vectors in terms of @{term "op \<bullet>"} products.\<close>
-
-lemma vector_eq: "x = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y \<and> y \<bullet> y = x \<bullet> x"
-  (is "?lhs \<longleftrightarrow> ?rhs")
-proof
-  assume ?lhs
-  then show ?rhs by simp
-next
-  assume ?rhs
-  then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y \<bullet> y = 0"
-    by simp
-  then have "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0"
-    by (simp add: inner_diff inner_commute)
-  then have "(x - y) \<bullet> (x - y) = 0"
-    by (simp add: field_simps inner_diff inner_commute)
-  then show "x = y" by simp
-qed
-
-lemma norm_triangle_half_r:
-  "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
-  using dist_triangle_half_r unfolding dist_norm[symmetric] by auto
-
-lemma norm_triangle_half_l:
-  assumes "norm (x - y) < e / 2"
-    and "norm (x' - y) < e / 2"
-  shows "norm (x - x') < e"
-  using dist_triangle_half_l[OF assms[unfolded dist_norm[symmetric]]]
-  unfolding dist_norm[symmetric] .
-
-lemma norm_triangle_le: "norm x + norm y \<le> e \<Longrightarrow> norm (x + y) \<le> e"
-  by (rule norm_triangle_ineq [THEN order_trans])
-
-lemma norm_triangle_lt: "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
-  by (rule norm_triangle_ineq [THEN le_less_trans])
-
-lemma setsum_clauses:
-  shows "setsum f {} = 0"
-    and "finite S \<Longrightarrow> setsum f (insert x S) = (if x \<in> S then setsum f S else f x + setsum f S)"
-  by (auto simp add: insert_absorb)
-
-lemma setsum_norm_le:
-  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
-  assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
-  shows "norm (setsum f S) \<le> setsum g S"
-  by (rule order_trans [OF norm_setsum setsum_mono]) (simp add: fg)
-
-lemma setsum_norm_bound:
-  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
-  assumes K: "\<forall>x \<in> S. norm (f x) \<le> K"
-  shows "norm (setsum f S) \<le> of_nat (card S) * K"
-  using setsum_norm_le[OF K] setsum_constant[symmetric]
-  by simp
-
-lemma setsum_group:
-  assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
-  shows "setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) T = setsum g S"
-  apply (subst setsum_image_gen[OF fS, of g f])
-  apply (rule setsum.mono_neutral_right[OF fT fST])
-  apply (auto intro: setsum.neutral)
-  done
-
-lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
-proof
-  assume "\<forall>x. x \<bullet> y = x \<bullet> z"
-  then have "\<forall>x. x \<bullet> (y - z) = 0"
-    by (simp add: inner_diff)
-  then have "(y - z) \<bullet> (y - z) = 0" ..
-  then show "y = z" by simp
-qed simp
-
-lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = y"
-proof
-  assume "\<forall>z. x \<bullet> z = y \<bullet> z"
-  then have "\<forall>z. (x - y) \<bullet> z = 0"
-    by (simp add: inner_diff)
-  then have "(x - y) \<bullet> (x - y) = 0" ..
-  then show "x = y" by simp
-qed simp
-
-
-subsection \<open>Orthogonality.\<close>
-
-context real_inner
-begin
-
-definition "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
-
-lemma orthogonal_clauses:
-  "orthogonal a 0"
-  "orthogonal a x \<Longrightarrow> orthogonal a (c *\<^sub>R x)"
-  "orthogonal a x \<Longrightarrow> orthogonal a (- x)"
-  "orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x + y)"
-  "orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x - y)"
-  "orthogonal 0 a"
-  "orthogonal x a \<Longrightarrow> orthogonal (c *\<^sub>R x) a"
-  "orthogonal x a \<Longrightarrow> orthogonal (- x) a"
-  "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"
-  "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x - y) a"
-  unfolding orthogonal_def inner_add inner_diff by auto
-
-end
-
-lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
-  by (simp add: orthogonal_def inner_commute)
-
+lemma hull_redundant_eq: "a \<in> (S hull s) \<longleftrightarrow> S hull (insert a s) = S hull s"
+  unfolding hull_def by blast
+
+lemma hull_redundant: "a \<in> (S hull s) \<Longrightarrow> S hull (insert a s) = S hull s"
+  by (metis hull_redundant_eq)
 
 subsection \<open>Linear functions.\<close>
 
@@ -317,365 +194,7 @@
   shows "f (a *\<^sub>R x + b *\<^sub>R y) = a *\<^sub>R f x +  b *\<^sub>R f y"
   using linear_add[of f] linear_cmul[of f] assms by simp
 
-lemma linear_componentwise:
-  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
-  assumes lf: "linear f"
-  shows "(f x) \<bullet> j = (\<Sum>i\<in>Basis. (x\<bullet>i) * (f i\<bullet>j))" (is "?lhs = ?rhs")
-proof -
-  have "?rhs = (\<Sum>i\<in>Basis. (x\<bullet>i) *\<^sub>R (f i))\<bullet>j"
-    by (simp add: inner_setsum_left)
-  then show ?thesis
-    unfolding linear_setsum_mul[OF lf, symmetric]
-    unfolding euclidean_representation ..
-qed
-
-
-subsection \<open>Bilinear functions.\<close>
-
-definition "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
-
-lemma bilinear_ladd: "bilinear h \<Longrightarrow> h (x + y) z = h x z + h y z"
-  by (simp add: bilinear_def linear_iff)
-
-lemma bilinear_radd: "bilinear h \<Longrightarrow> h x (y + z) = h x y + h x z"
-  by (simp add: bilinear_def linear_iff)
-
-lemma bilinear_lmul: "bilinear h \<Longrightarrow> h (c *\<^sub>R x) y = c *\<^sub>R h x y"
-  by (simp add: bilinear_def linear_iff)
-
-lemma bilinear_rmul: "bilinear h \<Longrightarrow> h x (c *\<^sub>R y) = c *\<^sub>R h x y"
-  by (simp add: bilinear_def linear_iff)
-
-lemma bilinear_lneg: "bilinear h \<Longrightarrow> h (- x) y = - h x y"
-  by (drule bilinear_lmul [of _ "- 1"]) simp
-
-lemma bilinear_rneg: "bilinear h \<Longrightarrow> h x (- y) = - h x y"
-  by (drule bilinear_rmul [of _ _ "- 1"]) simp
-
-lemma (in ab_group_add) eq_add_iff: "x = x + y \<longleftrightarrow> y = 0"
-  using add_left_imp_eq[of x y 0] by auto
-
-lemma bilinear_lzero:
-  assumes "bilinear h"
-  shows "h 0 x = 0"
-  using bilinear_ladd [OF assms, of 0 0 x] by (simp add: eq_add_iff field_simps)
-
-lemma bilinear_rzero:
-  assumes "bilinear h"
-  shows "h x 0 = 0"
-  using bilinear_radd [OF assms, of x 0 0 ] by (simp add: eq_add_iff field_simps)
-
-lemma bilinear_lsub: "bilinear h \<Longrightarrow> h (x - y) z = h x z - h y z"
-  using bilinear_ladd [of h x "- y"] by (simp add: bilinear_lneg)
-
-lemma bilinear_rsub: "bilinear h \<Longrightarrow> h z (x - y) = h z x - h z y"
-  using bilinear_radd [of h _ x "- y"] by (simp add: bilinear_rneg)
-
-lemma bilinear_setsum:
-  assumes bh: "bilinear h"
-    and fS: "finite S"
-    and fT: "finite T"
-  shows "h (setsum f S) (setsum g T) = setsum (\<lambda>(i,j). h (f i) (g j)) (S \<times> T) "
-proof -
-  have "h (setsum f S) (setsum g T) = setsum (\<lambda>x. h (f x) (setsum g T)) S"
-    apply (rule linear_setsum[unfolded o_def])
-    using bh fS
-    apply (auto simp add: bilinear_def)
-    done
-  also have "\<dots> = setsum (\<lambda>x. setsum (\<lambda>y. h (f x) (g y)) T) S"
-    apply (rule setsum.cong, simp)
-    apply (rule linear_setsum[unfolded o_def])
-    using bh fT
-    apply (auto simp add: bilinear_def)
-    done
-  finally show ?thesis
-    unfolding setsum.cartesian_product .
-qed
-
-
-subsection \<open>Adjoints.\<close>
-
-definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
-
-lemma adjoint_unique:
-  assumes "\<forall>x y. inner (f x) y = inner x (g y)"
-  shows "adjoint f = g"
-  unfolding adjoint_def
-proof (rule some_equality)
-  show "\<forall>x y. inner (f x) y = inner x (g y)"
-    by (rule assms)
-next
-  fix h
-  assume "\<forall>x y. inner (f x) y = inner x (h y)"
-  then have "\<forall>x y. inner x (g y) = inner x (h y)"
-    using assms by simp
-  then have "\<forall>x y. inner x (g y - h y) = 0"
-    by (simp add: inner_diff_right)
-  then have "\<forall>y. inner (g y - h y) (g y - h y) = 0"
-    by simp
-  then have "\<forall>y. h y = g y"
-    by simp
-  then show "h = g" by (simp add: ext)
-qed
-
-text \<open>TODO: The following lemmas about adjoints should hold for any
-Hilbert space (i.e. complete inner product space).
-(see @{url "http://en.wikipedia.org/wiki/Hermitian_adjoint"})
-\<close>
-
-lemma adjoint_works:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes lf: "linear f"
-  shows "x \<bullet> adjoint f y = f x \<bullet> y"
-proof -
-  have "\<forall>y. \<exists>w. \<forall>x. f x \<bullet> y = x \<bullet> w"
-  proof (intro allI exI)
-    fix y :: "'m" and x
-    let ?w = "(\<Sum>i\<in>Basis. (f i \<bullet> y) *\<^sub>R i) :: 'n"
-    have "f x \<bullet> y = f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i) \<bullet> y"
-      by (simp add: euclidean_representation)
-    also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<bullet> y"
-      unfolding linear_setsum[OF lf]
-      by (simp add: linear_cmul[OF lf])
-    finally show "f x \<bullet> y = x \<bullet> ?w"
-      by (simp add: inner_setsum_left inner_setsum_right mult.commute)
-  qed
-  then show ?thesis
-    unfolding adjoint_def choice_iff
-    by (intro someI2_ex[where Q="\<lambda>f'. x \<bullet> f' y = f x \<bullet> y"]) auto
-qed
-
-lemma adjoint_clauses:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes lf: "linear f"
-  shows "x \<bullet> adjoint f y = f x \<bullet> y"
-    and "adjoint f y \<bullet> x = y \<bullet> f x"
-  by (simp_all add: adjoint_works[OF lf] inner_commute)
-
-lemma adjoint_linear:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes lf: "linear f"
-  shows "linear (adjoint f)"
-  by (simp add: lf linear_iff euclidean_eq_iff[where 'a='n] euclidean_eq_iff[where 'a='m]
-    adjoint_clauses[OF lf] inner_distrib)
-
-lemma adjoint_adjoint:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes lf: "linear f"
-  shows "adjoint (adjoint f) = f"
-  by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])
-
-
-subsection \<open>Interlude: Some properties of real sets\<close>
-
-lemma seq_mono_lemma:
-  assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n"
-    and "\<forall>n \<ge> m. e n \<le> e m"
-  shows "\<forall>n \<ge> m. d n < e m"
-  using assms
-  apply auto
-  apply (erule_tac x="n" in allE)
-  apply (erule_tac x="n" in allE)
-  apply auto
-  done
-
-lemma infinite_enumerate:
-  assumes fS: "infinite S"
-  shows "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> S)"
-  unfolding subseq_def
-  using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto
-
-lemma approachable_lt_le: "(\<exists>(d::real) > 0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)"
-  apply auto
-  apply (rule_tac x="d/2" in exI)
-  apply auto
-  done
-
-lemma approachable_lt_le2:  \<comment>\<open>like the above, but pushes aside an extra formula\<close>
-    "(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
-  apply auto
-  apply (rule_tac x="d/2" in exI, auto)
-  done
-
-lemma triangle_lemma:
-  fixes x y z :: real
-  assumes x: "0 \<le> x"
-    and y: "0 \<le> y"
-    and z: "0 \<le> z"
-    and xy: "x\<^sup>2 \<le> y\<^sup>2 + z\<^sup>2"
-  shows "x \<le> y + z"
-proof -
-  have "y\<^sup>2 + z\<^sup>2 \<le> y\<^sup>2 + 2 * y * z + z\<^sup>2"
-    using z y by simp
-  with xy have th: "x\<^sup>2 \<le> (y + z)\<^sup>2"
-    by (simp add: power2_eq_square field_simps)
-  from y z have yz: "y + z \<ge> 0"
-    by arith
-  from power2_le_imp_le[OF th yz] show ?thesis .
-qed
-
-
-subsection \<open>A generic notion of "hull" (convex, affine, conic hull and closure).\<close>
-
-definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
-  where "S hull s = \<Inter>{t. S t \<and> s \<subseteq> t}"
-
-lemma hull_same: "S s \<Longrightarrow> S hull s = s"
-  unfolding hull_def by auto
-
-lemma hull_in: "(\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)) \<Longrightarrow> S (S hull s)"
-  unfolding hull_def Ball_def by auto
-
-lemma hull_eq: "(\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)) \<Longrightarrow> (S hull s) = s \<longleftrightarrow> S s"
-  using hull_same[of S s] hull_in[of S s] by metis
-
-lemma hull_hull [simp]: "S hull (S hull s) = S hull s"
-  unfolding hull_def by blast
-
-lemma hull_subset[intro]: "s \<subseteq> (S hull s)"
-  unfolding hull_def by blast
-
-lemma hull_mono: "s \<subseteq> t \<Longrightarrow> (S hull s) \<subseteq> (S hull t)"
-  unfolding hull_def by blast
-
-lemma hull_antimono: "\<forall>x. S x \<longrightarrow> T x \<Longrightarrow> (T hull s) \<subseteq> (S hull s)"
-  unfolding hull_def by blast
-
-lemma hull_minimal: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (S hull s) \<subseteq> t"
-  unfolding hull_def by blast
-
-lemma subset_hull: "S t \<Longrightarrow> S hull s \<subseteq> t \<longleftrightarrow> s \<subseteq> t"
-  unfolding hull_def by blast
-
-lemma hull_UNIV [simp]: "S hull UNIV = UNIV"
-  unfolding hull_def by auto
-
-lemma hull_unique: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> S t' \<Longrightarrow> t \<subseteq> t') \<Longrightarrow> (S hull s = t)"
-  unfolding hull_def by auto
-
-lemma hull_induct: "(\<And>x. x\<in> S \<Longrightarrow> P x) \<Longrightarrow> Q {x. P x} \<Longrightarrow> \<forall>x\<in> Q hull S. P x"
-  using hull_minimal[of S "{x. P x}" Q]
-  by (auto simp add: subset_eq)
-
-lemma hull_inc: "x \<in> S \<Longrightarrow> x \<in> P hull S"
-  by (metis hull_subset subset_eq)
-
-lemma hull_union_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))"
-  unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2)
-
-lemma hull_union:
-  assumes T: "\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)"
-  shows "S hull (s \<union> t) = S hull (S hull s \<union> S hull t)"
-  apply rule
-  apply (rule hull_mono)
-  unfolding Un_subset_iff
-  apply (metis hull_subset Un_upper1 Un_upper2 subset_trans)
-  apply (rule hull_minimal)
-  apply (metis hull_union_subset)
-  apply (metis hull_in T)
-  done
-
-lemma hull_redundant_eq: "a \<in> (S hull s) \<longleftrightarrow> S hull (insert a s) = S hull s"
-  unfolding hull_def by blast
-
-lemma hull_redundant: "a \<in> (S hull s) \<Longrightarrow> S hull (insert a s) = S hull s"
-  by (metis hull_redundant_eq)
-
-
-subsection \<open>Archimedean properties and useful consequences\<close>
-
-text\<open>Bernoulli's inequality\<close>
-proposition Bernoulli_inequality:
-  fixes x :: real
-  assumes "-1 \<le> x"
-    shows "1 + n * x \<le> (1 + x) ^ n"
-proof (induct n)
-  case 0
-  then show ?case by simp
-next
-  case (Suc n)
-  have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
-    by (simp add: algebra_simps)
-  also have "... = (1 + x) * (1 + n*x)"
-    by (auto simp: power2_eq_square algebra_simps  of_nat_Suc)
-  also have "... \<le> (1 + x) ^ Suc n"
-    using Suc.hyps assms mult_left_mono by fastforce
-  finally show ?case .
-qed
-
-corollary Bernoulli_inequality_even:
-  fixes x :: real
-  assumes "even n"
-    shows "1 + n * x \<le> (1 + x) ^ n"
-proof (cases "-1 \<le> x \<or> n=0")
-  case True
-  then show ?thesis
-    by (auto simp: Bernoulli_inequality)
-next
-  case False
-  then have "real n \<ge> 1"
-    by simp
-  with False have "n * x \<le> -1"
-    by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
-  then have "1 + n * x \<le> 0"
-    by auto
-  also have "... \<le> (1 + x) ^ n"
-    using assms
-    using zero_le_even_power by blast
-  finally show ?thesis .
-qed
-
-corollary real_arch_pow:
-  fixes x :: real
-  assumes x: "1 < x"
-  shows "\<exists>n. y < x^n"
-proof -
-  from x have x0: "x - 1 > 0"
-    by arith
-  from reals_Archimedean3[OF x0, rule_format, of y]
-  obtain n :: nat where n: "y < real n * (x - 1)" by metis
-  from x0 have x00: "x- 1 \<ge> -1" by arith
-  from Bernoulli_inequality[OF x00, of n] n
-  have "y < x^n" by auto
-  then show ?thesis by metis
-qed
-
-corollary real_arch_pow_inv:
-  fixes x y :: real
-  assumes y: "y > 0"
-    and x1: "x < 1"
-  shows "\<exists>n. x^n < y"
-proof (cases "x > 0")
-  case True
-  with x1 have ix: "1 < 1/x" by (simp add: field_simps)
-  from real_arch_pow[OF ix, of "1/y"]
-  obtain n where n: "1/y < (1/x)^n" by blast
-  then show ?thesis using y \<open>x > 0\<close>
-    by (auto simp add: field_simps)
-next
-  case False
-  with y x1 show ?thesis
-    apply auto
-    apply (rule exI[where x=1])
-    apply auto
-    done
-qed
-
-lemma forall_pos_mono:
-  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
-    (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
-  by (metis real_arch_inverse)
-
-lemma forall_pos_mono_1:
-  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
-    (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
-  apply (rule forall_pos_mono)
-  apply auto
-  apply (metis Suc_pred of_nat_Suc)
-  done
-
-
-subsection\<open>A bit of linear algebra.\<close>
+subsection \<open>Subspaces of vector spaces\<close>
 
 definition (in real_vector) subspace :: "'a set \<Rightarrow> bool"
   where "subspace S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>x \<in> S. \<forall>y \<in> S. x + y \<in> S) \<and> (\<forall>c. \<forall>x \<in> S. c *\<^sub>R x \<in> S)"
@@ -714,25 +233,6 @@
     using f by induct (simp_all add: subspace_0 [OF sA] subspace_add [OF sA])
 qed (simp add: subspace_0 [OF sA])
 
-lemma subspace_linear_image:
-  assumes lf: "linear f"
-    and sS: "subspace S"
-  shows "subspace (f ` S)"
-  using lf sS linear_0[OF lf]
-  unfolding linear_iff subspace_def
-  apply (auto simp add: image_iff)
-  apply (rule_tac x="x + y" in bexI)
-  apply auto
-  apply (rule_tac x="c *\<^sub>R x" in bexI)
-  apply auto
-  done
-
-lemma subspace_linear_vimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace (f -` S)"
-  by (auto simp add: subspace_def linear_iff linear_0[of f])
-
-lemma subspace_linear_preimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace {x. f x \<in> S}"
-  by (auto simp add: subspace_def linear_iff linear_0[of f])
-
 lemma subspace_trivial: "subspace {0}"
   by (simp add: subspace_def)
 
@@ -768,6 +268,9 @@
 lemma span_minimal: "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> span S \<subseteq> T"
   unfolding span_def by (rule hull_minimal)
 
+lemma span_UNIV: "span UNIV = UNIV"
+  by (intro span_unique) auto
+
 lemma (in real_vector) span_induct:
   assumes x: "x \<in> span S"
     and P: "subspace P"
@@ -805,10 +308,8 @@
   by (metis order_antisym span_def hull_minimal)
 
 lemma (in real_vector) span_induct':
-  assumes SP: "\<forall>x \<in> S. P x"
-    and P: "subspace {x. P x}"
-  shows "\<forall>x \<in> span S. P x"
-  using span_induct SP P by blast
+  "\<forall>x \<in> S. P x \<Longrightarrow> subspace {x. P x} \<Longrightarrow> \<forall>x \<in> span S. P x"
+  unfolding span_def by (rule hull_induct) auto
 
 inductive_set (in real_vector) span_induct_alt_help for S :: "'a set"
 where
@@ -901,6 +402,10 @@
 lemma span_inc: "S \<subseteq> span S"
   by (metis subset_eq span_superset)
 
+lemma span_eq: "span S = span T \<longleftrightarrow> S \<subseteq> span T \<and> T \<subseteq> span S"
+  using span_inc[unfolded subset_eq] using span_mono[of T "span S"] span_mono[of S "span T"]
+  by (auto simp add: span_span)
+
 lemma (in real_vector) dependent_0:
   assumes "0 \<in> A"
   shows "dependent A"
@@ -926,8 +431,43 @@
 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)
 
+text \<open>The key breakdown property.\<close>
+
+lemma span_singleton: "span {x} = range (\<lambda>k. k *\<^sub>R x)"
+proof (rule span_unique)
+  show "{x} \<subseteq> range (\<lambda>k. k *\<^sub>R x)"
+    by (fast intro: scaleR_one [symmetric])
+  show "subspace (range (\<lambda>k. k *\<^sub>R x))"
+    unfolding subspace_def
+    by (auto intro: scaleR_add_left [symmetric])
+next
+  fix T
+  assume "{x} \<subseteq> T" and "subspace T"
+  then show "range (\<lambda>k. k *\<^sub>R x) \<subseteq> T"
+    unfolding subspace_def by auto
+qed
+
 text \<open>Mapping under linear image.\<close>
 
+lemma subspace_linear_image:
+  assumes lf: "linear f"
+    and sS: "subspace S"
+  shows "subspace (f ` S)"
+  using lf sS linear_0[OF lf]
+  unfolding linear_iff subspace_def
+  apply (auto simp add: image_iff)
+  apply (rule_tac x="x + y" in bexI)
+  apply auto
+  apply (rule_tac x="c *\<^sub>R x" in bexI)
+  apply auto
+  done
+
+lemma subspace_linear_vimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace (f -` S)"
+  by (auto simp add: subspace_def linear_iff linear_0[of f])
+
+lemma subspace_linear_preimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace {x. f x \<in> S}"
+  by (auto simp add: subspace_def linear_iff linear_0[of f])
+
 lemma span_linear_image:
   assumes lf: "linear f"
   shows "span (f ` S) = f ` span S"
@@ -944,6 +484,12 @@
     by (intro span_minimal subspace_linear_vimage lf)
 qed
 
+lemma spans_image:
+  assumes lf: "linear f"
+    and VB: "V \<subseteq> span B"
+  shows "f ` V \<subseteq> span (f ` B)"
+  unfolding span_linear_image[OF lf] by (metis VB image_mono)
+
 lemma span_union: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
 proof (rule span_unique)
   show "A \<union> B \<subseteq> (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
@@ -962,22 +508,6 @@
     by (auto intro!: subspace_add elim: span_induct)
 qed
 
-text \<open>The key breakdown property.\<close>
-
-lemma span_singleton: "span {x} = range (\<lambda>k. k *\<^sub>R x)"
-proof (rule span_unique)
-  show "{x} \<subseteq> range (\<lambda>k. k *\<^sub>R x)"
-    by (fast intro: scaleR_one [symmetric])
-  show "subspace (range (\<lambda>k. k *\<^sub>R x))"
-    unfolding subspace_def
-    by (auto intro: scaleR_add_left [symmetric])
-next
-  fix T
-  assume "{x} \<subseteq> T" and "subspace T"
-  then show "range (\<lambda>k. k *\<^sub>R x) \<subseteq> T"
-    unfolding subspace_def by auto
-qed
-
 lemma span_insert: "span (insert a S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
 proof -
   have "span ({a} \<union> S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
@@ -1164,32 +694,65 @@
   ultimately show ?thesis by blast
 qed
 
-
-lemma span_finite:
-  assumes fS: "finite S"
-  shows "span S = {y. \<exists>u. setsum (\<lambda>v. u v *\<^sub>R v) S = y}"
-  (is "_ = ?rhs")
+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
+  apply safe
+  subgoal for x S u
+    by (intro exI[of _ "\<lambda>x. if x \<in> S then u x else 0"])
+        (auto intro!: setsum.mono_neutral_cong_right)
+  apply auto
+  done
+
+lemma dependent_alt:
+  "dependent B \<longleftrightarrow>
+    (\<exists>X. finite {x. X x \<noteq> 0} \<and> {x. X x \<noteq> 0} \<subseteq> B \<and> (\<Sum>x|X x \<noteq> 0. X x *\<^sub>R x) = 0 \<and> (\<exists>x. X x \<noteq> 0))"
+  unfolding dependent_explicit
+  apply safe
+  subgoal for S u v
+    apply (intro exI[of _ "\<lambda>x. if x \<in> S then u x else 0"])
+    apply (subst setsum.mono_neutral_cong_left[where T=S])
+    apply (auto intro!: setsum.mono_neutral_cong_right cong: rev_conj_cong)
+    done
+  apply auto
+  done
+
+lemma independent_alt:
+  "independent B \<longleftrightarrow>
+    (\<forall>X. finite {x. X x \<noteq> 0} \<longrightarrow> {x. X x \<noteq> 0} \<subseteq> B \<longrightarrow> (\<Sum>x|X x \<noteq> 0. X x *\<^sub>R x) = 0 \<longrightarrow> (\<forall>x. X x = 0))"
+  unfolding dependent_alt by auto
+
+lemma independentD_alt:
+  "independent B \<Longrightarrow> finite {x. X x \<noteq> 0} \<Longrightarrow> {x. X x \<noteq> 0} \<subseteq> B \<Longrightarrow> (\<Sum>x|X x \<noteq> 0. X x *\<^sub>R x) = 0 \<Longrightarrow> X x = 0"
+  unfolding independent_alt by blast
+
+lemma independentD_unique:
+  assumes B: "independent B"
+    and X: "finite {x. X x \<noteq> 0}" "{x. X x \<noteq> 0} \<subseteq> B"
+    and Y: "finite {x. Y x \<noteq> 0}" "{x. Y x \<noteq> 0} \<subseteq> B"
+    and "(\<Sum>x | X x \<noteq> 0. X x *\<^sub>R x) = (\<Sum>x| Y x \<noteq> 0. Y x *\<^sub>R x)"
+  shows "X = Y"
 proof -
-  {
-    fix y
-    assume y: "y \<in> span S"
-    from y obtain S' u where fS': "finite S'"
-      and SS': "S' \<subseteq> S"
-      and u: "setsum (\<lambda>v. u v *\<^sub>R v) S' = y"
-      unfolding span_explicit by blast
-    let ?u = "\<lambda>x. if x \<in> S' then u x else 0"
-    have "setsum (\<lambda>v. ?u v *\<^sub>R v) S = setsum (\<lambda>v. u v *\<^sub>R v) S'"
-      using SS' fS by (auto intro!: setsum.mono_neutral_cong_right)
-    then have "setsum (\<lambda>v. ?u v *\<^sub>R v) S = y" by (metis u)
-    then have "y \<in> ?rhs" by auto
-  }
-  moreover
-  {
-    fix y u
-    assume u: "setsum (\<lambda>v. u v *\<^sub>R v) S = y"
-    then have "y \<in> span S" using fS unfolding span_explicit by auto
-  }
-  ultimately show ?thesis by blast
+  have "X x - Y x = 0" for x
+    using B
+  proof (rule independentD_alt)
+    have "{x. X x - Y x \<noteq> 0} \<subseteq> {x. X x \<noteq> 0} \<union> {x. Y x \<noteq> 0}"
+      by auto
+    then show "finite {x. X x - Y x \<noteq> 0}" "{x. X x - Y x \<noteq> 0} \<subseteq> B"
+      using X Y by (auto dest: finite_subset)
+    then have "(\<Sum>x | X x - Y x \<noteq> 0. (X x - Y x) *\<^sub>R x) = (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. (X v - Y v) *\<^sub>R v)"
+      using X Y by (intro setsum.mono_neutral_cong_left) auto
+    also have "\<dots> = (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. X v *\<^sub>R v) - (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. Y v *\<^sub>R v)"
+      by (simp add: scaleR_diff_left setsum_subtractf assms)
+    also have "(\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. X v *\<^sub>R v) = (\<Sum>v\<in>{S. X S \<noteq> 0}. X v *\<^sub>R v)"
+      using X Y by (intro setsum.mono_neutral_cong_right) auto
+    also have "(\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. Y v *\<^sub>R v) = (\<Sum>v\<in>{S. Y S \<noteq> 0}. Y v *\<^sub>R v)"
+      using X Y by (intro setsum.mono_neutral_cong_right) auto
+    finally show "(\<Sum>x | X x - Y x \<noteq> 0. (X x - Y x) *\<^sub>R x) = 0"
+      using assms by simp
+  qed
+  then show ?thesis
+    by auto
 qed
 
 text \<open>This is useful for building a basis step-by-step.\<close>
@@ -1225,6 +788,235 @@
   qed
 qed
 
+lemma independent_Union_directed:
+  assumes directed: "\<And>c d. c \<in> C \<Longrightarrow> d \<in> C \<Longrightarrow> c \<subseteq> d \<or> d \<subseteq> c"
+  assumes indep: "\<And>c. c \<in> C \<Longrightarrow> independent c"
+  shows "independent (\<Union>C)"
+proof
+  assume "dependent (\<Union>C)"
+  then obtain u v S where S: "finite S" "S \<subseteq> \<Union>C" "v \<in> S" "u v \<noteq> 0" "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0"
+    by (auto simp: dependent_explicit)
+
+  have "S \<noteq> {}"
+    using \<open>v \<in> S\<close> by auto
+  have "\<exists>c\<in>C. S \<subseteq> c"
+    using \<open>finite S\<close> \<open>S \<noteq> {}\<close> \<open>S \<subseteq> \<Union>C\<close>
+  proof (induction rule: finite_ne_induct)
+    case (insert i I)
+    then obtain c d where cd: "c \<in> C" "d \<in> C" and iI: "I \<subseteq> c" "i \<in> d"
+      by blast
+    from directed[OF cd] cd have "c \<union> d \<in> C"
+      by (auto simp: sup.absorb1 sup.absorb2)
+    with iI show ?case
+      by (intro bexI[of _ "c \<union> d"]) auto
+  qed auto
+  then obtain c where "c \<in> C" "S \<subseteq> c"
+    by auto
+  have "dependent c"
+    unfolding dependent_explicit
+    by (intro exI[of _ S] exI[of _ u] bexI[of _ v] conjI) fact+
+  with indep[OF \<open>c \<in> C\<close>] show False
+    by auto
+qed
+
+text \<open>Hence we can create a maximal independent subset.\<close>
+
+lemma maximal_independent_subset_extend:
+  assumes "S \<subseteq> V" "independent S"
+  shows "\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
+proof -
+  let ?C = "{B. S \<subseteq> B \<and> independent B \<and> B \<subseteq> V}"
+  have "\<exists>M\<in>?C. \<forall>X\<in>?C. M \<subseteq> X \<longrightarrow> X = M"
+  proof (rule subset_Zorn)
+    fix C :: "'a set set" assume "subset.chain ?C C"
+    then have C: "\<And>c. c \<in> C \<Longrightarrow> c \<subseteq> V" "\<And>c. c \<in> C \<Longrightarrow> S \<subseteq> c" "\<And>c. c \<in> C \<Longrightarrow> independent c"
+      "\<And>c d. c \<in> C \<Longrightarrow> d \<in> C \<Longrightarrow> c \<subseteq> d \<or> d \<subseteq> c"
+      unfolding subset.chain_def by blast+
+
+    show "\<exists>U\<in>?C. \<forall>X\<in>C. X \<subseteq> U"
+    proof cases
+      assume "C = {}" with assms show ?thesis
+        by (auto intro!: exI[of _ S])
+    next
+      assume "C \<noteq> {}"
+      with C(2) have "S \<subseteq> \<Union>C"
+        by auto
+      moreover have "independent (\<Union>C)"
+        by (intro independent_Union_directed C)
+      moreover have "\<Union>C \<subseteq> V"
+        using C by auto
+      ultimately show ?thesis
+        by auto
+    qed
+  qed
+  then obtain B where B: "independent B" "B \<subseteq> V" "S \<subseteq> B"
+    and max: "\<And>S. independent S \<Longrightarrow> S \<subseteq> V \<Longrightarrow> B \<subseteq> S \<Longrightarrow> S = B"
+    by auto
+  moreover
+  { assume "\<not> V \<subseteq> span B"
+    then obtain v where "v \<in> V" "v \<notin> span B"
+      by auto
+    with B have "independent (insert v B)"
+      unfolding independent_insert by auto
+    from max[OF this] \<open>v \<in> V\<close> \<open>B \<subseteq> V\<close>
+    have "v \<in> B"
+      by auto
+    with \<open>v \<notin> span B\<close> have False
+      by (auto intro: span_superset) }
+  ultimately show ?thesis
+    by (auto intro!: exI[of _ B])
+qed
+
+
+lemma maximal_independent_subset:
+  "\<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
+  by (metis maximal_independent_subset_extend[of "{}"] empty_subsetI independent_empty)
+
+lemma span_finite:
+  assumes fS: "finite S"
+  shows "span S = {y. \<exists>u. setsum (\<lambda>v. u v *\<^sub>R v) S = y}"
+  (is "_ = ?rhs")
+proof -
+  {
+    fix y
+    assume y: "y \<in> span S"
+    from y obtain S' u where fS': "finite S'"
+      and SS': "S' \<subseteq> S"
+      and u: "setsum (\<lambda>v. u v *\<^sub>R v) S' = y"
+      unfolding span_explicit by blast
+    let ?u = "\<lambda>x. if x \<in> S' then u x else 0"
+    have "setsum (\<lambda>v. ?u v *\<^sub>R v) S = setsum (\<lambda>v. u v *\<^sub>R v) S'"
+      using SS' fS by (auto intro!: setsum.mono_neutral_cong_right)
+    then have "setsum (\<lambda>v. ?u v *\<^sub>R v) S = y" by (metis u)
+    then have "y \<in> ?rhs" by auto
+  }
+  moreover
+  {
+    fix y u
+    assume u: "setsum (\<lambda>v. u v *\<^sub>R v) S = y"
+    then have "y \<in> span S" using fS unfolding span_explicit by auto
+  }
+  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)"
+      by (auto simp add: scaleR_add_left setsum.distrib
+               intro!: arg_cong2[where f="op +"]  setsum.mono_neutral_cong_right X)
+    also have "\<dots> = x + y"
+      by (simp add: X(3)[symmetric])
+    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"
+      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 "\<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>Linear functions are equal on a subspace if they are on a spanning set.\<close>
+
+lemma subspace_kernel:
+  assumes lf: "linear f"
+  shows "subspace {x. f x = 0}"
+  apply (simp add: subspace_def)
+  apply (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf])
+  done
+
+lemma linear_eq_0_span:
+  assumes lf: "linear f" and f0: "\<forall>x\<in>B. f x = 0"
+  shows "\<forall>x \<in> span B. f x = 0"
+  using f0 subspace_kernel[OF lf]
+  by (rule span_induct')
+
+lemma linear_eq_0: "linear f \<Longrightarrow> S \<subseteq> span B \<Longrightarrow> \<forall>x\<in>B. f x = 0 \<Longrightarrow> \<forall>x\<in>S. f x = 0"
+  using linear_eq_0_span[of f B] by auto
+
+lemma linear_eq_span:  "linear f \<Longrightarrow> linear g \<Longrightarrow> \<forall>x\<in>B. f x = g x \<Longrightarrow> \<forall>x \<in> span B. f x = g x"
+  using linear_eq_0_span[of "\<lambda>x. f x - g x" B] by (auto simp: linear_compose_sub)
+
+lemma linear_eq: "linear f \<Longrightarrow> linear g \<Longrightarrow> S \<subseteq> span B \<Longrightarrow> \<forall>x\<in>B. f x = g x \<Longrightarrow> \<forall>x\<in>S. f x = g x"
+  using linear_eq_span[of f g B] by auto
+
 text \<open>The degenerate case of the Exchange Lemma.\<close>
 
 lemma spanning_subset_independent:
@@ -1264,6 +1056,114 @@
   then show "A \<subseteq> B" by blast
 qed
 
+text \<open>Relation between bases and injectivity/surjectivity of map.\<close>
+
+lemma spanning_surjective_image:
+  assumes us: "UNIV \<subseteq> span S"
+    and lf: "linear f"
+    and sf: "surj f"
+  shows "UNIV \<subseteq> span (f ` S)"
+proof -
+  have "UNIV \<subseteq> f ` UNIV"
+    using sf by (auto simp add: surj_def)
+  also have " \<dots> \<subseteq> span (f ` S)"
+    using spans_image[OF lf us] .
+  finally show ?thesis .
+qed
+
+lemma independent_inj_on_image:
+  assumes iS: "independent S"
+    and lf: "linear f"
+    and fi: "inj_on f (span S)"
+  shows "independent (f ` S)"
+proof -
+  {
+    fix a
+    assume a: "a \<in> S" "f a \<in> span (f ` S - {f a})"
+    have eq: "f ` S - {f a} = f ` (S - {a})"
+      using fi \<open>a\<in>S\<close> by (auto simp add: inj_on_def span_superset)
+    from a have "f a \<in> f ` span (S - {a})"
+      unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast
+    then have "a \<in> span (S - {a})"
+      by (rule inj_on_image_mem_iff_alt[OF fi, rotated])
+         (insert span_mono[of "S - {a}" S], auto intro: span_superset \<open>a\<in>S\<close>)
+    with a(1) iS have False
+      by (simp add: dependent_def)
+  }
+  then show ?thesis
+    unfolding dependent_def by blast
+qed
+
+lemma independent_injective_image:
+  "independent S \<Longrightarrow> linear f \<Longrightarrow> inj f \<Longrightarrow> independent (f ` S)"
+  using independent_inj_on_image[of S f] by (auto simp: subset_inj_on)
+
+text \<open>Detailed theorems about left and right invertibility in general case.\<close>
+
+lemma linear_inj_on_left_inverse:
+  assumes lf: "linear f" and fi: "inj_on f (span S)"
+  shows "\<exists>g. range g \<subseteq> span S \<and> linear g \<and> (\<forall>x\<in>span S. g (f x) = x)"
+proof -
+  obtain B where "independent B" "B \<subseteq> S" "S \<subseteq> span B"
+    using maximal_independent_subset[of S] by auto
+  then have "span S = span B"
+    unfolding span_eq by (auto simp: span_superset)
+  with linear_independent_extend_subspace[OF independent_inj_on_image, OF \<open>independent B\<close> lf] fi
+  obtain g where g: "linear g" "\<forall>x\<in>f ` B. g x = inv_into B f x" "range g = span (inv_into B f ` f ` B)"
+    by fastforce
+  have fB: "inj_on f B"
+    using fi by (auto simp: \<open>span S = span B\<close> intro: subset_inj_on span_superset)
+
+  have "\<forall>x\<in>span B. g (f x) = x"
+  proof (intro linear_eq_span)
+    show "linear (\<lambda>x. x)" "linear (\<lambda>x. g (f x))"
+      using linear_id linear_compose[OF \<open>linear f\<close> \<open>linear g\<close>] by (auto simp: id_def comp_def)
+    show "\<forall>x \<in> B. g (f x) = x"
+      using g fi \<open>span S = span B\<close> by (auto simp: fB)
+  qed
+  moreover
+  have "inv_into B f ` f ` B \<subseteq> B"
+    by (auto simp: fB)
+  then have "range g \<subseteq> span S"
+    unfolding g \<open>span S = span B\<close> by (intro span_mono)
+  ultimately show ?thesis
+    using \<open>span S = span B\<close> \<open>linear g\<close> by auto
+qed
+
+lemma linear_injective_left_inverse: "linear f \<Longrightarrow> inj f \<Longrightarrow> \<exists>g. linear g \<and> g \<circ> f = id"
+  using linear_inj_on_left_inverse[of f UNIV] by (auto simp: fun_eq_iff span_UNIV)
+
+lemma linear_surj_right_inverse:
+  assumes lf: "linear f" and sf: "span T \<subseteq> f`span S"
+  shows "\<exists>g. range g \<subseteq> span S \<and> linear g \<and> (\<forall>x\<in>span T. f (g x) = x)"
+proof -
+  obtain B where "independent B" "B \<subseteq> T" "T \<subseteq> span B"
+    using maximal_independent_subset[of T] by auto
+  then have "span T = span B"
+    unfolding span_eq by (auto simp: span_superset)
+
+  from linear_independent_extend_subspace[OF \<open>independent B\<close>, of "inv_into (span S) f"]
+  obtain g where g: "linear g" "\<forall>x\<in>B. g x = inv_into (span S) f x" "range g = span (inv_into (span S) f`B)"
+    by auto
+  moreover have "x \<in> B \<Longrightarrow> f (inv_into (span S) f x) = x" for x
+    using \<open>B \<subseteq> T\<close> \<open>span T \<subseteq> f`span S\<close> by (intro f_inv_into_f) (auto intro: span_superset)
+  ultimately have "\<forall>x\<in>B. f (g x) = x"
+    by auto
+  then have "\<forall>x\<in>span B. f (g x) = x"
+    using linear_id linear_compose[OF \<open>linear g\<close> \<open>linear f\<close>]
+    by (intro linear_eq_span) (auto simp: id_def comp_def)
+  moreover have "inv_into (span S) f ` B \<subseteq> span S"
+    using \<open>B \<subseteq> T\<close> \<open>span T \<subseteq> f`span S\<close> by (auto intro: inv_into_into span_superset)
+  then have "range g \<subseteq> span S"
+    unfolding g by (intro span_minimal subspace_span) auto
+  ultimately show ?thesis
+    using \<open>linear g\<close> \<open>span T = span B\<close> by auto
+qed
+
+lemma linear_surjective_right_inverse: "linear f \<Longrightarrow> surj f \<Longrightarrow> \<exists>g. linear g \<and> f \<circ> g = id"
+  using linear_surj_right_inverse[of f UNIV UNIV]
+  by (auto simp: span_UNIV fun_eq_iff)
+
 text \<open>The general case of the Exchange Lemma, the key to what follows.\<close>
 
 lemma exchange_lemma:
@@ -1391,6 +1291,487 @@
 qed
 
 
+subsection \<open>More interesting properties of the norm.\<close>
+
+lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
+  by auto
+
+notation inner (infix "\<bullet>" 70)
+
+lemma square_bound_lemma:
+  fixes x :: real
+  shows "x < (1 + x) * (1 + x)"
+proof -
+  have "(x + 1/2)\<^sup>2 + 3/4 > 0"
+    using zero_le_power2[of "x+1/2"] by arith
+  then show ?thesis
+    by (simp add: field_simps power2_eq_square)
+qed
+
+lemma square_continuous:
+  fixes e :: real
+  shows "e > 0 \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> \<bar>y * y - x * x\<bar> < e)"
+  using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
+  by (force simp add: power2_eq_square)
+
+
+lemma norm_eq_0_dot: "norm x = 0 \<longleftrightarrow> x \<bullet> x = (0::real)"
+  by simp (* TODO: delete *)
+
+lemma norm_triangle_sub:
+  fixes x y :: "'a::real_normed_vector"
+  shows "norm x \<le> norm y + norm (x - y)"
+  using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
+
+lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> x \<bullet> x \<le> y \<bullet> y"
+  by (simp add: norm_eq_sqrt_inner)
+
+lemma norm_lt: "norm x < norm y \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
+  by (simp add: norm_eq_sqrt_inner)
+
+lemma norm_eq: "norm x = norm y \<longleftrightarrow> x \<bullet> x = y \<bullet> y"
+  apply (subst order_eq_iff)
+  apply (auto simp: norm_le)
+  done
+
+lemma norm_eq_1: "norm x = 1 \<longleftrightarrow> x \<bullet> x = 1"
+  by (simp add: norm_eq_sqrt_inner)
+
+text\<open>Squaring equations and inequalities involving norms.\<close>
+
+lemma dot_square_norm: "x \<bullet> x = (norm x)\<^sup>2"
+  by (simp only: power2_norm_eq_inner) (* TODO: move? *)
+
+lemma norm_eq_square: "norm x = a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x = a\<^sup>2"
+  by (auto simp add: norm_eq_sqrt_inner)
+
+lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x \<le> a\<^sup>2"
+  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
+  using norm_ge_zero[of x]
+  apply arith
+  done
+
+lemma norm_ge_square: "norm x \<ge> a \<longleftrightarrow> a \<le> 0 \<or> x \<bullet> x \<ge> a\<^sup>2"
+  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
+  using norm_ge_zero[of x]
+  apply arith
+  done
+
+lemma norm_lt_square: "norm x < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a\<^sup>2"
+  by (metis not_le norm_ge_square)
+
+lemma norm_gt_square: "norm x > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a\<^sup>2"
+  by (metis norm_le_square not_less)
+
+text\<open>Dot product in terms of the norm rather than conversely.\<close>
+
+lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left
+  inner_scaleR_left inner_scaleR_right
+
+lemma dot_norm: "x \<bullet> y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
+  unfolding power2_norm_eq_inner inner_simps inner_commute by auto
+
+lemma dot_norm_neg: "x \<bullet> y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
+  unfolding power2_norm_eq_inner inner_simps inner_commute
+  by (auto simp add: algebra_simps)
+
+text\<open>Equality of vectors in terms of @{term "op \<bullet>"} products.\<close>
+
+lemma linear_componentwise:
+  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
+  assumes lf: "linear f"
+  shows "(f x) \<bullet> j = (\<Sum>i\<in>Basis. (x\<bullet>i) * (f i\<bullet>j))" (is "?lhs = ?rhs")
+proof -
+  have "?rhs = (\<Sum>i\<in>Basis. (x\<bullet>i) *\<^sub>R (f i))\<bullet>j"
+    by (simp add: inner_setsum_left)
+  then show ?thesis
+    unfolding linear_setsum_mul[OF lf, symmetric]
+    unfolding euclidean_representation ..
+qed
+
+lemma vector_eq: "x = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y \<and> y \<bullet> y = x \<bullet> x"
+  (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs by simp
+next
+  assume ?rhs
+  then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y \<bullet> y = 0"
+    by simp
+  then have "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0"
+    by (simp add: inner_diff inner_commute)
+  then have "(x - y) \<bullet> (x - y) = 0"
+    by (simp add: field_simps inner_diff inner_commute)
+  then show "x = y" by simp
+qed
+
+lemma norm_triangle_half_r:
+  "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
+  using dist_triangle_half_r unfolding dist_norm[symmetric] by auto
+
+lemma norm_triangle_half_l:
+  assumes "norm (x - y) < e / 2"
+    and "norm (x' - y) < e / 2"
+  shows "norm (x - x') < e"
+  using dist_triangle_half_l[OF assms[unfolded dist_norm[symmetric]]]
+  unfolding dist_norm[symmetric] .
+
+lemma norm_triangle_le: "norm x + norm y \<le> e \<Longrightarrow> norm (x + y) \<le> e"
+  by (rule norm_triangle_ineq [THEN order_trans])
+
+lemma norm_triangle_lt: "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
+  by (rule norm_triangle_ineq [THEN le_less_trans])
+
+lemma setsum_clauses:
+  shows "setsum f {} = 0"
+    and "finite S \<Longrightarrow> setsum f (insert x S) = (if x \<in> S then setsum f S else f x + setsum f S)"
+  by (auto simp add: insert_absorb)
+
+lemma setsum_norm_le:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
+  shows "norm (setsum f S) \<le> setsum g S"
+  by (rule order_trans [OF norm_setsum setsum_mono]) (simp add: fg)
+
+lemma setsum_norm_bound:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  assumes K: "\<forall>x \<in> S. norm (f x) \<le> K"
+  shows "norm (setsum f S) \<le> of_nat (card S) * K"
+  using setsum_norm_le[OF K] setsum_constant[symmetric]
+  by simp
+
+lemma setsum_group:
+  assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
+  shows "setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) T = setsum g S"
+  apply (subst setsum_image_gen[OF fS, of g f])
+  apply (rule setsum.mono_neutral_right[OF fT fST])
+  apply (auto intro: setsum.neutral)
+  done
+
+lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
+proof
+  assume "\<forall>x. x \<bullet> y = x \<bullet> z"
+  then have "\<forall>x. x \<bullet> (y - z) = 0"
+    by (simp add: inner_diff)
+  then have "(y - z) \<bullet> (y - z) = 0" ..
+  then show "y = z" by simp
+qed simp
+
+lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = y"
+proof
+  assume "\<forall>z. x \<bullet> z = y \<bullet> z"
+  then have "\<forall>z. (x - y) \<bullet> z = 0"
+    by (simp add: inner_diff)
+  then have "(x - y) \<bullet> (x - y) = 0" ..
+  then show "x = y" by simp
+qed simp
+
+
+subsection \<open>Orthogonality.\<close>
+
+context real_inner
+begin
+
+definition "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
+
+lemma orthogonal_clauses:
+  "orthogonal a 0"
+  "orthogonal a x \<Longrightarrow> orthogonal a (c *\<^sub>R x)"
+  "orthogonal a x \<Longrightarrow> orthogonal a (- x)"
+  "orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x + y)"
+  "orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x - y)"
+  "orthogonal 0 a"
+  "orthogonal x a \<Longrightarrow> orthogonal (c *\<^sub>R x) a"
+  "orthogonal x a \<Longrightarrow> orthogonal (- x) a"
+  "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"
+  "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x - y) a"
+  unfolding orthogonal_def inner_add inner_diff by auto
+
+end
+
+lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
+  by (simp add: orthogonal_def inner_commute)
+
+
+subsection \<open>Bilinear functions.\<close>
+
+definition "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
+
+lemma bilinear_ladd: "bilinear h \<Longrightarrow> h (x + y) z = h x z + h y z"
+  by (simp add: bilinear_def linear_iff)
+
+lemma bilinear_radd: "bilinear h \<Longrightarrow> h x (y + z) = h x y + h x z"
+  by (simp add: bilinear_def linear_iff)
+
+lemma bilinear_lmul: "bilinear h \<Longrightarrow> h (c *\<^sub>R x) y = c *\<^sub>R h x y"
+  by (simp add: bilinear_def linear_iff)
+
+lemma bilinear_rmul: "bilinear h \<Longrightarrow> h x (c *\<^sub>R y) = c *\<^sub>R h x y"
+  by (simp add: bilinear_def linear_iff)
+
+lemma bilinear_lneg: "bilinear h \<Longrightarrow> h (- x) y = - h x y"
+  by (drule bilinear_lmul [of _ "- 1"]) simp
+
+lemma bilinear_rneg: "bilinear h \<Longrightarrow> h x (- y) = - h x y"
+  by (drule bilinear_rmul [of _ _ "- 1"]) simp
+
+lemma (in ab_group_add) eq_add_iff: "x = x + y \<longleftrightarrow> y = 0"
+  using add_left_imp_eq[of x y 0] by auto
+
+lemma bilinear_lzero:
+  assumes "bilinear h"
+  shows "h 0 x = 0"
+  using bilinear_ladd [OF assms, of 0 0 x] by (simp add: eq_add_iff field_simps)
+
+lemma bilinear_rzero:
+  assumes "bilinear h"
+  shows "h x 0 = 0"
+  using bilinear_radd [OF assms, of x 0 0 ] by (simp add: eq_add_iff field_simps)
+
+lemma bilinear_lsub: "bilinear h \<Longrightarrow> h (x - y) z = h x z - h y z"
+  using bilinear_ladd [of h x "- y"] by (simp add: bilinear_lneg)
+
+lemma bilinear_rsub: "bilinear h \<Longrightarrow> h z (x - y) = h z x - h z y"
+  using bilinear_radd [of h _ x "- y"] by (simp add: bilinear_rneg)
+
+lemma bilinear_setsum:
+  assumes bh: "bilinear h"
+    and fS: "finite S"
+    and fT: "finite T"
+  shows "h (setsum f S) (setsum g T) = setsum (\<lambda>(i,j). h (f i) (g j)) (S \<times> T) "
+proof -
+  have "h (setsum f S) (setsum g T) = setsum (\<lambda>x. h (f x) (setsum g T)) S"
+    apply (rule linear_setsum[unfolded o_def])
+    using bh fS
+    apply (auto simp add: bilinear_def)
+    done
+  also have "\<dots> = setsum (\<lambda>x. setsum (\<lambda>y. h (f x) (g y)) T) S"
+    apply (rule setsum.cong, simp)
+    apply (rule linear_setsum[unfolded o_def])
+    using bh fT
+    apply (auto simp add: bilinear_def)
+    done
+  finally show ?thesis
+    unfolding setsum.cartesian_product .
+qed
+
+
+subsection \<open>Adjoints.\<close>
+
+definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
+
+lemma adjoint_unique:
+  assumes "\<forall>x y. inner (f x) y = inner x (g y)"
+  shows "adjoint f = g"
+  unfolding adjoint_def
+proof (rule some_equality)
+  show "\<forall>x y. inner (f x) y = inner x (g y)"
+    by (rule assms)
+next
+  fix h
+  assume "\<forall>x y. inner (f x) y = inner x (h y)"
+  then have "\<forall>x y. inner x (g y) = inner x (h y)"
+    using assms by simp
+  then have "\<forall>x y. inner x (g y - h y) = 0"
+    by (simp add: inner_diff_right)
+  then have "\<forall>y. inner (g y - h y) (g y - h y) = 0"
+    by simp
+  then have "\<forall>y. h y = g y"
+    by simp
+  then show "h = g" by (simp add: ext)
+qed
+
+text \<open>TODO: The following lemmas about adjoints should hold for any
+Hilbert space (i.e. complete inner product space).
+(see @{url "http://en.wikipedia.org/wiki/Hermitian_adjoint"})
+\<close>
+
+lemma adjoint_works:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes lf: "linear f"
+  shows "x \<bullet> adjoint f y = f x \<bullet> y"
+proof -
+  have "\<forall>y. \<exists>w. \<forall>x. f x \<bullet> y = x \<bullet> w"
+  proof (intro allI exI)
+    fix y :: "'m" and x
+    let ?w = "(\<Sum>i\<in>Basis. (f i \<bullet> y) *\<^sub>R i) :: 'n"
+    have "f x \<bullet> y = f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i) \<bullet> y"
+      by (simp add: euclidean_representation)
+    also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<bullet> y"
+      unfolding linear_setsum[OF lf]
+      by (simp add: linear_cmul[OF lf])
+    finally show "f x \<bullet> y = x \<bullet> ?w"
+      by (simp add: inner_setsum_left inner_setsum_right mult.commute)
+  qed
+  then show ?thesis
+    unfolding adjoint_def choice_iff
+    by (intro someI2_ex[where Q="\<lambda>f'. x \<bullet> f' y = f x \<bullet> y"]) auto
+qed
+
+lemma adjoint_clauses:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes lf: "linear f"
+  shows "x \<bullet> adjoint f y = f x \<bullet> y"
+    and "adjoint f y \<bullet> x = y \<bullet> f x"
+  by (simp_all add: adjoint_works[OF lf] inner_commute)
+
+lemma adjoint_linear:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes lf: "linear f"
+  shows "linear (adjoint f)"
+  by (simp add: lf linear_iff euclidean_eq_iff[where 'a='n] euclidean_eq_iff[where 'a='m]
+    adjoint_clauses[OF lf] inner_distrib)
+
+lemma adjoint_adjoint:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes lf: "linear f"
+  shows "adjoint (adjoint f) = f"
+  by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])
+
+
+subsection \<open>Interlude: Some properties of real sets\<close>
+
+lemma seq_mono_lemma:
+  assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n"
+    and "\<forall>n \<ge> m. e n \<le> e m"
+  shows "\<forall>n \<ge> m. d n < e m"
+  using assms
+  apply auto
+  apply (erule_tac x="n" in allE)
+  apply (erule_tac x="n" in allE)
+  apply auto
+  done
+
+lemma infinite_enumerate:
+  assumes fS: "infinite S"
+  shows "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> S)"
+  unfolding subseq_def
+  using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto
+
+lemma approachable_lt_le: "(\<exists>(d::real) > 0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)"
+  apply auto
+  apply (rule_tac x="d/2" in exI)
+  apply auto
+  done
+
+lemma approachable_lt_le2:  \<comment>\<open>like the above, but pushes aside an extra formula\<close>
+    "(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
+  apply auto
+  apply (rule_tac x="d/2" in exI, auto)
+  done
+
+lemma triangle_lemma:
+  fixes x y z :: real
+  assumes x: "0 \<le> x"
+    and y: "0 \<le> y"
+    and z: "0 \<le> z"
+    and xy: "x\<^sup>2 \<le> y\<^sup>2 + z\<^sup>2"
+  shows "x \<le> y + z"
+proof -
+  have "y\<^sup>2 + z\<^sup>2 \<le> y\<^sup>2 + 2 * y * z + z\<^sup>2"
+    using z y by simp
+  with xy have th: "x\<^sup>2 \<le> (y + z)\<^sup>2"
+    by (simp add: power2_eq_square field_simps)
+  from y z have yz: "y + z \<ge> 0"
+    by arith
+  from power2_le_imp_le[OF th yz] show ?thesis .
+qed
+
+
+
+subsection \<open>Archimedean properties and useful consequences\<close>
+
+text\<open>Bernoulli's inequality\<close>
+proposition Bernoulli_inequality:
+  fixes x :: real
+  assumes "-1 \<le> x"
+    shows "1 + n * x \<le> (1 + x) ^ n"
+proof (induct n)
+  case 0
+  then show ?case by simp
+next
+  case (Suc n)
+  have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
+    by (simp add: algebra_simps)
+  also have "... = (1 + x) * (1 + n*x)"
+    by (auto simp: power2_eq_square algebra_simps  of_nat_Suc)
+  also have "... \<le> (1 + x) ^ Suc n"
+    using Suc.hyps assms mult_left_mono by fastforce
+  finally show ?case .
+qed
+
+corollary Bernoulli_inequality_even:
+  fixes x :: real
+  assumes "even n"
+    shows "1 + n * x \<le> (1 + x) ^ n"
+proof (cases "-1 \<le> x \<or> n=0")
+  case True
+  then show ?thesis
+    by (auto simp: Bernoulli_inequality)
+next
+  case False
+  then have "real n \<ge> 1"
+    by simp
+  with False have "n * x \<le> -1"
+    by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
+  then have "1 + n * x \<le> 0"
+    by auto
+  also have "... \<le> (1 + x) ^ n"
+    using assms
+    using zero_le_even_power by blast
+  finally show ?thesis .
+qed
+
+corollary real_arch_pow:
+  fixes x :: real
+  assumes x: "1 < x"
+  shows "\<exists>n. y < x^n"
+proof -
+  from x have x0: "x - 1 > 0"
+    by arith
+  from reals_Archimedean3[OF x0, rule_format, of y]
+  obtain n :: nat where n: "y < real n * (x - 1)" by metis
+  from x0 have x00: "x- 1 \<ge> -1" by arith
+  from Bernoulli_inequality[OF x00, of n] n
+  have "y < x^n" by auto
+  then show ?thesis by metis
+qed
+
+corollary real_arch_pow_inv:
+  fixes x y :: real
+  assumes y: "y > 0"
+    and x1: "x < 1"
+  shows "\<exists>n. x^n < y"
+proof (cases "x > 0")
+  case True
+  with x1 have ix: "1 < 1/x" by (simp add: field_simps)
+  from real_arch_pow[OF ix, of "1/y"]
+  obtain n where n: "1/y < (1/x)^n" by blast
+  then show ?thesis using y \<open>x > 0\<close>
+    by (auto simp add: field_simps)
+next
+  case False
+  with y x1 show ?thesis
+    apply auto
+    apply (rule exI[where x=1])
+    apply auto
+    done
+qed
+
+lemma forall_pos_mono:
+  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
+    (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
+  by (metis real_arch_inverse)
+
+lemma forall_pos_mono_1:
+  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
+    (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
+  apply (rule forall_pos_mono)
+  apply auto
+  apply (metis Suc_pred of_nat_Suc)
+  done
+
+
 subsection \<open>Euclidean Spaces as Typeclass\<close>
 
 lemma independent_Basis: "independent Basis"
@@ -1625,53 +2006,6 @@
   shows "(finite S \<Longrightarrow> card S > DIM('a)) \<Longrightarrow> dependent S"
   by (metis independent_bound not_less)
 
-text \<open>Hence we can create a maximal independent subset.\<close>
-
-lemma maximal_independent_subset_extend:
-  fixes S :: "'a::euclidean_space set"
-  assumes sv: "S \<subseteq> V"
-    and iS: "independent S"
-  shows "\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
-  using sv iS
-proof (induct "DIM('a) - card S" arbitrary: S rule: less_induct)
-  case less
-  note sv = \<open>S \<subseteq> V\<close> and i = \<open>independent S\<close>
-  let ?P = "\<lambda>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
-  let ?ths = "\<exists>x. ?P x"
-  let ?d = "DIM('a)"
-  show ?ths
-  proof (cases "V \<subseteq> span S")
-    case True
-    then show ?thesis
-      using sv i by blast
-  next
-    case False
-    then obtain a where a: "a \<in> V" "a \<notin> span S"
-      by blast
-    from a have aS: "a \<notin> S"
-      by (auto simp add: span_superset)
-    have th0: "insert a S \<subseteq> V"
-      using a sv by blast
-    from independent_insert[of a S]  i a
-    have th1: "independent (insert a S)"
-      by auto
-    have mlt: "?d - card (insert a S) < ?d - card S"
-      using aS a independent_bound[OF th1] by auto
-
-    from less(1)[OF mlt th0 th1]
-    obtain B where B: "insert a S \<subseteq> B" "B \<subseteq> V" "independent B" " V \<subseteq> span B"
-      by blast
-    from B have "?P B" by auto
-    then show ?thesis by blast
-  qed
-qed
-
-lemma maximal_independent_subset:
-  "\<exists>(B:: ('a::euclidean_space) set). B\<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
-  by (metis maximal_independent_subset_extend[of "{}:: ('a::euclidean_space) set"]
-    empty_subsetI independent_empty)
-
-
 text \<open>Notion of dimension.\<close>
 
 definition "dim V = (SOME n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> card B = n)"
@@ -1845,12 +2179,6 @@
   shows "span S = span T \<Longrightarrow> dim S = dim T"
   by (metis dim_span)
 
-lemma spans_image:
-  assumes lf: "linear f"
-    and VB: "V \<subseteq> span B"
-  shows "f ` V \<subseteq> span (f ` B)"
-  unfolding span_linear_image[OF lf] by (metis VB image_mono)
-
 lemma dim_image_le:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes lf: "linear f"
@@ -1870,43 +2198,6 @@
   finally show ?thesis .
 qed
 
-text \<open>Relation between bases and injectivity/surjectivity of map.\<close>
-
-lemma spanning_surjective_image:
-  assumes us: "UNIV \<subseteq> span S"
-    and lf: "linear f"
-    and sf: "surj f"
-  shows "UNIV \<subseteq> span (f ` S)"
-proof -
-  have "UNIV \<subseteq> f ` UNIV"
-    using sf by (auto simp add: surj_def)
-  also have " \<dots> \<subseteq> span (f ` S)"
-    using spans_image[OF lf us] .
-  finally show ?thesis .
-qed
-
-lemma independent_injective_image:
-  assumes iS: "independent S"
-    and lf: "linear f"
-    and fi: "inj f"
-  shows "independent (f ` S)"
-proof -
-  {
-    fix a
-    assume a: "a \<in> S" "f a \<in> span (f ` S - {f a})"
-    have eq: "f ` S - {f a} = f ` (S - {a})"
-      using fi by (auto simp add: inj_on_def)
-    from a have "f a \<in> f ` span (S - {a})"
-      unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast
-    then have "a \<in> span (S - {a})"
-      using fi by (auto simp add: inj_on_def)
-    with a(1) iS have False
-      by (simp add: dependent_def)
-  }
-  then show ?thesis
-    unfolding dependent_def by blast
-qed
-
 text \<open>Picking an orthogonal replacement for a spanning set.\<close>
 
 lemma vector_sub_project_orthogonal:
@@ -2016,10 +2307,6 @@
     by auto
 qed
 
-lemma span_eq: "span S = span T \<longleftrightarrow> S \<subseteq> span T \<and> T \<subseteq> span S"
-  using span_inc[unfolded subset_eq] using span_mono[of T "span S"] span_mono[of S "span T"]
-  by (auto simp add: span_span)
-
 text \<open>Low-dimensional subset is in a hyperplane (weak orthogonal complement).\<close>
 
 lemma span_not_univ_orthogonal:
@@ -2166,152 +2453,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"
-    by (simp_all add: independent_insert)
-  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"
-        by (simp add: eq)
-      {
-        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)"
-      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 \<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)"
-      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 \<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:
@@ -2368,41 +2509,6 @@
     by blast
 qed
 
-text \<open>Linear functions are equal on a subspace if they are on a spanning set.\<close>
-
-lemma subspace_kernel:
-  assumes lf: "linear f"
-  shows "subspace {x. f x = 0}"
-  apply (simp add: subspace_def)
-  apply (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf])
-  done
-
-lemma linear_eq_0_span:
-  assumes lf: "linear f" and f0: "\<forall>x\<in>B. f x = 0"
-  shows "\<forall>x \<in> span B. f x = 0"
-  using f0 subspace_kernel[OF lf]
-  by (rule span_induct')
-
-lemma linear_eq_0:
-  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"
-  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"
-proof -
-  let ?h = "\<lambda>x. f x - g x"
-  from fg have fg': "\<forall>x\<in> B. ?h x = 0" by simp
-  from linear_eq_0[OF linear_compose_sub[OF lf lg] S fg']
-  show ?thesis by simp
-qed
-
 lemma linear_eq_stdbasis:
   fixes f :: "'a::euclidean_space \<Rightarrow> _"
   assumes lf: "linear f"
@@ -2449,43 +2555,6 @@
   shows "f = g"
   using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis] fg] by blast
 
-text \<open>Detailed theorems about left and right invertibility in general case.\<close>
-
-lemma linear_injective_left_inverse:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes lf: "linear f"
-    and fi: "inj f"
-  shows "\<exists>g. linear g \<and> g \<circ> f = id"
-proof -
-  from linear_independent_extend[OF independent_injective_image, OF independent_Basis, OF lf fi]
-  obtain h :: "'b \<Rightarrow> 'a" where h: "linear h" "\<forall>x \<in> f ` Basis. h x = inv f x"
-    by blast
-  from h(2) have th: "\<forall>i\<in>Basis. (h \<circ> f) i = id i"
-    using inv_o_cancel[OF fi, unfolded fun_eq_iff id_def o_def]
-    by auto
-  from linear_eq_stdbasis[OF linear_compose[OF lf h(1)] linear_id th]
-  have "h \<circ> f = id" .
-  then show ?thesis
-    using h(1) by blast
-qed
-
-lemma linear_surjective_right_inverse:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes lf: "linear f"
-    and sf: "surj f"
-  shows "\<exists>g. linear g \<and> f \<circ> g = id"
-proof -
-  from linear_independent_extend[OF independent_Basis[where 'a='b],of "inv f"]
-  obtain h :: "'b \<Rightarrow> 'a" where h: "linear h" "\<forall>x\<in>Basis. h x = inv f x"
-    by blast
-  from h(2) have th: "\<forall>i\<in>Basis. (f \<circ> h) i = id i"
-    using sf by (auto simp add: surj_iff_all)
-  from linear_eq_stdbasis[OF linear_compose[OF h(1) lf] linear_id th]
-  have "f \<circ> h = id" .
-  then show ?thesis
-    using h(1) by blast
-qed
-
 text \<open>An injective map @{typ "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"} is also surjective.\<close>
 
 lemma linear_injective_imp_surjective: