--- 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: