# HG changeset patch # User huffman # Date 1312993422 25200 # Node ID 691c52e900cab050b18f1958a21f5e6571d756a3 # Parent 0f35a870ecf16263c295ca32815c03b3071329b4 split Linear_Algebra.thy from Euclidean_Space.thy diff -r 0f35a870ecf1 -r 691c52e900ca src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Aug 10 08:42:26 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Aug 10 09:23:42 2011 -0700 @@ -1,1586 +1,18 @@ (* Title: HOL/Multivariate_Analysis/Euclidean_Space.thy - Author: Amine Chaieb, University of Cambridge + Author: Johannes Hölzl, TU München + Author: Brian Huffman, Portland State University *) -header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*} +header {* Finite-Dimensional Inner Product Spaces *} theory Euclidean_Space imports Complex_Main - "~~/src/HOL/Library/Infinite_Set" "~~/src/HOL/Library/Inner_Product" - L2_Norm - "~~/src/HOL/Library/Convex" -uses - "~~/src/HOL/Library/positivstellensatz.ML" (* FIXME duplicate use!? *) - ("normarith.ML") -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 "\" 70) - -subsection {* A connectedness or intermediate value lemma with several applications. *} - -lemma connected_real_lemma: - fixes f :: "real \ 'a::metric_space" - assumes ab: "a \ b" and fa: "f a \ e1" and fb: "f b \ e2" - and dst: "\e x. a <= x \ x <= b \ 0 < e ==> \d > 0. \y. abs(y - x) < d \ dist(f y) (f x) < e" - and e1: "\y \ e1. \e > 0. \y'. dist y' y < e \ y' \ e1" - and e2: "\y \ e2. \e > 0. \y'. dist y' y < e \ y' \ e2" - and e12: "~(\x \ a. x <= b \ f x \ e1 \ f x \ e2)" - shows "\x \ a. x <= b \ f x \ e1 \ f x \ e2" (is "\ x. ?P x") -proof- - let ?S = "{c. \x \ a. x <= c \ f x \ e1}" - have Se: " \x. x \ ?S" apply (rule exI[where x=a]) by (auto simp add: fa) - have Sub: "\y. isUb UNIV ?S y" - apply (rule exI[where x= b]) - using ab fb e12 by (auto simp add: isUb_def setle_def) - from reals_complete[OF Se Sub] obtain l where - l: "isLub UNIV ?S l"by blast - have alb: "a \ l" "l \ b" using l ab fa fb e12 - apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) - by (metis linorder_linear) - have ale1: "\z \ a. z < l \ f z \ e1" using l - apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) - by (metis linorder_linear not_le) - have th1: "\z x e d :: real. z <= x + e \ e < d ==> z < x \ abs(z - x) < d" by arith - have th2: "\e x:: real. 0 < e ==> ~(x + e <= x)" by arith - have "\d::real. 0 < d \ 0 < d/2 \ d/2 < d" by simp - then have th3: "\d::real. d > 0 \ \e > 0. e < d" by blast - {assume le2: "f l \ e2" - from le2 fa fb e12 alb have la: "l \ a" by metis - hence lap: "l - a > 0" using alb by arith - from e2[rule_format, OF le2] obtain e where - e: "e > 0" "\y. dist y (f l) < e \ y \ e2" by metis - from dst[OF alb e(1)] obtain d where - d: "d > 0" "\y. \y - l\ < d \ dist (f y) (f l) < e" by metis - let ?d' = "min (d/2) ((l - a)/2)" - have "?d' < d \ 0 < ?d' \ ?d' < l - a" using lap d(1) - by (simp add: min_max.less_infI2) - then have "\d'. d' < d \ d' >0 \ l - d' > a" by auto - then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis - from d e have th0: "\y. \y - l\ < d \ f y \ e2" by metis - from th0[rule_format, of "l - d'"] d' have "f (l - d') \ e2" by auto - moreover - have "f (l - d') \ e1" using ale1[rule_format, of "l -d'"] d' by auto - ultimately have False using e12 alb d' by auto} - moreover - {assume le1: "f l \ e1" - from le1 fa fb e12 alb have lb: "l \ b" by metis - hence blp: "b - l > 0" using alb by arith - from e1[rule_format, OF le1] obtain e where - e: "e > 0" "\y. dist y (f l) < e \ y \ e1" by metis - from dst[OF alb e(1)] obtain d where - d: "d > 0" "\y. \y - l\ < d \ dist (f y) (f l) < e" by metis - have "\d::real. 0 < d \ d/2 < d \ 0 < d/2" by simp - then have "\d'. d' < d \ d' >0" using d(1) by blast - then obtain d' where d': "d' > 0" "d' < d" by metis - from d e have th0: "\y. \y - l\ < d \ f y \ e1" by auto - hence "\y. l \ y \ y \ l + d' \ f y \ e1" using d' by auto - with ale1 have "\y. a \ y \ y \ l + d' \ f y \ e1" by auto - with l d' have False - by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) } - ultimately show ?thesis using alb by metis -qed - -text{* One immediately useful corollary is the existence of square roots! --- Should help to get rid of all the development of square-root for reals as a special case *} - -lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)" -proof- - have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith - thus ?thesis by (simp add: field_simps power2_eq_square) -qed - -lemma square_continuous: "0 < (e::real) ==> \d. 0 < d \ (\y. abs(y - x) < d \ abs(y * y - x * x) < e)" - using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_eq, rule_format, of e x] apply (auto simp add: power2_eq_square) - apply (rule_tac x="s" in exI) - apply auto - apply (erule_tac x=y in allE) - apply auto - done - -lemma real_le_lsqrt: "0 <= x \ 0 <= y \ x <= y^2 ==> sqrt x <= y" - using real_sqrt_le_iff[of x "y^2"] by simp - -lemma real_le_rsqrt: "x^2 \ y \ x \ sqrt y" - using real_sqrt_le_mono[of "x^2" y] by simp - -lemma real_less_rsqrt: "x^2 < y \ x < sqrt y" - using real_sqrt_less_mono[of "x^2" y] by simp - -lemma sqrt_even_pow2: assumes n: "even n" - shows "sqrt(2 ^ n) = 2 ^ (n div 2)" -proof- - from n obtain m where m: "n = 2*m" unfolding even_mult_two_ex .. - from m have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)" - by (simp only: power_mult[symmetric] mult_commute) - then show ?thesis using m by simp -qed - -lemma real_div_sqrt: "0 <= x ==> x / sqrt(x) = sqrt(x)" - apply (cases "x = 0", simp_all) - using sqrt_divide_self_eq[of x] - apply (simp add: inverse_eq_divide field_simps) - done - -text{* Hence derive more interesting properties of the norm. *} - -(* FIXME: same as norm_scaleR -lemma norm_mul[simp]: "norm(a *\<^sub>R x) = abs(a) * norm x" - by (simp add: norm_vector_def setL2_right_distrib abs_mult) -*) - -lemma norm_eq_0_dot: "(norm x = 0) \ (inner x x = (0::real))" - by (simp add: setL2_def power2_eq_square) - -lemma norm_cauchy_schwarz: - shows "inner x y <= norm x * norm y" - using Cauchy_Schwarz_ineq2[of x y] by auto - -lemma norm_cauchy_schwarz_abs: - shows "\inner x y\ \ norm x * norm y" - by (rule Cauchy_Schwarz_ineq2) - -lemma norm_triangle_sub: - fixes x y :: "'a::real_normed_vector" - shows "norm x \ norm y + norm (x - y)" - using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps) - -lemma real_abs_norm: "\norm x\ = norm x" - by (rule abs_norm_cancel) -lemma real_abs_sub_norm: "\norm x - norm y\ <= norm(x - y)" - by (rule norm_triangle_ineq3) -lemma norm_le: "norm(x) <= norm(y) \ x \ x <= y \ y" - by (simp add: norm_eq_sqrt_inner) -lemma norm_lt: "norm(x) < norm(y) \ x \ x < y \ y" - by (simp add: norm_eq_sqrt_inner) -lemma norm_eq: "norm(x) = norm (y) \ x \ x = y \ y" - apply(subst order_eq_iff) unfolding norm_le by auto -lemma norm_eq_1: "norm(x) = 1 \ x \ x = 1" - unfolding norm_eq_sqrt_inner by auto - -text{* Squaring equations and inequalities involving norms. *} - -lemma dot_square_norm: "x \ x = norm(x)^2" - by (simp add: norm_eq_sqrt_inner) - -lemma norm_eq_square: "norm(x) = a \ 0 <= a \ x \ x = a^2" - by (auto simp add: norm_eq_sqrt_inner) - -lemma real_abs_le_square_iff: "\x\ \ \y\ \ (x::real)^2 \ y^2" -proof - assume "\x\ \ \y\" - then have "\x\\ \ \y\\" by (rule power_mono, simp) - then show "x\ \ y\" by simp -next - assume "x\ \ y\" - then have "sqrt (x\) \ sqrt (y\)" by (rule real_sqrt_le_mono) - then show "\x\ \ \y\" by simp -qed - -lemma norm_le_square: "norm(x) <= a \ 0 <= a \ x \ x <= a^2" - apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) - using norm_ge_zero[of x] - apply arith - done - -lemma norm_ge_square: "norm(x) >= a \ a <= 0 \ x \ x >= a ^ 2" - apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) - using norm_ge_zero[of x] - apply arith - done - -lemma norm_lt_square: "norm(x) < a \ 0 < a \ x \ x < a^2" - by (metis not_le norm_ge_square) -lemma norm_gt_square: "norm(x) > a \ a < 0 \ x \ x > a^2" - by (metis norm_le_square not_less) - -text{* Dot product in terms of the norm rather than conversely. *} - -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 \ y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2" - unfolding power2_norm_eq_inner inner_simps inner_commute by auto - -lemma dot_norm_neg: "x \ y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2" - unfolding power2_norm_eq_inner inner_simps inner_commute by(auto simp add:algebra_simps) - -text{* Equality of vectors in terms of @{term "op \"} products. *} - -lemma vector_eq: "x = y \ x \ x = x \ y \ y \ y = x \ x" (is "?lhs \ ?rhs") -proof - assume ?lhs then show ?rhs by simp -next - assume ?rhs - then have "x \ x - x \ y = 0 \ x \ y - y \ y = 0" by simp - hence "x \ (x - y) = 0 \ y \ (x - y) = 0" by (simp add: inner_simps inner_commute) - then have "(x - y) \ (x - y) = 0" by (simp add: field_simps inner_simps inner_commute) - then show "x = y" by (simp) -qed - -subsection{* General linear decision procedure for normed spaces. *} - -lemma norm_cmul_rule_thm: - fixes x :: "'a::real_normed_vector" - shows "b >= norm(x) ==> \c\ * b >= norm(scaleR c x)" - unfolding norm_scaleR - apply (erule mult_left_mono) - apply simp - done - - (* FIXME: Move all these theorems into the ML code using lemma antiquotation *) -lemma norm_add_rule_thm: - fixes x1 x2 :: "'a::real_normed_vector" - shows "norm x1 \ b1 \ norm x2 \ b2 \ norm (x1 + x2) \ b1 + b2" - by (rule order_trans [OF norm_triangle_ineq add_mono]) - -lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \ b == a - b \ 0" - by (simp add: field_simps) - -lemma pth_1: - fixes x :: "'a::real_normed_vector" - shows "x == scaleR 1 x" by simp - -lemma pth_2: - fixes x :: "'a::real_normed_vector" - shows "x - y == x + -y" by (atomize (full)) simp - -lemma pth_3: - fixes x :: "'a::real_normed_vector" - shows "- x == scaleR (-1) x" by simp - -lemma pth_4: - fixes x :: "'a::real_normed_vector" - shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all - -lemma pth_5: - fixes x :: "'a::real_normed_vector" - shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp - -lemma pth_6: - fixes x :: "'a::real_normed_vector" - shows "scaleR c (x + y) == scaleR c x + scaleR c y" - by (simp add: scaleR_right_distrib) - -lemma pth_7: - fixes x :: "'a::real_normed_vector" - shows "0 + x == x" and "x + 0 == x" by simp_all - -lemma pth_8: - fixes x :: "'a::real_normed_vector" - shows "scaleR c x + scaleR d x == scaleR (c + d) x" - by (simp add: scaleR_left_distrib) - -lemma pth_9: - fixes x :: "'a::real_normed_vector" shows - "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z" - "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z" - "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)" - by (simp_all add: algebra_simps) - -lemma pth_a: - fixes x :: "'a::real_normed_vector" - shows "scaleR 0 x + y == y" by simp - -lemma pth_b: - fixes x :: "'a::real_normed_vector" shows - "scaleR c x + scaleR d y == scaleR c x + scaleR d y" - "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)" - "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)" - "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))" - by (simp_all add: algebra_simps) - -lemma pth_c: - fixes x :: "'a::real_normed_vector" shows - "scaleR c x + scaleR d y == scaleR d y + scaleR c x" - "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)" - "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)" - "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)" - by (simp_all add: algebra_simps) - -lemma pth_d: - fixes x :: "'a::real_normed_vector" - shows "x + 0 == x" by simp - -lemma norm_imp_pos_and_ge: - fixes x :: "'a::real_normed_vector" - shows "norm x == n \ norm x \ 0 \ n \ norm x" - by atomize auto - -lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \ 0 \ -x \ 0" by arith - -lemma norm_pths: - fixes x :: "'a::real_normed_vector" shows - "x = y \ norm (x - y) \ 0" - "x \ y \ \ (norm (x - y) \ 0)" - using norm_ge_zero[of "x - y"] by auto - -use "normarith.ML" - -method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) -*} "prove simple linear statements about vector norms" - - -text{* Hence more metric properties. *} - -lemma norm_triangle_half_r: - shows "norm (y - x1) < e / 2 \ norm (y - x2) < e / 2 \ norm (x1 - x2) < e" - using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto - -lemma norm_triangle_half_l: assumes "norm (x - y) < e / 2" "norm (x' - (y)) < e / 2" - shows "norm (x - x') < e" - using dist_triangle_half_l[OF assms[unfolded dist_norm[THEN sym]]] - unfolding dist_norm[THEN sym] . - -lemma norm_triangle_le: "norm(x) + norm y <= e ==> norm(x + y) <= e" - by (metis order_trans norm_triangle_ineq) - -lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e" - by (metis basic_trans_rules(21) norm_triangle_ineq) - -lemma dist_triangle_add: - fixes x y x' y' :: "'a::real_normed_vector" - shows "dist (x + y) (x' + y') <= dist x x' + dist y y'" - by norm - -lemma dist_triangle_add_half: - fixes x x' y y' :: "'a::real_normed_vector" - shows "dist x x' < e / 2 \ dist y y' < e / 2 \ dist(x + y) (x' + y') < e" - by norm - -lemma setsum_clauses: - shows "setsum f {} = 0" - and "finite S \ setsum f (insert x S) = - (if x \ S then setsum f S else f x + setsum f S)" - by (auto simp add: insert_absorb) - -lemma setsum_norm: - fixes f :: "'a \ 'b::real_normed_vector" - assumes fS: "finite S" - shows "norm (setsum f S) <= setsum (\x. norm(f x)) S" -proof(induct rule: finite_induct[OF fS]) - case 1 thus ?case by simp -next - case (2 x S) - from "2.hyps" have "norm (setsum f (insert x S)) \ norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq) - also have "\ \ norm (f x) + setsum (\x. norm(f x)) S" - using "2.hyps" by simp - finally show ?case using "2.hyps" by simp -qed - -lemma setsum_norm_le: - fixes f :: "'a \ 'b::real_normed_vector" - assumes fS: "finite S" - and fg: "\x \ S. norm (f x) \ g x" - shows "norm (setsum f S) \ setsum g S" -proof- - from fg have "setsum (\x. norm(f x)) S <= setsum g S" - by - (rule setsum_mono, simp) - then show ?thesis using setsum_norm[OF fS, of f] fg - by arith -qed - -lemma setsum_norm_bound: - fixes f :: "'a \ 'b::real_normed_vector" - assumes fS: "finite S" - and K: "\x \ S. norm (f x) \ K" - shows "norm (setsum f S) \ of_nat (card S) * K" - using setsum_norm_le[OF fS K] setsum_constant[symmetric] - by simp - -lemma setsum_group: - assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \ T" - shows "setsum (\y. setsum g {x. x\ S \ f x = y}) T = setsum g S" - apply (subst setsum_image_gen[OF fS, of g f]) - apply (rule setsum_mono_zero_right[OF fT fST]) - by (auto intro: setsum_0') - -lemma dot_lsum: "finite S \ setsum f S \ y = setsum (\x. f x \ y) S " - apply(induct rule: finite_induct) by(auto simp add: inner_simps) - -lemma dot_rsum: "finite S \ y \ setsum f S = setsum (\x. y \ f x) S " - apply(induct rule: finite_induct) by(auto simp add: inner_simps) - -lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = z" -proof - assume "\x. x \ y = x \ z" - hence "\x. x \ (y - z) = 0" by (simp add: inner_simps) - hence "(y - z) \ (y - z) = 0" .. - thus "y = z" by simp -qed simp - -lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ x = y" -proof - assume "\z. x \ z = y \ z" - hence "\z. (x - y) \ z = 0" by (simp add: inner_simps) - hence "(x - y) \ (x - y) = 0" .. - thus "x = y" by simp -qed simp - -subsection{* Orthogonality. *} - -context real_inner + "~~/src/HOL/Library/Product_Vector" begin -definition "orthogonal x y \ (x \ y = 0)" - -lemma orthogonal_clauses: - "orthogonal a 0" - "orthogonal a x \ orthogonal a (c *\<^sub>R x)" - "orthogonal a x \ orthogonal a (-x)" - "orthogonal a x \ orthogonal a y \ orthogonal a (x + y)" - "orthogonal a x \ orthogonal a y \ orthogonal a (x - y)" - "orthogonal 0 a" - "orthogonal x a \ orthogonal (c *\<^sub>R x) a" - "orthogonal x a \ orthogonal (-x) a" - "orthogonal x a \ orthogonal y a \ orthogonal (x + y) a" - "orthogonal x a \ orthogonal y a \ orthogonal (x - y) a" - unfolding orthogonal_def inner_simps inner_add_left inner_add_right inner_diff_left inner_diff_right (*FIXME*) by auto - -end - -lemma orthogonal_commute: "orthogonal x y \ orthogonal y x" - by (simp add: orthogonal_def inner_commute) - -subsection{* Linear functions. *} - -definition - linear :: "('a::real_vector \ 'b::real_vector) \ bool" where - "linear f \ (\x y. f(x + y) = f x + f y) \ (\c x. f(c *\<^sub>R x) = c *\<^sub>R f x)" - -lemma linearI: assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" - shows "linear f" using assms unfolding linear_def by auto - -lemma linear_compose_cmul: "linear f ==> linear (\x. c *\<^sub>R f x)" - by (simp add: linear_def algebra_simps) - -lemma linear_compose_neg: "linear f ==> linear (\x. -(f(x)))" - by (simp add: linear_def) - -lemma linear_compose_add: "linear f \ linear g ==> linear (\x. f(x) + g(x))" - by (simp add: linear_def algebra_simps) - -lemma linear_compose_sub: "linear f \ linear g ==> linear (\x. f x - g x)" - by (simp add: linear_def algebra_simps) - -lemma linear_compose: "linear f \ linear g ==> linear (g o f)" - by (simp add: linear_def) - -lemma linear_id: "linear id" by (simp add: linear_def id_def) - -lemma linear_zero: "linear (\x. 0)" by (simp add: linear_def) - -lemma linear_compose_setsum: - assumes fS: "finite S" and lS: "\a \ S. linear (f a)" - shows "linear(\x. setsum (\a. f a x) S)" - using lS - apply (induct rule: finite_induct[OF fS]) - by (auto simp add: linear_zero intro: linear_compose_add) - -lemma linear_0: "linear f \ f 0 = 0" - unfolding linear_def - apply clarsimp - apply (erule allE[where x="0::'a"]) - apply simp - done - -lemma linear_cmul: "linear f ==> f(c *\<^sub>R x) = c *\<^sub>R f x" by (simp add: linear_def) - -lemma linear_neg: "linear f ==> f (-x) = - f x" - using linear_cmul [where c="-1"] by simp - -lemma linear_add: "linear f ==> f(x + y) = f x + f y" by (metis linear_def) - -lemma linear_sub: "linear f ==> f(x - y) = f x - f y" - by (simp add: diff_minus linear_add linear_neg) - -lemma linear_setsum: - assumes lf: "linear f" and fS: "finite S" - shows "f (setsum g S) = setsum (f o g) S" -proof (induct rule: finite_induct[OF fS]) - case 1 thus ?case by (simp add: linear_0[OF lf]) -next - case (2 x F) - have "f (setsum g (insert x F)) = f (g x + setsum g F)" using "2.hyps" - by simp - also have "\ = f (g x) + f (setsum g F)" using linear_add[OF lf] by simp - also have "\ = setsum (f o g) (insert x F)" using "2.hyps" by simp - finally show ?case . -qed - -lemma linear_setsum_mul: - assumes lf: "linear f" and fS: "finite S" - shows "f (setsum (\i. c i *\<^sub>R v i) S) = setsum (\i. c i *\<^sub>R f (v i)) S" - using linear_setsum[OF lf fS, of "\i. c i *\<^sub>R v i" , unfolded o_def] - linear_cmul[OF lf] by simp - -lemma linear_injective_0: - assumes lf: "linear f" - shows "inj f \ (\x. f x = 0 \ x = 0)" -proof- - have "inj f \ (\ x y. f x = f y \ x = y)" by (simp add: inj_on_def) - also have "\ \ (\ x y. f x - f y = 0 \ x - y = 0)" by simp - also have "\ \ (\ x y. f (x - y) = 0 \ x - y = 0)" - by (simp add: linear_sub[OF lf]) - also have "\ \ (\ x. f x = 0 \ x = 0)" by auto - finally show ?thesis . -qed - -subsection{* Bilinear functions. *} - -definition "bilinear f \ (\x. linear(\y. f x y)) \ (\y. linear(\x. f x y))" - -lemma bilinear_ladd: "bilinear h ==> h (x + y) z = (h x z) + (h y z)" - by (simp add: bilinear_def linear_def) -lemma bilinear_radd: "bilinear h ==> h x (y + z) = (h x y) + (h x z)" - by (simp add: bilinear_def linear_def) - -lemma bilinear_lmul: "bilinear h ==> h (c *\<^sub>R x) y = c *\<^sub>R (h x y)" - by (simp add: bilinear_def linear_def) - -lemma bilinear_rmul: "bilinear h ==> h x (c *\<^sub>R y) = c *\<^sub>R (h x y)" - by (simp add: bilinear_def linear_def) - -lemma bilinear_lneg: "bilinear h ==> h (- x) y = -(h x y)" - by (simp only: scaleR_minus1_left [symmetric] bilinear_lmul) - -lemma bilinear_rneg: "bilinear h ==> h x (- y) = - h x y" - by (simp only: scaleR_minus1_left [symmetric] bilinear_rmul) - -lemma (in ab_group_add) eq_add_iff: "x = x + y \ y = 0" - using add_imp_eq[of x y 0] by auto - -lemma bilinear_lzero: - assumes bh: "bilinear h" shows "h 0 x = 0" - using bilinear_ladd[OF bh, of 0 0 x] - by (simp add: eq_add_iff field_simps) - -lemma bilinear_rzero: - assumes bh: "bilinear h" shows "h x 0 = 0" - using bilinear_radd[OF bh, of x 0 0 ] - by (simp add: eq_add_iff field_simps) - -lemma bilinear_lsub: "bilinear h ==> h (x - y) z = h x z - h y z" - by (simp add: diff_minus bilinear_ladd bilinear_lneg) - -lemma bilinear_rsub: "bilinear h ==> h z (x - y) = h z x - h z y" - by (simp add: diff_minus bilinear_radd 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 (\(i,j). h (f i) (g j)) (S \ T) " -proof- - have "h (setsum f S) (setsum g T) = setsum (\x. h (f x) (setsum g T)) S" - apply (rule linear_setsum[unfolded o_def]) - using bh fS by (auto simp add: bilinear_def) - also have "\ = setsum (\x. setsum (\y. h (f x) (g y)) T) S" - apply (rule setsum_cong, simp) - apply (rule linear_setsum[unfolded o_def]) - using bh fT by (auto simp add: bilinear_def) - finally show ?thesis unfolding setsum_cartesian_product . -qed - -subsection{* Adjoints. *} - -definition "adjoint f = (SOME f'. \x y. f x \ y = x \ f' y)" - -lemma adjoint_unique: - assumes "\x y. inner (f x) y = inner x (g y)" - shows "adjoint f = g" -unfolding adjoint_def -proof (rule some_equality) - show "\x y. inner (f x) y = inner x (g y)" using assms . -next - fix h assume "\x y. inner (f x) y = inner x (h y)" - hence "\x y. inner x (g y) = inner x (h y)" using assms by simp - hence "\x y. inner x (g y - h y) = 0" by (simp add: inner_diff_right) - hence "\y. inner (g y - h y) (g y - h y) = 0" by simp - hence "\y. h y = g y" by simp - thus "h = g" by (simp add: ext) -qed - -lemma choice_iff: "(\x. \y. P x y) \ (\f. \x. P x (f x))" by metis - -subsection{* Interlude: Some properties of real sets *} - -lemma seq_mono_lemma: assumes "\(n::nat) \ m. (d n :: real) < e n" and "\n \ m. e n <= e m" - shows "\n \ 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 "\r. subseq r \ (\n. r n \ S)" -unfolding subseq_def -using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto - -lemma approachable_lt_le: "(\(d::real)>0. \x. f x < d \ P x) \ (\d>0. \x. f x \ d \ P x)" -apply auto -apply (rule_tac x="d/2" in exI) -apply auto -done - - -lemma triangle_lemma: - assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x^2 <= y^2 + z^2" - shows "x <= y + z" -proof- - have "y^2 + z^2 \ y^2 + 2*y*z + z^2" using z y by (simp add: mult_nonneg_nonneg) - with xy have th: "x ^2 \ (y+z)^2" by (simp add: power2_eq_square field_simps) - from y z have yz: "y + z \ 0" by arith - from power2_le_imp_le[OF th yz] show ?thesis . -qed - -text {* TODO: move to NthRoot *} -lemma sqrt_add_le_add_sqrt: - assumes x: "0 \ x" and y: "0 \ y" - shows "sqrt (x + y) \ sqrt x + sqrt y" -apply (rule power2_le_imp_le) -apply (simp add: real_sum_squared_expand add_nonneg_nonneg x y) -apply (simp add: mult_nonneg_nonneg x y) -apply (simp add: add_nonneg_nonneg x y) -done - -subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *} - -definition hull :: "'a set set \ 'a set \ 'a set" (infixl "hull" 75) where - "S hull s = Inter {t. t \ S \ s \ t}" - -lemma hull_same: "s \ S \ S hull s = s" - unfolding hull_def by auto - -lemma hull_in: "(\T. T \ S ==> Inter T \ S) ==> (S hull s) \ S" -unfolding hull_def subset_iff by auto - -lemma hull_eq: "(\T. T \ S ==> Inter T \ S) ==> (S hull s) = s \ s \ S" -using hull_same[of s S] hull_in[of S s] by metis - - -lemma hull_hull: "S hull (S hull s) = S hull s" - unfolding hull_def by blast - -lemma hull_subset[intro]: "s \ (S hull s)" - unfolding hull_def by blast - -lemma hull_mono: " s \ t ==> (S hull s) \ (S hull t)" - unfolding hull_def by blast - -lemma hull_antimono: "S \ T ==> (T hull s) \ (S hull s)" - unfolding hull_def by blast - -lemma hull_minimal: "s \ t \ t \ S ==> (S hull s) \ t" - unfolding hull_def by blast - -lemma subset_hull: "t \ S ==> S hull s \ t \ s \ t" - unfolding hull_def by blast - -lemma hull_unique: "s \ t \ t \ S \ (\t'. s \ t' \ t' \ S ==> t \ t') - ==> (S hull s = t)" -unfolding hull_def by auto - -lemma hull_induct: "(\x. x\ S \ P x) \ Q {x. P x} \ \x\ Q hull S. P x" - using hull_minimal[of S "{x. P x}" Q] - by (auto simp add: subset_eq Collect_def mem_def) - -lemma hull_inc: "x \ S \ x \ P hull S" by (metis hull_subset subset_eq) - -lemma hull_union_subset: "(S hull s) \ (S hull t) \ (S hull (s \ t))" -unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2) - -lemma hull_union: assumes T: "\T. T \ S ==> Inter T \ S" - shows "S hull (s \ t) = S hull (S hull s \ 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 \ (S hull s) \ (S hull (insert a s) = S hull s)" - unfolding hull_def by blast - -lemma hull_redundant: "a \ (S hull s) ==> (S hull (insert a s) = S hull s)" -by (metis hull_redundant_eq) - -text{* Archimedian properties and useful consequences. *} - -lemma real_arch_simple: "\n. x <= real (n::nat)" - using reals_Archimedean2[of x] apply auto by (rule_tac x="Suc n" in exI, auto) -lemmas real_arch_lt = reals_Archimedean2 - -lemmas real_arch = reals_Archimedean3 - -lemma real_arch_inv: "0 < e \ (\n::nat. n \ 0 \ 0 < inverse (real n) \ inverse (real n) < e)" - using reals_Archimedean - apply (auto simp add: field_simps) - apply (subgoal_tac "inverse (real n) > 0") - apply arith - apply simp - done - -lemma real_pow_lbound: "0 <= x ==> 1 + real n * x <= (1 + x) ^ n" -proof(induct n) - case 0 thus ?case by simp -next - case (Suc n) - hence h: "1 + real n * x \ (1 + x) ^ n" by simp - from h have p: "1 \ (1 + x) ^ n" using Suc.prems by simp - from h have "1 + real n * x + x \ (1 + x) ^ n + x" by simp - also have "\ \ (1 + x) ^ Suc n" apply (subst diff_le_0_iff_le[symmetric]) - apply (simp add: field_simps) - using mult_left_mono[OF p Suc.prems] by simp - finally show ?case by (simp add: real_of_nat_Suc field_simps) -qed - -lemma real_arch_pow: assumes x: "1 < (x::real)" shows "\n. y < x^n" -proof- - from x have x0: "x - 1 > 0" by arith - from real_arch[OF x0, rule_format, of y] - obtain n::nat where n:"y < real n * (x - 1)" by metis - from x0 have x00: "x- 1 \ 0" by arith - from real_pow_lbound[OF x00, of n] n - have "y < x^n" by auto - then show ?thesis by metis -qed - -lemma real_arch_pow2: "\n. (x::real) < 2^ n" - using real_arch_pow[of 2 x] by simp - -lemma real_arch_pow_inv: assumes y: "(y::real) > 0" and x1: "x < 1" - shows "\n. x^n < y" -proof- - {assume x0: "x > 0" - from x0 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 - have ?thesis using y x0 by (auto simp add: field_simps power_divide) } - moreover - {assume "\ x > 0" with y x1 have ?thesis apply auto by (rule exI[where x=1], auto)} - ultimately show ?thesis by metis -qed - -lemma forall_pos_mono: "(\d e::real. d < e \ P d ==> P e) \ (\n::nat. n \ 0 ==> P(inverse(real n))) \ (\e. 0 < e ==> P e)" - by (metis real_arch_inv) - -lemma forall_pos_mono_1: "(\d e::real. d < e \ P d ==> P e) \ (\n. P(inverse(real (Suc n)))) ==> 0 < e ==> P e" - apply (rule forall_pos_mono) - apply auto - apply (atomize) - apply (erule_tac x="n - 1" in allE) - apply auto - done - -lemma real_archimedian_rdiv_eq_0: assumes x0: "x \ 0" and c: "c \ 0" and xc: "\(m::nat)>0. real m * x \ c" - shows "x = 0" -proof- - {assume "x \ 0" with x0 have xp: "x > 0" by arith - from real_arch[OF xp, rule_format, of c] obtain n::nat where n: "c < real n * x" by blast - with xc[rule_format, of n] have "n = 0" by arith - with n c have False by simp} - then show ?thesis by blast -qed - -subsection {* Geometric progression *} - -lemma sum_gp_basic: "((1::'a::{field}) - x) * setsum (\i. x^i) {0 .. n} = (1 - x^(Suc n))" - (is "?lhs = ?rhs") -proof- - {assume x1: "x = 1" hence ?thesis by simp} - moreover - {assume x1: "x\1" - hence x1': "x - 1 \ 0" "1 - x \ 0" "x - 1 = - (1 - x)" "- (1 - x) \ 0" by auto - from geometric_sum[OF x1, of "Suc n", unfolded x1'] - have "(- (1 - x)) * setsum (\i. x^i) {0 .. n} = - (1 - x^(Suc n))" - unfolding atLeastLessThanSuc_atLeastAtMost - using x1' apply (auto simp only: field_simps) - apply (simp add: field_simps) - done - then have ?thesis by (simp add: field_simps) } - ultimately show ?thesis by metis -qed - -lemma sum_gp_multiplied: assumes mn: "m <= n" - shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n" - (is "?lhs = ?rhs") -proof- - let ?S = "{0..(n - m)}" - from mn have mn': "n - m \ 0" by arith - let ?f = "op + m" - have i: "inj_on ?f ?S" unfolding inj_on_def by auto - have f: "?f ` ?S = {m..n}" - using mn apply (auto simp add: image_iff Bex_def) by arith - have th: "op ^ x o op + m = (\i. x^m * x^i)" - by (rule ext, simp add: power_add power_mult) - from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]] - have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp - then show ?thesis unfolding sum_gp_basic using mn - by (simp add: field_simps power_add[symmetric]) -qed - -lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} = - (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m) - else (x^ m - x^ (Suc n)) / (1 - x))" -proof- - {assume nm: "n < m" hence ?thesis by simp} - moreover - {assume "\ n < m" hence nm: "m \ n" by arith - {assume x: "x = 1" hence ?thesis by simp} - moreover - {assume x: "x \ 1" hence nz: "1 - x \ 0" by simp - from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)} - ultimately have ?thesis by metis - } - ultimately show ?thesis by metis -qed - -lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} = - (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))" - unfolding sum_gp[of x m "m + n"] power_Suc - by (simp add: field_simps power_add) - - -subsection{* A bit of linear algebra. *} - -definition (in real_vector) - subspace :: "'a set \ bool" where - "subspace S \ 0 \ S \ (\x\ S. \y \S. x + y \ S) \ (\c. \x \S. c *\<^sub>R x \S )" - -definition (in real_vector) "span S = (subspace hull S)" -definition (in real_vector) "dependent S \ (\a \ S. a \ span(S - {a}))" -abbreviation (in real_vector) "independent s == ~(dependent s)" - -text {* Closure properties of subspaces. *} - -lemma subspace_UNIV[simp]: "subspace(UNIV)" by (simp add: subspace_def) - -lemma (in real_vector) subspace_0: "subspace S ==> 0 \ S" by (metis subspace_def) - -lemma (in real_vector) subspace_add: "subspace S \ x \ S \ y \ S ==> x + y \ S" - by (metis subspace_def) - -lemma (in real_vector) subspace_mul: "subspace S \ x \ S \ c *\<^sub>R x \ S" - by (metis subspace_def) - -lemma subspace_neg: "subspace S \ x \ S \ - x \ S" - by (metis scaleR_minus1_left subspace_mul) - -lemma subspace_sub: "subspace S \ x \ S \ y \ S \ x - y \ S" - by (metis diff_minus subspace_add subspace_neg) - -lemma (in real_vector) subspace_setsum: - assumes sA: "subspace A" and fB: "finite B" - and f: "\x\ B. f x \ A" - shows "setsum f B \ A" - using fB f sA - apply(induct rule: finite_induct[OF fB]) - by (simp add: subspace_def sA, auto simp add: sA subspace_add) - -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_def subspace_def - apply (auto simp add: image_iff) - apply (rule_tac x="x + y" in bexI, auto) - apply (rule_tac x="c *\<^sub>R x" in bexI, auto) - done - -lemma subspace_linear_preimage: "linear f ==> subspace S ==> subspace {x. f x \ S}" - by (auto simp add: subspace_def linear_def linear_0[of f]) - -lemma subspace_trivial: "subspace {0}" - by (simp add: subspace_def) - -lemma (in real_vector) subspace_inter: "subspace A \ subspace B ==> subspace (A \ B)" - by (simp add: subspace_def) - -lemma (in real_vector) span_mono: "A \ B ==> span A \ span B" - by (metis span_def hull_mono) - -lemma (in real_vector) subspace_span: "subspace(span S)" - unfolding span_def - apply (rule hull_in[unfolded mem_def]) - apply (simp only: subspace_def Inter_iff Int_iff subset_eq) - apply auto - apply (erule_tac x="X" in ballE) - apply (simp add: mem_def) - apply blast - apply (erule_tac x="X" in ballE) - apply (erule_tac x="X" in ballE) - apply (erule_tac x="X" in ballE) - apply (clarsimp simp add: mem_def) - apply simp - apply simp - apply simp - apply (erule_tac x="X" in ballE) - apply (erule_tac x="X" in ballE) - apply (simp add: mem_def) - apply simp - apply simp - done - -lemma (in real_vector) span_clauses: - "a \ S ==> a \ span S" - "0 \ span S" - "x\ span S \ y \ span S ==> x + y \ span S" - "x \ span S \ c *\<^sub>R x \ span S" - by (metis span_def hull_subset subset_eq) - (metis subspace_span subspace_def)+ - -lemma (in real_vector) span_induct: assumes SP: "\x. x \ S ==> P x" - and P: "subspace P" and x: "x \ span S" shows "P x" -proof- - from SP have SP': "S \ P" by (simp add: mem_def subset_eq) - from P have P': "P \ subspace" by (simp add: mem_def) - from x hull_minimal[OF SP' P', unfolded span_def[symmetric]] - show "P x" by (metis mem_def subset_eq) -qed - -lemma span_empty[simp]: "span {} = {0}" - apply (simp add: span_def) - apply (rule hull_unique) - apply (auto simp add: mem_def subspace_def) - unfolding mem_def[of "0::'a", symmetric] - apply simp - done - -lemma (in real_vector) independent_empty[intro]: "independent {}" - by (simp add: dependent_def) - -lemma dependent_single[simp]: - "dependent {x} \ x = 0" - unfolding dependent_def by auto - -lemma (in real_vector) independent_mono: "independent A \ B \ A ==> independent B" - apply (clarsimp simp add: dependent_def span_mono) - apply (subgoal_tac "span (B - {a}) \ span (A - {a})") - apply force - apply (rule span_mono) - apply auto - done - -lemma (in real_vector) span_subspace: "A \ B \ B \ span A \ subspace B \ span A = B" - by (metis order_antisym span_def hull_minimal mem_def) - -lemma (in real_vector) span_induct': assumes SP: "\x \ S. P x" - and P: "subspace P" shows "\x \ span S. P x" - using span_induct SP P by blast - -inductive (in real_vector) span_induct_alt_help for S:: "'a \ bool" - where - span_induct_alt_help_0: "span_induct_alt_help S 0" - | span_induct_alt_help_S: "x \ S \ span_induct_alt_help S z \ span_induct_alt_help S (c *\<^sub>R x + z)" - -lemma span_induct_alt': - assumes h0: "h 0" and hS: "\c x y. x \ S \ h y \ h (c *\<^sub>R x + y)" shows "\x \ span S. h x" -proof- - {fix x:: "'a" assume x: "span_induct_alt_help S x" - have "h x" - apply (rule span_induct_alt_help.induct[OF x]) - apply (rule h0) - apply (rule hS, assumption, assumption) - done} - note th0 = this - {fix x assume x: "x \ span S" - - have "span_induct_alt_help S x" - proof(rule span_induct[where x=x and S=S]) - show "x \ span S" using x . - next - fix x assume xS : "x \ S" - from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1] - show "span_induct_alt_help S x" by simp - next - have "span_induct_alt_help S 0" by (rule span_induct_alt_help_0) - moreover - {fix x y assume h: "span_induct_alt_help S x" "span_induct_alt_help S y" - from h - have "span_induct_alt_help S (x + y)" - apply (induct rule: span_induct_alt_help.induct) - apply simp - unfolding add_assoc - apply (rule span_induct_alt_help_S) - apply assumption - apply simp - done} - moreover - {fix c x assume xt: "span_induct_alt_help S x" - then have "span_induct_alt_help S (c *\<^sub>R x)" - apply (induct rule: span_induct_alt_help.induct) - apply (simp add: span_induct_alt_help_0) - apply (simp add: scaleR_right_distrib) - apply (rule span_induct_alt_help_S) - apply assumption - apply simp - done - } - ultimately show "subspace (span_induct_alt_help S)" - unfolding subspace_def mem_def Ball_def by blast - qed} - with th0 show ?thesis by blast -qed - -lemma span_induct_alt: - assumes h0: "h 0" and hS: "\c x y. x \ S \ h y \ h (c *\<^sub>R x + y)" and x: "x \ span S" - shows "h x" -using span_induct_alt'[of h S] h0 hS x by blast - -text {* Individual closure properties. *} - -lemma span_span: "span (span A) = span A" - unfolding span_def hull_hull .. - -lemma (in real_vector) span_superset: "x \ S ==> x \ span S" by (metis span_clauses(1)) - -lemma (in real_vector) span_0: "0 \ span S" by (metis subspace_span subspace_0) - -lemma span_inc: "S \ span S" - by (metis subset_eq span_superset) - -lemma (in real_vector) dependent_0: assumes "0\A" shows "dependent A" - unfolding dependent_def apply(rule_tac x=0 in bexI) - using assms span_0 by auto - -lemma (in real_vector) span_add: "x \ span S \ y \ span S ==> x + y \ span S" - by (metis subspace_add subspace_span) - -lemma (in real_vector) span_mul: "x \ span S ==> (c *\<^sub>R x) \ span S" - by (metis subspace_span subspace_mul) - -lemma span_neg: "x \ span S ==> - x \ span S" - by (metis subspace_neg subspace_span) - -lemma span_sub: "x \ span S \ y \ span S ==> x - y \ span S" - by (metis subspace_span subspace_sub) - -lemma (in real_vector) span_setsum: "finite A \ \x \ A. f x \ span S ==> setsum f A \ span S" - by (rule subspace_setsum, rule subspace_span) - -lemma span_add_eq: "x \ span S \ x + y \ span S \ y \ span S" - apply (auto simp only: span_add span_sub) - apply (subgoal_tac "(x + y) - x \ span S", simp) - by (simp only: span_add span_sub) - -text {* Mapping under linear image. *} - -lemma span_linear_image: assumes lf: "linear f" - shows "span (f ` S) = f ` (span S)" -proof- - {fix x - assume x: "x \ span (f ` S)" - have "x \ f ` span S" - apply (rule span_induct[where x=x and S = "f ` S"]) - apply (clarsimp simp add: image_iff) - apply (frule span_superset) - apply blast - apply (simp only: mem_def) - apply (rule subspace_linear_image[OF lf]) - apply (rule subspace_span) - apply (rule x) - done} - moreover - {fix x assume x: "x \ span S" - have th0:"(\a. f a \ span (f ` S)) = {x. f x \ span (f ` S)}" apply (rule set_eqI) - unfolding mem_def Collect_def .. - have "f x \ span (f ` S)" - apply (rule span_induct[where S=S]) - apply (rule span_superset) - apply simp - apply (subst th0) - apply (rule subspace_linear_preimage[OF lf subspace_span, of "f ` S"]) - apply (rule x) - done} - ultimately show ?thesis by blast -qed - -text {* The key breakdown property. *} - -lemma span_breakdown: - assumes bS: "b \ S" and aS: "a \ span S" - shows "\k. a - k *\<^sub>R b \ span (S - {b})" (is "?P a") -proof- - {fix x assume xS: "x \ S" - {assume ab: "x = b" - then have "?P x" - apply simp - apply (rule exI[where x="1"], simp) - by (rule span_0)} - moreover - {assume ab: "x \ b" - then have "?P x" using xS - apply - - apply (rule exI[where x=0]) - apply (rule span_superset) - by simp} - ultimately have "?P x" by blast} - moreover have "subspace ?P" - unfolding subspace_def - apply auto - apply (simp add: mem_def) - apply (rule exI[where x=0]) - using span_0[of "S - {b}"] - apply (simp add: mem_def) - apply (clarsimp simp add: mem_def) - apply (rule_tac x="k + ka" in exI) - apply (subgoal_tac "x + y - (k + ka) *\<^sub>R b = (x - k*\<^sub>R b) + (y - ka *\<^sub>R b)") - apply (simp only: ) - apply (rule span_add[unfolded mem_def]) - apply assumption+ - apply (simp add: algebra_simps) - apply (clarsimp simp add: mem_def) - apply (rule_tac x= "c*k" in exI) - apply (subgoal_tac "c *\<^sub>R x - (c * k) *\<^sub>R b = c*\<^sub>R (x - k*\<^sub>R b)") - apply (simp only: ) - apply (rule span_mul[unfolded mem_def]) - apply assumption - by (simp add: algebra_simps) - ultimately show "?P a" using aS span_induct[where S=S and P= "?P"] by metis -qed - -lemma span_breakdown_eq: - "x \ span (insert a S) \ (\k. (x - k *\<^sub>R a) \ span S)" (is "?lhs \ ?rhs") -proof- - {assume x: "x \ span (insert a S)" - from x span_breakdown[of "a" "insert a S" "x"] - have ?rhs apply clarsimp - apply (rule_tac x= "k" in exI) - apply (rule set_rev_mp[of _ "span (S - {a})" _]) - apply assumption - apply (rule span_mono) - apply blast - done} - moreover - { fix k assume k: "x - k *\<^sub>R a \ span S" - have eq: "x = (x - k *\<^sub>R a) + k *\<^sub>R a" by simp - have "(x - k *\<^sub>R a) + k *\<^sub>R a \ span (insert a S)" - apply (rule span_add) - apply (rule set_rev_mp[of _ "span S" _]) - apply (rule k) - apply (rule span_mono) - apply blast - apply (rule span_mul) - apply (rule span_superset) - apply blast - done - then have ?lhs using eq by metis} - ultimately show ?thesis by blast -qed - -text {* Hence some "reversal" results. *} - -lemma in_span_insert: - assumes a: "a \ span (insert b S)" and na: "a \ span S" - shows "b \ span (insert a S)" -proof- - from span_breakdown[of b "insert b S" a, OF insertI1 a] - obtain k where k: "a - k*\<^sub>R b \ span (S - {b})" by auto - {assume k0: "k = 0" - with k have "a \ span S" - apply (simp) - apply (rule set_rev_mp) - apply assumption - apply (rule span_mono) - apply blast - done - with na have ?thesis by blast} - moreover - {assume k0: "k \ 0" - have eq: "b = (1/k) *\<^sub>R a - ((1/k) *\<^sub>R a - b)" by simp - from k0 have eq': "(1/k) *\<^sub>R (a - k*\<^sub>R b) = (1/k) *\<^sub>R a - b" - by (simp add: algebra_simps) - from k have "(1/k) *\<^sub>R (a - k*\<^sub>R b) \ span (S - {b})" - by (rule span_mul) - hence th: "(1/k) *\<^sub>R a - b \ span (S - {b})" - unfolding eq' . - - from k - have ?thesis - apply (subst eq) - apply (rule span_sub) - apply (rule span_mul) - apply (rule span_superset) - apply blast - apply (rule set_rev_mp) - apply (rule th) - apply (rule span_mono) - using na by blast} - ultimately show ?thesis by blast -qed - -lemma in_span_delete: - assumes a: "a \ span S" - and na: "a \ span (S-{b})" - shows "b \ span (insert a (S - {b}))" - apply (rule in_span_insert) - apply (rule set_rev_mp) - apply (rule a) - apply (rule span_mono) - apply blast - apply (rule na) - done - -text {* Transitivity property. *} - -lemma span_trans: - assumes x: "x \ span S" and y: "y \ span (insert x S)" - shows "y \ span S" -proof- - from span_breakdown[of x "insert x S" y, OF insertI1 y] - obtain k where k: "y -k*\<^sub>R x \ span (S - {x})" by auto - have eq: "y = (y - k *\<^sub>R x) + k *\<^sub>R x" by simp - show ?thesis - apply (subst eq) - apply (rule span_add) - apply (rule set_rev_mp) - apply (rule k) - apply (rule span_mono) - apply blast - apply (rule span_mul) - by (rule x) -qed - -lemma span_insert_0[simp]: "span (insert 0 S) = span S" - using span_mono[of S "insert 0 S"] by (auto intro: span_trans span_0) - -text {* An explicit expansion is sometimes needed. *} - -lemma span_explicit: - "span P = {y. \S u. finite S \ S \ P \ setsum (\v. u v *\<^sub>R v) S = y}" - (is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \S u. ?Q S u y}") -proof- - {fix x assume x: "x \ ?E" - then obtain S u where fS: "finite S" and SP: "S\P" and u: "setsum (\v. u v *\<^sub>R v) S = x" - by blast - have "x \ span P" - unfolding u[symmetric] - apply (rule span_setsum[OF fS]) - using span_mono[OF SP] - by (auto intro: span_superset span_mul)} - moreover - have "\x \ span P. x \ ?E" - unfolding mem_def Collect_def - proof(rule span_induct_alt') - show "?h 0" - apply (rule exI[where x="{}"]) by simp - next - fix c x y - assume x: "x \ P" and hy: "?h y" - from hy obtain S u where fS: "finite S" and SP: "S\P" - and u: "setsum (\v. u v *\<^sub>R v) S = y" by blast - let ?S = "insert x S" - let ?u = "\y. if y = x then (if x \ S then u y + c else c) - else u y" - from fS SP x have th0: "finite (insert x S)" "insert x S \ P" by blast+ - {assume xS: "x \ S" - have S1: "S = (S - {x}) \ {x}" - and Sss:"finite (S - {x})" "finite {x}" "(S -{x}) \ {x} = {}" using xS fS by auto - have "setsum (\v. ?u v *\<^sub>R v) ?S =(\v\S - {x}. u v *\<^sub>R v) + (u x + c) *\<^sub>R x" - using xS - by (simp add: setsum_Un_disjoint[OF Sss, unfolded S1[symmetric]] - setsum_clauses(2)[OF fS] cong del: if_weak_cong) - also have "\ = (\v\S. u v *\<^sub>R v) + c *\<^sub>R x" - apply (simp add: setsum_Un_disjoint[OF Sss, unfolded S1[symmetric]]) - by (simp add: algebra_simps) - also have "\ = c*\<^sub>R x + y" - by (simp add: add_commute u) - finally have "setsum (\v. ?u v *\<^sub>R v) ?S = c*\<^sub>R x + y" . - then have "?Q ?S ?u (c*\<^sub>R x + y)" using th0 by blast} - moreover - {assume xS: "x \ S" - have th00: "(\v\S. (if v = x then c else u v) *\<^sub>R v) = y" - unfolding u[symmetric] - apply (rule setsum_cong2) - using xS by auto - have "?Q ?S ?u (c*\<^sub>R x + y)" using fS xS th0 - by (simp add: th00 setsum_clauses add_commute cong del: if_weak_cong)} - ultimately have "?Q ?S ?u (c*\<^sub>R x + y)" - by (cases "x \ S", simp, simp) - then show "?h (c*\<^sub>R x + y)" - apply - - apply (rule exI[where x="?S"]) - apply (rule exI[where x="?u"]) by metis - qed - ultimately show ?thesis by blast -qed - -lemma dependent_explicit: - "dependent P \ (\S u. finite S \ S \ P \ (\v\S. u v \ 0 \ setsum (\v. u v *\<^sub>R v) S = 0))" (is "?lhs = ?rhs") -proof- - {assume dP: "dependent P" - then obtain a S u where aP: "a \ P" and fS: "finite S" - and SP: "S \ P - {a}" and ua: "setsum (\v. u v *\<^sub>R v) S = a" - unfolding dependent_def span_explicit by blast - let ?S = "insert a S" - let ?u = "\y. if y = a then - 1 else u y" - let ?v = a - from aP SP have aS: "a \ S" by blast - from fS SP aP have th0: "finite ?S" "?S \ P" "?v \ ?S" "?u ?v \ 0" by auto - have s0: "setsum (\v. ?u v *\<^sub>R v) ?S = 0" - using fS aS - apply (simp add: setsum_clauses field_simps) - apply (subst (2) ua[symmetric]) - apply (rule setsum_cong2) - by auto - with th0 have ?rhs - apply - - apply (rule exI[where x= "?S"]) - apply (rule exI[where x= "?u"]) - by clarsimp} - moreover - {fix S u v assume fS: "finite S" - and SP: "S \ P" and vS: "v \ S" and uv: "u v \ 0" - and u: "setsum (\v. u v *\<^sub>R v) S = 0" - let ?a = v - let ?S = "S - {v}" - let ?u = "\i. (- u i) / u v" - have th0: "?a \ P" "finite ?S" "?S \ P" using fS SP vS by auto - have "setsum (\v. ?u v *\<^sub>R v) ?S = setsum (\v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v" - using fS vS uv - by (simp add: setsum_diff1 divide_inverse field_simps) - also have "\ = ?a" - unfolding scaleR_right.setsum [symmetric] u - using uv by simp - finally have "setsum (\v. ?u v *\<^sub>R v) ?S = ?a" . - with th0 have ?lhs - unfolding dependent_def span_explicit - apply - - apply (rule bexI[where x= "?a"]) - apply (simp_all del: scaleR_minus_left) - apply (rule exI[where x= "?S"]) - by (auto simp del: scaleR_minus_left)} - ultimately show ?thesis by blast -qed - - -lemma span_finite: - assumes fS: "finite S" - shows "span S = {y. \u. setsum (\v. u v *\<^sub>R v) S = y}" - (is "_ = ?rhs") -proof- - {fix y assume y: "y \ span S" - from y obtain S' u where fS': "finite S'" and SS': "S' \ S" and - u: "setsum (\v. u v *\<^sub>R v) S' = y" unfolding span_explicit by blast - let ?u = "\x. if x \ S' then u x else 0" - have "setsum (\v. ?u v *\<^sub>R v) S = setsum (\v. u v *\<^sub>R v) S'" - using SS' fS by (auto intro!: setsum_mono_zero_cong_right) - hence "setsum (\v. ?u v *\<^sub>R v) S = y" by (metis u) - hence "y \ ?rhs" by auto} - moreover - {fix y u assume u: "setsum (\v. u v *\<^sub>R v) S = y" - then have "y \ span S" using fS unfolding span_explicit by auto} - ultimately show ?thesis by blast -qed - -lemma Int_Un_cancel: "(A \ B) \ A = A" "(A \ B) \ B = B" by auto - -lemma span_union: "span (A \ B) = (\(a, b). a + b) ` (span A \ span B)" -proof safe - fix x assume "x \ span (A \ B)" - then obtain S u where S: "finite S" "S \ A \ B" and x: "x = (\v\S. u v *\<^sub>R v)" - unfolding span_explicit by auto - - let ?Sa = "\v\S\A. u v *\<^sub>R v" - let ?Sb = "(\v\S\(B - A). u v *\<^sub>R v)" - show "x \ (\(a, b). a + b) ` (span A \ span B)" - proof - show "x = (case (?Sa, ?Sb) of (a, b) \ a + b)" - unfolding x using S - by (simp, subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong) - - from S have "?Sa \ span A" unfolding span_explicit - by (auto intro!: exI[of _ "S \ A"]) - moreover from S have "?Sb \ span B" unfolding span_explicit - by (auto intro!: exI[of _ "S \ (B - A)"]) - ultimately show "(?Sa, ?Sb) \ span A \ span B" by simp - qed -next - fix a b assume "a \ span A" and "b \ span B" - then obtain Sa ua Sb ub where span: - "finite Sa" "Sa \ A" "a = (\v\Sa. ua v *\<^sub>R v)" - "finite Sb" "Sb \ B" "b = (\v\Sb. ub v *\<^sub>R v)" - unfolding span_explicit by auto - let "?u v" = "(if v \ Sa then ua v else 0) + (if v \ Sb then ub v else 0)" - from span have "finite (Sa \ Sb)" "Sa \ Sb \ A \ B" - and "a + b = (\v\(Sa\Sb). ?u v *\<^sub>R v)" - unfolding setsum_addf scaleR_left_distrib - by (auto simp add: if_distrib cond_application_beta setsum_cases Int_Un_cancel) - thus "a + b \ span (A \ B)" - unfolding span_explicit by (auto intro!: exI[of _ ?u]) -qed - -text {* This is useful for building a basis step-by-step. *} - -lemma independent_insert: - "independent(insert a S) \ - (if a \ S then independent S - else independent S \ a \ span S)" (is "?lhs \ ?rhs") -proof- - {assume aS: "a \ S" - hence ?thesis using insert_absorb[OF aS] by simp} - moreover - {assume aS: "a \ S" - {assume i: ?lhs - then have ?rhs using aS - apply simp - apply (rule conjI) - apply (rule independent_mono) - apply assumption - apply blast - by (simp add: dependent_def)} - moreover - {assume i: ?rhs - have ?lhs using i aS - apply simp - apply (auto simp add: dependent_def) - apply (case_tac "aa = a", auto) - apply (subgoal_tac "insert a S - {aa} = insert a (S - {aa})") - apply simp - apply (subgoal_tac "a \ span (insert aa (S - {aa}))") - apply (subgoal_tac "insert aa (S - {aa}) = S") - apply simp - apply blast - apply (rule in_span_insert) - apply assumption - apply blast - apply blast - done} - ultimately have ?thesis by blast} - ultimately show ?thesis by blast -qed - -text {* The degenerate case of the Exchange Lemma. *} - -lemma mem_delete: "x \ (A - {a}) \ x \ a \ x \ A" - by blast - -lemma spanning_subset_independent: - assumes BA: "B \ A" and iA: "independent A" - and AsB: "A \ span B" - shows "A = B" -proof - from BA show "B \ A" . -next - from span_mono[OF BA] span_mono[OF AsB] - have sAB: "span A = span B" unfolding span_span by blast - - {fix x assume x: "x \ A" - from iA have th0: "x \ span (A - {x})" - unfolding dependent_def using x by blast - from x have xsA: "x \ span A" by (blast intro: span_superset) - have "A - {x} \ A" by blast - hence th1:"span (A - {x}) \ span A" by (metis span_mono) - {assume xB: "x \ B" - from xB BA have "B \ A -{x}" by blast - hence "span B \ span (A - {x})" by (metis span_mono) - with th1 th0 sAB have "x \ span A" by blast - with x have False by (metis span_superset)} - then have "x \ B" by blast} - then show "A \ B" by blast -qed - -text {* The general case of the Exchange Lemma, the key to what follows. *} - -lemma exchange_lemma: - assumes f:"finite t" and i: "independent s" - and sp:"s \ span t" - shows "\t'. (card t' = card t) \ finite t' \ s \ t' \ t' \ s \ t \ s \ span t'" -using f i sp -proof(induct "card (t - s)" arbitrary: s t rule: less_induct) - case less - note ft = `finite t` and s = `independent s` and sp = `s \ span t` - let ?P = "\t'. (card t' = card t) \ finite t' \ s \ t' \ t' \ s \ t \ s \ span t'" - let ?ths = "\t'. ?P t'" - {assume st: "s \ t" - from st ft span_mono[OF st] have ?ths apply - apply (rule exI[where x=t]) - by (auto intro: span_superset)} - moreover - {assume st: "t \ s" - - from spanning_subset_independent[OF st s sp] - st ft span_mono[OF st] have ?ths apply - apply (rule exI[where x=t]) - by (auto intro: span_superset)} - moreover - {assume st: "\ s \ t" "\ t \ s" - from st(2) obtain b where b: "b \ t" "b \ s" by blast - from b have "t - {b} - s \ t - s" by blast - then have cardlt: "card (t - {b} - s) < card (t - s)" using ft - by (auto intro: psubset_card_mono) - from b ft have ct0: "card t \ 0" by auto - {assume stb: "s \ span(t -{b})" - from ft have ftb: "finite (t -{b})" by auto - from less(1)[OF cardlt ftb s stb] - obtain u where u: "card u = card (t-{b})" "s \ u" "u \ s \ (t - {b})" "s \ span u" and fu: "finite u" by blast - let ?w = "insert b u" - have th0: "s \ insert b u" using u by blast - from u(3) b have "u \ s \ t" by blast - then have th1: "insert b u \ s \ t" using u b by blast - have bu: "b \ u" using b u by blast - from u(1) ft b have "card u = (card t - 1)" by auto - then - have th2: "card (insert b u) = card t" - using card_insert_disjoint[OF fu bu] ct0 by auto - from u(4) have "s \ span u" . - also have "\ \ span (insert b u)" apply (rule span_mono) by blast - finally have th3: "s \ span (insert b u)" . - from th0 th1 th2 th3 fu have th: "?P ?w" by blast - from th have ?ths by blast} - moreover - {assume stb: "\ s \ span(t -{b})" - from stb obtain a where a: "a \ s" "a \ span (t - {b})" by blast - have ab: "a \ b" using a b by blast - have at: "a \ t" using a ab span_superset[of a "t- {b}"] by auto - have mlt: "card ((insert a (t - {b})) - s) < card (t - s)" - using cardlt ft a b by auto - have ft': "finite (insert a (t - {b}))" using ft by auto - {fix x assume xs: "x \ s" - have t: "t \ (insert b (insert a (t -{b})))" using b by auto - from b(1) have "b \ span t" by (simp add: span_superset) - have bs: "b \ span (insert a (t - {b}))" apply(rule in_span_delete) - using a sp unfolding subset_eq by auto - from xs sp have "x \ span t" by blast - with span_mono[OF t] - have x: "x \ span (insert b (insert a (t - {b})))" .. - from span_trans[OF bs x] have "x \ span (insert a (t - {b}))" .} - then have sp': "s \ span (insert a (t - {b}))" by blast - - from less(1)[OF mlt ft' s sp'] obtain u where - u: "card u = card (insert a (t -{b}))" "finite u" "s \ u" "u \ s \ insert a (t -{b})" - "s \ span u" by blast - from u a b ft at ct0 have "?P u" by auto - then have ?ths by blast } - ultimately have ?ths by blast - } - ultimately - show ?ths by blast -qed - -text {* This implies corresponding size bounds. *} - -lemma independent_span_bound: - assumes f: "finite t" and i: "independent s" and sp:"s \ span t" - shows "finite s \ card s \ card t" - by (metis exchange_lemma[OF f i sp] finite_subset card_mono) - - -lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\ (UNIV::'a::finite set)}" -proof- - have eq: "{f x |x. x\ UNIV} = f ` UNIV" by auto - show ?thesis unfolding eq - apply (rule finite_imageI) - apply (rule finite) - done -qed - -subsection{* Euclidean Spaces as Typeclass*} +subsection {* Type class of Euclidean spaces *} class euclidean_space = real_inner + fixes dimension :: "'a itself \ nat" @@ -1621,67 +53,6 @@ "norm (basis i) = (if i < DIM('a) then 1 else 0)" unfolding norm_eq_sqrt_inner dot_basis by simp -lemma (in euclidean_space) basis_inj[simp, intro]: "inj_on basis {.. 'c::real_vector" assumes *: "inj_on f {.. (\a u. a < D \ (\i\{..R f i) \ f a)" -proof - - from * have eq: "\i. i < D \ f ` {..i. inj_on f ({..i. finite (f ` {..d. \ 0 < d; basis ` {d..} = {0::'a::euclidean_space}; - independent (basis ` {.. 'a) {.. \ P d" - shows "P DIM('a::euclidean_space)" - using DIM_positive basis_finite independent_basis basis_inj - by (rule assms) - -lemma (in euclidean_space) dimension_eq: - assumes "\i. i < d \ basis i \ 0" - assumes "\i. d \ i \ basis i = 0" - shows "DIM('a) = d" -proof (rule linorder_cases [of "DIM('a)" d]) - assume "DIM('a) < d" - hence "basis DIM('a) \ 0" by (rule assms) - thus ?thesis by simp -next - assume "d < DIM('a)" - hence "basis d \ 0" by simp - thus ?thesis by (simp add: assms) -next - assume "DIM('a) = d" thus ?thesis . -qed - -lemma (in euclidean_space) range_basis: - "range basis = insert 0 (basis ` {.. {DIM('a)..}" by auto - show ?thesis unfolding * image_Un basis_finite by auto -qed - -lemma (in euclidean_space) range_basis_finite[intro]: - "finite (range basis)" - unfolding range_basis by auto - lemma (in euclidean_space) basis_neq_0 [intro]: assumes "i 0" using assms by simp @@ -1773,1522 +144,18 @@ by (simp add: DIM_positive) lemma euclidean_inner: - "x \ (y::'a) = (\i (y $$ i))" -proof - - have "x \ y = (\iR basis i) \ - (\iR (basis i :: 'a))" - by (subst (1 2) euclidean_representation) simp - also have "\ = (\i (y $$ i))" - unfolding inner_left.setsum inner_right.setsum - by (auto simp add: dot_basis if_distrib setsum_cases intro!: setsum_cong) - finally show ?thesis . -qed - -lemma span_basis: "span (range basis) = (UNIV :: 'a::euclidean_space set)" -proof - - { fix x :: 'a - have "(\iR basis i) \ span (range basis :: 'a set)" - by (simp add: span_setsum span_mul span_superset) - hence "x \ span (range basis)" - by (simp only: euclidean_representation [symmetric]) - } thus ?thesis by auto -qed - -lemma basis_representation: - "\u. x = (\v\basis ` {..R (v\'a\euclidean_space))" -proof - - have "x\UNIV" by auto from this[unfolded span_basis[THEN sym]] - have "\u. (\v\basis ` {..R v) = x" - unfolding range_basis span_insert_0 apply(subst (asm) span_finite) by auto - thus ?thesis by fastsimp -qed - -lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..'a) ` {.. span (basis ` {..ix$$i\ \ norm (x::'a::euclidean_space)" unfolding euclidean_component_def - apply(rule order_trans[OF real_inner_class.Cauchy_Schwarz_ineq2]) by auto - -lemma norm_bound_component_le: "norm (x::'a::euclidean_space) \ e \ \x$$i\ <= e" - by (metis component_le_norm order_trans) - -lemma norm_bound_component_lt: "norm (x::'a::euclidean_space) < e \ \x$$i\ < e" - by (metis component_le_norm basic_trans_rules(21)) - -lemma norm_le_l1: "norm (x::'a::euclidean_space) \ (\ix $$ i\)" - apply (subst euclidean_representation[of x]) - apply (rule order_trans[OF setsum_norm]) - by (auto intro!: setsum_mono) - -lemma setsum_norm_allsubsets_bound: - fixes f:: "'a \ 'n::euclidean_space" - assumes fP: "finite P" and fPs: "\Q. Q \ P \ norm (setsum f Q) \ e" - shows "setsum (\x. norm (f x)) P \ 2 * real DIM('n) * e" -proof- - let ?d = "real DIM('n)" - let ?nf = "\x. norm (f x)" - let ?U = "{..x. setsum (\i. \f x $$ i\) ?U) P = setsum (\i. setsum (\x. \f x $$ i\) P) ?U" - by (rule setsum_commute) - have th1: "2 * ?d * e = of_nat (card ?U) * (2 * e)" by (simp add: real_of_nat_def) - have "setsum ?nf P \ setsum (\x. setsum (\i. \f x $$ i\) ?U) P" - apply (rule setsum_mono) by (rule norm_le_l1) - also have "\ \ 2 * ?d * e" - unfolding th0 th1 - proof(rule setsum_bounded) - fix i assume i: "i \ ?U" - let ?Pp = "{x. x\ P \ f x $$ i \ 0}" - let ?Pn = "{x. x \ P \ f x $$ i < 0}" - have thp: "P = ?Pp \ ?Pn" by auto - have thp0: "?Pp \ ?Pn ={}" by auto - have PpP: "?Pp \ P" and PnP: "?Pn \ P" by blast+ - have Ppe:"setsum (\x. \f x $$ i\) ?Pp \ e" - using component_le_norm[of "setsum (\x. f x) ?Pp" i] fPs[OF PpP] - unfolding euclidean_component.setsum by(auto intro: abs_le_D1) - have Pne: "setsum (\x. \f x $$ i\) ?Pn \ e" - using component_le_norm[of "setsum (\x. - f x) ?Pn" i] fPs[OF PnP] - unfolding euclidean_component.setsum euclidean_component.minus - by(auto simp add: setsum_negf intro: abs_le_D1) - have "setsum (\x. \f x $$ i\) P = setsum (\x. \f x $$ i\) ?Pp + setsum (\x. \f x $$ i\) ?Pn" - apply (subst thp) - apply (rule setsum_Un_zero) - using fP thp0 by auto - also have "\ \ 2*e" using Pne Ppe by arith - finally show "setsum (\x. \f x $$ i\) P \ 2*e" . - qed - finally show ?thesis . -qed - -lemma choice_iff': "(\xy. P x y) \ (\f. \xix. P i x) \ - (\x::'a. \i ?rhs") -proof- - let ?S = "{..ii y \ (\i < DIM('a). x $$ i \ y $$ i)" - and eucl_less: "x < y \ (\i < DIM('a). x $$ i < y $$ i)" - -lemma eucl_less_not_refl[simp, intro!]: "\ x < (x::'a::ordered_euclidean_space)" - unfolding eucl_less[where 'a='a] by auto - -lemma euclidean_trans[trans]: - fixes x y z :: "'a::ordered_euclidean_space" - shows "x < y \ y < z \ x < z" - and "x \ y \ y < z \ x < z" - and "x \ y \ y \ z \ x \ z" - by (force simp: eucl_less[where 'a='a] eucl_le[where 'a='a])+ - -subsection {* Linearity and Bilinearity continued *} - -lemma linear_bounded: - fixes f:: "'a::euclidean_space \ 'b::real_normed_vector" - assumes lf: "linear f" - shows "\B. \x. norm (f x) \ B * norm x" -proof- - let ?S = "{..i. (x$$i) *\<^sub>R (basis i)) ?S))" - apply(subst euclidean_representation[of x]) .. - also have "\ = norm (setsum (\ i. (x$$i) *\<^sub>R f (basis i)) ?S)" - using linear_setsum[OF lf fS, of ?g, unfolded o_def] linear_cmul[OF lf] by auto - finally have th0: "norm (f x) = norm (setsum (\i. (x$$i) *\<^sub>R f (basis i))?S)" . - {fix i assume i: "i \ ?S" - from component_le_norm[of x i] - have "norm ((x$$i) *\<^sub>R f (basis i :: 'a)) \ norm (f (basis i)) * norm x" - unfolding norm_scaleR - apply (simp only: mult_commute) - apply (rule mult_mono) - by (auto simp add: field_simps) } - then have th: "\i\ ?S. norm ((x$$i) *\<^sub>R f (basis i :: 'a)) \ norm (f (basis i)) * norm x" by metis - from setsum_norm_le[OF fS, of "\i. (x$$i) *\<^sub>R (f (basis i))", OF th] - have "norm (f x) \ ?B * norm x" unfolding th0 setsum_left_distrib by metis} - then show ?thesis by blast -qed - -lemma linear_bounded_pos: - fixes f:: "'a::euclidean_space \ 'b::real_normed_vector" - assumes lf: "linear f" - shows "\B > 0. \x. norm (f x) \ B * norm x" -proof- - from linear_bounded[OF lf] obtain B where - B: "\x. norm (f x) \ B * norm x" by blast - let ?K = "\B\ + 1" - have Kp: "?K > 0" by arith - { assume C: "B < 0" - have "((\\ i. 1)::'a) \ 0" unfolding euclidean_eq[where 'a='a] - by(auto intro!:exI[where x=0] simp add:euclidean_component.zero) - hence "norm ((\\ i. 1)::'a) > 0" by auto - with C have "B * norm ((\\ i. 1)::'a) < 0" - by (simp add: mult_less_0_iff) - with B[rule_format, of "(\\ i. 1)::'a"] norm_ge_zero[of "f ((\\ i. 1)::'a)"] have False by simp - } - then have Bp: "B \ 0" by (metis not_leE) - {fix x::"'a" - have "norm (f x) \ ?K * norm x" - using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp - apply (auto simp add: field_simps split add: abs_split) - apply (erule order_trans, simp) - done - } - then show ?thesis using Kp by blast -qed - -lemma linear_conv_bounded_linear: - fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" - shows "linear f \ bounded_linear f" -proof - assume "linear f" - show "bounded_linear f" - proof - fix x y show "f (x + y) = f x + f y" - using `linear f` unfolding linear_def by simp - next - fix r x show "f (scaleR r x) = scaleR r (f x)" - using `linear f` unfolding linear_def by simp - next - have "\B. \x. norm (f x) \ B * norm x" - using `linear f` by (rule linear_bounded) - thus "\K. \x. norm (f x) \ norm x * K" - by (simp add: mult_commute) - qed -next - assume "bounded_linear f" - then interpret f: bounded_linear f . - show "linear f" - by (simp add: f.add f.scaleR linear_def) -qed - -lemma bounded_linearI': fixes f::"'a::euclidean_space \ 'b::real_normed_vector" - assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" - shows "bounded_linear f" unfolding linear_conv_bounded_linear[THEN sym] - by(rule linearI[OF assms]) - - -lemma bilinear_bounded: - fixes h:: "'m::euclidean_space \ 'n::euclidean_space \ 'k::real_normed_vector" - assumes bh: "bilinear h" - shows "\B. \x y. norm (h x y) \ B * norm x * norm y" -proof- - let ?M = "{..i. (x$$i) *\<^sub>R basis i) ?M) (setsum (\i. (y$$i) *\<^sub>R basis i) ?N))" - apply(subst euclidean_representation[where 'a='m]) - apply(subst euclidean_representation[where 'a='n]) .. - also have "\ = norm (setsum (\ (i,j). h ((x$$i) *\<^sub>R basis i) ((y$$j) *\<^sub>R basis j)) (?M \ ?N))" - unfolding bilinear_setsum[OF bh fM fN] .. - finally have th: "norm (h x y) = \" . - have "norm (h x y) \ ?B * norm x * norm y" - apply (simp add: setsum_left_distrib th) - apply (rule setsum_norm_le) - using fN fM - apply simp - apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] field_simps simp del: scaleR_scaleR) - apply (rule mult_mono) - apply (auto simp add: zero_le_mult_iff component_le_norm) - apply (rule mult_mono) - apply (auto simp add: zero_le_mult_iff component_le_norm) - done} - then show ?thesis by metis -qed - -lemma bilinear_bounded_pos: - fixes h:: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector" - assumes bh: "bilinear h" - shows "\B > 0. \x y. norm (h x y) \ B * norm x * norm y" -proof- - from bilinear_bounded[OF bh] obtain B where - B: "\x y. norm (h x y) \ B * norm x * norm y" by blast - let ?K = "\B\ + 1" - have Kp: "?K > 0" by arith - have KB: "B < ?K" by arith - {fix x::'a and y::'b - from KB Kp - have "B * norm x * norm y \ ?K * norm x * norm y" - apply - - apply (rule mult_right_mono, rule mult_right_mono) - by auto - then have "norm (h x y) \ ?K * norm x * norm y" - using B[rule_format, of x y] by simp} - with Kp show ?thesis by blast -qed - -lemma bilinear_conv_bounded_bilinear: - fixes h :: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector" - shows "bilinear h \ bounded_bilinear h" -proof - assume "bilinear h" - show "bounded_bilinear h" - proof - fix x y z show "h (x + y) z = h x z + h y z" - using `bilinear h` unfolding bilinear_def linear_def by simp - next - fix x y z show "h x (y + z) = h x y + h x z" - using `bilinear h` unfolding bilinear_def linear_def by simp - next - fix r x y show "h (scaleR r x) y = scaleR r (h x y)" - using `bilinear h` unfolding bilinear_def linear_def - by simp - next - fix r x y show "h x (scaleR r y) = scaleR r (h x y)" - using `bilinear h` unfolding bilinear_def linear_def - by simp - next - have "\B. \x y. norm (h x y) \ B * norm x * norm y" - using `bilinear h` by (rule bilinear_bounded) - thus "\K. \x y. norm (h x y) \ norm x * norm y * K" - by (simp add: mult_ac) - qed -next - assume "bounded_bilinear h" - then interpret h: bounded_bilinear h . - show "bilinear h" - unfolding bilinear_def linear_conv_bounded_linear - using h.bounded_linear_left h.bounded_linear_right - by simp -qed - -subsection {* We continue. *} - -lemma independent_bound: - fixes S:: "('a::euclidean_space) set" - shows "independent S \ finite S \ card S <= DIM('a::euclidean_space)" - using independent_span_bound[of "(basis::nat=>'a) ` {.. card S > DIM('a)) ==> dependent S" - by (metis independent_bound not_less) - -text {* Hence we can create a maximal independent subset. *} - -lemma maximal_independent_subset_extend: - assumes sv: "(S::('a::euclidean_space) set) \ V" and iS: "independent S" - shows "\B. S \ B \ B \ V \ independent B \ V \ span B" - using sv iS -proof(induct "DIM('a) - card S" arbitrary: S rule: less_induct) - case less - note sv = `S \ V` and i = `independent S` - let ?P = "\B. S \ B \ B \ V \ independent B \ V \ span B" - let ?ths = "\x. ?P x" - let ?d = "DIM('a)" - {assume "V \ span S" - then have ?ths using sv i by blast } - moreover - {assume VS: "\ V \ span S" - from VS obtain a where a: "a \ V" "a \ span S" by blast - from a have aS: "a \ S" by (auto simp add: span_superset) - have th0: "insert a S \ 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 \ B" "B \ V" "independent B" " V \ span B" - by blast - from B have "?P B" by auto - then have ?ths by blast} - ultimately show ?ths by blast -qed - -lemma maximal_independent_subset: - "\(B:: ('a::euclidean_space) set). B\ V \ independent B \ V \ span B" - by (metis maximal_independent_subset_extend[of "{}:: ('a::euclidean_space) set"] empty_subsetI independent_empty) - - -text {* Notion of dimension. *} - -definition "dim V = (SOME n. \B. B \ V \ independent B \ V \ span B \ (card B = n))" - -lemma basis_exists: "\B. (B :: ('a::euclidean_space) set) \ V \ independent B \ V \ span B \ (card B = dim V)" -unfolding dim_def some_eq_ex[of "\n. \B. B \ V \ independent B \ V \ span B \ (card B = n)"] -using maximal_independent_subset[of V] independent_bound -by auto - -text {* Consequences of independence or spanning for cardinality. *} - -lemma independent_card_le_dim: - assumes "(B::('a::euclidean_space) set) \ V" and "independent B" shows "card B \ dim V" -proof - - from basis_exists[of V] `B \ V` - obtain B' where "independent B'" and "B \ span B'" and "card B' = dim V" by blast - with independent_span_bound[OF _ `independent B` `B \ span B'`] independent_bound[of B'] - show ?thesis by auto -qed - -lemma span_card_ge_dim: "(B::('a::euclidean_space) set) \ V \ V \ span B \ finite B \ dim V \ card B" - by (metis basis_exists[of V] independent_span_bound subset_trans) - -lemma basis_card_eq_dim: - "B \ (V:: ('a::euclidean_space) set) \ V \ span B \ independent B \ finite B \ card B = dim V" - by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_bound) - -lemma dim_unique: "(B::('a::euclidean_space) set) \ V \ V \ span B \ independent B \ card B = n \ dim V = n" - by (metis basis_card_eq_dim) - -text {* More lemmas about dimension. *} - -lemma dim_UNIV: "dim (UNIV :: ('a::euclidean_space) set) = DIM('a)" - apply (rule dim_unique[of "(basis::nat=>'a) ` {.. T \ dim S \ dim T" - using basis_exists[of T] basis_exists[of S] - by (metis independent_card_le_dim subset_trans) - -lemma dim_subset_UNIV: "dim (S:: ('a::euclidean_space) set) \ DIM('a)" - by (metis dim_subset subset_UNIV dim_UNIV) - -text {* Converses to those. *} - -lemma card_ge_dim_independent: - assumes BV:"(B::('a::euclidean_space) set) \ V" and iB:"independent B" and dVB:"dim V \ card B" - shows "V \ span B" -proof- - {fix a assume aV: "a \ V" - {assume aB: "a \ span B" - then have iaB: "independent (insert a B)" using iB aV BV by (simp add: independent_insert) - from aV BV have th0: "insert a B \ V" by blast - from aB have "a \B" by (auto simp add: span_superset) - with independent_card_le_dim[OF th0 iaB] dVB independent_bound[OF iB] have False by auto } - then have "a \ span B" by blast} - then show ?thesis by blast -qed - -lemma card_le_dim_spanning: - assumes BV: "(B:: ('a::euclidean_space) set) \ V" and VB: "V \ span B" - and fB: "finite B" and dVB: "dim V \ card B" - shows "independent B" -proof- - {fix a assume a: "a \ B" "a \ span (B -{a})" - from a fB have c0: "card B \ 0" by auto - from a fB have cb: "card (B -{a}) = card B - 1" by auto - from BV a have th0: "B -{a} \ V" by blast - {fix x assume x: "x \ V" - from a have eq: "insert a (B -{a}) = B" by blast - from x VB have x': "x \ span B" by blast - from span_trans[OF a(2), unfolded eq, OF x'] - have "x \ span (B -{a})" . } - then have th1: "V \ span (B -{a})" by blast - have th2: "finite (B -{a})" using fB by auto - from span_card_ge_dim[OF th0 th1 th2] - have c: "dim V \ card (B -{a})" . - from c c0 dVB cb have False by simp} - then show ?thesis unfolding dependent_def by blast -qed - -lemma card_eq_dim: "(B:: ('a::euclidean_space) set) \ V \ card B = dim V \ finite B \ independent B \ V \ span B" - by (metis order_eq_iff card_le_dim_spanning - card_ge_dim_independent) - -text {* More general size bound lemmas. *} - -lemma independent_bound_general: - "independent (S:: ('a::euclidean_space) set) \ finite S \ card S \ dim S" - by (metis independent_card_le_dim independent_bound subset_refl) - -lemma dependent_biggerset_general: "(finite (S:: ('a::euclidean_space) set) \ card S > dim S) \ dependent S" - using independent_bound_general[of S] by (metis linorder_not_le) - -lemma dim_span: "dim (span (S:: ('a::euclidean_space) set)) = dim S" -proof- - have th0: "dim S \ dim (span S)" - by (auto simp add: subset_eq intro: dim_subset span_superset) - from basis_exists[of S] - obtain B where B: "B \ S" "independent B" "S \ span B" "card B = dim S" by blast - from B have fB: "finite B" "card B = dim S" using independent_bound by blast+ - have bSS: "B \ span S" using B(1) by (metis subset_eq span_inc) - have sssB: "span S \ span B" using span_mono[OF B(3)] by (simp add: span_span) - from span_card_ge_dim[OF bSS sssB fB(1)] th0 show ?thesis - using fB(2) by arith -qed - -lemma subset_le_dim: "(S:: ('a::euclidean_space) set) \ span T \ dim S \ dim T" - by (metis dim_span dim_subset) - -lemma span_eq_dim: "span (S:: ('a::euclidean_space) set) = span T ==> dim S = dim T" - by (metis dim_span) - -lemma spans_image: - assumes lf: "linear f" and VB: "V \ span B" - shows "f ` V \ span (f ` B)" - unfolding span_linear_image[OF lf] - by (metis VB image_mono) - -lemma dim_image_le: - fixes f :: "'a::euclidean_space \ 'b::euclidean_space" - assumes lf: "linear f" shows "dim (f ` S) \ dim (S)" -proof- - from basis_exists[of S] obtain B where - B: "B \ S" "independent B" "S \ span B" "card B = dim S" by blast - from B have fB: "finite B" "card B = dim S" using independent_bound by blast+ - have "dim (f ` S) \ card (f ` B)" - apply (rule span_card_ge_dim) - using lf B fB by (auto simp add: span_linear_image spans_image subset_image_iff) - also have "\ \ dim S" using card_image_le[OF fB(1)] fB by simp - finally show ?thesis . -qed - -text {* Relation between bases and injectivity/surjectivity of map. *} - -lemma spanning_surjective_image: - assumes us: "UNIV \ span S" - and lf: "linear f" and sf: "surj f" - shows "UNIV \ span (f ` S)" -proof- - have "UNIV \ f ` UNIV" using sf by (auto simp add: surj_def) - also have " \ \ 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 \ S" "f a \ 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 \ f ` span (S -{a})" - unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast - hence "a \ 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 {* Picking an orthogonal replacement for a spanning set. *} - - (* FIXME : Move to some general theory ?*) -definition "pairwise R S \ (\x \ S. \y\ S. x\y \ R x y)" - -lemma vector_sub_project_orthogonal: "(b::'a::euclidean_space) \ (x - ((b \ x) / (b \ b)) *\<^sub>R b) = 0" - unfolding inner_simps by auto - -lemma basis_orthogonal: - fixes B :: "('a::euclidean_space) set" - assumes fB: "finite B" - shows "\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C" - (is " \C. ?P B C") -proof(induct rule: finite_induct[OF fB]) - case 1 thus ?case apply (rule exI[where x="{}"]) by (auto simp add: pairwise_def) -next - case (2 a B) - note fB = `finite B` and aB = `a \ B` - from `\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C` - obtain C where C: "finite C" "card C \ card B" - "span C = span B" "pairwise orthogonal C" by blast - let ?a = "a - setsum (\x. (x \ a / (x \ x)) *\<^sub>R x) C" - let ?C = "insert ?a C" - from C(1) have fC: "finite ?C" by simp - from fB aB C(1,2) have cC: "card ?C \ card (insert a B)" by (simp add: card_insert_if) - {fix x k - have th0: "\(a::'a) b c. a - (b - c) = c + (a - b)" by (simp add: field_simps) - have "x - k *\<^sub>R (a - (\x\C. (x \ a / (x \ x)) *\<^sub>R x)) \ span C \ x - k *\<^sub>R a \ span C" - apply (simp only: scaleR_right_diff_distrib th0) - apply (rule span_add_eq) - apply (rule span_mul) - apply (rule span_setsum[OF C(1)]) - apply clarify - apply (rule span_mul) - by (rule span_superset)} - then have SC: "span ?C = span (insert a B)" - unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto - thm pairwise_def - {fix x y assume xC: "x \ ?C" and yC: "y \ ?C" and xy: "x \ y" - {assume xa: "x = ?a" and ya: "y = ?a" - have "orthogonal x y" using xa ya xy by blast} - moreover - {assume xa: "x = ?a" and ya: "y \ ?a" "y \ C" - from ya have Cy: "C = insert y (C - {y})" by blast - have fth: "finite (C - {y})" using C by simp - have "orthogonal x y" - using xa ya - unfolding orthogonal_def xa inner_simps diff_eq_0_iff_eq - apply simp - apply (subst Cy) - using C(1) fth - apply (simp only: setsum_clauses) - apply (auto simp add: inner_simps inner_commute[of y a] dot_lsum[OF fth]) - apply (rule setsum_0') - apply clarsimp - apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format]) - by auto} - moreover - {assume xa: "x \ ?a" "x \ C" and ya: "y = ?a" - from xa have Cx: "C = insert x (C - {x})" by blast - have fth: "finite (C - {x})" using C by simp - have "orthogonal x y" - using xa ya - unfolding orthogonal_def ya inner_simps diff_eq_0_iff_eq - apply simp - apply (subst Cx) - using C(1) fth - apply (simp only: setsum_clauses) - apply (subst inner_commute[of x]) - apply (auto simp add: inner_simps inner_commute[of x a] dot_rsum[OF fth]) - apply (rule setsum_0') - apply clarsimp - apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format]) - by auto} - moreover - {assume xa: "x \ C" and ya: "y \ C" - have "orthogonal x y" using xa ya xy C(4) unfolding pairwise_def by blast} - ultimately have "orthogonal x y" using xC yC by blast} - then have CPO: "pairwise orthogonal ?C" unfolding pairwise_def by blast - from fC cC SC CPO have "?P (insert a B) ?C" by blast - then show ?case by blast -qed - -lemma orthogonal_basis_exists: - fixes V :: "('a::euclidean_space) set" - shows "\B. independent B \ B \ span V \ V \ span B \ (card B = dim V) \ pairwise orthogonal B" -proof- - from basis_exists[of V] obtain B where B: "B \ V" "independent B" "V \ span B" "card B = dim V" by blast - from B have fB: "finite B" "card B = dim V" using independent_bound by auto - from basis_orthogonal[OF fB(1)] obtain C where - C: "finite C" "card C \ card B" "span C = span B" "pairwise orthogonal C" by blast - from C B - have CSV: "C \ span V" by (metis span_inc span_mono subset_trans) - from span_mono[OF B(3)] C have SVC: "span V \ span C" by (simp add: span_span) - from card_le_dim_spanning[OF CSV SVC C(1)] C(2,3) fB - have iC: "independent C" by (simp add: dim_span) - from C fB have "card C \ dim V" by simp - moreover have "dim V \ card C" using span_card_ge_dim[OF CSV SVC C(1)] - by (simp add: dim_span) - ultimately have CdV: "card C = dim V" using C(1) by simp - from C B CSV CdV iC show ?thesis by auto -qed - -lemma span_eq: "span S = span T \ S \ span T \ T \ 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 {* Low-dimensional subset is in a hyperplane (weak orthogonal complement). *} - -lemma span_not_univ_orthogonal: fixes S::"('a::euclidean_space) set" - assumes sU: "span S \ UNIV" - shows "\(a::'a). a \0 \ (\x \ span S. a \ x = 0)" -proof- - from sU obtain a where a: "a \ span S" by blast - from orthogonal_basis_exists obtain B where - B: "independent B" "B \ span S" "S \ span B" "card B = dim S" "pairwise orthogonal B" - by blast - from B have fB: "finite B" "card B = dim S" using independent_bound by auto - from span_mono[OF B(2)] span_mono[OF B(3)] - have sSB: "span S = span B" by (simp add: span_span) - let ?a = "a - setsum (\b. (a \ b / (b \ b)) *\<^sub>R b) B" - have "setsum (\b. (a \ b / (b \ b)) *\<^sub>R b) B \ span S" - unfolding sSB - apply (rule span_setsum[OF fB(1)]) - apply clarsimp - apply (rule span_mul) - by (rule span_superset) - with a have a0:"?a \ 0" by auto - have "\x\span B. ?a \ x = 0" - proof(rule span_induct') - show "subspace (\x. ?a \ x = 0)" by (auto simp add: subspace_def mem_def inner_simps) -next - {fix x assume x: "x \ B" - from x have B': "B = insert x (B - {x})" by blast - have fth: "finite (B - {x})" using fB by simp - have "?a \ x = 0" - apply (subst B') using fB fth - unfolding setsum_clauses(2)[OF fth] - apply simp unfolding inner_simps - apply (clarsimp simp add: inner_simps dot_lsum) - apply (rule setsum_0', rule ballI) - unfolding inner_commute - by (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])} - then show "\x \ B. ?a \ x = 0" by blast - qed - with a0 show ?thesis unfolding sSB by (auto intro: exI[where x="?a"]) -qed - -lemma span_not_univ_subset_hyperplane: - assumes SU: "span S \ (UNIV ::('a::euclidean_space) set)" - shows "\ a. a \0 \ span S \ {x. a \ x = 0}" - using span_not_univ_orthogonal[OF SU] by auto - -lemma lowdim_subset_hyperplane: fixes S::"('a::euclidean_space) set" - assumes d: "dim S < DIM('a)" - shows "\(a::'a). a \ 0 \ span S \ {x. a \ x = 0}" -proof- - {assume "span S = UNIV" - hence "dim (span S) = dim (UNIV :: ('a) set)" by simp - hence "dim S = DIM('a)" by (simp add: dim_span dim_UNIV) - with d have False by arith} - hence th: "span S \ UNIV" by blast - from span_not_univ_subset_hyperplane[OF th] show ?thesis . -qed - -text {* We can extend a linear basis-basis injection to the whole set. *} - -lemma linear_indep_image_lemma: - assumes lf: "linear f" and fB: "finite B" - and ifB: "independent (f ` B)" - and fi: "inj_on f B" and xsB: "x \ span B" - and fx: "f x = 0" - shows "x = 0" - using fB ifB fi xsB fx -proof(induct arbitrary: x rule: finite_induct[OF fB]) - case 1 thus ?case by (auto simp add: span_empty) -next - case (2 a b x) - have fb: "finite b" using "2.prems" by simp - have th0: "f ` b \ f ` (insert a b)" - apply (rule image_mono) by blast - from independent_mono[ OF "2.prems"(2) th0] - have ifb: "independent (f ` b)" . - have fib: "inj_on f b" - apply (rule subset_inj_on [OF "2.prems"(3)]) - by blast - from span_breakdown[of a "insert a b", simplified, OF "2.prems"(4)] - obtain k where k: "x - k*\<^sub>R a \ span (b -{a})" by blast - have "f (x - k*\<^sub>R a) \ span (f ` b)" - unfolding span_linear_image[OF lf] - apply (rule imageI) - using k span_mono[of "b-{a}" b] by blast - hence "f x - k*\<^sub>R f a \ span (f ` b)" - by (simp add: linear_sub[OF lf] linear_cmul[OF lf]) - hence th: "-k *\<^sub>R f a \ span (f ` b)" - using "2.prems"(5) by simp - {assume k0: "k = 0" - from k0 k have "x \ span (b -{a})" by simp - then have "x \ span b" using span_mono[of "b-{a}" b] - by blast} - moreover - {assume k0: "k \ 0" - from span_mul[OF th, of "- 1/ k"] k0 - have th1: "f a \ span (f ` b)" - by auto - from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric] - have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast - from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"] - have "f a \ span (f ` b)" using tha - using "2.hyps"(2) - "2.prems"(3) by auto - with th1 have False by blast - then have "x \ span b" by blast} - ultimately have xsb: "x \ span b" by blast - from "2.hyps"(3)[OF fb ifb fib xsb "2.prems"(5)] - show "x = 0" . -qed - -text {* We can extend a linear mapping from basis. *} + by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp -lemma linear_independent_extend_lemma: - fixes f :: "'a::real_vector \ 'b::real_vector" - assumes fi: "finite B" and ib: "independent B" - shows "\g. (\x\ span B. \y\ span B. g (x + y) = g x + g y) - \ (\x\ span B. \c. g (c*\<^sub>R x) = c *\<^sub>R g x) - \ (\x\ B. g x = f x)" -using ib fi -proof(induct rule: finite_induct[OF fi]) - case 1 thus ?case by (auto simp add: span_empty) -next - case (2 a b) - from "2.prems" "2.hyps" have ibf: "independent b" "finite b" - by (simp_all add: independent_insert) - from "2.hyps"(3)[OF ibf] obtain g where - g: "\x\span b. \y\span b. g (x + y) = g x + g y" - "\x\span b. \c. g (c *\<^sub>R x) = c *\<^sub>R g x" "\x\b. g x = f x" by blast - let ?h = "\z. SOME k. (z - k *\<^sub>R a) \ span b" - {fix z assume z: "z \ span (insert a b)" - have th0: "z - ?h z *\<^sub>R a \ span b" - apply (rule someI_ex) - unfolding span_breakdown_eq[symmetric] - using z . - {fix k assume k: "z - k *\<^sub>R a \ span b" - have eq: "z - ?h z *\<^sub>R a - (z - k*\<^sub>R a) = (k - ?h z) *\<^sub>R a" - by (simp add: field_simps scaleR_left_distrib [symmetric]) - from span_sub[OF th0 k] - have khz: "(k - ?h z) *\<^sub>R a \ span b" by (simp add: eq) - {assume "k \ ?h z" hence k0: "k - ?h z \ 0" by simp - from k0 span_mul[OF khz, of "1 /(k - ?h z)"] - have "a \ span b" by simp - with "2.prems"(1) "2.hyps"(2) have False - by (auto simp add: dependent_def)} - then have "k = ?h z" by blast} - with th0 have "z - ?h z *\<^sub>R a \ span b \ (\k. z - k *\<^sub>R a \ span b \ k = ?h z)" by blast} - note h = this - let ?g = "\z. ?h z *\<^sub>R f a + g (z - ?h z *\<^sub>R a)" - {fix x y assume x: "x \ span (insert a b)" and y: "y \ span (insert a b)" - have tha: "\(x::'a) y a k l. (x + y) - (k + l) *\<^sub>R a = (x - k *\<^sub>R a) + (y - l *\<^sub>R a)" - by (simp add: algebra_simps) - have addh: "?h (x + y) = ?h x + ?h y" - apply (rule conjunct2[OF h, rule_format, symmetric]) - apply (rule span_add[OF x y]) - unfolding tha - by (metis span_add x y conjunct1[OF h, rule_format]) - 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" and c:: real assume x: "x \ span (insert a b)" - have tha: "\(x::'a) c k a. c *\<^sub>R x - (c * k) *\<^sub>R a = c *\<^sub>R (x - k *\<^sub>R a)" - by (simp add: algebra_simps) - have hc: "?h (c *\<^sub>R x) = c * ?h x" - apply (rule conjunct2[OF h, rule_format, symmetric]) - apply (metis span_mul x) - by (metis tha span_mul x conjunct1[OF h]) - have "?g (c *\<^sub>R x) = c*\<^sub>R ?g x" - unfolding hc tha g(2)[rule_format, OF conjunct1[OF h, OF x]] - by (simp add: algebra_simps)} - moreover - {fix x assume x: "x \ (insert a b)" - {assume xa: "x = a" - have ha1: "1 = ?h a" - apply (rule conjunct2[OF h, rule_format]) - apply (metis span_superset insertI1) - using conjunct1[OF h, OF span_superset, OF insertI1] - by (auto simp add: span_0) - - from xa ha1[symmetric] have "?g x = f x" - apply simp - using g(2)[rule_format, OF span_0, of 0] - by simp} - moreover - {assume xb: "x \ b" - have h0: "0 = ?h x" - apply (rule conjunct2[OF h, rule_format]) - apply (metis span_superset x) - apply simp - apply (metis span_superset xb) - done - have "?g x = f x" - by (simp add: h0[symmetric] g(3)[rule_format, OF xb])} - ultimately have "?g x = f x" using x by blast } - ultimately show ?case apply - apply (rule exI[where x="?g"]) by blast -qed - -lemma linear_independent_extend: - assumes iB: "independent (B:: ('a::euclidean_space) set)" - shows "\g. linear g \ (\x\B. g x = f x)" -proof- - from maximal_independent_subset_extend[of B UNIV] iB - obtain C where C: "B \ C" "independent C" "\x. x \ span C" by auto - - from C(2) independent_bound[of C] linear_independent_extend_lemma[of C f] - obtain g where g: "(\x\ span C. \y\ span C. g (x + y) = g x + g y) - \ (\x\ span C. \c. g (c*\<^sub>R x) = c *\<^sub>R g x) - \ (\x\ C. g x = f x)" by blast - from g show ?thesis unfolding linear_def using C - apply clarsimp by blast -qed - -text {* Can construct an isomorphism between spaces of same dimension. *} - -lemma card_le_inj: assumes fA: "finite A" and fB: "finite B" - and c: "card A \ card B" shows "(\f. f ` A \ B \ inj_on f A)" -using fB c -proof(induct arbitrary: B rule: finite_induct[OF fA]) - case 1 thus ?case by simp -next - case (2 x s t) - thus ?case - proof(induct rule: finite_induct[OF "2.prems"(1)]) - case 1 then show ?case by simp - next - case (2 y t) - from "2.prems"(1,2,5) "2.hyps"(1,2) have cst:"card s \ card t" by simp - from "2.prems"(3) [OF "2.hyps"(1) cst] obtain f where - f: "f ` s \ t \ inj_on f s" by blast - from f "2.prems"(2) "2.hyps"(2) show ?case - apply - - apply (rule exI[where x = "\z. if z = x then y else f z"]) - by (auto simp add: inj_on_def) - qed -qed - -lemma card_subset_eq: assumes fB: "finite B" and AB: "A \ B" and - c: "card A = card B" - shows "A = B" -proof- - from fB AB have fA: "finite A" by (auto intro: finite_subset) - from fA fB have fBA: "finite (B - A)" by auto - have e: "A \ (B - A) = {}" by blast - have eq: "A \ (B - A) = B" using AB by blast - from card_Un_disjoint[OF fA fBA e, unfolded eq c] - have "card (B - A) = 0" by arith - hence "B - A = {}" unfolding card_eq_0_iff using fA fB by simp - with AB show "A = B" by blast -qed - -lemma subspace_isomorphism: - assumes s: "subspace (S:: ('a::euclidean_space) set)" - and t: "subspace (T :: ('b::euclidean_space) set)" - and d: "dim S = dim T" - shows "\f. linear f \ f ` S = T \ inj_on f S" -proof- - from basis_exists[of S] independent_bound obtain B where - B: "B \ S" "independent B" "S \ span B" "card B = dim S" and fB: "finite B" by blast - from basis_exists[of T] independent_bound obtain C where - C: "C \ T" "independent C" "T \ span C" "card C = dim T" and fC: "finite C" by blast - from B(4) C(4) card_le_inj[of B C] d obtain f where - f: "f ` B \ C" "inj_on f B" using `finite B` `finite C` by auto - from linear_independent_extend[OF B(2)] obtain g where - g: "linear g" "\x\ B. g x = f x" by blast - from inj_on_iff_eq_card[OF fB, of f] f(2) - have "card (f ` B) = card B" by simp - with B(4) C(4) have ceq: "card (f ` B) = card C" using d - by simp - have "g ` B = f ` B" using g(2) - by (auto simp add: image_iff) - also have "\ = C" using card_subset_eq[OF fC f(1) ceq] . - finally have gBC: "g ` B = C" . - have gi: "inj_on g B" using f(2) g(2) - by (auto simp add: inj_on_def) - note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi] - {fix x y assume x: "x \ S" and y: "y \ S" and gxy:"g x = g y" - from B(3) x y have x': "x \ span B" and y': "y \ span B" by blast+ - from gxy have th0: "g (x - y) = 0" by (simp add: linear_sub[OF g(1)]) - have th1: "x - y \ span B" using x' y' by (metis span_sub) - have "x=y" using g0[OF th1 th0] by simp } - then have giS: "inj_on g S" - unfolding inj_on_def by blast - from span_subspace[OF B(1,3) s] - have "g ` S = span (g ` B)" by (simp add: span_linear_image[OF g(1)]) - also have "\ = span C" unfolding gBC .. - also have "\ = T" using span_subspace[OF C(1,3) t] . - finally have gS: "g ` S = T" . - from g(1) gS giS show ?thesis by blast -qed - -text {* Linear functions are equal on a subspace if they are on a spanning set. *} - -lemma subspace_kernel: - assumes lf: "linear f" - shows "subspace {x. f x = 0}" -apply (simp add: subspace_def) -by (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf]) - -lemma linear_eq_0_span: - assumes lf: "linear f" and f0: "\x\B. f x = 0" - shows "\x \ span B. f x = 0" -proof - fix x assume x: "x \ span B" - let ?P = "\x. f x = 0" - from subspace_kernel[OF lf] have "subspace ?P" unfolding Collect_def . - with x f0 span_induct[of B "?P" x] show "f x = 0" by blast -qed - -lemma linear_eq_0: - assumes lf: "linear f" and SB: "S \ span B" and f0: "\x\B. f x = 0" - shows "\x \ S. f x = 0" - by (metis linear_eq_0_span[OF lf] subset_eq SB f0) - -lemma linear_eq: - assumes lf: "linear f" and lg: "linear g" and S: "S \ span B" - and fg: "\ x\ B. f x = g x" - shows "\x\ S. f x = g x" -proof- - let ?h = "\x. f x - g x" - from fg have fg': "\x\ 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: - assumes lf: "linear (f::'a::euclidean_space \ _)" and lg: "linear g" - and fg: "\i (UNIV :: 'a set)" - from equalityD2[OF span_basis'[where 'a='a]] - have IU: " (UNIV :: 'a set) \ span ?I" by blast - have "f x = g x" apply(rule linear_eq[OF lf lg IU,rule_format]) using fg x by auto } - then show ?thesis by (auto intro: ext) -qed - -text {* Similar results for bilinear functions. *} - -lemma bilinear_eq: - assumes bf: "bilinear f" - and bg: "bilinear g" - and SB: "S \ span B" and TC: "T \ span C" - and fg: "\x\ B. \y\ C. f x y = g x y" - shows "\x\S. \y\T. f x y = g x y " -proof- - let ?P = "\x. \y\ span C. f x y = g x y" - from bf bg have sp: "subspace ?P" - unfolding bilinear_def linear_def subspace_def bf bg - by(auto simp add: span_0 mem_def bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf]) - - have "\x \ span B. \y\ span C. f x y = g x y" - apply - - apply (rule ballI) - apply (rule span_induct[of B ?P]) - defer - apply (rule sp) - apply assumption - apply (clarsimp simp add: Ball_def) - apply (rule_tac P="\y. f xa y = g xa y" and S=C in span_induct) - using fg - apply (auto simp add: subspace_def) - using bf bg unfolding bilinear_def linear_def - by(auto simp add: span_0 mem_def bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf]) - then show ?thesis using SB TC by (auto intro: ext) -qed - -lemma bilinear_eq_stdbasis: fixes f::"'a::euclidean_space \ 'b::euclidean_space \ _" - assumes bf: "bilinear f" - and bg: "bilinear g" - and fg: "\ijx \ (basis ` {..y\ (basis ` {.. 'b::euclidean_space" - assumes lf: "linear f" and fi: "inj f" - shows "\g. linear g \ g o f = id" -proof- - from linear_independent_extend[OF independent_injective_image, OF independent_basis, OF lf fi] - obtain h:: "'b => 'a" where h: "linear h" - " \x \ f ` basis ` {..i f) (basis i) = id (basis 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 o f = id" . - then show ?thesis using h(1) by blast -qed - -lemma linear_surjective_right_inverse: fixes f::"'a::euclidean_space => 'b::euclidean_space" - assumes lf: "linear f" and sf: "surj f" - shows "\g. linear g \ f o g = id" -proof- - from linear_independent_extend[OF independent_basis[where 'a='b],of "inv f"] - obtain h:: "'b \ 'a" where - h: "linear h" "\ x\ basis ` {..i 'b::euclidean_space"} is also surjective. *} - -lemma linear_injective_imp_surjective: fixes f::"'a::euclidean_space => 'a::euclidean_space" - assumes lf: "linear f" and fi: "inj f" - shows "surj f" -proof- - let ?U = "UNIV :: 'a set" - from basis_exists[of ?U] obtain B - where B: "B \ ?U" "independent B" "?U \ span B" "card B = dim ?U" - by blast - from B(4) have d: "dim ?U = card B" by simp - have th: "?U \ span (f ` B)" - apply (rule card_ge_dim_independent) - apply blast - apply (rule independent_injective_image[OF B(2) lf fi]) - apply (rule order_eq_refl) - apply (rule sym) - unfolding d - apply (rule card_image) - apply (rule subset_inj_on[OF fi]) - by blast - from th show ?thesis - unfolding span_linear_image[OF lf] surj_def - using B(3) by blast -qed - -text {* And vice versa. *} - -lemma surjective_iff_injective_gen: - assumes fS: "finite S" and fT: "finite T" and c: "card S = card T" - and ST: "f ` S \ T" - shows "(\y \ T. \x \ S. f x = y) \ inj_on f S" (is "?lhs \ ?rhs") -proof- - {assume h: "?lhs" - {fix x y assume x: "x \ S" and y: "y \ S" and f: "f x = f y" - from x fS have S0: "card S \ 0" by auto - {assume xy: "x \ y" - have th: "card S \ card (f ` (S - {y}))" - unfolding c - apply (rule card_mono) - apply (rule finite_imageI) - using fS apply simp - using h xy x y f unfolding subset_eq image_iff - apply auto - apply (case_tac "xa = f x") - apply (rule bexI[where x=x]) - apply auto - done - also have " \ \ card (S -{y})" - apply (rule card_image_le) - using fS by simp - also have "\ \ card S - 1" using y fS by simp - finally have False using S0 by arith } - then have "x = y" by blast} - then have ?rhs unfolding inj_on_def by blast} - moreover - {assume h: ?rhs - have "f ` S = T" - apply (rule card_subset_eq[OF fT ST]) - unfolding card_image[OF h] using c . - then have ?lhs by blast} - ultimately show ?thesis by blast -qed +subsection {* Class instances *} -lemma linear_surjective_imp_injective: fixes f::"'a::euclidean_space => 'a::euclidean_space" - assumes lf: "linear f" and sf: "surj f" - shows "inj f" -proof- - let ?U = "UNIV :: 'a set" - from basis_exists[of ?U] obtain B - where B: "B \ ?U" "independent B" "?U \ span B" and d: "card B = dim ?U" - by blast - {fix x assume x: "x \ span B" and fx: "f x = 0" - from B(2) have fB: "finite B" using independent_bound by auto - have fBi: "independent (f ` B)" - apply (rule card_le_dim_spanning[of "f ` B" ?U]) - apply blast - using sf B(3) - unfolding span_linear_image[OF lf] surj_def subset_eq image_iff - apply blast - using fB apply blast - unfolding d[symmetric] - apply (rule card_image_le) - apply (rule fB) - done - have th0: "dim ?U \ card (f ` B)" - apply (rule span_card_ge_dim) - apply blast - unfolding span_linear_image[OF lf] - apply (rule subset_trans[where B = "f ` UNIV"]) - using sf unfolding surj_def apply blast - apply (rule image_mono) - apply (rule B(3)) - apply (metis finite_imageI fB) - done - - moreover have "card (f ` B) \ card B" - by (rule card_image_le, rule fB) - ultimately have th1: "card B = card (f ` B)" unfolding d by arith - have fiB: "inj_on f B" - unfolding surjective_iff_injective_gen[OF fB finite_imageI[OF fB] th1 subset_refl, symmetric] by blast - from linear_indep_image_lemma[OF lf fB fBi fiB x] fx - have "x = 0" by blast} - note th = this - from th show ?thesis unfolding linear_injective_0[OF lf] - using B(3) by blast -qed - -text {* Hence either is enough for isomorphism. *} - -lemma left_right_inverse_eq: - assumes fg: "f o g = id" and gh: "g o h = id" - shows "f = h" -proof- - have "f = f o (g o h)" unfolding gh by simp - also have "\ = (f o g) o h" by (simp add: o_assoc) - finally show "f = h" unfolding fg by simp -qed - -lemma isomorphism_expand: - "f o g = id \ g o f = id \ (\x. f(g x) = x) \ (\x. g(f x) = x)" - by (simp add: fun_eq_iff o_def id_def) - -lemma linear_injective_isomorphism: fixes f::"'a::euclidean_space => 'a::euclidean_space" - assumes lf: "linear f" and fi: "inj f" - shows "\f'. linear f' \ (\x. f' (f x) = x) \ (\x. f (f' x) = x)" -unfolding isomorphism_expand[symmetric] -using linear_surjective_right_inverse[OF lf linear_injective_imp_surjective[OF lf fi]] linear_injective_left_inverse[OF lf fi] -by (metis left_right_inverse_eq) - -lemma linear_surjective_isomorphism: fixes f::"'a::euclidean_space => 'a::euclidean_space" - assumes lf: "linear f" and sf: "surj f" - shows "\f'. linear f' \ (\x. f' (f x) = x) \ (\x. f (f' x) = x)" -unfolding isomorphism_expand[symmetric] -using linear_surjective_right_inverse[OF lf sf] linear_injective_left_inverse[OF lf linear_surjective_imp_injective[OF lf sf]] -by (metis left_right_inverse_eq) - -text {* Left and right inverses are the same for @{typ "'a::euclidean_space => 'a::euclidean_space"}. *} - -lemma linear_inverse_left: fixes f::"'a::euclidean_space => 'a::euclidean_space" - assumes lf: "linear f" and lf': "linear f'" - shows "f o f' = id \ f' o f = id" -proof- - {fix f f':: "'a => 'a" - assume lf: "linear f" "linear f'" and f: "f o f' = id" - from f have sf: "surj f" - apply (auto simp add: o_def id_def surj_def) - by metis - from linear_surjective_isomorphism[OF lf(1) sf] lf f - have "f' o f = id" unfolding fun_eq_iff o_def id_def - by metis} - then show ?thesis using lf lf' by metis -qed - -text {* Moreover, a one-sided inverse is automatically linear. *} - -lemma left_inverse_linear: fixes f::"'a::euclidean_space => 'a::euclidean_space" - assumes lf: "linear f" and gf: "g o f = id" - shows "linear g" -proof- - from gf have fi: "inj f" apply (auto simp add: inj_on_def o_def id_def fun_eq_iff) - by metis - from linear_injective_isomorphism[OF lf fi] - obtain h:: "'a \ 'a" where - h: "linear h" "\x. h (f x) = x" "\x. f (h x) = x" by blast - have "h = g" apply (rule ext) using gf h(2,3) - apply (simp add: o_def id_def fun_eq_iff) - by metis - with h(1) show ?thesis by blast -qed - -subsection {* Infinity norm *} - -definition "infnorm (x::'a::euclidean_space) = Sup {abs(x$$i) |i. ii. i \ (UNIV :: 'n set)" - by auto - -lemma infnorm_set_image: - "{abs((x::'a::euclidean_space)$$i) |i. ii. abs(x$$i)) ` {.. {}" - unfolding infnorm_set_image - by auto - -lemma infnorm_pos_le: "0 \ infnorm (x::'a::euclidean_space)" - unfolding infnorm_def - unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma] - unfolding infnorm_set_image - by auto - -lemma infnorm_triangle: "infnorm ((x::'a::euclidean_space) + y) \ infnorm x + infnorm y" -proof- - have th: "\x y (z::real). x - y <= z \ x - z <= y" by arith - have th1: "\S f. f ` S = { f i| i. i \ S}" by blast - have th2: "\x (y::real). abs(x + y) - abs(x) <= abs(y)" by arith - have *:"\i. i \ {.. i {}" by blast - have th1: "\S f. f ` S = { f i| i. i \ S}" by blast - show ?thesis unfolding infnorm_def - apply(subst Sup_finite_ge_iff) using Sup_finite_in[OF fS S0] - using infnorm_set_image using True by auto -qed - -lemma infnorm_mul_lemma: "infnorm(a *\<^sub>R x) <= \a\ * infnorm x" - apply (subst infnorm_def) - unfolding Sup_finite_le_iff[OF infnorm_set_lemma] - unfolding infnorm_set_image ball_simps euclidean_scaleR abs_mult - using component_le_infnorm[of x] by(auto intro: mult_mono) - -lemma infnorm_mul: "infnorm(a *\<^sub>R x) = abs a * infnorm x" -proof- - {assume a0: "a = 0" hence ?thesis by (simp add: infnorm_0) } - moreover - {assume a0: "a \ 0" - from a0 have th: "(1/a) *\<^sub>R (a *\<^sub>R x) = x" by simp - from a0 have ap: "\a\ > 0" by arith - from infnorm_mul_lemma[of "1/a" "a *\<^sub>R x"] - have "infnorm x \ 1/\a\ * infnorm (a*\<^sub>R x)" - unfolding th by simp - with ap have "\a\ * infnorm x \ \a\ * (1/\a\ * infnorm (a *\<^sub>R x))" by (simp add: field_simps) - then have "\a\ * infnorm x \ infnorm (a*\<^sub>R x)" - using ap by (simp add: field_simps) - with infnorm_mul_lemma[of a x] have ?thesis by arith } - ultimately show ?thesis by blast -qed - -lemma infnorm_pos_lt: "infnorm x > 0 \ x \ 0" - using infnorm_pos_le[of x] infnorm_eq_0[of x] by arith - -text {* Prove that it differs only up to a bound from Euclidean norm. *} - -lemma infnorm_le_norm: "infnorm x \ norm x" - unfolding infnorm_def Sup_finite_le_iff[OF infnorm_set_lemma] - unfolding infnorm_set_image ball_simps - by (metis component_le_norm) - -lemma card_enum: "card {1 .. n} = n" by auto - -lemma norm_le_infnorm: "norm(x) <= sqrt(real DIM('a)) * infnorm(x::'a::euclidean_space)" -proof- - let ?d = "DIM('a)" - have "real ?d \ 0" by simp - hence d2: "(sqrt (real ?d))^2 = real ?d" - by (auto intro: real_sqrt_pow2) - have th: "sqrt (real ?d) * infnorm x \ 0" - by (simp add: zero_le_mult_iff infnorm_pos_le) - have th1: "x \ x \ (sqrt (real ?d) * infnorm x)^2" - unfolding power_mult_distrib d2 - unfolding real_of_nat_def apply(subst euclidean_inner) - apply (subst power2_abs[symmetric]) - apply(rule order_trans[OF setsum_bounded[where K="\infnorm x\\"]]) - apply(auto simp add: power2_eq_square[symmetric]) - apply (subst power2_abs[symmetric]) - apply (rule power_mono) - unfolding infnorm_def Sup_finite_ge_iff[OF infnorm_set_lemma] - unfolding infnorm_set_image bex_simps apply(rule_tac x=i in bexI) by auto - from real_le_lsqrt[OF inner_ge_zero th th1] - show ?thesis unfolding norm_eq_sqrt_inner id_def . -qed - -text {* Equality in Cauchy-Schwarz and triangle inequalities. *} - -lemma norm_cauchy_schwarz_eq: "x \ y = norm x * norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x" (is "?lhs \ ?rhs") -proof- - {assume h: "x = 0" - hence ?thesis by simp} - moreover - {assume h: "y = 0" - hence ?thesis by simp} - moreover - {assume x: "x \ 0" and y: "y \ 0" - from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"] - have "?rhs \ (norm y * (norm y * norm x * norm x - norm x * (x \ y)) - norm x * (norm y * (y \ x) - norm x * norm y * norm y) = 0)" - using x y - unfolding inner_simps - unfolding power2_norm_eq_inner[symmetric] power2_eq_square diff_eq_0_iff_eq apply (simp add: inner_commute) - apply (simp add: field_simps) by metis - also have "\ \ (2 * norm x * norm y * (norm x * norm y - x \ y) = 0)" using x y - by (simp add: field_simps inner_commute) - also have "\ \ ?lhs" using x y - apply simp - by metis - finally have ?thesis by blast} - ultimately show ?thesis by blast -qed - -lemma norm_cauchy_schwarz_abs_eq: - shows "abs(x \ y) = norm x * norm y \ - norm x *\<^sub>R y = norm y *\<^sub>R x \ norm(x) *\<^sub>R y = - norm y *\<^sub>R x" (is "?lhs \ ?rhs") -proof- - have th: "\(x::real) a. a \ 0 \ abs x = a \ x = a \ x = - a" by arith - have "?rhs \ norm x *\<^sub>R y = norm y *\<^sub>R x \ norm (- x) *\<^sub>R y = norm y *\<^sub>R (- x)" - by simp - also have "\ \(x \ y = norm x * norm y \ - (-x) \ y = norm x * norm y)" - unfolding norm_cauchy_schwarz_eq[symmetric] - unfolding norm_minus_cancel norm_scaleR .. - also have "\ \ ?lhs" - unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] inner_simps by auto - finally show ?thesis .. -qed - -lemma norm_triangle_eq: - fixes x y :: "'a::real_inner" - shows "norm(x + y) = norm x + norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x" -proof- - {assume x: "x =0 \ y =0" - hence ?thesis by (cases "x=0", simp_all)} - moreover - {assume x: "x \ 0" and y: "y \ 0" - hence "norm x \ 0" "norm y \ 0" - by simp_all - hence n: "norm x > 0" "norm y > 0" - using norm_ge_zero[of x] norm_ge_zero[of y] - by arith+ - have th: "\(a::real) b c. a + b + c \ 0 ==> (a = b + c \ a^2 = (b + c)^2)" by algebra - have "norm(x + y) = norm x + norm y \ norm(x + y)^ 2 = (norm x + norm y) ^2" - apply (rule th) using n norm_ge_zero[of "x + y"] - by arith - also have "\ \ norm x *\<^sub>R y = norm y *\<^sub>R x" - unfolding norm_cauchy_schwarz_eq[symmetric] - unfolding power2_norm_eq_inner inner_simps - by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps) - finally have ?thesis .} - ultimately show ?thesis by blast -qed - -subsection {* Collinearity *} - -definition - collinear :: "'a::real_vector set \ bool" where - "collinear S \ (\u. \x \ S. \ y \ S. \c. x - y = c *\<^sub>R u)" - -lemma collinear_empty: "collinear {}" by (simp add: collinear_def) - -lemma collinear_sing: "collinear {x}" - by (simp add: collinear_def) - -lemma collinear_2: "collinear {x, y}" - apply (simp add: collinear_def) - apply (rule exI[where x="x - y"]) - apply auto - apply (rule exI[where x=1], simp) - apply (rule exI[where x="- 1"], simp) - done - -lemma collinear_lemma: "collinear {0,x,y} \ x = 0 \ y = 0 \ (\c. y = c *\<^sub>R x)" (is "?lhs \ ?rhs") -proof- - {assume "x=0 \ y = 0" hence ?thesis - by (cases "x = 0", simp_all add: collinear_2 insert_commute)} - moreover - {assume x: "x \ 0" and y: "y \ 0" - {assume h: "?lhs" - then obtain u where u: "\ x\ {0,x,y}. \y\ {0,x,y}. \c. x - y = c *\<^sub>R u" unfolding collinear_def by blast - from u[rule_format, of x 0] u[rule_format, of y 0] - obtain cx and cy where - cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u" - by auto - from cx x have cx0: "cx \ 0" by auto - from cy y have cy0: "cy \ 0" by auto - let ?d = "cy / cx" - from cx cy cx0 have "y = ?d *\<^sub>R x" - by simp - hence ?rhs using x y by blast} - moreover - {assume h: "?rhs" - then obtain c where c: "y = c *\<^sub>R x" using x y by blast - have ?lhs unfolding collinear_def c - apply (rule exI[where x=x]) - apply auto - apply (rule exI[where x="- 1"], simp) - apply (rule exI[where x= "-c"], simp) - apply (rule exI[where x=1], simp) - apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib) - apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib) - done} - ultimately have ?thesis by blast} - ultimately show ?thesis by blast -qed - -lemma norm_cauchy_schwarz_equal: - shows "abs(x \ y) = norm x * norm y \ collinear {0,x,y}" -unfolding norm_cauchy_schwarz_abs_eq -apply (cases "x=0", simp_all add: collinear_2) -apply (cases "y=0", simp_all add: collinear_2 insert_commute) -unfolding collinear_lemma -apply simp -apply (subgoal_tac "norm x \ 0") -apply (subgoal_tac "norm y \ 0") -apply (rule iffI) -apply (cases "norm x *\<^sub>R y = norm y *\<^sub>R x") -apply (rule exI[where x="(1/norm x) * norm y"]) -apply (drule sym) -unfolding scaleR_scaleR[symmetric] -apply (simp add: field_simps) -apply (rule exI[where x="(1/norm x) * - norm y"]) -apply clarify -apply (drule sym) -unfolding scaleR_scaleR[symmetric] -apply (simp add: field_simps) -apply (erule exE) -apply (erule ssubst) -unfolding scaleR_scaleR -unfolding norm_scaleR -apply (subgoal_tac "norm x * c = \c\ * norm x \ norm x * c = - \c\ * norm x") -apply (case_tac "c <= 0", simp add: field_simps) -apply (simp add: field_simps) -apply (case_tac "c <= 0", simp add: field_simps) -apply (simp add: field_simps) -apply simp -apply simp -done - -subsection "Instantiate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}." +subsubsection {* Type @{typ real} *} instantiation real :: euclidean_space begin @@ -3307,18 +174,7 @@ end -lemma basis_real_range: "basis ` {..<1} = {1::real}" by auto - -instance real::ordered_euclidean_space - by default (auto simp add: euclidean_component_def) - -lemma Eucl_real_simps[simp]: - "(x::real) $$ 0 = x" - "(\\ i. f i) = ((f 0)::real)" - "\i. i > 0 \ x $$ i = 0" - defer apply(subst euclidean_eq) apply safe - unfolding euclidean_lambda_beta' - unfolding euclidean_component_def by auto +subsubsection {* Type @{typ complex} *} instantiation complex :: euclidean_space begin @@ -3353,14 +209,10 @@ end -lemma complex_basis[simp]: - shows "basis 0 = (1::complex)" and "basis 1 = ii" and "basis (Suc 0) = ii" - unfolding basis_complex_def by auto - lemma DIM_complex[simp]: "DIM(complex) = 2" by (rule dimension_complex_def) -section {* Products Spaces *} +subsubsection {* Type @{typ "'a \ 'b"} *} instantiation prod :: (euclidean_space, euclidean_space) euclidean_space begin @@ -3400,18 +252,4 @@ end -lemma DIM_prod[simp]: "DIM('a \ 'b) = DIM('b::euclidean_space) + DIM('a::euclidean_space)" - (* FIXME: why this orientation? Why not "DIM('a) + DIM('b)" ? *) - unfolding dimension_prod_def by (rule add_commute) - -instantiation prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space -begin - -definition "x \ (y::('a\'b)) \ (\i'b). x $$ i \ y $$ i)" -definition "x < (y::('a\'b)) \ (\i'b). x $$ i < y $$ i)" - -instance proof qed (auto simp: less_prod_def less_eq_prod_def) end - - -end diff -r 0f35a870ecf1 -r 691c52e900ca src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Aug 10 09:23:42 2011 -0700 @@ -0,0 +1,3181 @@ +(* Title: HOL/Multivariate_Analysis/Linear_Algebra.thy + Author: Amine Chaieb, University of Cambridge +*) + +header {* Elementary linear algebra on Euclidean spaces *} + +theory Linear_Algebra +imports + Euclidean_Space + "~~/src/HOL/Library/Infinite_Set" + L2_Norm + "~~/src/HOL/Library/Convex" +uses + "~~/src/HOL/Library/positivstellensatz.ML" (* FIXME duplicate use!? *) + ("normarith.ML") +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 "\" 70) + +subsection {* A connectedness or intermediate value lemma with several applications. *} + +lemma connected_real_lemma: + fixes f :: "real \ 'a::metric_space" + assumes ab: "a \ b" and fa: "f a \ e1" and fb: "f b \ e2" + and dst: "\e x. a <= x \ x <= b \ 0 < e ==> \d > 0. \y. abs(y - x) < d \ dist(f y) (f x) < e" + and e1: "\y \ e1. \e > 0. \y'. dist y' y < e \ y' \ e1" + and e2: "\y \ e2. \e > 0. \y'. dist y' y < e \ y' \ e2" + and e12: "~(\x \ a. x <= b \ f x \ e1 \ f x \ e2)" + shows "\x \ a. x <= b \ f x \ e1 \ f x \ e2" (is "\ x. ?P x") +proof- + let ?S = "{c. \x \ a. x <= c \ f x \ e1}" + have Se: " \x. x \ ?S" apply (rule exI[where x=a]) by (auto simp add: fa) + have Sub: "\y. isUb UNIV ?S y" + apply (rule exI[where x= b]) + using ab fb e12 by (auto simp add: isUb_def setle_def) + from reals_complete[OF Se Sub] obtain l where + l: "isLub UNIV ?S l"by blast + have alb: "a \ l" "l \ b" using l ab fa fb e12 + apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) + by (metis linorder_linear) + have ale1: "\z \ a. z < l \ f z \ e1" using l + apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) + by (metis linorder_linear not_le) + have th1: "\z x e d :: real. z <= x + e \ e < d ==> z < x \ abs(z - x) < d" by arith + have th2: "\e x:: real. 0 < e ==> ~(x + e <= x)" by arith + have "\d::real. 0 < d \ 0 < d/2 \ d/2 < d" by simp + then have th3: "\d::real. d > 0 \ \e > 0. e < d" by blast + {assume le2: "f l \ e2" + from le2 fa fb e12 alb have la: "l \ a" by metis + hence lap: "l - a > 0" using alb by arith + from e2[rule_format, OF le2] obtain e where + e: "e > 0" "\y. dist y (f l) < e \ y \ e2" by metis + from dst[OF alb e(1)] obtain d where + d: "d > 0" "\y. \y - l\ < d \ dist (f y) (f l) < e" by metis + let ?d' = "min (d/2) ((l - a)/2)" + have "?d' < d \ 0 < ?d' \ ?d' < l - a" using lap d(1) + by (simp add: min_max.less_infI2) + then have "\d'. d' < d \ d' >0 \ l - d' > a" by auto + then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis + from d e have th0: "\y. \y - l\ < d \ f y \ e2" by metis + from th0[rule_format, of "l - d'"] d' have "f (l - d') \ e2" by auto + moreover + have "f (l - d') \ e1" using ale1[rule_format, of "l -d'"] d' by auto + ultimately have False using e12 alb d' by auto} + moreover + {assume le1: "f l \ e1" + from le1 fa fb e12 alb have lb: "l \ b" by metis + hence blp: "b - l > 0" using alb by arith + from e1[rule_format, OF le1] obtain e where + e: "e > 0" "\y. dist y (f l) < e \ y \ e1" by metis + from dst[OF alb e(1)] obtain d where + d: "d > 0" "\y. \y - l\ < d \ dist (f y) (f l) < e" by metis + have "\d::real. 0 < d \ d/2 < d \ 0 < d/2" by simp + then have "\d'. d' < d \ d' >0" using d(1) by blast + then obtain d' where d': "d' > 0" "d' < d" by metis + from d e have th0: "\y. \y - l\ < d \ f y \ e1" by auto + hence "\y. l \ y \ y \ l + d' \ f y \ e1" using d' by auto + with ale1 have "\y. a \ y \ y \ l + d' \ f y \ e1" by auto + with l d' have False + by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) } + ultimately show ?thesis using alb by metis +qed + +text{* One immediately useful corollary is the existence of square roots! --- Should help to get rid of all the development of square-root for reals as a special case *} + +lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)" +proof- + have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith + thus ?thesis by (simp add: field_simps power2_eq_square) +qed + +lemma square_continuous: "0 < (e::real) ==> \d. 0 < d \ (\y. abs(y - x) < d \ abs(y * y - x * x) < e)" + using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_eq, rule_format, of e x] apply (auto simp add: power2_eq_square) + apply (rule_tac x="s" in exI) + apply auto + apply (erule_tac x=y in allE) + apply auto + done + +lemma real_le_lsqrt: "0 <= x \ 0 <= y \ x <= y^2 ==> sqrt x <= y" + using real_sqrt_le_iff[of x "y^2"] by simp + +lemma real_le_rsqrt: "x^2 \ y \ x \ sqrt y" + using real_sqrt_le_mono[of "x^2" y] by simp + +lemma real_less_rsqrt: "x^2 < y \ x < sqrt y" + using real_sqrt_less_mono[of "x^2" y] by simp + +lemma sqrt_even_pow2: assumes n: "even n" + shows "sqrt(2 ^ n) = 2 ^ (n div 2)" +proof- + from n obtain m where m: "n = 2*m" unfolding even_mult_two_ex .. + from m have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)" + by (simp only: power_mult[symmetric] mult_commute) + then show ?thesis using m by simp +qed + +lemma real_div_sqrt: "0 <= x ==> x / sqrt(x) = sqrt(x)" + apply (cases "x = 0", simp_all) + using sqrt_divide_self_eq[of x] + apply (simp add: inverse_eq_divide field_simps) + done + +text{* Hence derive more interesting properties of the norm. *} + +(* FIXME: same as norm_scaleR +lemma norm_mul[simp]: "norm(a *\<^sub>R x) = abs(a) * norm x" + by (simp add: norm_vector_def setL2_right_distrib abs_mult) +*) + +lemma norm_eq_0_dot: "(norm x = 0) \ (inner x x = (0::real))" + by (simp add: setL2_def power2_eq_square) + +lemma norm_cauchy_schwarz: + shows "inner x y <= norm x * norm y" + using Cauchy_Schwarz_ineq2[of x y] by auto + +lemma norm_cauchy_schwarz_abs: + shows "\inner x y\ \ norm x * norm y" + by (rule Cauchy_Schwarz_ineq2) + +lemma norm_triangle_sub: + fixes x y :: "'a::real_normed_vector" + shows "norm x \ norm y + norm (x - y)" + using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps) + +lemma real_abs_norm: "\norm x\ = norm x" + by (rule abs_norm_cancel) +lemma real_abs_sub_norm: "\norm x - norm y\ <= norm(x - y)" + by (rule norm_triangle_ineq3) +lemma norm_le: "norm(x) <= norm(y) \ x \ x <= y \ y" + by (simp add: norm_eq_sqrt_inner) +lemma norm_lt: "norm(x) < norm(y) \ x \ x < y \ y" + by (simp add: norm_eq_sqrt_inner) +lemma norm_eq: "norm(x) = norm (y) \ x \ x = y \ y" + apply(subst order_eq_iff) unfolding norm_le by auto +lemma norm_eq_1: "norm(x) = 1 \ x \ x = 1" + unfolding norm_eq_sqrt_inner by auto + +text{* Squaring equations and inequalities involving norms. *} + +lemma dot_square_norm: "x \ x = norm(x)^2" + by (simp add: norm_eq_sqrt_inner) + +lemma norm_eq_square: "norm(x) = a \ 0 <= a \ x \ x = a^2" + by (auto simp add: norm_eq_sqrt_inner) + +lemma real_abs_le_square_iff: "\x\ \ \y\ \ (x::real)^2 \ y^2" +proof + assume "\x\ \ \y\" + then have "\x\\ \ \y\\" by (rule power_mono, simp) + then show "x\ \ y\" by simp +next + assume "x\ \ y\" + then have "sqrt (x\) \ sqrt (y\)" by (rule real_sqrt_le_mono) + then show "\x\ \ \y\" by simp +qed + +lemma norm_le_square: "norm(x) <= a \ 0 <= a \ x \ x <= a^2" + apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) + using norm_ge_zero[of x] + apply arith + done + +lemma norm_ge_square: "norm(x) >= a \ a <= 0 \ x \ x >= a ^ 2" + apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) + using norm_ge_zero[of x] + apply arith + done + +lemma norm_lt_square: "norm(x) < a \ 0 < a \ x \ x < a^2" + by (metis not_le norm_ge_square) +lemma norm_gt_square: "norm(x) > a \ a < 0 \ x \ x > a^2" + by (metis norm_le_square not_less) + +text{* Dot product in terms of the norm rather than conversely. *} + +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 \ y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2" + unfolding power2_norm_eq_inner inner_simps inner_commute by auto + +lemma dot_norm_neg: "x \ y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2" + unfolding power2_norm_eq_inner inner_simps inner_commute by(auto simp add:algebra_simps) + +text{* Equality of vectors in terms of @{term "op \"} products. *} + +lemma vector_eq: "x = y \ x \ x = x \ y \ y \ y = x \ x" (is "?lhs \ ?rhs") +proof + assume ?lhs then show ?rhs by simp +next + assume ?rhs + then have "x \ x - x \ y = 0 \ x \ y - y \ y = 0" by simp + hence "x \ (x - y) = 0 \ y \ (x - y) = 0" by (simp add: inner_simps inner_commute) + then have "(x - y) \ (x - y) = 0" by (simp add: field_simps inner_simps inner_commute) + then show "x = y" by (simp) +qed + +subsection{* General linear decision procedure for normed spaces. *} + +lemma norm_cmul_rule_thm: + fixes x :: "'a::real_normed_vector" + shows "b >= norm(x) ==> \c\ * b >= norm(scaleR c x)" + unfolding norm_scaleR + apply (erule mult_left_mono) + apply simp + done + + (* FIXME: Move all these theorems into the ML code using lemma antiquotation *) +lemma norm_add_rule_thm: + fixes x1 x2 :: "'a::real_normed_vector" + shows "norm x1 \ b1 \ norm x2 \ b2 \ norm (x1 + x2) \ b1 + b2" + by (rule order_trans [OF norm_triangle_ineq add_mono]) + +lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \ b == a - b \ 0" + by (simp add: field_simps) + +lemma pth_1: + fixes x :: "'a::real_normed_vector" + shows "x == scaleR 1 x" by simp + +lemma pth_2: + fixes x :: "'a::real_normed_vector" + shows "x - y == x + -y" by (atomize (full)) simp + +lemma pth_3: + fixes x :: "'a::real_normed_vector" + shows "- x == scaleR (-1) x" by simp + +lemma pth_4: + fixes x :: "'a::real_normed_vector" + shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all + +lemma pth_5: + fixes x :: "'a::real_normed_vector" + shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp + +lemma pth_6: + fixes x :: "'a::real_normed_vector" + shows "scaleR c (x + y) == scaleR c x + scaleR c y" + by (simp add: scaleR_right_distrib) + +lemma pth_7: + fixes x :: "'a::real_normed_vector" + shows "0 + x == x" and "x + 0 == x" by simp_all + +lemma pth_8: + fixes x :: "'a::real_normed_vector" + shows "scaleR c x + scaleR d x == scaleR (c + d) x" + by (simp add: scaleR_left_distrib) + +lemma pth_9: + fixes x :: "'a::real_normed_vector" shows + "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z" + "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z" + "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)" + by (simp_all add: algebra_simps) + +lemma pth_a: + fixes x :: "'a::real_normed_vector" + shows "scaleR 0 x + y == y" by simp + +lemma pth_b: + fixes x :: "'a::real_normed_vector" shows + "scaleR c x + scaleR d y == scaleR c x + scaleR d y" + "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)" + "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)" + "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))" + by (simp_all add: algebra_simps) + +lemma pth_c: + fixes x :: "'a::real_normed_vector" shows + "scaleR c x + scaleR d y == scaleR d y + scaleR c x" + "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)" + "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)" + "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)" + by (simp_all add: algebra_simps) + +lemma pth_d: + fixes x :: "'a::real_normed_vector" + shows "x + 0 == x" by simp + +lemma norm_imp_pos_and_ge: + fixes x :: "'a::real_normed_vector" + shows "norm x == n \ norm x \ 0 \ n \ norm x" + by atomize auto + +lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \ 0 \ -x \ 0" by arith + +lemma norm_pths: + fixes x :: "'a::real_normed_vector" shows + "x = y \ norm (x - y) \ 0" + "x \ y \ \ (norm (x - y) \ 0)" + using norm_ge_zero[of "x - y"] by auto + +use "normarith.ML" + +method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) +*} "prove simple linear statements about vector norms" + + +text{* Hence more metric properties. *} + +lemma norm_triangle_half_r: + shows "norm (y - x1) < e / 2 \ norm (y - x2) < e / 2 \ norm (x1 - x2) < e" + using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto + +lemma norm_triangle_half_l: assumes "norm (x - y) < e / 2" "norm (x' - (y)) < e / 2" + shows "norm (x - x') < e" + using dist_triangle_half_l[OF assms[unfolded dist_norm[THEN sym]]] + unfolding dist_norm[THEN sym] . + +lemma norm_triangle_le: "norm(x) + norm y <= e ==> norm(x + y) <= e" + by (metis order_trans norm_triangle_ineq) + +lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e" + by (metis basic_trans_rules(21) norm_triangle_ineq) + +lemma dist_triangle_add: + fixes x y x' y' :: "'a::real_normed_vector" + shows "dist (x + y) (x' + y') <= dist x x' + dist y y'" + by norm + +lemma dist_triangle_add_half: + fixes x x' y y' :: "'a::real_normed_vector" + shows "dist x x' < e / 2 \ dist y y' < e / 2 \ dist(x + y) (x' + y') < e" + by norm + +lemma setsum_clauses: + shows "setsum f {} = 0" + and "finite S \ setsum f (insert x S) = + (if x \ S then setsum f S else f x + setsum f S)" + by (auto simp add: insert_absorb) + +lemma setsum_norm: + fixes f :: "'a \ 'b::real_normed_vector" + assumes fS: "finite S" + shows "norm (setsum f S) <= setsum (\x. norm(f x)) S" +proof(induct rule: finite_induct[OF fS]) + case 1 thus ?case by simp +next + case (2 x S) + from "2.hyps" have "norm (setsum f (insert x S)) \ norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq) + also have "\ \ norm (f x) + setsum (\x. norm(f x)) S" + using "2.hyps" by simp + finally show ?case using "2.hyps" by simp +qed + +lemma setsum_norm_le: + fixes f :: "'a \ 'b::real_normed_vector" + assumes fS: "finite S" + and fg: "\x \ S. norm (f x) \ g x" + shows "norm (setsum f S) \ setsum g S" +proof- + from fg have "setsum (\x. norm(f x)) S <= setsum g S" + by - (rule setsum_mono, simp) + then show ?thesis using setsum_norm[OF fS, of f] fg + by arith +qed + +lemma setsum_norm_bound: + fixes f :: "'a \ 'b::real_normed_vector" + assumes fS: "finite S" + and K: "\x \ S. norm (f x) \ K" + shows "norm (setsum f S) \ of_nat (card S) * K" + using setsum_norm_le[OF fS K] setsum_constant[symmetric] + by simp + +lemma setsum_group: + assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \ T" + shows "setsum (\y. setsum g {x. x\ S \ f x = y}) T = setsum g S" + apply (subst setsum_image_gen[OF fS, of g f]) + apply (rule setsum_mono_zero_right[OF fT fST]) + by (auto intro: setsum_0') + +lemma dot_lsum: "finite S \ setsum f S \ y = setsum (\x. f x \ y) S " + apply(induct rule: finite_induct) by(auto simp add: inner_simps) + +lemma dot_rsum: "finite S \ y \ setsum f S = setsum (\x. y \ f x) S " + apply(induct rule: finite_induct) by(auto simp add: inner_simps) + +lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = z" +proof + assume "\x. x \ y = x \ z" + hence "\x. x \ (y - z) = 0" by (simp add: inner_simps) + hence "(y - z) \ (y - z) = 0" .. + thus "y = z" by simp +qed simp + +lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ x = y" +proof + assume "\z. x \ z = y \ z" + hence "\z. (x - y) \ z = 0" by (simp add: inner_simps) + hence "(x - y) \ (x - y) = 0" .. + thus "x = y" by simp +qed simp + +subsection{* Orthogonality. *} + +context real_inner +begin + +definition "orthogonal x y \ (x \ y = 0)" + +lemma orthogonal_clauses: + "orthogonal a 0" + "orthogonal a x \ orthogonal a (c *\<^sub>R x)" + "orthogonal a x \ orthogonal a (-x)" + "orthogonal a x \ orthogonal a y \ orthogonal a (x + y)" + "orthogonal a x \ orthogonal a y \ orthogonal a (x - y)" + "orthogonal 0 a" + "orthogonal x a \ orthogonal (c *\<^sub>R x) a" + "orthogonal x a \ orthogonal (-x) a" + "orthogonal x a \ orthogonal y a \ orthogonal (x + y) a" + "orthogonal x a \ orthogonal y a \ orthogonal (x - y) a" + unfolding orthogonal_def inner_simps inner_add_left inner_add_right inner_diff_left inner_diff_right (*FIXME*) by auto + +end + +lemma orthogonal_commute: "orthogonal x y \ orthogonal y x" + by (simp add: orthogonal_def inner_commute) + +subsection{* Linear functions. *} + +definition + linear :: "('a::real_vector \ 'b::real_vector) \ bool" where + "linear f \ (\x y. f(x + y) = f x + f y) \ (\c x. f(c *\<^sub>R x) = c *\<^sub>R f x)" + +lemma linearI: assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" + shows "linear f" using assms unfolding linear_def by auto + +lemma linear_compose_cmul: "linear f ==> linear (\x. c *\<^sub>R f x)" + by (simp add: linear_def algebra_simps) + +lemma linear_compose_neg: "linear f ==> linear (\x. -(f(x)))" + by (simp add: linear_def) + +lemma linear_compose_add: "linear f \ linear g ==> linear (\x. f(x) + g(x))" + by (simp add: linear_def algebra_simps) + +lemma linear_compose_sub: "linear f \ linear g ==> linear (\x. f x - g x)" + by (simp add: linear_def algebra_simps) + +lemma linear_compose: "linear f \ linear g ==> linear (g o f)" + by (simp add: linear_def) + +lemma linear_id: "linear id" by (simp add: linear_def id_def) + +lemma linear_zero: "linear (\x. 0)" by (simp add: linear_def) + +lemma linear_compose_setsum: + assumes fS: "finite S" and lS: "\a \ S. linear (f a)" + shows "linear(\x. setsum (\a. f a x) S)" + using lS + apply (induct rule: finite_induct[OF fS]) + by (auto simp add: linear_zero intro: linear_compose_add) + +lemma linear_0: "linear f \ f 0 = 0" + unfolding linear_def + apply clarsimp + apply (erule allE[where x="0::'a"]) + apply simp + done + +lemma linear_cmul: "linear f ==> f(c *\<^sub>R x) = c *\<^sub>R f x" by (simp add: linear_def) + +lemma linear_neg: "linear f ==> f (-x) = - f x" + using linear_cmul [where c="-1"] by simp + +lemma linear_add: "linear f ==> f(x + y) = f x + f y" by (metis linear_def) + +lemma linear_sub: "linear f ==> f(x - y) = f x - f y" + by (simp add: diff_minus linear_add linear_neg) + +lemma linear_setsum: + assumes lf: "linear f" and fS: "finite S" + shows "f (setsum g S) = setsum (f o g) S" +proof (induct rule: finite_induct[OF fS]) + case 1 thus ?case by (simp add: linear_0[OF lf]) +next + case (2 x F) + have "f (setsum g (insert x F)) = f (g x + setsum g F)" using "2.hyps" + by simp + also have "\ = f (g x) + f (setsum g F)" using linear_add[OF lf] by simp + also have "\ = setsum (f o g) (insert x F)" using "2.hyps" by simp + finally show ?case . +qed + +lemma linear_setsum_mul: + assumes lf: "linear f" and fS: "finite S" + shows "f (setsum (\i. c i *\<^sub>R v i) S) = setsum (\i. c i *\<^sub>R f (v i)) S" + using linear_setsum[OF lf fS, of "\i. c i *\<^sub>R v i" , unfolded o_def] + linear_cmul[OF lf] by simp + +lemma linear_injective_0: + assumes lf: "linear f" + shows "inj f \ (\x. f x = 0 \ x = 0)" +proof- + have "inj f \ (\ x y. f x = f y \ x = y)" by (simp add: inj_on_def) + also have "\ \ (\ x y. f x - f y = 0 \ x - y = 0)" by simp + also have "\ \ (\ x y. f (x - y) = 0 \ x - y = 0)" + by (simp add: linear_sub[OF lf]) + also have "\ \ (\ x. f x = 0 \ x = 0)" by auto + finally show ?thesis . +qed + +subsection{* Bilinear functions. *} + +definition "bilinear f \ (\x. linear(\y. f x y)) \ (\y. linear(\x. f x y))" + +lemma bilinear_ladd: "bilinear h ==> h (x + y) z = (h x z) + (h y z)" + by (simp add: bilinear_def linear_def) +lemma bilinear_radd: "bilinear h ==> h x (y + z) = (h x y) + (h x z)" + by (simp add: bilinear_def linear_def) + +lemma bilinear_lmul: "bilinear h ==> h (c *\<^sub>R x) y = c *\<^sub>R (h x y)" + by (simp add: bilinear_def linear_def) + +lemma bilinear_rmul: "bilinear h ==> h x (c *\<^sub>R y) = c *\<^sub>R (h x y)" + by (simp add: bilinear_def linear_def) + +lemma bilinear_lneg: "bilinear h ==> h (- x) y = -(h x y)" + by (simp only: scaleR_minus1_left [symmetric] bilinear_lmul) + +lemma bilinear_rneg: "bilinear h ==> h x (- y) = - h x y" + by (simp only: scaleR_minus1_left [symmetric] bilinear_rmul) + +lemma (in ab_group_add) eq_add_iff: "x = x + y \ y = 0" + using add_imp_eq[of x y 0] by auto + +lemma bilinear_lzero: + assumes bh: "bilinear h" shows "h 0 x = 0" + using bilinear_ladd[OF bh, of 0 0 x] + by (simp add: eq_add_iff field_simps) + +lemma bilinear_rzero: + assumes bh: "bilinear h" shows "h x 0 = 0" + using bilinear_radd[OF bh, of x 0 0 ] + by (simp add: eq_add_iff field_simps) + +lemma bilinear_lsub: "bilinear h ==> h (x - y) z = h x z - h y z" + by (simp add: diff_minus bilinear_ladd bilinear_lneg) + +lemma bilinear_rsub: "bilinear h ==> h z (x - y) = h z x - h z y" + by (simp add: diff_minus bilinear_radd 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 (\(i,j). h (f i) (g j)) (S \ T) " +proof- + have "h (setsum f S) (setsum g T) = setsum (\x. h (f x) (setsum g T)) S" + apply (rule linear_setsum[unfolded o_def]) + using bh fS by (auto simp add: bilinear_def) + also have "\ = setsum (\x. setsum (\y. h (f x) (g y)) T) S" + apply (rule setsum_cong, simp) + apply (rule linear_setsum[unfolded o_def]) + using bh fT by (auto simp add: bilinear_def) + finally show ?thesis unfolding setsum_cartesian_product . +qed + +subsection{* Adjoints. *} + +definition "adjoint f = (SOME f'. \x y. f x \ y = x \ f' y)" + +lemma adjoint_unique: + assumes "\x y. inner (f x) y = inner x (g y)" + shows "adjoint f = g" +unfolding adjoint_def +proof (rule some_equality) + show "\x y. inner (f x) y = inner x (g y)" using assms . +next + fix h assume "\x y. inner (f x) y = inner x (h y)" + hence "\x y. inner x (g y) = inner x (h y)" using assms by simp + hence "\x y. inner x (g y - h y) = 0" by (simp add: inner_diff_right) + hence "\y. inner (g y - h y) (g y - h y) = 0" by simp + hence "\y. h y = g y" by simp + thus "h = g" by (simp add: ext) +qed + +lemma choice_iff: "(\x. \y. P x y) \ (\f. \x. P x (f x))" by metis + +subsection{* Interlude: Some properties of real sets *} + +lemma seq_mono_lemma: assumes "\(n::nat) \ m. (d n :: real) < e n" and "\n \ m. e n <= e m" + shows "\n \ 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 "\r. subseq r \ (\n. r n \ S)" +unfolding subseq_def +using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto + +lemma approachable_lt_le: "(\(d::real)>0. \x. f x < d \ P x) \ (\d>0. \x. f x \ d \ P x)" +apply auto +apply (rule_tac x="d/2" in exI) +apply auto +done + + +lemma triangle_lemma: + assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x^2 <= y^2 + z^2" + shows "x <= y + z" +proof- + have "y^2 + z^2 \ y^2 + 2*y*z + z^2" using z y by (simp add: mult_nonneg_nonneg) + with xy have th: "x ^2 \ (y+z)^2" by (simp add: power2_eq_square field_simps) + from y z have yz: "y + z \ 0" by arith + from power2_le_imp_le[OF th yz] show ?thesis . +qed + +text {* TODO: move to NthRoot *} +lemma sqrt_add_le_add_sqrt: + assumes x: "0 \ x" and y: "0 \ y" + shows "sqrt (x + y) \ sqrt x + sqrt y" +apply (rule power2_le_imp_le) +apply (simp add: real_sum_squared_expand add_nonneg_nonneg x y) +apply (simp add: mult_nonneg_nonneg x y) +apply (simp add: add_nonneg_nonneg x y) +done + +subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *} + +definition hull :: "'a set set \ 'a set \ 'a set" (infixl "hull" 75) where + "S hull s = Inter {t. t \ S \ s \ t}" + +lemma hull_same: "s \ S \ S hull s = s" + unfolding hull_def by auto + +lemma hull_in: "(\T. T \ S ==> Inter T \ S) ==> (S hull s) \ S" +unfolding hull_def subset_iff by auto + +lemma hull_eq: "(\T. T \ S ==> Inter T \ S) ==> (S hull s) = s \ s \ S" +using hull_same[of s S] hull_in[of S s] by metis + + +lemma hull_hull: "S hull (S hull s) = S hull s" + unfolding hull_def by blast + +lemma hull_subset[intro]: "s \ (S hull s)" + unfolding hull_def by blast + +lemma hull_mono: " s \ t ==> (S hull s) \ (S hull t)" + unfolding hull_def by blast + +lemma hull_antimono: "S \ T ==> (T hull s) \ (S hull s)" + unfolding hull_def by blast + +lemma hull_minimal: "s \ t \ t \ S ==> (S hull s) \ t" + unfolding hull_def by blast + +lemma subset_hull: "t \ S ==> S hull s \ t \ s \ t" + unfolding hull_def by blast + +lemma hull_unique: "s \ t \ t \ S \ (\t'. s \ t' \ t' \ S ==> t \ t') + ==> (S hull s = t)" +unfolding hull_def by auto + +lemma hull_induct: "(\x. x\ S \ P x) \ Q {x. P x} \ \x\ Q hull S. P x" + using hull_minimal[of S "{x. P x}" Q] + by (auto simp add: subset_eq Collect_def mem_def) + +lemma hull_inc: "x \ S \ x \ P hull S" by (metis hull_subset subset_eq) + +lemma hull_union_subset: "(S hull s) \ (S hull t) \ (S hull (s \ t))" +unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2) + +lemma hull_union: assumes T: "\T. T \ S ==> Inter T \ S" + shows "S hull (s \ t) = S hull (S hull s \ 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 \ (S hull s) \ (S hull (insert a s) = S hull s)" + unfolding hull_def by blast + +lemma hull_redundant: "a \ (S hull s) ==> (S hull (insert a s) = S hull s)" +by (metis hull_redundant_eq) + +text{* Archimedian properties and useful consequences. *} + +lemma real_arch_simple: "\n. x <= real (n::nat)" + using reals_Archimedean2[of x] apply auto by (rule_tac x="Suc n" in exI, auto) +lemmas real_arch_lt = reals_Archimedean2 + +lemmas real_arch = reals_Archimedean3 + +lemma real_arch_inv: "0 < e \ (\n::nat. n \ 0 \ 0 < inverse (real n) \ inverse (real n) < e)" + using reals_Archimedean + apply (auto simp add: field_simps) + apply (subgoal_tac "inverse (real n) > 0") + apply arith + apply simp + done + +lemma real_pow_lbound: "0 <= x ==> 1 + real n * x <= (1 + x) ^ n" +proof(induct n) + case 0 thus ?case by simp +next + case (Suc n) + hence h: "1 + real n * x \ (1 + x) ^ n" by simp + from h have p: "1 \ (1 + x) ^ n" using Suc.prems by simp + from h have "1 + real n * x + x \ (1 + x) ^ n + x" by simp + also have "\ \ (1 + x) ^ Suc n" apply (subst diff_le_0_iff_le[symmetric]) + apply (simp add: field_simps) + using mult_left_mono[OF p Suc.prems] by simp + finally show ?case by (simp add: real_of_nat_Suc field_simps) +qed + +lemma real_arch_pow: assumes x: "1 < (x::real)" shows "\n. y < x^n" +proof- + from x have x0: "x - 1 > 0" by arith + from real_arch[OF x0, rule_format, of y] + obtain n::nat where n:"y < real n * (x - 1)" by metis + from x0 have x00: "x- 1 \ 0" by arith + from real_pow_lbound[OF x00, of n] n + have "y < x^n" by auto + then show ?thesis by metis +qed + +lemma real_arch_pow2: "\n. (x::real) < 2^ n" + using real_arch_pow[of 2 x] by simp + +lemma real_arch_pow_inv: assumes y: "(y::real) > 0" and x1: "x < 1" + shows "\n. x^n < y" +proof- + {assume x0: "x > 0" + from x0 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 + have ?thesis using y x0 by (auto simp add: field_simps power_divide) } + moreover + {assume "\ x > 0" with y x1 have ?thesis apply auto by (rule exI[where x=1], auto)} + ultimately show ?thesis by metis +qed + +lemma forall_pos_mono: "(\d e::real. d < e \ P d ==> P e) \ (\n::nat. n \ 0 ==> P(inverse(real n))) \ (\e. 0 < e ==> P e)" + by (metis real_arch_inv) + +lemma forall_pos_mono_1: "(\d e::real. d < e \ P d ==> P e) \ (\n. P(inverse(real (Suc n)))) ==> 0 < e ==> P e" + apply (rule forall_pos_mono) + apply auto + apply (atomize) + apply (erule_tac x="n - 1" in allE) + apply auto + done + +lemma real_archimedian_rdiv_eq_0: assumes x0: "x \ 0" and c: "c \ 0" and xc: "\(m::nat)>0. real m * x \ c" + shows "x = 0" +proof- + {assume "x \ 0" with x0 have xp: "x > 0" by arith + from real_arch[OF xp, rule_format, of c] obtain n::nat where n: "c < real n * x" by blast + with xc[rule_format, of n] have "n = 0" by arith + with n c have False by simp} + then show ?thesis by blast +qed + +subsection {* Geometric progression *} + +lemma sum_gp_basic: "((1::'a::{field}) - x) * setsum (\i. x^i) {0 .. n} = (1 - x^(Suc n))" + (is "?lhs = ?rhs") +proof- + {assume x1: "x = 1" hence ?thesis by simp} + moreover + {assume x1: "x\1" + hence x1': "x - 1 \ 0" "1 - x \ 0" "x - 1 = - (1 - x)" "- (1 - x) \ 0" by auto + from geometric_sum[OF x1, of "Suc n", unfolded x1'] + have "(- (1 - x)) * setsum (\i. x^i) {0 .. n} = - (1 - x^(Suc n))" + unfolding atLeastLessThanSuc_atLeastAtMost + using x1' apply (auto simp only: field_simps) + apply (simp add: field_simps) + done + then have ?thesis by (simp add: field_simps) } + ultimately show ?thesis by metis +qed + +lemma sum_gp_multiplied: assumes mn: "m <= n" + shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n" + (is "?lhs = ?rhs") +proof- + let ?S = "{0..(n - m)}" + from mn have mn': "n - m \ 0" by arith + let ?f = "op + m" + have i: "inj_on ?f ?S" unfolding inj_on_def by auto + have f: "?f ` ?S = {m..n}" + using mn apply (auto simp add: image_iff Bex_def) by arith + have th: "op ^ x o op + m = (\i. x^m * x^i)" + by (rule ext, simp add: power_add power_mult) + from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]] + have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp + then show ?thesis unfolding sum_gp_basic using mn + by (simp add: field_simps power_add[symmetric]) +qed + +lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} = + (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m) + else (x^ m - x^ (Suc n)) / (1 - x))" +proof- + {assume nm: "n < m" hence ?thesis by simp} + moreover + {assume "\ n < m" hence nm: "m \ n" by arith + {assume x: "x = 1" hence ?thesis by simp} + moreover + {assume x: "x \ 1" hence nz: "1 - x \ 0" by simp + from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)} + ultimately have ?thesis by metis + } + ultimately show ?thesis by metis +qed + +lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} = + (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))" + unfolding sum_gp[of x m "m + n"] power_Suc + by (simp add: field_simps power_add) + + +subsection{* A bit of linear algebra. *} + +definition (in real_vector) + subspace :: "'a set \ bool" where + "subspace S \ 0 \ S \ (\x\ S. \y \S. x + y \ S) \ (\c. \x \S. c *\<^sub>R x \S )" + +definition (in real_vector) "span S = (subspace hull S)" +definition (in real_vector) "dependent S \ (\a \ S. a \ span(S - {a}))" +abbreviation (in real_vector) "independent s == ~(dependent s)" + +text {* Closure properties of subspaces. *} + +lemma subspace_UNIV[simp]: "subspace(UNIV)" by (simp add: subspace_def) + +lemma (in real_vector) subspace_0: "subspace S ==> 0 \ S" by (metis subspace_def) + +lemma (in real_vector) subspace_add: "subspace S \ x \ S \ y \ S ==> x + y \ S" + by (metis subspace_def) + +lemma (in real_vector) subspace_mul: "subspace S \ x \ S \ c *\<^sub>R x \ S" + by (metis subspace_def) + +lemma subspace_neg: "subspace S \ x \ S \ - x \ S" + by (metis scaleR_minus1_left subspace_mul) + +lemma subspace_sub: "subspace S \ x \ S \ y \ S \ x - y \ S" + by (metis diff_minus subspace_add subspace_neg) + +lemma (in real_vector) subspace_setsum: + assumes sA: "subspace A" and fB: "finite B" + and f: "\x\ B. f x \ A" + shows "setsum f B \ A" + using fB f sA + apply(induct rule: finite_induct[OF fB]) + by (simp add: subspace_def sA, auto simp add: sA subspace_add) + +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_def subspace_def + apply (auto simp add: image_iff) + apply (rule_tac x="x + y" in bexI, auto) + apply (rule_tac x="c *\<^sub>R x" in bexI, auto) + done + +lemma subspace_linear_preimage: "linear f ==> subspace S ==> subspace {x. f x \ S}" + by (auto simp add: subspace_def linear_def linear_0[of f]) + +lemma subspace_trivial: "subspace {0}" + by (simp add: subspace_def) + +lemma (in real_vector) subspace_inter: "subspace A \ subspace B ==> subspace (A \ B)" + by (simp add: subspace_def) + +lemma (in real_vector) span_mono: "A \ B ==> span A \ span B" + by (metis span_def hull_mono) + +lemma (in real_vector) subspace_span: "subspace(span S)" + unfolding span_def + apply (rule hull_in[unfolded mem_def]) + apply (simp only: subspace_def Inter_iff Int_iff subset_eq) + apply auto + apply (erule_tac x="X" in ballE) + apply (simp add: mem_def) + apply blast + apply (erule_tac x="X" in ballE) + apply (erule_tac x="X" in ballE) + apply (erule_tac x="X" in ballE) + apply (clarsimp simp add: mem_def) + apply simp + apply simp + apply simp + apply (erule_tac x="X" in ballE) + apply (erule_tac x="X" in ballE) + apply (simp add: mem_def) + apply simp + apply simp + done + +lemma (in real_vector) span_clauses: + "a \ S ==> a \ span S" + "0 \ span S" + "x\ span S \ y \ span S ==> x + y \ span S" + "x \ span S \ c *\<^sub>R x \ span S" + by (metis span_def hull_subset subset_eq) + (metis subspace_span subspace_def)+ + +lemma (in real_vector) span_induct: assumes SP: "\x. x \ S ==> P x" + and P: "subspace P" and x: "x \ span S" shows "P x" +proof- + from SP have SP': "S \ P" by (simp add: mem_def subset_eq) + from P have P': "P \ subspace" by (simp add: mem_def) + from x hull_minimal[OF SP' P', unfolded span_def[symmetric]] + show "P x" by (metis mem_def subset_eq) +qed + +lemma span_empty[simp]: "span {} = {0}" + apply (simp add: span_def) + apply (rule hull_unique) + apply (auto simp add: mem_def subspace_def) + unfolding mem_def[of "0::'a", symmetric] + apply simp + done + +lemma (in real_vector) independent_empty[intro]: "independent {}" + by (simp add: dependent_def) + +lemma dependent_single[simp]: + "dependent {x} \ x = 0" + unfolding dependent_def by auto + +lemma (in real_vector) independent_mono: "independent A \ B \ A ==> independent B" + apply (clarsimp simp add: dependent_def span_mono) + apply (subgoal_tac "span (B - {a}) \ span (A - {a})") + apply force + apply (rule span_mono) + apply auto + done + +lemma (in real_vector) span_subspace: "A \ B \ B \ span A \ subspace B \ span A = B" + by (metis order_antisym span_def hull_minimal mem_def) + +lemma (in real_vector) span_induct': assumes SP: "\x \ S. P x" + and P: "subspace P" shows "\x \ span S. P x" + using span_induct SP P by blast + +inductive (in real_vector) span_induct_alt_help for S:: "'a \ bool" + where + span_induct_alt_help_0: "span_induct_alt_help S 0" + | span_induct_alt_help_S: "x \ S \ span_induct_alt_help S z \ span_induct_alt_help S (c *\<^sub>R x + z)" + +lemma span_induct_alt': + assumes h0: "h 0" and hS: "\c x y. x \ S \ h y \ h (c *\<^sub>R x + y)" shows "\x \ span S. h x" +proof- + {fix x:: "'a" assume x: "span_induct_alt_help S x" + have "h x" + apply (rule span_induct_alt_help.induct[OF x]) + apply (rule h0) + apply (rule hS, assumption, assumption) + done} + note th0 = this + {fix x assume x: "x \ span S" + + have "span_induct_alt_help S x" + proof(rule span_induct[where x=x and S=S]) + show "x \ span S" using x . + next + fix x assume xS : "x \ S" + from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1] + show "span_induct_alt_help S x" by simp + next + have "span_induct_alt_help S 0" by (rule span_induct_alt_help_0) + moreover + {fix x y assume h: "span_induct_alt_help S x" "span_induct_alt_help S y" + from h + have "span_induct_alt_help S (x + y)" + apply (induct rule: span_induct_alt_help.induct) + apply simp + unfolding add_assoc + apply (rule span_induct_alt_help_S) + apply assumption + apply simp + done} + moreover + {fix c x assume xt: "span_induct_alt_help S x" + then have "span_induct_alt_help S (c *\<^sub>R x)" + apply (induct rule: span_induct_alt_help.induct) + apply (simp add: span_induct_alt_help_0) + apply (simp add: scaleR_right_distrib) + apply (rule span_induct_alt_help_S) + apply assumption + apply simp + done + } + ultimately show "subspace (span_induct_alt_help S)" + unfolding subspace_def mem_def Ball_def by blast + qed} + with th0 show ?thesis by blast +qed + +lemma span_induct_alt: + assumes h0: "h 0" and hS: "\c x y. x \ S \ h y \ h (c *\<^sub>R x + y)" and x: "x \ span S" + shows "h x" +using span_induct_alt'[of h S] h0 hS x by blast + +text {* Individual closure properties. *} + +lemma span_span: "span (span A) = span A" + unfolding span_def hull_hull .. + +lemma (in real_vector) span_superset: "x \ S ==> x \ span S" by (metis span_clauses(1)) + +lemma (in real_vector) span_0: "0 \ span S" by (metis subspace_span subspace_0) + +lemma span_inc: "S \ span S" + by (metis subset_eq span_superset) + +lemma (in real_vector) dependent_0: assumes "0\A" shows "dependent A" + unfolding dependent_def apply(rule_tac x=0 in bexI) + using assms span_0 by auto + +lemma (in real_vector) span_add: "x \ span S \ y \ span S ==> x + y \ span S" + by (metis subspace_add subspace_span) + +lemma (in real_vector) span_mul: "x \ span S ==> (c *\<^sub>R x) \ span S" + by (metis subspace_span subspace_mul) + +lemma span_neg: "x \ span S ==> - x \ span S" + by (metis subspace_neg subspace_span) + +lemma span_sub: "x \ span S \ y \ span S ==> x - y \ span S" + by (metis subspace_span subspace_sub) + +lemma (in real_vector) span_setsum: "finite A \ \x \ A. f x \ span S ==> setsum f A \ span S" + by (rule subspace_setsum, rule subspace_span) + +lemma span_add_eq: "x \ span S \ x + y \ span S \ y \ span S" + apply (auto simp only: span_add span_sub) + apply (subgoal_tac "(x + y) - x \ span S", simp) + by (simp only: span_add span_sub) + +text {* Mapping under linear image. *} + +lemma span_linear_image: assumes lf: "linear f" + shows "span (f ` S) = f ` (span S)" +proof- + {fix x + assume x: "x \ span (f ` S)" + have "x \ f ` span S" + apply (rule span_induct[where x=x and S = "f ` S"]) + apply (clarsimp simp add: image_iff) + apply (frule span_superset) + apply blast + apply (simp only: mem_def) + apply (rule subspace_linear_image[OF lf]) + apply (rule subspace_span) + apply (rule x) + done} + moreover + {fix x assume x: "x \ span S" + have th0:"(\a. f a \ span (f ` S)) = {x. f x \ span (f ` S)}" apply (rule set_eqI) + unfolding mem_def Collect_def .. + have "f x \ span (f ` S)" + apply (rule span_induct[where S=S]) + apply (rule span_superset) + apply simp + apply (subst th0) + apply (rule subspace_linear_preimage[OF lf subspace_span, of "f ` S"]) + apply (rule x) + done} + ultimately show ?thesis by blast +qed + +text {* The key breakdown property. *} + +lemma span_breakdown: + assumes bS: "b \ S" and aS: "a \ span S" + shows "\k. a - k *\<^sub>R b \ span (S - {b})" (is "?P a") +proof- + {fix x assume xS: "x \ S" + {assume ab: "x = b" + then have "?P x" + apply simp + apply (rule exI[where x="1"], simp) + by (rule span_0)} + moreover + {assume ab: "x \ b" + then have "?P x" using xS + apply - + apply (rule exI[where x=0]) + apply (rule span_superset) + by simp} + ultimately have "?P x" by blast} + moreover have "subspace ?P" + unfolding subspace_def + apply auto + apply (simp add: mem_def) + apply (rule exI[where x=0]) + using span_0[of "S - {b}"] + apply (simp add: mem_def) + apply (clarsimp simp add: mem_def) + apply (rule_tac x="k + ka" in exI) + apply (subgoal_tac "x + y - (k + ka) *\<^sub>R b = (x - k*\<^sub>R b) + (y - ka *\<^sub>R b)") + apply (simp only: ) + apply (rule span_add[unfolded mem_def]) + apply assumption+ + apply (simp add: algebra_simps) + apply (clarsimp simp add: mem_def) + apply (rule_tac x= "c*k" in exI) + apply (subgoal_tac "c *\<^sub>R x - (c * k) *\<^sub>R b = c*\<^sub>R (x - k*\<^sub>R b)") + apply (simp only: ) + apply (rule span_mul[unfolded mem_def]) + apply assumption + by (simp add: algebra_simps) + ultimately show "?P a" using aS span_induct[where S=S and P= "?P"] by metis +qed + +lemma span_breakdown_eq: + "x \ span (insert a S) \ (\k. (x - k *\<^sub>R a) \ span S)" (is "?lhs \ ?rhs") +proof- + {assume x: "x \ span (insert a S)" + from x span_breakdown[of "a" "insert a S" "x"] + have ?rhs apply clarsimp + apply (rule_tac x= "k" in exI) + apply (rule set_rev_mp[of _ "span (S - {a})" _]) + apply assumption + apply (rule span_mono) + apply blast + done} + moreover + { fix k assume k: "x - k *\<^sub>R a \ span S" + have eq: "x = (x - k *\<^sub>R a) + k *\<^sub>R a" by simp + have "(x - k *\<^sub>R a) + k *\<^sub>R a \ span (insert a S)" + apply (rule span_add) + apply (rule set_rev_mp[of _ "span S" _]) + apply (rule k) + apply (rule span_mono) + apply blast + apply (rule span_mul) + apply (rule span_superset) + apply blast + done + then have ?lhs using eq by metis} + ultimately show ?thesis by blast +qed + +text {* Hence some "reversal" results. *} + +lemma in_span_insert: + assumes a: "a \ span (insert b S)" and na: "a \ span S" + shows "b \ span (insert a S)" +proof- + from span_breakdown[of b "insert b S" a, OF insertI1 a] + obtain k where k: "a - k*\<^sub>R b \ span (S - {b})" by auto + {assume k0: "k = 0" + with k have "a \ span S" + apply (simp) + apply (rule set_rev_mp) + apply assumption + apply (rule span_mono) + apply blast + done + with na have ?thesis by blast} + moreover + {assume k0: "k \ 0" + have eq: "b = (1/k) *\<^sub>R a - ((1/k) *\<^sub>R a - b)" by simp + from k0 have eq': "(1/k) *\<^sub>R (a - k*\<^sub>R b) = (1/k) *\<^sub>R a - b" + by (simp add: algebra_simps) + from k have "(1/k) *\<^sub>R (a - k*\<^sub>R b) \ span (S - {b})" + by (rule span_mul) + hence th: "(1/k) *\<^sub>R a - b \ span (S - {b})" + unfolding eq' . + + from k + have ?thesis + apply (subst eq) + apply (rule span_sub) + apply (rule span_mul) + apply (rule span_superset) + apply blast + apply (rule set_rev_mp) + apply (rule th) + apply (rule span_mono) + using na by blast} + ultimately show ?thesis by blast +qed + +lemma in_span_delete: + assumes a: "a \ span S" + and na: "a \ span (S-{b})" + shows "b \ span (insert a (S - {b}))" + apply (rule in_span_insert) + apply (rule set_rev_mp) + apply (rule a) + apply (rule span_mono) + apply blast + apply (rule na) + done + +text {* Transitivity property. *} + +lemma span_trans: + assumes x: "x \ span S" and y: "y \ span (insert x S)" + shows "y \ span S" +proof- + from span_breakdown[of x "insert x S" y, OF insertI1 y] + obtain k where k: "y -k*\<^sub>R x \ span (S - {x})" by auto + have eq: "y = (y - k *\<^sub>R x) + k *\<^sub>R x" by simp + show ?thesis + apply (subst eq) + apply (rule span_add) + apply (rule set_rev_mp) + apply (rule k) + apply (rule span_mono) + apply blast + apply (rule span_mul) + by (rule x) +qed + +lemma span_insert_0[simp]: "span (insert 0 S) = span S" + using span_mono[of S "insert 0 S"] by (auto intro: span_trans span_0) + +text {* An explicit expansion is sometimes needed. *} + +lemma span_explicit: + "span P = {y. \S u. finite S \ S \ P \ setsum (\v. u v *\<^sub>R v) S = y}" + (is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \S u. ?Q S u y}") +proof- + {fix x assume x: "x \ ?E" + then obtain S u where fS: "finite S" and SP: "S\P" and u: "setsum (\v. u v *\<^sub>R v) S = x" + by blast + have "x \ span P" + unfolding u[symmetric] + apply (rule span_setsum[OF fS]) + using span_mono[OF SP] + by (auto intro: span_superset span_mul)} + moreover + have "\x \ span P. x \ ?E" + unfolding mem_def Collect_def + proof(rule span_induct_alt') + show "?h 0" + apply (rule exI[where x="{}"]) by simp + next + fix c x y + assume x: "x \ P" and hy: "?h y" + from hy obtain S u where fS: "finite S" and SP: "S\P" + and u: "setsum (\v. u v *\<^sub>R v) S = y" by blast + let ?S = "insert x S" + let ?u = "\y. if y = x then (if x \ S then u y + c else c) + else u y" + from fS SP x have th0: "finite (insert x S)" "insert x S \ P" by blast+ + {assume xS: "x \ S" + have S1: "S = (S - {x}) \ {x}" + and Sss:"finite (S - {x})" "finite {x}" "(S -{x}) \ {x} = {}" using xS fS by auto + have "setsum (\v. ?u v *\<^sub>R v) ?S =(\v\S - {x}. u v *\<^sub>R v) + (u x + c) *\<^sub>R x" + using xS + by (simp add: setsum_Un_disjoint[OF Sss, unfolded S1[symmetric]] + setsum_clauses(2)[OF fS] cong del: if_weak_cong) + also have "\ = (\v\S. u v *\<^sub>R v) + c *\<^sub>R x" + apply (simp add: setsum_Un_disjoint[OF Sss, unfolded S1[symmetric]]) + by (simp add: algebra_simps) + also have "\ = c*\<^sub>R x + y" + by (simp add: add_commute u) + finally have "setsum (\v. ?u v *\<^sub>R v) ?S = c*\<^sub>R x + y" . + then have "?Q ?S ?u (c*\<^sub>R x + y)" using th0 by blast} + moreover + {assume xS: "x \ S" + have th00: "(\v\S. (if v = x then c else u v) *\<^sub>R v) = y" + unfolding u[symmetric] + apply (rule setsum_cong2) + using xS by auto + have "?Q ?S ?u (c*\<^sub>R x + y)" using fS xS th0 + by (simp add: th00 setsum_clauses add_commute cong del: if_weak_cong)} + ultimately have "?Q ?S ?u (c*\<^sub>R x + y)" + by (cases "x \ S", simp, simp) + then show "?h (c*\<^sub>R x + y)" + apply - + apply (rule exI[where x="?S"]) + apply (rule exI[where x="?u"]) by metis + qed + ultimately show ?thesis by blast +qed + +lemma dependent_explicit: + "dependent P \ (\S u. finite S \ S \ P \ (\v\S. u v \ 0 \ setsum (\v. u v *\<^sub>R v) S = 0))" (is "?lhs = ?rhs") +proof- + {assume dP: "dependent P" + then obtain a S u where aP: "a \ P" and fS: "finite S" + and SP: "S \ P - {a}" and ua: "setsum (\v. u v *\<^sub>R v) S = a" + unfolding dependent_def span_explicit by blast + let ?S = "insert a S" + let ?u = "\y. if y = a then - 1 else u y" + let ?v = a + from aP SP have aS: "a \ S" by blast + from fS SP aP have th0: "finite ?S" "?S \ P" "?v \ ?S" "?u ?v \ 0" by auto + have s0: "setsum (\v. ?u v *\<^sub>R v) ?S = 0" + using fS aS + apply (simp add: setsum_clauses field_simps) + apply (subst (2) ua[symmetric]) + apply (rule setsum_cong2) + by auto + with th0 have ?rhs + apply - + apply (rule exI[where x= "?S"]) + apply (rule exI[where x= "?u"]) + by clarsimp} + moreover + {fix S u v assume fS: "finite S" + and SP: "S \ P" and vS: "v \ S" and uv: "u v \ 0" + and u: "setsum (\v. u v *\<^sub>R v) S = 0" + let ?a = v + let ?S = "S - {v}" + let ?u = "\i. (- u i) / u v" + have th0: "?a \ P" "finite ?S" "?S \ P" using fS SP vS by auto + have "setsum (\v. ?u v *\<^sub>R v) ?S = setsum (\v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v" + using fS vS uv + by (simp add: setsum_diff1 divide_inverse field_simps) + also have "\ = ?a" + unfolding scaleR_right.setsum [symmetric] u + using uv by simp + finally have "setsum (\v. ?u v *\<^sub>R v) ?S = ?a" . + with th0 have ?lhs + unfolding dependent_def span_explicit + apply - + apply (rule bexI[where x= "?a"]) + apply (simp_all del: scaleR_minus_left) + apply (rule exI[where x= "?S"]) + by (auto simp del: scaleR_minus_left)} + ultimately show ?thesis by blast +qed + + +lemma span_finite: + assumes fS: "finite S" + shows "span S = {y. \u. setsum (\v. u v *\<^sub>R v) S = y}" + (is "_ = ?rhs") +proof- + {fix y assume y: "y \ span S" + from y obtain S' u where fS': "finite S'" and SS': "S' \ S" and + u: "setsum (\v. u v *\<^sub>R v) S' = y" unfolding span_explicit by blast + let ?u = "\x. if x \ S' then u x else 0" + have "setsum (\v. ?u v *\<^sub>R v) S = setsum (\v. u v *\<^sub>R v) S'" + using SS' fS by (auto intro!: setsum_mono_zero_cong_right) + hence "setsum (\v. ?u v *\<^sub>R v) S = y" by (metis u) + hence "y \ ?rhs" by auto} + moreover + {fix y u assume u: "setsum (\v. u v *\<^sub>R v) S = y" + then have "y \ span S" using fS unfolding span_explicit by auto} + ultimately show ?thesis by blast +qed + +lemma Int_Un_cancel: "(A \ B) \ A = A" "(A \ B) \ B = B" by auto + +lemma span_union: "span (A \ B) = (\(a, b). a + b) ` (span A \ span B)" +proof safe + fix x assume "x \ span (A \ B)" + then obtain S u where S: "finite S" "S \ A \ B" and x: "x = (\v\S. u v *\<^sub>R v)" + unfolding span_explicit by auto + + let ?Sa = "\v\S\A. u v *\<^sub>R v" + let ?Sb = "(\v\S\(B - A). u v *\<^sub>R v)" + show "x \ (\(a, b). a + b) ` (span A \ span B)" + proof + show "x = (case (?Sa, ?Sb) of (a, b) \ a + b)" + unfolding x using S + by (simp, subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong) + + from S have "?Sa \ span A" unfolding span_explicit + by (auto intro!: exI[of _ "S \ A"]) + moreover from S have "?Sb \ span B" unfolding span_explicit + by (auto intro!: exI[of _ "S \ (B - A)"]) + ultimately show "(?Sa, ?Sb) \ span A \ span B" by simp + qed +next + fix a b assume "a \ span A" and "b \ span B" + then obtain Sa ua Sb ub where span: + "finite Sa" "Sa \ A" "a = (\v\Sa. ua v *\<^sub>R v)" + "finite Sb" "Sb \ B" "b = (\v\Sb. ub v *\<^sub>R v)" + unfolding span_explicit by auto + let "?u v" = "(if v \ Sa then ua v else 0) + (if v \ Sb then ub v else 0)" + from span have "finite (Sa \ Sb)" "Sa \ Sb \ A \ B" + and "a + b = (\v\(Sa\Sb). ?u v *\<^sub>R v)" + unfolding setsum_addf scaleR_left_distrib + by (auto simp add: if_distrib cond_application_beta setsum_cases Int_Un_cancel) + thus "a + b \ span (A \ B)" + unfolding span_explicit by (auto intro!: exI[of _ ?u]) +qed + +text {* This is useful for building a basis step-by-step. *} + +lemma independent_insert: + "independent(insert a S) \ + (if a \ S then independent S + else independent S \ a \ span S)" (is "?lhs \ ?rhs") +proof- + {assume aS: "a \ S" + hence ?thesis using insert_absorb[OF aS] by simp} + moreover + {assume aS: "a \ S" + {assume i: ?lhs + then have ?rhs using aS + apply simp + apply (rule conjI) + apply (rule independent_mono) + apply assumption + apply blast + by (simp add: dependent_def)} + moreover + {assume i: ?rhs + have ?lhs using i aS + apply simp + apply (auto simp add: dependent_def) + apply (case_tac "aa = a", auto) + apply (subgoal_tac "insert a S - {aa} = insert a (S - {aa})") + apply simp + apply (subgoal_tac "a \ span (insert aa (S - {aa}))") + apply (subgoal_tac "insert aa (S - {aa}) = S") + apply simp + apply blast + apply (rule in_span_insert) + apply assumption + apply blast + apply blast + done} + ultimately have ?thesis by blast} + ultimately show ?thesis by blast +qed + +text {* The degenerate case of the Exchange Lemma. *} + +lemma mem_delete: "x \ (A - {a}) \ x \ a \ x \ A" + by blast + +lemma spanning_subset_independent: + assumes BA: "B \ A" and iA: "independent A" + and AsB: "A \ span B" + shows "A = B" +proof + from BA show "B \ A" . +next + from span_mono[OF BA] span_mono[OF AsB] + have sAB: "span A = span B" unfolding span_span by blast + + {fix x assume x: "x \ A" + from iA have th0: "x \ span (A - {x})" + unfolding dependent_def using x by blast + from x have xsA: "x \ span A" by (blast intro: span_superset) + have "A - {x} \ A" by blast + hence th1:"span (A - {x}) \ span A" by (metis span_mono) + {assume xB: "x \ B" + from xB BA have "B \ A -{x}" by blast + hence "span B \ span (A - {x})" by (metis span_mono) + with th1 th0 sAB have "x \ span A" by blast + with x have False by (metis span_superset)} + then have "x \ B" by blast} + then show "A \ B" by blast +qed + +text {* The general case of the Exchange Lemma, the key to what follows. *} + +lemma exchange_lemma: + assumes f:"finite t" and i: "independent s" + and sp:"s \ span t" + shows "\t'. (card t' = card t) \ finite t' \ s \ t' \ t' \ s \ t \ s \ span t'" +using f i sp +proof(induct "card (t - s)" arbitrary: s t rule: less_induct) + case less + note ft = `finite t` and s = `independent s` and sp = `s \ span t` + let ?P = "\t'. (card t' = card t) \ finite t' \ s \ t' \ t' \ s \ t \ s \ span t'" + let ?ths = "\t'. ?P t'" + {assume st: "s \ t" + from st ft span_mono[OF st] have ?ths apply - apply (rule exI[where x=t]) + by (auto intro: span_superset)} + moreover + {assume st: "t \ s" + + from spanning_subset_independent[OF st s sp] + st ft span_mono[OF st] have ?ths apply - apply (rule exI[where x=t]) + by (auto intro: span_superset)} + moreover + {assume st: "\ s \ t" "\ t \ s" + from st(2) obtain b where b: "b \ t" "b \ s" by blast + from b have "t - {b} - s \ t - s" by blast + then have cardlt: "card (t - {b} - s) < card (t - s)" using ft + by (auto intro: psubset_card_mono) + from b ft have ct0: "card t \ 0" by auto + {assume stb: "s \ span(t -{b})" + from ft have ftb: "finite (t -{b})" by auto + from less(1)[OF cardlt ftb s stb] + obtain u where u: "card u = card (t-{b})" "s \ u" "u \ s \ (t - {b})" "s \ span u" and fu: "finite u" by blast + let ?w = "insert b u" + have th0: "s \ insert b u" using u by blast + from u(3) b have "u \ s \ t" by blast + then have th1: "insert b u \ s \ t" using u b by blast + have bu: "b \ u" using b u by blast + from u(1) ft b have "card u = (card t - 1)" by auto + then + have th2: "card (insert b u) = card t" + using card_insert_disjoint[OF fu bu] ct0 by auto + from u(4) have "s \ span u" . + also have "\ \ span (insert b u)" apply (rule span_mono) by blast + finally have th3: "s \ span (insert b u)" . + from th0 th1 th2 th3 fu have th: "?P ?w" by blast + from th have ?ths by blast} + moreover + {assume stb: "\ s \ span(t -{b})" + from stb obtain a where a: "a \ s" "a \ span (t - {b})" by blast + have ab: "a \ b" using a b by blast + have at: "a \ t" using a ab span_superset[of a "t- {b}"] by auto + have mlt: "card ((insert a (t - {b})) - s) < card (t - s)" + using cardlt ft a b by auto + have ft': "finite (insert a (t - {b}))" using ft by auto + {fix x assume xs: "x \ s" + have t: "t \ (insert b (insert a (t -{b})))" using b by auto + from b(1) have "b \ span t" by (simp add: span_superset) + have bs: "b \ span (insert a (t - {b}))" apply(rule in_span_delete) + using a sp unfolding subset_eq by auto + from xs sp have "x \ span t" by blast + with span_mono[OF t] + have x: "x \ span (insert b (insert a (t - {b})))" .. + from span_trans[OF bs x] have "x \ span (insert a (t - {b}))" .} + then have sp': "s \ span (insert a (t - {b}))" by blast + + from less(1)[OF mlt ft' s sp'] obtain u where + u: "card u = card (insert a (t -{b}))" "finite u" "s \ u" "u \ s \ insert a (t -{b})" + "s \ span u" by blast + from u a b ft at ct0 have "?P u" by auto + then have ?ths by blast } + ultimately have ?ths by blast + } + ultimately + show ?ths by blast +qed + +text {* This implies corresponding size bounds. *} + +lemma independent_span_bound: + assumes f: "finite t" and i: "independent s" and sp:"s \ span t" + shows "finite s \ card s \ card t" + by (metis exchange_lemma[OF f i sp] finite_subset card_mono) + + +lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\ (UNIV::'a::finite set)}" +proof- + have eq: "{f x |x. x\ UNIV} = f ` UNIV" by auto + show ?thesis unfolding eq + apply (rule finite_imageI) + apply (rule finite) + done +qed + +subsection{* Euclidean Spaces as Typeclass*} + +lemma (in euclidean_space) basis_inj[simp, intro]: "inj_on basis {.. 'c::real_vector" assumes *: "inj_on f {.. (\a u. a < D \ (\i\{..R f i) \ f a)" +proof - + from * have eq: "\i. i < D \ f ` {..i. inj_on f ({..i. finite (f ` {..d. \ 0 < d; basis ` {d..} = {0::'a::euclidean_space}; + independent (basis ` {.. 'a) {.. \ P d" + shows "P DIM('a::euclidean_space)" + using DIM_positive basis_finite independent_basis basis_inj + by (rule assms) + +lemma (in euclidean_space) dimension_eq: + assumes "\i. i < d \ basis i \ 0" + assumes "\i. d \ i \ basis i = 0" + shows "DIM('a) = d" +proof (rule linorder_cases [of "DIM('a)" d]) + assume "DIM('a) < d" + hence "basis DIM('a) \ 0" by (rule assms) + thus ?thesis by simp +next + assume "d < DIM('a)" + hence "basis d \ 0" by simp + thus ?thesis by (simp add: assms) +next + assume "DIM('a) = d" thus ?thesis . +qed + +lemma (in euclidean_space) range_basis: + "range basis = insert 0 (basis ` {.. {DIM('a)..}" by auto + show ?thesis unfolding * image_Un basis_finite by auto +qed + +lemma (in euclidean_space) range_basis_finite[intro]: + "finite (range basis)" + unfolding range_basis by auto + +lemma span_basis: "span (range basis) = (UNIV :: 'a::euclidean_space set)" +proof - + { fix x :: 'a + have "(\iR basis i) \ span (range basis :: 'a set)" + by (simp add: span_setsum span_mul span_superset) + hence "x \ span (range basis)" + by (simp only: euclidean_representation [symmetric]) + } thus ?thesis by auto +qed + +lemma basis_representation: + "\u. x = (\v\basis ` {..R (v\'a\euclidean_space))" +proof - + have "x\UNIV" by auto from this[unfolded span_basis[THEN sym]] + have "\u. (\v\basis ` {..R v) = x" + unfolding range_basis span_insert_0 apply(subst (asm) span_finite) by auto + thus ?thesis by fastsimp +qed + +lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..'a) ` {.. span (basis ` {..x$$i\ \ norm (x::'a::euclidean_space)" + unfolding euclidean_component_def + apply(rule order_trans[OF real_inner_class.Cauchy_Schwarz_ineq2]) by auto + +lemma norm_bound_component_le: "norm (x::'a::euclidean_space) \ e \ \x$$i\ <= e" + by (metis component_le_norm order_trans) + +lemma norm_bound_component_lt: "norm (x::'a::euclidean_space) < e \ \x$$i\ < e" + by (metis component_le_norm basic_trans_rules(21)) + +lemma norm_le_l1: "norm (x::'a::euclidean_space) \ (\ix $$ i\)" + apply (subst euclidean_representation[of x]) + apply (rule order_trans[OF setsum_norm]) + by (auto intro!: setsum_mono) + +lemma setsum_norm_allsubsets_bound: + fixes f:: "'a \ 'n::euclidean_space" + assumes fP: "finite P" and fPs: "\Q. Q \ P \ norm (setsum f Q) \ e" + shows "setsum (\x. norm (f x)) P \ 2 * real DIM('n) * e" +proof- + let ?d = "real DIM('n)" + let ?nf = "\x. norm (f x)" + let ?U = "{..x. setsum (\i. \f x $$ i\) ?U) P = setsum (\i. setsum (\x. \f x $$ i\) P) ?U" + by (rule setsum_commute) + have th1: "2 * ?d * e = of_nat (card ?U) * (2 * e)" by (simp add: real_of_nat_def) + have "setsum ?nf P \ setsum (\x. setsum (\i. \f x $$ i\) ?U) P" + apply (rule setsum_mono) by (rule norm_le_l1) + also have "\ \ 2 * ?d * e" + unfolding th0 th1 + proof(rule setsum_bounded) + fix i assume i: "i \ ?U" + let ?Pp = "{x. x\ P \ f x $$ i \ 0}" + let ?Pn = "{x. x \ P \ f x $$ i < 0}" + have thp: "P = ?Pp \ ?Pn" by auto + have thp0: "?Pp \ ?Pn ={}" by auto + have PpP: "?Pp \ P" and PnP: "?Pn \ P" by blast+ + have Ppe:"setsum (\x. \f x $$ i\) ?Pp \ e" + using component_le_norm[of "setsum (\x. f x) ?Pp" i] fPs[OF PpP] + unfolding euclidean_component.setsum by(auto intro: abs_le_D1) + have Pne: "setsum (\x. \f x $$ i\) ?Pn \ e" + using component_le_norm[of "setsum (\x. - f x) ?Pn" i] fPs[OF PnP] + unfolding euclidean_component.setsum euclidean_component.minus + by(auto simp add: setsum_negf intro: abs_le_D1) + have "setsum (\x. \f x $$ i\) P = setsum (\x. \f x $$ i\) ?Pp + setsum (\x. \f x $$ i\) ?Pn" + apply (subst thp) + apply (rule setsum_Un_zero) + using fP thp0 by auto + also have "\ \ 2*e" using Pne Ppe by arith + finally show "setsum (\x. \f x $$ i\) P \ 2*e" . + qed + finally show ?thesis . +qed + +lemma choice_iff': "(\xy. P x y) \ (\f. \xix. P i x) \ + (\x::'a. \i ?rhs") +proof- + let ?S = "{..ii y \ (\i < DIM('a). x $$ i \ y $$ i)" + and eucl_less: "x < y \ (\i < DIM('a). x $$ i < y $$ i)" + +lemma eucl_less_not_refl[simp, intro!]: "\ x < (x::'a::ordered_euclidean_space)" + unfolding eucl_less[where 'a='a] by auto + +lemma euclidean_trans[trans]: + fixes x y z :: "'a::ordered_euclidean_space" + shows "x < y \ y < z \ x < z" + and "x \ y \ y < z \ x < z" + and "x \ y \ y \ z \ x \ z" + by (force simp: eucl_less[where 'a='a] eucl_le[where 'a='a])+ + +subsection {* Linearity and Bilinearity continued *} + +lemma linear_bounded: + fixes f:: "'a::euclidean_space \ 'b::real_normed_vector" + assumes lf: "linear f" + shows "\B. \x. norm (f x) \ B * norm x" +proof- + let ?S = "{..i. (x$$i) *\<^sub>R (basis i)) ?S))" + apply(subst euclidean_representation[of x]) .. + also have "\ = norm (setsum (\ i. (x$$i) *\<^sub>R f (basis i)) ?S)" + using linear_setsum[OF lf fS, of ?g, unfolded o_def] linear_cmul[OF lf] by auto + finally have th0: "norm (f x) = norm (setsum (\i. (x$$i) *\<^sub>R f (basis i))?S)" . + {fix i assume i: "i \ ?S" + from component_le_norm[of x i] + have "norm ((x$$i) *\<^sub>R f (basis i :: 'a)) \ norm (f (basis i)) * norm x" + unfolding norm_scaleR + apply (simp only: mult_commute) + apply (rule mult_mono) + by (auto simp add: field_simps) } + then have th: "\i\ ?S. norm ((x$$i) *\<^sub>R f (basis i :: 'a)) \ norm (f (basis i)) * norm x" by metis + from setsum_norm_le[OF fS, of "\i. (x$$i) *\<^sub>R (f (basis i))", OF th] + have "norm (f x) \ ?B * norm x" unfolding th0 setsum_left_distrib by metis} + then show ?thesis by blast +qed + +lemma linear_bounded_pos: + fixes f:: "'a::euclidean_space \ 'b::real_normed_vector" + assumes lf: "linear f" + shows "\B > 0. \x. norm (f x) \ B * norm x" +proof- + from linear_bounded[OF lf] obtain B where + B: "\x. norm (f x) \ B * norm x" by blast + let ?K = "\B\ + 1" + have Kp: "?K > 0" by arith + { assume C: "B < 0" + have "((\\ i. 1)::'a) \ 0" unfolding euclidean_eq[where 'a='a] + by(auto intro!:exI[where x=0] simp add:euclidean_component.zero) + hence "norm ((\\ i. 1)::'a) > 0" by auto + with C have "B * norm ((\\ i. 1)::'a) < 0" + by (simp add: mult_less_0_iff) + with B[rule_format, of "(\\ i. 1)::'a"] norm_ge_zero[of "f ((\\ i. 1)::'a)"] have False by simp + } + then have Bp: "B \ 0" by (metis not_leE) + {fix x::"'a" + have "norm (f x) \ ?K * norm x" + using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp + apply (auto simp add: field_simps split add: abs_split) + apply (erule order_trans, simp) + done + } + then show ?thesis using Kp by blast +qed + +lemma linear_conv_bounded_linear: + fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" + shows "linear f \ bounded_linear f" +proof + assume "linear f" + show "bounded_linear f" + proof + fix x y show "f (x + y) = f x + f y" + using `linear f` unfolding linear_def by simp + next + fix r x show "f (scaleR r x) = scaleR r (f x)" + using `linear f` unfolding linear_def by simp + next + have "\B. \x. norm (f x) \ B * norm x" + using `linear f` by (rule linear_bounded) + thus "\K. \x. norm (f x) \ norm x * K" + by (simp add: mult_commute) + qed +next + assume "bounded_linear f" + then interpret f: bounded_linear f . + show "linear f" + by (simp add: f.add f.scaleR linear_def) +qed + +lemma bounded_linearI': fixes f::"'a::euclidean_space \ 'b::real_normed_vector" + assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" + shows "bounded_linear f" unfolding linear_conv_bounded_linear[THEN sym] + by(rule linearI[OF assms]) + + +lemma bilinear_bounded: + fixes h:: "'m::euclidean_space \ 'n::euclidean_space \ 'k::real_normed_vector" + assumes bh: "bilinear h" + shows "\B. \x y. norm (h x y) \ B * norm x * norm y" +proof- + let ?M = "{..i. (x$$i) *\<^sub>R basis i) ?M) (setsum (\i. (y$$i) *\<^sub>R basis i) ?N))" + apply(subst euclidean_representation[where 'a='m]) + apply(subst euclidean_representation[where 'a='n]) .. + also have "\ = norm (setsum (\ (i,j). h ((x$$i) *\<^sub>R basis i) ((y$$j) *\<^sub>R basis j)) (?M \ ?N))" + unfolding bilinear_setsum[OF bh fM fN] .. + finally have th: "norm (h x y) = \" . + have "norm (h x y) \ ?B * norm x * norm y" + apply (simp add: setsum_left_distrib th) + apply (rule setsum_norm_le) + using fN fM + apply simp + apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] field_simps simp del: scaleR_scaleR) + apply (rule mult_mono) + apply (auto simp add: zero_le_mult_iff component_le_norm) + apply (rule mult_mono) + apply (auto simp add: zero_le_mult_iff component_le_norm) + done} + then show ?thesis by metis +qed + +lemma bilinear_bounded_pos: + fixes h:: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector" + assumes bh: "bilinear h" + shows "\B > 0. \x y. norm (h x y) \ B * norm x * norm y" +proof- + from bilinear_bounded[OF bh] obtain B where + B: "\x y. norm (h x y) \ B * norm x * norm y" by blast + let ?K = "\B\ + 1" + have Kp: "?K > 0" by arith + have KB: "B < ?K" by arith + {fix x::'a and y::'b + from KB Kp + have "B * norm x * norm y \ ?K * norm x * norm y" + apply - + apply (rule mult_right_mono, rule mult_right_mono) + by auto + then have "norm (h x y) \ ?K * norm x * norm y" + using B[rule_format, of x y] by simp} + with Kp show ?thesis by blast +qed + +lemma bilinear_conv_bounded_bilinear: + fixes h :: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector" + shows "bilinear h \ bounded_bilinear h" +proof + assume "bilinear h" + show "bounded_bilinear h" + proof + fix x y z show "h (x + y) z = h x z + h y z" + using `bilinear h` unfolding bilinear_def linear_def by simp + next + fix x y z show "h x (y + z) = h x y + h x z" + using `bilinear h` unfolding bilinear_def linear_def by simp + next + fix r x y show "h (scaleR r x) y = scaleR r (h x y)" + using `bilinear h` unfolding bilinear_def linear_def + by simp + next + fix r x y show "h x (scaleR r y) = scaleR r (h x y)" + using `bilinear h` unfolding bilinear_def linear_def + by simp + next + have "\B. \x y. norm (h x y) \ B * norm x * norm y" + using `bilinear h` by (rule bilinear_bounded) + thus "\K. \x y. norm (h x y) \ norm x * norm y * K" + by (simp add: mult_ac) + qed +next + assume "bounded_bilinear h" + then interpret h: bounded_bilinear h . + show "bilinear h" + unfolding bilinear_def linear_conv_bounded_linear + using h.bounded_linear_left h.bounded_linear_right + by simp +qed + +subsection {* We continue. *} + +lemma independent_bound: + fixes S:: "('a::euclidean_space) set" + shows "independent S \ finite S \ card S <= DIM('a::euclidean_space)" + using independent_span_bound[of "(basis::nat=>'a) ` {.. card S > DIM('a)) ==> dependent S" + by (metis independent_bound not_less) + +text {* Hence we can create a maximal independent subset. *} + +lemma maximal_independent_subset_extend: + assumes sv: "(S::('a::euclidean_space) set) \ V" and iS: "independent S" + shows "\B. S \ B \ B \ V \ independent B \ V \ span B" + using sv iS +proof(induct "DIM('a) - card S" arbitrary: S rule: less_induct) + case less + note sv = `S \ V` and i = `independent S` + let ?P = "\B. S \ B \ B \ V \ independent B \ V \ span B" + let ?ths = "\x. ?P x" + let ?d = "DIM('a)" + {assume "V \ span S" + then have ?ths using sv i by blast } + moreover + {assume VS: "\ V \ span S" + from VS obtain a where a: "a \ V" "a \ span S" by blast + from a have aS: "a \ S" by (auto simp add: span_superset) + have th0: "insert a S \ 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 \ B" "B \ V" "independent B" " V \ span B" + by blast + from B have "?P B" by auto + then have ?ths by blast} + ultimately show ?ths by blast +qed + +lemma maximal_independent_subset: + "\(B:: ('a::euclidean_space) set). B\ V \ independent B \ V \ span B" + by (metis maximal_independent_subset_extend[of "{}:: ('a::euclidean_space) set"] empty_subsetI independent_empty) + + +text {* Notion of dimension. *} + +definition "dim V = (SOME n. \B. B \ V \ independent B \ V \ span B \ (card B = n))" + +lemma basis_exists: "\B. (B :: ('a::euclidean_space) set) \ V \ independent B \ V \ span B \ (card B = dim V)" +unfolding dim_def some_eq_ex[of "\n. \B. B \ V \ independent B \ V \ span B \ (card B = n)"] +using maximal_independent_subset[of V] independent_bound +by auto + +text {* Consequences of independence or spanning for cardinality. *} + +lemma independent_card_le_dim: + assumes "(B::('a::euclidean_space) set) \ V" and "independent B" shows "card B \ dim V" +proof - + from basis_exists[of V] `B \ V` + obtain B' where "independent B'" and "B \ span B'" and "card B' = dim V" by blast + with independent_span_bound[OF _ `independent B` `B \ span B'`] independent_bound[of B'] + show ?thesis by auto +qed + +lemma span_card_ge_dim: "(B::('a::euclidean_space) set) \ V \ V \ span B \ finite B \ dim V \ card B" + by (metis basis_exists[of V] independent_span_bound subset_trans) + +lemma basis_card_eq_dim: + "B \ (V:: ('a::euclidean_space) set) \ V \ span B \ independent B \ finite B \ card B = dim V" + by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_bound) + +lemma dim_unique: "(B::('a::euclidean_space) set) \ V \ V \ span B \ independent B \ card B = n \ dim V = n" + by (metis basis_card_eq_dim) + +text {* More lemmas about dimension. *} + +lemma dim_UNIV: "dim (UNIV :: ('a::euclidean_space) set) = DIM('a)" + apply (rule dim_unique[of "(basis::nat=>'a) ` {.. T \ dim S \ dim T" + using basis_exists[of T] basis_exists[of S] + by (metis independent_card_le_dim subset_trans) + +lemma dim_subset_UNIV: "dim (S:: ('a::euclidean_space) set) \ DIM('a)" + by (metis dim_subset subset_UNIV dim_UNIV) + +text {* Converses to those. *} + +lemma card_ge_dim_independent: + assumes BV:"(B::('a::euclidean_space) set) \ V" and iB:"independent B" and dVB:"dim V \ card B" + shows "V \ span B" +proof- + {fix a assume aV: "a \ V" + {assume aB: "a \ span B" + then have iaB: "independent (insert a B)" using iB aV BV by (simp add: independent_insert) + from aV BV have th0: "insert a B \ V" by blast + from aB have "a \B" by (auto simp add: span_superset) + with independent_card_le_dim[OF th0 iaB] dVB independent_bound[OF iB] have False by auto } + then have "a \ span B" by blast} + then show ?thesis by blast +qed + +lemma card_le_dim_spanning: + assumes BV: "(B:: ('a::euclidean_space) set) \ V" and VB: "V \ span B" + and fB: "finite B" and dVB: "dim V \ card B" + shows "independent B" +proof- + {fix a assume a: "a \ B" "a \ span (B -{a})" + from a fB have c0: "card B \ 0" by auto + from a fB have cb: "card (B -{a}) = card B - 1" by auto + from BV a have th0: "B -{a} \ V" by blast + {fix x assume x: "x \ V" + from a have eq: "insert a (B -{a}) = B" by blast + from x VB have x': "x \ span B" by blast + from span_trans[OF a(2), unfolded eq, OF x'] + have "x \ span (B -{a})" . } + then have th1: "V \ span (B -{a})" by blast + have th2: "finite (B -{a})" using fB by auto + from span_card_ge_dim[OF th0 th1 th2] + have c: "dim V \ card (B -{a})" . + from c c0 dVB cb have False by simp} + then show ?thesis unfolding dependent_def by blast +qed + +lemma card_eq_dim: "(B:: ('a::euclidean_space) set) \ V \ card B = dim V \ finite B \ independent B \ V \ span B" + by (metis order_eq_iff card_le_dim_spanning + card_ge_dim_independent) + +text {* More general size bound lemmas. *} + +lemma independent_bound_general: + "independent (S:: ('a::euclidean_space) set) \ finite S \ card S \ dim S" + by (metis independent_card_le_dim independent_bound subset_refl) + +lemma dependent_biggerset_general: "(finite (S:: ('a::euclidean_space) set) \ card S > dim S) \ dependent S" + using independent_bound_general[of S] by (metis linorder_not_le) + +lemma dim_span: "dim (span (S:: ('a::euclidean_space) set)) = dim S" +proof- + have th0: "dim S \ dim (span S)" + by (auto simp add: subset_eq intro: dim_subset span_superset) + from basis_exists[of S] + obtain B where B: "B \ S" "independent B" "S \ span B" "card B = dim S" by blast + from B have fB: "finite B" "card B = dim S" using independent_bound by blast+ + have bSS: "B \ span S" using B(1) by (metis subset_eq span_inc) + have sssB: "span S \ span B" using span_mono[OF B(3)] by (simp add: span_span) + from span_card_ge_dim[OF bSS sssB fB(1)] th0 show ?thesis + using fB(2) by arith +qed + +lemma subset_le_dim: "(S:: ('a::euclidean_space) set) \ span T \ dim S \ dim T" + by (metis dim_span dim_subset) + +lemma span_eq_dim: "span (S:: ('a::euclidean_space) set) = span T ==> dim S = dim T" + by (metis dim_span) + +lemma spans_image: + assumes lf: "linear f" and VB: "V \ span B" + shows "f ` V \ span (f ` B)" + unfolding span_linear_image[OF lf] + by (metis VB image_mono) + +lemma dim_image_le: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes lf: "linear f" shows "dim (f ` S) \ dim (S)" +proof- + from basis_exists[of S] obtain B where + B: "B \ S" "independent B" "S \ span B" "card B = dim S" by blast + from B have fB: "finite B" "card B = dim S" using independent_bound by blast+ + have "dim (f ` S) \ card (f ` B)" + apply (rule span_card_ge_dim) + using lf B fB by (auto simp add: span_linear_image spans_image subset_image_iff) + also have "\ \ dim S" using card_image_le[OF fB(1)] fB by simp + finally show ?thesis . +qed + +text {* Relation between bases and injectivity/surjectivity of map. *} + +lemma spanning_surjective_image: + assumes us: "UNIV \ span S" + and lf: "linear f" and sf: "surj f" + shows "UNIV \ span (f ` S)" +proof- + have "UNIV \ f ` UNIV" using sf by (auto simp add: surj_def) + also have " \ \ 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 \ S" "f a \ 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 \ f ` span (S -{a})" + unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast + hence "a \ 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 {* Picking an orthogonal replacement for a spanning set. *} + + (* FIXME : Move to some general theory ?*) +definition "pairwise R S \ (\x \ S. \y\ S. x\y \ R x y)" + +lemma vector_sub_project_orthogonal: "(b::'a::euclidean_space) \ (x - ((b \ x) / (b \ b)) *\<^sub>R b) = 0" + unfolding inner_simps by auto + +lemma basis_orthogonal: + fixes B :: "('a::euclidean_space) set" + assumes fB: "finite B" + shows "\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C" + (is " \C. ?P B C") +proof(induct rule: finite_induct[OF fB]) + case 1 thus ?case apply (rule exI[where x="{}"]) by (auto simp add: pairwise_def) +next + case (2 a B) + note fB = `finite B` and aB = `a \ B` + from `\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C` + obtain C where C: "finite C" "card C \ card B" + "span C = span B" "pairwise orthogonal C" by blast + let ?a = "a - setsum (\x. (x \ a / (x \ x)) *\<^sub>R x) C" + let ?C = "insert ?a C" + from C(1) have fC: "finite ?C" by simp + from fB aB C(1,2) have cC: "card ?C \ card (insert a B)" by (simp add: card_insert_if) + {fix x k + have th0: "\(a::'a) b c. a - (b - c) = c + (a - b)" by (simp add: field_simps) + have "x - k *\<^sub>R (a - (\x\C. (x \ a / (x \ x)) *\<^sub>R x)) \ span C \ x - k *\<^sub>R a \ span C" + apply (simp only: scaleR_right_diff_distrib th0) + apply (rule span_add_eq) + apply (rule span_mul) + apply (rule span_setsum[OF C(1)]) + apply clarify + apply (rule span_mul) + by (rule span_superset)} + then have SC: "span ?C = span (insert a B)" + unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto + thm pairwise_def + {fix x y assume xC: "x \ ?C" and yC: "y \ ?C" and xy: "x \ y" + {assume xa: "x = ?a" and ya: "y = ?a" + have "orthogonal x y" using xa ya xy by blast} + moreover + {assume xa: "x = ?a" and ya: "y \ ?a" "y \ C" + from ya have Cy: "C = insert y (C - {y})" by blast + have fth: "finite (C - {y})" using C by simp + have "orthogonal x y" + using xa ya + unfolding orthogonal_def xa inner_simps diff_eq_0_iff_eq + apply simp + apply (subst Cy) + using C(1) fth + apply (simp only: setsum_clauses) + apply (auto simp add: inner_simps inner_commute[of y a] dot_lsum[OF fth]) + apply (rule setsum_0') + apply clarsimp + apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format]) + by auto} + moreover + {assume xa: "x \ ?a" "x \ C" and ya: "y = ?a" + from xa have Cx: "C = insert x (C - {x})" by blast + have fth: "finite (C - {x})" using C by simp + have "orthogonal x y" + using xa ya + unfolding orthogonal_def ya inner_simps diff_eq_0_iff_eq + apply simp + apply (subst Cx) + using C(1) fth + apply (simp only: setsum_clauses) + apply (subst inner_commute[of x]) + apply (auto simp add: inner_simps inner_commute[of x a] dot_rsum[OF fth]) + apply (rule setsum_0') + apply clarsimp + apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format]) + by auto} + moreover + {assume xa: "x \ C" and ya: "y \ C" + have "orthogonal x y" using xa ya xy C(4) unfolding pairwise_def by blast} + ultimately have "orthogonal x y" using xC yC by blast} + then have CPO: "pairwise orthogonal ?C" unfolding pairwise_def by blast + from fC cC SC CPO have "?P (insert a B) ?C" by blast + then show ?case by blast +qed + +lemma orthogonal_basis_exists: + fixes V :: "('a::euclidean_space) set" + shows "\B. independent B \ B \ span V \ V \ span B \ (card B = dim V) \ pairwise orthogonal B" +proof- + from basis_exists[of V] obtain B where B: "B \ V" "independent B" "V \ span B" "card B = dim V" by blast + from B have fB: "finite B" "card B = dim V" using independent_bound by auto + from basis_orthogonal[OF fB(1)] obtain C where + C: "finite C" "card C \ card B" "span C = span B" "pairwise orthogonal C" by blast + from C B + have CSV: "C \ span V" by (metis span_inc span_mono subset_trans) + from span_mono[OF B(3)] C have SVC: "span V \ span C" by (simp add: span_span) + from card_le_dim_spanning[OF CSV SVC C(1)] C(2,3) fB + have iC: "independent C" by (simp add: dim_span) + from C fB have "card C \ dim V" by simp + moreover have "dim V \ card C" using span_card_ge_dim[OF CSV SVC C(1)] + by (simp add: dim_span) + ultimately have CdV: "card C = dim V" using C(1) by simp + from C B CSV CdV iC show ?thesis by auto +qed + +lemma span_eq: "span S = span T \ S \ span T \ T \ 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 {* Low-dimensional subset is in a hyperplane (weak orthogonal complement). *} + +lemma span_not_univ_orthogonal: fixes S::"('a::euclidean_space) set" + assumes sU: "span S \ UNIV" + shows "\(a::'a). a \0 \ (\x \ span S. a \ x = 0)" +proof- + from sU obtain a where a: "a \ span S" by blast + from orthogonal_basis_exists obtain B where + B: "independent B" "B \ span S" "S \ span B" "card B = dim S" "pairwise orthogonal B" + by blast + from B have fB: "finite B" "card B = dim S" using independent_bound by auto + from span_mono[OF B(2)] span_mono[OF B(3)] + have sSB: "span S = span B" by (simp add: span_span) + let ?a = "a - setsum (\b. (a \ b / (b \ b)) *\<^sub>R b) B" + have "setsum (\b. (a \ b / (b \ b)) *\<^sub>R b) B \ span S" + unfolding sSB + apply (rule span_setsum[OF fB(1)]) + apply clarsimp + apply (rule span_mul) + by (rule span_superset) + with a have a0:"?a \ 0" by auto + have "\x\span B. ?a \ x = 0" + proof(rule span_induct') + show "subspace (\x. ?a \ x = 0)" by (auto simp add: subspace_def mem_def inner_simps) +next + {fix x assume x: "x \ B" + from x have B': "B = insert x (B - {x})" by blast + have fth: "finite (B - {x})" using fB by simp + have "?a \ x = 0" + apply (subst B') using fB fth + unfolding setsum_clauses(2)[OF fth] + apply simp unfolding inner_simps + apply (clarsimp simp add: inner_simps dot_lsum) + apply (rule setsum_0', rule ballI) + unfolding inner_commute + by (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])} + then show "\x \ B. ?a \ x = 0" by blast + qed + with a0 show ?thesis unfolding sSB by (auto intro: exI[where x="?a"]) +qed + +lemma span_not_univ_subset_hyperplane: + assumes SU: "span S \ (UNIV ::('a::euclidean_space) set)" + shows "\ a. a \0 \ span S \ {x. a \ x = 0}" + using span_not_univ_orthogonal[OF SU] by auto + +lemma lowdim_subset_hyperplane: fixes S::"('a::euclidean_space) set" + assumes d: "dim S < DIM('a)" + shows "\(a::'a). a \ 0 \ span S \ {x. a \ x = 0}" +proof- + {assume "span S = UNIV" + hence "dim (span S) = dim (UNIV :: ('a) set)" by simp + hence "dim S = DIM('a)" by (simp add: dim_span dim_UNIV) + with d have False by arith} + hence th: "span S \ UNIV" by blast + from span_not_univ_subset_hyperplane[OF th] show ?thesis . +qed + +text {* We can extend a linear basis-basis injection to the whole set. *} + +lemma linear_indep_image_lemma: + assumes lf: "linear f" and fB: "finite B" + and ifB: "independent (f ` B)" + and fi: "inj_on f B" and xsB: "x \ span B" + and fx: "f x = 0" + shows "x = 0" + using fB ifB fi xsB fx +proof(induct arbitrary: x rule: finite_induct[OF fB]) + case 1 thus ?case by (auto simp add: span_empty) +next + case (2 a b x) + have fb: "finite b" using "2.prems" by simp + have th0: "f ` b \ f ` (insert a b)" + apply (rule image_mono) by blast + from independent_mono[ OF "2.prems"(2) th0] + have ifb: "independent (f ` b)" . + have fib: "inj_on f b" + apply (rule subset_inj_on [OF "2.prems"(3)]) + by blast + from span_breakdown[of a "insert a b", simplified, OF "2.prems"(4)] + obtain k where k: "x - k*\<^sub>R a \ span (b -{a})" by blast + have "f (x - k*\<^sub>R a) \ span (f ` b)" + unfolding span_linear_image[OF lf] + apply (rule imageI) + using k span_mono[of "b-{a}" b] by blast + hence "f x - k*\<^sub>R f a \ span (f ` b)" + by (simp add: linear_sub[OF lf] linear_cmul[OF lf]) + hence th: "-k *\<^sub>R f a \ span (f ` b)" + using "2.prems"(5) by simp + {assume k0: "k = 0" + from k0 k have "x \ span (b -{a})" by simp + then have "x \ span b" using span_mono[of "b-{a}" b] + by blast} + moreover + {assume k0: "k \ 0" + from span_mul[OF th, of "- 1/ k"] k0 + have th1: "f a \ span (f ` b)" + by auto + from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric] + have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast + from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"] + have "f a \ span (f ` b)" using tha + using "2.hyps"(2) + "2.prems"(3) by auto + with th1 have False by blast + then have "x \ span b" by blast} + ultimately have xsb: "x \ span b" by blast + from "2.hyps"(3)[OF fb ifb fib xsb "2.prems"(5)] + show "x = 0" . +qed + +text {* We can extend a linear mapping from basis. *} + +lemma linear_independent_extend_lemma: + fixes f :: "'a::real_vector \ 'b::real_vector" + assumes fi: "finite B" and ib: "independent B" + shows "\g. (\x\ span B. \y\ span B. g (x + y) = g x + g y) + \ (\x\ span B. \c. g (c*\<^sub>R x) = c *\<^sub>R g x) + \ (\x\ B. g x = f x)" +using ib fi +proof(induct rule: finite_induct[OF fi]) + case 1 thus ?case by (auto simp add: span_empty) +next + case (2 a b) + from "2.prems" "2.hyps" have ibf: "independent b" "finite b" + by (simp_all add: independent_insert) + from "2.hyps"(3)[OF ibf] obtain g where + g: "\x\span b. \y\span b. g (x + y) = g x + g y" + "\x\span b. \c. g (c *\<^sub>R x) = c *\<^sub>R g x" "\x\b. g x = f x" by blast + let ?h = "\z. SOME k. (z - k *\<^sub>R a) \ span b" + {fix z assume z: "z \ span (insert a b)" + have th0: "z - ?h z *\<^sub>R a \ span b" + apply (rule someI_ex) + unfolding span_breakdown_eq[symmetric] + using z . + {fix k assume k: "z - k *\<^sub>R a \ span b" + have eq: "z - ?h z *\<^sub>R a - (z - k*\<^sub>R a) = (k - ?h z) *\<^sub>R a" + by (simp add: field_simps scaleR_left_distrib [symmetric]) + from span_sub[OF th0 k] + have khz: "(k - ?h z) *\<^sub>R a \ span b" by (simp add: eq) + {assume "k \ ?h z" hence k0: "k - ?h z \ 0" by simp + from k0 span_mul[OF khz, of "1 /(k - ?h z)"] + have "a \ span b" by simp + with "2.prems"(1) "2.hyps"(2) have False + by (auto simp add: dependent_def)} + then have "k = ?h z" by blast} + with th0 have "z - ?h z *\<^sub>R a \ span b \ (\k. z - k *\<^sub>R a \ span b \ k = ?h z)" by blast} + note h = this + let ?g = "\z. ?h z *\<^sub>R f a + g (z - ?h z *\<^sub>R a)" + {fix x y assume x: "x \ span (insert a b)" and y: "y \ span (insert a b)" + have tha: "\(x::'a) y a k l. (x + y) - (k + l) *\<^sub>R a = (x - k *\<^sub>R a) + (y - l *\<^sub>R a)" + by (simp add: algebra_simps) + have addh: "?h (x + y) = ?h x + ?h y" + apply (rule conjunct2[OF h, rule_format, symmetric]) + apply (rule span_add[OF x y]) + unfolding tha + by (metis span_add x y conjunct1[OF h, rule_format]) + 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" and c:: real assume x: "x \ span (insert a b)" + have tha: "\(x::'a) c k a. c *\<^sub>R x - (c * k) *\<^sub>R a = c *\<^sub>R (x - k *\<^sub>R a)" + by (simp add: algebra_simps) + have hc: "?h (c *\<^sub>R x) = c * ?h x" + apply (rule conjunct2[OF h, rule_format, symmetric]) + apply (metis span_mul x) + by (metis tha span_mul x conjunct1[OF h]) + have "?g (c *\<^sub>R x) = c*\<^sub>R ?g x" + unfolding hc tha g(2)[rule_format, OF conjunct1[OF h, OF x]] + by (simp add: algebra_simps)} + moreover + {fix x assume x: "x \ (insert a b)" + {assume xa: "x = a" + have ha1: "1 = ?h a" + apply (rule conjunct2[OF h, rule_format]) + apply (metis span_superset insertI1) + using conjunct1[OF h, OF span_superset, OF insertI1] + by (auto simp add: span_0) + + from xa ha1[symmetric] have "?g x = f x" + apply simp + using g(2)[rule_format, OF span_0, of 0] + by simp} + moreover + {assume xb: "x \ b" + have h0: "0 = ?h x" + apply (rule conjunct2[OF h, rule_format]) + apply (metis span_superset x) + apply simp + apply (metis span_superset xb) + done + have "?g x = f x" + by (simp add: h0[symmetric] g(3)[rule_format, OF xb])} + ultimately have "?g x = f x" using x by blast } + ultimately show ?case apply - apply (rule exI[where x="?g"]) by blast +qed + +lemma linear_independent_extend: + assumes iB: "independent (B:: ('a::euclidean_space) set)" + shows "\g. linear g \ (\x\B. g x = f x)" +proof- + from maximal_independent_subset_extend[of B UNIV] iB + obtain C where C: "B \ C" "independent C" "\x. x \ span C" by auto + + from C(2) independent_bound[of C] linear_independent_extend_lemma[of C f] + obtain g where g: "(\x\ span C. \y\ span C. g (x + y) = g x + g y) + \ (\x\ span C. \c. g (c*\<^sub>R x) = c *\<^sub>R g x) + \ (\x\ C. g x = f x)" by blast + from g show ?thesis unfolding linear_def using C + apply clarsimp by blast +qed + +text {* Can construct an isomorphism between spaces of same dimension. *} + +lemma card_le_inj: assumes fA: "finite A" and fB: "finite B" + and c: "card A \ card B" shows "(\f. f ` A \ B \ inj_on f A)" +using fB c +proof(induct arbitrary: B rule: finite_induct[OF fA]) + case 1 thus ?case by simp +next + case (2 x s t) + thus ?case + proof(induct rule: finite_induct[OF "2.prems"(1)]) + case 1 then show ?case by simp + next + case (2 y t) + from "2.prems"(1,2,5) "2.hyps"(1,2) have cst:"card s \ card t" by simp + from "2.prems"(3) [OF "2.hyps"(1) cst] obtain f where + f: "f ` s \ t \ inj_on f s" by blast + from f "2.prems"(2) "2.hyps"(2) show ?case + apply - + apply (rule exI[where x = "\z. if z = x then y else f z"]) + by (auto simp add: inj_on_def) + qed +qed + +lemma card_subset_eq: assumes fB: "finite B" and AB: "A \ B" and + c: "card A = card B" + shows "A = B" +proof- + from fB AB have fA: "finite A" by (auto intro: finite_subset) + from fA fB have fBA: "finite (B - A)" by auto + have e: "A \ (B - A) = {}" by blast + have eq: "A \ (B - A) = B" using AB by blast + from card_Un_disjoint[OF fA fBA e, unfolded eq c] + have "card (B - A) = 0" by arith + hence "B - A = {}" unfolding card_eq_0_iff using fA fB by simp + with AB show "A = B" by blast +qed + +lemma subspace_isomorphism: + assumes s: "subspace (S:: ('a::euclidean_space) set)" + and t: "subspace (T :: ('b::euclidean_space) set)" + and d: "dim S = dim T" + shows "\f. linear f \ f ` S = T \ inj_on f S" +proof- + from basis_exists[of S] independent_bound obtain B where + B: "B \ S" "independent B" "S \ span B" "card B = dim S" and fB: "finite B" by blast + from basis_exists[of T] independent_bound obtain C where + C: "C \ T" "independent C" "T \ span C" "card C = dim T" and fC: "finite C" by blast + from B(4) C(4) card_le_inj[of B C] d obtain f where + f: "f ` B \ C" "inj_on f B" using `finite B` `finite C` by auto + from linear_independent_extend[OF B(2)] obtain g where + g: "linear g" "\x\ B. g x = f x" by blast + from inj_on_iff_eq_card[OF fB, of f] f(2) + have "card (f ` B) = card B" by simp + with B(4) C(4) have ceq: "card (f ` B) = card C" using d + by simp + have "g ` B = f ` B" using g(2) + by (auto simp add: image_iff) + also have "\ = C" using card_subset_eq[OF fC f(1) ceq] . + finally have gBC: "g ` B = C" . + have gi: "inj_on g B" using f(2) g(2) + by (auto simp add: inj_on_def) + note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi] + {fix x y assume x: "x \ S" and y: "y \ S" and gxy:"g x = g y" + from B(3) x y have x': "x \ span B" and y': "y \ span B" by blast+ + from gxy have th0: "g (x - y) = 0" by (simp add: linear_sub[OF g(1)]) + have th1: "x - y \ span B" using x' y' by (metis span_sub) + have "x=y" using g0[OF th1 th0] by simp } + then have giS: "inj_on g S" + unfolding inj_on_def by blast + from span_subspace[OF B(1,3) s] + have "g ` S = span (g ` B)" by (simp add: span_linear_image[OF g(1)]) + also have "\ = span C" unfolding gBC .. + also have "\ = T" using span_subspace[OF C(1,3) t] . + finally have gS: "g ` S = T" . + from g(1) gS giS show ?thesis by blast +qed + +text {* Linear functions are equal on a subspace if they are on a spanning set. *} + +lemma subspace_kernel: + assumes lf: "linear f" + shows "subspace {x. f x = 0}" +apply (simp add: subspace_def) +by (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf]) + +lemma linear_eq_0_span: + assumes lf: "linear f" and f0: "\x\B. f x = 0" + shows "\x \ span B. f x = 0" +proof + fix x assume x: "x \ span B" + let ?P = "\x. f x = 0" + from subspace_kernel[OF lf] have "subspace ?P" unfolding Collect_def . + with x f0 span_induct[of B "?P" x] show "f x = 0" by blast +qed + +lemma linear_eq_0: + assumes lf: "linear f" and SB: "S \ span B" and f0: "\x\B. f x = 0" + shows "\x \ S. f x = 0" + by (metis linear_eq_0_span[OF lf] subset_eq SB f0) + +lemma linear_eq: + assumes lf: "linear f" and lg: "linear g" and S: "S \ span B" + and fg: "\ x\ B. f x = g x" + shows "\x\ S. f x = g x" +proof- + let ?h = "\x. f x - g x" + from fg have fg': "\x\ 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: + assumes lf: "linear (f::'a::euclidean_space \ _)" and lg: "linear g" + and fg: "\i (UNIV :: 'a set)" + from equalityD2[OF span_basis'[where 'a='a]] + have IU: " (UNIV :: 'a set) \ span ?I" by blast + have "f x = g x" apply(rule linear_eq[OF lf lg IU,rule_format]) using fg x by auto } + then show ?thesis by (auto intro: ext) +qed + +text {* Similar results for bilinear functions. *} + +lemma bilinear_eq: + assumes bf: "bilinear f" + and bg: "bilinear g" + and SB: "S \ span B" and TC: "T \ span C" + and fg: "\x\ B. \y\ C. f x y = g x y" + shows "\x\S. \y\T. f x y = g x y " +proof- + let ?P = "\x. \y\ span C. f x y = g x y" + from bf bg have sp: "subspace ?P" + unfolding bilinear_def linear_def subspace_def bf bg + by(auto simp add: span_0 mem_def bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf]) + + have "\x \ span B. \y\ span C. f x y = g x y" + apply - + apply (rule ballI) + apply (rule span_induct[of B ?P]) + defer + apply (rule sp) + apply assumption + apply (clarsimp simp add: Ball_def) + apply (rule_tac P="\y. f xa y = g xa y" and S=C in span_induct) + using fg + apply (auto simp add: subspace_def) + using bf bg unfolding bilinear_def linear_def + by(auto simp add: span_0 mem_def bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf]) + then show ?thesis using SB TC by (auto intro: ext) +qed + +lemma bilinear_eq_stdbasis: fixes f::"'a::euclidean_space \ 'b::euclidean_space \ _" + assumes bf: "bilinear f" + and bg: "bilinear g" + and fg: "\ijx \ (basis ` {..y\ (basis ` {.. 'b::euclidean_space" + assumes lf: "linear f" and fi: "inj f" + shows "\g. linear g \ g o f = id" +proof- + from linear_independent_extend[OF independent_injective_image, OF independent_basis, OF lf fi] + obtain h:: "'b => 'a" where h: "linear h" + " \x \ f ` basis ` {..i f) (basis i) = id (basis 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 o f = id" . + then show ?thesis using h(1) by blast +qed + +lemma linear_surjective_right_inverse: fixes f::"'a::euclidean_space => 'b::euclidean_space" + assumes lf: "linear f" and sf: "surj f" + shows "\g. linear g \ f o g = id" +proof- + from linear_independent_extend[OF independent_basis[where 'a='b],of "inv f"] + obtain h:: "'b \ 'a" where + h: "linear h" "\ x\ basis ` {..i 'b::euclidean_space"} is also surjective. *} + +lemma linear_injective_imp_surjective: fixes f::"'a::euclidean_space => 'a::euclidean_space" + assumes lf: "linear f" and fi: "inj f" + shows "surj f" +proof- + let ?U = "UNIV :: 'a set" + from basis_exists[of ?U] obtain B + where B: "B \ ?U" "independent B" "?U \ span B" "card B = dim ?U" + by blast + from B(4) have d: "dim ?U = card B" by simp + have th: "?U \ span (f ` B)" + apply (rule card_ge_dim_independent) + apply blast + apply (rule independent_injective_image[OF B(2) lf fi]) + apply (rule order_eq_refl) + apply (rule sym) + unfolding d + apply (rule card_image) + apply (rule subset_inj_on[OF fi]) + by blast + from th show ?thesis + unfolding span_linear_image[OF lf] surj_def + using B(3) by blast +qed + +text {* And vice versa. *} + +lemma surjective_iff_injective_gen: + assumes fS: "finite S" and fT: "finite T" and c: "card S = card T" + and ST: "f ` S \ T" + shows "(\y \ T. \x \ S. f x = y) \ inj_on f S" (is "?lhs \ ?rhs") +proof- + {assume h: "?lhs" + {fix x y assume x: "x \ S" and y: "y \ S" and f: "f x = f y" + from x fS have S0: "card S \ 0" by auto + {assume xy: "x \ y" + have th: "card S \ card (f ` (S - {y}))" + unfolding c + apply (rule card_mono) + apply (rule finite_imageI) + using fS apply simp + using h xy x y f unfolding subset_eq image_iff + apply auto + apply (case_tac "xa = f x") + apply (rule bexI[where x=x]) + apply auto + done + also have " \ \ card (S -{y})" + apply (rule card_image_le) + using fS by simp + also have "\ \ card S - 1" using y fS by simp + finally have False using S0 by arith } + then have "x = y" by blast} + then have ?rhs unfolding inj_on_def by blast} + moreover + {assume h: ?rhs + have "f ` S = T" + apply (rule card_subset_eq[OF fT ST]) + unfolding card_image[OF h] using c . + then have ?lhs by blast} + ultimately show ?thesis by blast +qed + +lemma linear_surjective_imp_injective: fixes f::"'a::euclidean_space => 'a::euclidean_space" + assumes lf: "linear f" and sf: "surj f" + shows "inj f" +proof- + let ?U = "UNIV :: 'a set" + from basis_exists[of ?U] obtain B + where B: "B \ ?U" "independent B" "?U \ span B" and d: "card B = dim ?U" + by blast + {fix x assume x: "x \ span B" and fx: "f x = 0" + from B(2) have fB: "finite B" using independent_bound by auto + have fBi: "independent (f ` B)" + apply (rule card_le_dim_spanning[of "f ` B" ?U]) + apply blast + using sf B(3) + unfolding span_linear_image[OF lf] surj_def subset_eq image_iff + apply blast + using fB apply blast + unfolding d[symmetric] + apply (rule card_image_le) + apply (rule fB) + done + have th0: "dim ?U \ card (f ` B)" + apply (rule span_card_ge_dim) + apply blast + unfolding span_linear_image[OF lf] + apply (rule subset_trans[where B = "f ` UNIV"]) + using sf unfolding surj_def apply blast + apply (rule image_mono) + apply (rule B(3)) + apply (metis finite_imageI fB) + done + + moreover have "card (f ` B) \ card B" + by (rule card_image_le, rule fB) + ultimately have th1: "card B = card (f ` B)" unfolding d by arith + have fiB: "inj_on f B" + unfolding surjective_iff_injective_gen[OF fB finite_imageI[OF fB] th1 subset_refl, symmetric] by blast + from linear_indep_image_lemma[OF lf fB fBi fiB x] fx + have "x = 0" by blast} + note th = this + from th show ?thesis unfolding linear_injective_0[OF lf] + using B(3) by blast +qed + +text {* Hence either is enough for isomorphism. *} + +lemma left_right_inverse_eq: + assumes fg: "f o g = id" and gh: "g o h = id" + shows "f = h" +proof- + have "f = f o (g o h)" unfolding gh by simp + also have "\ = (f o g) o h" by (simp add: o_assoc) + finally show "f = h" unfolding fg by simp +qed + +lemma isomorphism_expand: + "f o g = id \ g o f = id \ (\x. f(g x) = x) \ (\x. g(f x) = x)" + by (simp add: fun_eq_iff o_def id_def) + +lemma linear_injective_isomorphism: fixes f::"'a::euclidean_space => 'a::euclidean_space" + assumes lf: "linear f" and fi: "inj f" + shows "\f'. linear f' \ (\x. f' (f x) = x) \ (\x. f (f' x) = x)" +unfolding isomorphism_expand[symmetric] +using linear_surjective_right_inverse[OF lf linear_injective_imp_surjective[OF lf fi]] linear_injective_left_inverse[OF lf fi] +by (metis left_right_inverse_eq) + +lemma linear_surjective_isomorphism: fixes f::"'a::euclidean_space => 'a::euclidean_space" + assumes lf: "linear f" and sf: "surj f" + shows "\f'. linear f' \ (\x. f' (f x) = x) \ (\x. f (f' x) = x)" +unfolding isomorphism_expand[symmetric] +using linear_surjective_right_inverse[OF lf sf] linear_injective_left_inverse[OF lf linear_surjective_imp_injective[OF lf sf]] +by (metis left_right_inverse_eq) + +text {* Left and right inverses are the same for @{typ "'a::euclidean_space => 'a::euclidean_space"}. *} + +lemma linear_inverse_left: fixes f::"'a::euclidean_space => 'a::euclidean_space" + assumes lf: "linear f" and lf': "linear f'" + shows "f o f' = id \ f' o f = id" +proof- + {fix f f':: "'a => 'a" + assume lf: "linear f" "linear f'" and f: "f o f' = id" + from f have sf: "surj f" + apply (auto simp add: o_def id_def surj_def) + by metis + from linear_surjective_isomorphism[OF lf(1) sf] lf f + have "f' o f = id" unfolding fun_eq_iff o_def id_def + by metis} + then show ?thesis using lf lf' by metis +qed + +text {* Moreover, a one-sided inverse is automatically linear. *} + +lemma left_inverse_linear: fixes f::"'a::euclidean_space => 'a::euclidean_space" + assumes lf: "linear f" and gf: "g o f = id" + shows "linear g" +proof- + from gf have fi: "inj f" apply (auto simp add: inj_on_def o_def id_def fun_eq_iff) + by metis + from linear_injective_isomorphism[OF lf fi] + obtain h:: "'a \ 'a" where + h: "linear h" "\x. h (f x) = x" "\x. f (h x) = x" by blast + have "h = g" apply (rule ext) using gf h(2,3) + apply (simp add: o_def id_def fun_eq_iff) + by metis + with h(1) show ?thesis by blast +qed + +subsection {* Infinity norm *} + +definition "infnorm (x::'a::euclidean_space) = Sup {abs(x$$i) |i. ii. i \ (UNIV :: 'n set)" + by auto + +lemma infnorm_set_image: + "{abs((x::'a::euclidean_space)$$i) |i. ii. abs(x$$i)) ` {.. {}" + unfolding infnorm_set_image + by auto + +lemma infnorm_pos_le: "0 \ infnorm (x::'a::euclidean_space)" + unfolding infnorm_def + unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma] + unfolding infnorm_set_image + by auto + +lemma infnorm_triangle: "infnorm ((x::'a::euclidean_space) + y) \ infnorm x + infnorm y" +proof- + have th: "\x y (z::real). x - y <= z \ x - z <= y" by arith + have th1: "\S f. f ` S = { f i| i. i \ S}" by blast + have th2: "\x (y::real). abs(x + y) - abs(x) <= abs(y)" by arith + have *:"\i. i \ {.. i {}" by blast + have th1: "\S f. f ` S = { f i| i. i \ S}" by blast + show ?thesis unfolding infnorm_def + apply(subst Sup_finite_ge_iff) using Sup_finite_in[OF fS S0] + using infnorm_set_image using True by auto +qed + +lemma infnorm_mul_lemma: "infnorm(a *\<^sub>R x) <= \a\ * infnorm x" + apply (subst infnorm_def) + unfolding Sup_finite_le_iff[OF infnorm_set_lemma] + unfolding infnorm_set_image ball_simps euclidean_scaleR abs_mult + using component_le_infnorm[of x] by(auto intro: mult_mono) + +lemma infnorm_mul: "infnorm(a *\<^sub>R x) = abs a * infnorm x" +proof- + {assume a0: "a = 0" hence ?thesis by (simp add: infnorm_0) } + moreover + {assume a0: "a \ 0" + from a0 have th: "(1/a) *\<^sub>R (a *\<^sub>R x) = x" by simp + from a0 have ap: "\a\ > 0" by arith + from infnorm_mul_lemma[of "1/a" "a *\<^sub>R x"] + have "infnorm x \ 1/\a\ * infnorm (a*\<^sub>R x)" + unfolding th by simp + with ap have "\a\ * infnorm x \ \a\ * (1/\a\ * infnorm (a *\<^sub>R x))" by (simp add: field_simps) + then have "\a\ * infnorm x \ infnorm (a*\<^sub>R x)" + using ap by (simp add: field_simps) + with infnorm_mul_lemma[of a x] have ?thesis by arith } + ultimately show ?thesis by blast +qed + +lemma infnorm_pos_lt: "infnorm x > 0 \ x \ 0" + using infnorm_pos_le[of x] infnorm_eq_0[of x] by arith + +text {* Prove that it differs only up to a bound from Euclidean norm. *} + +lemma infnorm_le_norm: "infnorm x \ norm x" + unfolding infnorm_def Sup_finite_le_iff[OF infnorm_set_lemma] + unfolding infnorm_set_image ball_simps + by (metis component_le_norm) + +lemma card_enum: "card {1 .. n} = n" by auto + +lemma norm_le_infnorm: "norm(x) <= sqrt(real DIM('a)) * infnorm(x::'a::euclidean_space)" +proof- + let ?d = "DIM('a)" + have "real ?d \ 0" by simp + hence d2: "(sqrt (real ?d))^2 = real ?d" + by (auto intro: real_sqrt_pow2) + have th: "sqrt (real ?d) * infnorm x \ 0" + by (simp add: zero_le_mult_iff infnorm_pos_le) + have th1: "x \ x \ (sqrt (real ?d) * infnorm x)^2" + unfolding power_mult_distrib d2 + unfolding real_of_nat_def apply(subst euclidean_inner) + apply (subst power2_abs[symmetric]) + apply(rule order_trans[OF setsum_bounded[where K="\infnorm x\\"]]) + apply(auto simp add: power2_eq_square[symmetric]) + apply (subst power2_abs[symmetric]) + apply (rule power_mono) + unfolding infnorm_def Sup_finite_ge_iff[OF infnorm_set_lemma] + unfolding infnorm_set_image bex_simps apply(rule_tac x=i in bexI) by auto + from real_le_lsqrt[OF inner_ge_zero th th1] + show ?thesis unfolding norm_eq_sqrt_inner id_def . +qed + +text {* Equality in Cauchy-Schwarz and triangle inequalities. *} + +lemma norm_cauchy_schwarz_eq: "x \ y = norm x * norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x" (is "?lhs \ ?rhs") +proof- + {assume h: "x = 0" + hence ?thesis by simp} + moreover + {assume h: "y = 0" + hence ?thesis by simp} + moreover + {assume x: "x \ 0" and y: "y \ 0" + from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"] + have "?rhs \ (norm y * (norm y * norm x * norm x - norm x * (x \ y)) - norm x * (norm y * (y \ x) - norm x * norm y * norm y) = 0)" + using x y + unfolding inner_simps + unfolding power2_norm_eq_inner[symmetric] power2_eq_square diff_eq_0_iff_eq apply (simp add: inner_commute) + apply (simp add: field_simps) by metis + also have "\ \ (2 * norm x * norm y * (norm x * norm y - x \ y) = 0)" using x y + by (simp add: field_simps inner_commute) + also have "\ \ ?lhs" using x y + apply simp + by metis + finally have ?thesis by blast} + ultimately show ?thesis by blast +qed + +lemma norm_cauchy_schwarz_abs_eq: + shows "abs(x \ y) = norm x * norm y \ + norm x *\<^sub>R y = norm y *\<^sub>R x \ norm(x) *\<^sub>R y = - norm y *\<^sub>R x" (is "?lhs \ ?rhs") +proof- + have th: "\(x::real) a. a \ 0 \ abs x = a \ x = a \ x = - a" by arith + have "?rhs \ norm x *\<^sub>R y = norm y *\<^sub>R x \ norm (- x) *\<^sub>R y = norm y *\<^sub>R (- x)" + by simp + also have "\ \(x \ y = norm x * norm y \ + (-x) \ y = norm x * norm y)" + unfolding norm_cauchy_schwarz_eq[symmetric] + unfolding norm_minus_cancel norm_scaleR .. + also have "\ \ ?lhs" + unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] inner_simps by auto + finally show ?thesis .. +qed + +lemma norm_triangle_eq: + fixes x y :: "'a::real_inner" + shows "norm(x + y) = norm x + norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x" +proof- + {assume x: "x =0 \ y =0" + hence ?thesis by (cases "x=0", simp_all)} + moreover + {assume x: "x \ 0" and y: "y \ 0" + hence "norm x \ 0" "norm y \ 0" + by simp_all + hence n: "norm x > 0" "norm y > 0" + using norm_ge_zero[of x] norm_ge_zero[of y] + by arith+ + have th: "\(a::real) b c. a + b + c \ 0 ==> (a = b + c \ a^2 = (b + c)^2)" by algebra + have "norm(x + y) = norm x + norm y \ norm(x + y)^ 2 = (norm x + norm y) ^2" + apply (rule th) using n norm_ge_zero[of "x + y"] + by arith + also have "\ \ norm x *\<^sub>R y = norm y *\<^sub>R x" + unfolding norm_cauchy_schwarz_eq[symmetric] + unfolding power2_norm_eq_inner inner_simps + by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps) + finally have ?thesis .} + ultimately show ?thesis by blast +qed + +subsection {* Collinearity *} + +definition + collinear :: "'a::real_vector set \ bool" where + "collinear S \ (\u. \x \ S. \ y \ S. \c. x - y = c *\<^sub>R u)" + +lemma collinear_empty: "collinear {}" by (simp add: collinear_def) + +lemma collinear_sing: "collinear {x}" + by (simp add: collinear_def) + +lemma collinear_2: "collinear {x, y}" + apply (simp add: collinear_def) + apply (rule exI[where x="x - y"]) + apply auto + apply (rule exI[where x=1], simp) + apply (rule exI[where x="- 1"], simp) + done + +lemma collinear_lemma: "collinear {0,x,y} \ x = 0 \ y = 0 \ (\c. y = c *\<^sub>R x)" (is "?lhs \ ?rhs") +proof- + {assume "x=0 \ y = 0" hence ?thesis + by (cases "x = 0", simp_all add: collinear_2 insert_commute)} + moreover + {assume x: "x \ 0" and y: "y \ 0" + {assume h: "?lhs" + then obtain u where u: "\ x\ {0,x,y}. \y\ {0,x,y}. \c. x - y = c *\<^sub>R u" unfolding collinear_def by blast + from u[rule_format, of x 0] u[rule_format, of y 0] + obtain cx and cy where + cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u" + by auto + from cx x have cx0: "cx \ 0" by auto + from cy y have cy0: "cy \ 0" by auto + let ?d = "cy / cx" + from cx cy cx0 have "y = ?d *\<^sub>R x" + by simp + hence ?rhs using x y by blast} + moreover + {assume h: "?rhs" + then obtain c where c: "y = c *\<^sub>R x" using x y by blast + have ?lhs unfolding collinear_def c + apply (rule exI[where x=x]) + apply auto + apply (rule exI[where x="- 1"], simp) + apply (rule exI[where x= "-c"], simp) + apply (rule exI[where x=1], simp) + apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib) + apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib) + done} + ultimately have ?thesis by blast} + ultimately show ?thesis by blast +qed + +lemma norm_cauchy_schwarz_equal: + shows "abs(x \ y) = norm x * norm y \ collinear {0,x,y}" +unfolding norm_cauchy_schwarz_abs_eq +apply (cases "x=0", simp_all add: collinear_2) +apply (cases "y=0", simp_all add: collinear_2 insert_commute) +unfolding collinear_lemma +apply simp +apply (subgoal_tac "norm x \ 0") +apply (subgoal_tac "norm y \ 0") +apply (rule iffI) +apply (cases "norm x *\<^sub>R y = norm y *\<^sub>R x") +apply (rule exI[where x="(1/norm x) * norm y"]) +apply (drule sym) +unfolding scaleR_scaleR[symmetric] +apply (simp add: field_simps) +apply (rule exI[where x="(1/norm x) * - norm y"]) +apply clarify +apply (drule sym) +unfolding scaleR_scaleR[symmetric] +apply (simp add: field_simps) +apply (erule exE) +apply (erule ssubst) +unfolding scaleR_scaleR +unfolding norm_scaleR +apply (subgoal_tac "norm x * c = \c\ * norm x \ norm x * c = - \c\ * norm x") +apply (case_tac "c <= 0", simp add: field_simps) +apply (simp add: field_simps) +apply (case_tac "c <= 0", simp add: field_simps) +apply (simp add: field_simps) +apply simp +apply simp +done + +subsection "Instantiate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}." + +lemma basis_real_range: "basis ` {..<1} = {1::real}" by auto + +instance real::ordered_euclidean_space + by default (auto simp add: euclidean_component_def) + +lemma Eucl_real_simps[simp]: + "(x::real) $$ 0 = x" + "(\\ i. f i) = ((f 0)::real)" + "\i. i > 0 \ x $$ i = 0" + defer apply(subst euclidean_eq) apply safe + unfolding euclidean_lambda_beta' + unfolding euclidean_component_def by auto + +lemma complex_basis[simp]: + shows "basis 0 = (1::complex)" and "basis 1 = ii" and "basis (Suc 0) = ii" + unfolding basis_complex_def by auto + +section {* Products Spaces *} + +lemma DIM_prod[simp]: "DIM('a \ 'b) = DIM('b::euclidean_space) + DIM('a::euclidean_space)" + (* FIXME: why this orientation? Why not "DIM('a) + DIM('b)" ? *) + unfolding dimension_prod_def by (rule add_commute) + +instantiation prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space +begin + +definition "x \ (y::('a\'b)) \ (\i'b). x $$ i \ y $$ i)" +definition "x < (y::('a\'b)) \ (\i'b). x $$ i < y $$ i)" + +instance proof qed (auto simp: less_prod_def less_eq_prod_def) +end + + +end diff -r 0f35a870ecf1 -r 691c52e900ca src/HOL/Multivariate_Analysis/Operator_Norm.thy --- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy Wed Aug 10 08:42:26 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy Wed Aug 10 09:23:42 2011 -0700 @@ -5,7 +5,7 @@ header {* Operator Norm *} theory Operator_Norm -imports Euclidean_Space +imports Linear_Algebra begin definition "onorm f = Sup {norm (f x)| x. norm x = 1}" diff -r 0f35a870ecf1 -r 691c52e900ca src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 10 08:42:26 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 10 09:23:42 2011 -0700 @@ -7,7 +7,7 @@ header {* Elementary topology in Euclidean space. *} theory Topology_Euclidean_Space -imports SEQ Euclidean_Space "~~/src/HOL/Library/Glbs" +imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" begin (* to be moved elsewhere *)