44133

1 
(* Title: HOL/Multivariate_Analysis/Linear_Algebra.thy


2 
Author: Amine Chaieb, University of Cambridge


3 
*)


4 


5 
header {* Elementary linear algebra on Euclidean spaces *}


6 


7 
theory Linear_Algebra


8 
imports


9 
Euclidean_Space


10 
"~~/src/HOL/Library/Infinite_Set"


11 
L2_Norm


12 
"~~/src/HOL/Library/Convex"


13 
uses


14 
"~~/src/HOL/Library/positivstellensatz.ML" (* FIXME duplicate use!? *)


15 
("normarith.ML")


16 
begin


17 


18 
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"


19 
by auto


20 


21 
notation inner (infix "\<bullet>" 70)


22 


23 
subsection {* A connectedness or intermediate value lemma with several applications. *}


24 


25 
lemma connected_real_lemma:


26 
fixes f :: "real \<Rightarrow> 'a::metric_space"


27 
assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2"


28 
and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y  x) < d \<longrightarrow> dist(f y) (f x) < e"


29 
and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1"


30 
and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2"


31 
and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)"


32 
shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x")


33 
proof


34 
let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}"


35 
have Se: " \<exists>x. x \<in> ?S" apply (rule exI[where x=a]) by (auto simp add: fa)


36 
have Sub: "\<exists>y. isUb UNIV ?S y"


37 
apply (rule exI[where x= b])


38 
using ab fb e12 by (auto simp add: isUb_def setle_def)


39 
from reals_complete[OF Se Sub] obtain l where


40 
l: "isLub UNIV ?S l"by blast


41 
have alb: "a \<le> l" "l \<le> b" using l ab fa fb e12


42 
apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)


43 
by (metis linorder_linear)


44 
have ale1: "\<forall>z \<ge> a. z < l \<longrightarrow> f z \<in> e1" using l


45 
apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)


46 
by (metis linorder_linear not_le)


47 
have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z  x) < d" by arith


48 
have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith


49 
have "\<And>d::real. 0 < d \<Longrightarrow> 0 < d/2 \<and> d/2 < d" by simp


50 
then have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by blast


51 
{assume le2: "f l \<in> e2"


52 
from le2 fa fb e12 alb have la: "l \<noteq> a" by metis


53 
hence lap: "l  a > 0" using alb by arith


54 
from e2[rule_format, OF le2] obtain e where


55 
e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis


56 
from dst[OF alb e(1)] obtain d where


57 
d: "d > 0" "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis


58 
let ?d' = "min (d/2) ((l  a)/2)"


59 
have "?d' < d \<and> 0 < ?d' \<and> ?d' < l  a" using lap d(1)


60 
by (simp add: min_max.less_infI2)


61 
then have "\<exists>d'. d' < d \<and> d' >0 \<and> l  d' > a" by auto


62 
then obtain d' where d': "d' > 0" "d' < d" "l  d' > a" by metis


63 
from d e have th0: "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> f y \<in> e2" by metis


64 
from th0[rule_format, of "l  d'"] d' have "f (l  d') \<in> e2" by auto


65 
moreover


66 
have "f (l  d') \<in> e1" using ale1[rule_format, of "l d'"] d' by auto


67 
ultimately have False using e12 alb d' by auto}


68 
moreover


69 
{assume le1: "f l \<in> e1"


70 
from le1 fa fb e12 alb have lb: "l \<noteq> b" by metis


71 
hence blp: "b  l > 0" using alb by arith


72 
from e1[rule_format, OF le1] obtain e where


73 
e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis


74 
from dst[OF alb e(1)] obtain d where


75 
d: "d > 0" "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis


76 
have "\<And>d::real. 0 < d \<Longrightarrow> d/2 < d \<and> 0 < d/2" by simp


77 
then have "\<exists>d'. d' < d \<and> d' >0" using d(1) by blast


78 
then obtain d' where d': "d' > 0" "d' < d" by metis


79 
from d e have th0: "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> f y \<in> e1" by auto


80 
hence "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto


81 
with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" by auto


82 
with l d' have False


83 
by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) }


84 
ultimately show ?thesis using alb by metis


85 
qed


86 


87 
text{* One immediately useful corollary is the existence of square roots!  Should help to get rid of all the development of squareroot for reals as a special case *}


88 


89 
lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)"


90 
proof


91 
have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith


92 
thus ?thesis by (simp add: field_simps power2_eq_square)


93 
qed


94 


95 
lemma square_continuous: "0 < (e::real) ==> \<exists>d. 0 < d \<and> (\<forall>y. abs(y  x) < d \<longrightarrow> abs(y * y  x * x) < e)"


96 
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)


97 
apply (rule_tac x="s" in exI)


98 
apply auto


99 
apply (erule_tac x=y in allE)


100 
apply auto


101 
done


102 


103 
lemma real_le_lsqrt: "0 <= x \<Longrightarrow> 0 <= y \<Longrightarrow> x <= y^2 ==> sqrt x <= y"


104 
using real_sqrt_le_iff[of x "y^2"] by simp


105 


106 
lemma real_le_rsqrt: "x^2 \<le> y \<Longrightarrow> x \<le> sqrt y"


107 
using real_sqrt_le_mono[of "x^2" y] by simp


108 


109 
lemma real_less_rsqrt: "x^2 < y \<Longrightarrow> x < sqrt y"


110 
using real_sqrt_less_mono[of "x^2" y] by simp


111 


112 
lemma sqrt_even_pow2: assumes n: "even n"


113 
shows "sqrt(2 ^ n) = 2 ^ (n div 2)"


114 
proof


115 
from n obtain m where m: "n = 2*m" unfolding even_mult_two_ex ..


116 
from m have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)"


117 
by (simp only: power_mult[symmetric] mult_commute)


118 
then show ?thesis using m by simp


119 
qed


120 


121 
lemma real_div_sqrt: "0 <= x ==> x / sqrt(x) = sqrt(x)"


122 
apply (cases "x = 0", simp_all)


123 
using sqrt_divide_self_eq[of x]


124 
apply (simp add: inverse_eq_divide field_simps)


125 
done


126 


127 
text{* Hence derive more interesting properties of the norm. *}


128 


129 
(* FIXME: same as norm_scaleR


130 
lemma norm_mul[simp]: "norm(a *\<^sub>R x) = abs(a) * norm x"


131 
by (simp add: norm_vector_def setL2_right_distrib abs_mult)


132 
*)


133 


134 
lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"


135 
by (simp add: setL2_def power2_eq_square)


136 


137 
lemma norm_cauchy_schwarz:


138 
shows "inner x y <= norm x * norm y"


139 
using Cauchy_Schwarz_ineq2[of x y] by auto


140 


141 
lemma norm_cauchy_schwarz_abs:


142 
shows "\<bar>inner x y\<bar> \<le> norm x * norm y"


143 
by (rule Cauchy_Schwarz_ineq2)


144 


145 
lemma norm_triangle_sub:


146 
fixes x y :: "'a::real_normed_vector"


147 
shows "norm x \<le> norm y + norm (x  y)"


148 
using norm_triangle_ineq[of "y" "x  y"] by (simp add: field_simps)


149 


150 
lemma real_abs_norm: "\<bar>norm x\<bar> = norm x"


151 
by (rule abs_norm_cancel)


152 
lemma real_abs_sub_norm: "\<bar>norm x  norm y\<bar> <= norm(x  y)"


153 
by (rule norm_triangle_ineq3)


154 
lemma norm_le: "norm(x) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"


155 
by (simp add: norm_eq_sqrt_inner)


156 
lemma norm_lt: "norm(x) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"


157 
by (simp add: norm_eq_sqrt_inner)


158 
lemma norm_eq: "norm(x) = norm (y) \<longleftrightarrow> x \<bullet> x = y \<bullet> y"


159 
apply(subst order_eq_iff) unfolding norm_le by auto


160 
lemma norm_eq_1: "norm(x) = 1 \<longleftrightarrow> x \<bullet> x = 1"


161 
unfolding norm_eq_sqrt_inner by auto


162 


163 
text{* Squaring equations and inequalities involving norms. *}


164 


165 
lemma dot_square_norm: "x \<bullet> x = norm(x)^2"


166 
by (simp add: norm_eq_sqrt_inner)


167 


168 
lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"


169 
by (auto simp add: norm_eq_sqrt_inner)


170 


171 
lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"


172 
proof


173 
assume "\<bar>x\<bar> \<le> \<bar>y\<bar>"


174 
then have "\<bar>x\<bar>\<twosuperior> \<le> \<bar>y\<bar>\<twosuperior>" by (rule power_mono, simp)


175 
then show "x\<twosuperior> \<le> y\<twosuperior>" by simp


176 
next


177 
assume "x\<twosuperior> \<le> y\<twosuperior>"


178 
then have "sqrt (x\<twosuperior>) \<le> sqrt (y\<twosuperior>)" by (rule real_sqrt_le_mono)


179 
then show "\<bar>x\<bar> \<le> \<bar>y\<bar>" by simp


180 
qed


181 


182 
lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2"


183 
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])


184 
using norm_ge_zero[of x]


185 
apply arith


186 
done


187 


188 
lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2"


189 
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])


190 
using norm_ge_zero[of x]


191 
apply arith


192 
done


193 


194 
lemma norm_lt_square: "norm(x) < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a^2"


195 
by (metis not_le norm_ge_square)


196 
lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a^2"


197 
by (metis norm_le_square not_less)


198 


199 
text{* Dot product in terms of the norm rather than conversely. *}


200 


201 
lemmas inner_simps = inner.add_left inner.add_right inner.diff_right inner.diff_left


202 
inner.scaleR_left inner.scaleR_right


203 


204 
lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2  norm x ^ 2  norm y ^ 2) / 2"


205 
unfolding power2_norm_eq_inner inner_simps inner_commute by auto


206 


207 
lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2)  norm(x  y) ^ 2) / 2"


208 
unfolding power2_norm_eq_inner inner_simps inner_commute by(auto simp add:algebra_simps)


209 


210 
text{* Equality of vectors in terms of @{term "op \<bullet>"} products. *}


211 


212 
lemma vector_eq: "x = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y \<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs")


213 
proof


214 
assume ?lhs then show ?rhs by simp


215 
next


216 
assume ?rhs


217 
then have "x \<bullet> x  x \<bullet> y = 0 \<and> x \<bullet> y  y \<bullet> y = 0" by simp


218 
hence "x \<bullet> (x  y) = 0 \<and> y \<bullet> (x  y) = 0" by (simp add: inner_simps inner_commute)


219 
then have "(x  y) \<bullet> (x  y) = 0" by (simp add: field_simps inner_simps inner_commute)


220 
then show "x = y" by (simp)


221 
qed


222 


223 
subsection{* General linear decision procedure for normed spaces. *}


224 


225 
lemma norm_cmul_rule_thm:


226 
fixes x :: "'a::real_normed_vector"


227 
shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"


228 
unfolding norm_scaleR


229 
apply (erule mult_left_mono)


230 
apply simp


231 
done


232 


233 
(* FIXME: Move all these theorems into the ML code using lemma antiquotation *)


234 
lemma norm_add_rule_thm:


235 
fixes x1 x2 :: "'a::real_normed_vector"


236 
shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"


237 
by (rule order_trans [OF norm_triangle_ineq add_mono])


238 


239 
lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a  b \<ge> 0"


240 
by (simp add: field_simps)


241 


242 
lemma pth_1:


243 
fixes x :: "'a::real_normed_vector"


244 
shows "x == scaleR 1 x" by simp


245 


246 
lemma pth_2:


247 
fixes x :: "'a::real_normed_vector"


248 
shows "x  y == x + y" by (atomize (full)) simp


249 


250 
lemma pth_3:


251 
fixes x :: "'a::real_normed_vector"


252 
shows " x == scaleR (1) x" by simp


253 


254 
lemma pth_4:


255 
fixes x :: "'a::real_normed_vector"


256 
shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all


257 


258 
lemma pth_5:


259 
fixes x :: "'a::real_normed_vector"


260 
shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp


261 


262 
lemma pth_6:


263 
fixes x :: "'a::real_normed_vector"


264 
shows "scaleR c (x + y) == scaleR c x + scaleR c y"


265 
by (simp add: scaleR_right_distrib)


266 


267 
lemma pth_7:


268 
fixes x :: "'a::real_normed_vector"


269 
shows "0 + x == x" and "x + 0 == x" by simp_all


270 


271 
lemma pth_8:


272 
fixes x :: "'a::real_normed_vector"


273 
shows "scaleR c x + scaleR d x == scaleR (c + d) x"


274 
by (simp add: scaleR_left_distrib)


275 


276 
lemma pth_9:


277 
fixes x :: "'a::real_normed_vector" shows


278 
"(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"


279 
"scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"


280 
"(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"


281 
by (simp_all add: algebra_simps)


282 


283 
lemma pth_a:


284 
fixes x :: "'a::real_normed_vector"


285 
shows "scaleR 0 x + y == y" by simp


286 


287 
lemma pth_b:


288 
fixes x :: "'a::real_normed_vector" shows


289 
"scaleR c x + scaleR d y == scaleR c x + scaleR d y"


290 
"(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"


291 
"scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"


292 
"(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"


293 
by (simp_all add: algebra_simps)


294 


295 
lemma pth_c:


296 
fixes x :: "'a::real_normed_vector" shows


297 
"scaleR c x + scaleR d y == scaleR d y + scaleR c x"


298 
"(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"


299 
"scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"


300 
"(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"


301 
by (simp_all add: algebra_simps)


302 


303 
lemma pth_d:


304 
fixes x :: "'a::real_normed_vector"


305 
shows "x + 0 == x" by simp


306 


307 
lemma norm_imp_pos_and_ge:


308 
fixes x :: "'a::real_normed_vector"


309 
shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"


310 
by atomize auto


311 


312 
lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> x \<ge> 0" by arith


313 


314 
lemma norm_pths:


315 
fixes x :: "'a::real_normed_vector" shows


316 
"x = y \<longleftrightarrow> norm (x  y) \<le> 0"


317 
"x \<noteq> y \<longleftrightarrow> \<not> (norm (x  y) \<le> 0)"


318 
using norm_ge_zero[of "x  y"] by auto


319 


320 
use "normarith.ML"


321 


322 
method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)


323 
*} "prove simple linear statements about vector norms"


324 


325 


326 
text{* Hence more metric properties. *}


327 


328 
lemma norm_triangle_half_r:


329 
shows "norm (y  x1) < e / 2 \<Longrightarrow> norm (y  x2) < e / 2 \<Longrightarrow> norm (x1  x2) < e"


330 
using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto


331 


332 
lemma norm_triangle_half_l: assumes "norm (x  y) < e / 2" "norm (x'  (y)) < e / 2"


333 
shows "norm (x  x') < e"


334 
using dist_triangle_half_l[OF assms[unfolded dist_norm[THEN sym]]]


335 
unfolding dist_norm[THEN sym] .


336 


337 
lemma norm_triangle_le: "norm(x) + norm y <= e ==> norm(x + y) <= e"


338 
by (metis order_trans norm_triangle_ineq)


339 


340 
lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e"


341 
by (metis basic_trans_rules(21) norm_triangle_ineq)


342 


343 
lemma dist_triangle_add:


344 
fixes x y x' y' :: "'a::real_normed_vector"


345 
shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"


346 
by norm


347 


348 
lemma dist_triangle_add_half:


349 
fixes x x' y y' :: "'a::real_normed_vector"


350 
shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"


351 
by norm


352 


353 
lemma setsum_clauses:


354 
shows "setsum f {} = 0"


355 
and "finite S \<Longrightarrow> setsum f (insert x S) =


356 
(if x \<in> S then setsum f S else f x + setsum f S)"


357 
by (auto simp add: insert_absorb)


358 


359 
lemma setsum_norm:


360 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"


361 
assumes fS: "finite S"


362 
shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"


363 
proof(induct rule: finite_induct[OF fS])


364 
case 1 thus ?case by simp


365 
next


366 
case (2 x S)


367 
from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq)


368 
also have "\<dots> \<le> norm (f x) + setsum (\<lambda>x. norm(f x)) S"


369 
using "2.hyps" by simp


370 
finally show ?case using "2.hyps" by simp


371 
qed


372 


373 
lemma setsum_norm_le:


374 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"


375 
assumes fS: "finite S"


376 
and fg: "\<forall>x \<in> S. norm (f x) \<le> g x"


377 
shows "norm (setsum f S) \<le> setsum g S"


378 
proof


379 
from fg have "setsum (\<lambda>x. norm(f x)) S <= setsum g S"


380 
by  (rule setsum_mono, simp)


381 
then show ?thesis using setsum_norm[OF fS, of f] fg


382 
by arith


383 
qed


384 


385 
lemma setsum_norm_bound:


386 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"


387 
assumes fS: "finite S"


388 
and K: "\<forall>x \<in> S. norm (f x) \<le> K"


389 
shows "norm (setsum f S) \<le> of_nat (card S) * K"


390 
using setsum_norm_le[OF fS K] setsum_constant[symmetric]


391 
by simp


392 


393 
lemma setsum_group:


394 
assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"


395 
shows "setsum (\<lambda>y. setsum g {x. x\<in> S \<and> f x = y}) T = setsum g S"


396 
apply (subst setsum_image_gen[OF fS, of g f])


397 
apply (rule setsum_mono_zero_right[OF fT fST])


398 
by (auto intro: setsum_0')


399 


400 
lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> y = setsum (\<lambda>x. f x \<bullet> y) S "


401 
apply(induct rule: finite_induct) by(auto simp add: inner_simps)


402 


403 
lemma dot_rsum: "finite S \<Longrightarrow> y \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "


404 
apply(induct rule: finite_induct) by(auto simp add: inner_simps)


405 


406 
lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"


407 
proof


408 
assume "\<forall>x. x \<bullet> y = x \<bullet> z"


409 
hence "\<forall>x. x \<bullet> (y  z) = 0" by (simp add: inner_simps)


410 
hence "(y  z) \<bullet> (y  z) = 0" ..


411 
thus "y = z" by simp


412 
qed simp


413 


414 
lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = y"


415 
proof


416 
assume "\<forall>z. x \<bullet> z = y \<bullet> z"


417 
hence "\<forall>z. (x  y) \<bullet> z = 0" by (simp add: inner_simps)


418 
hence "(x  y) \<bullet> (x  y) = 0" ..


419 
thus "x = y" by simp


420 
qed simp


421 


422 
subsection{* Orthogonality. *}


423 


424 
context real_inner


425 
begin


426 


427 
definition "orthogonal x y \<longleftrightarrow> (x \<bullet> y = 0)"


428 


429 
lemma orthogonal_clauses:


430 
"orthogonal a 0"


431 
"orthogonal a x \<Longrightarrow> orthogonal a (c *\<^sub>R x)"


432 
"orthogonal a x \<Longrightarrow> orthogonal a (x)"


433 
"orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x + y)"


434 
"orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x  y)"


435 
"orthogonal 0 a"


436 
"orthogonal x a \<Longrightarrow> orthogonal (c *\<^sub>R x) a"


437 
"orthogonal x a \<Longrightarrow> orthogonal (x) a"


438 
"orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"


439 
"orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x  y) a"


440 
unfolding orthogonal_def inner_simps inner_add_left inner_add_right inner_diff_left inner_diff_right (*FIXME*) by auto


441 


442 
end


443 


444 
lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"


445 
by (simp add: orthogonal_def inner_commute)


446 


447 
subsection{* Linear functions. *}


448 


449 
definition


450 
linear :: "('a::real_vector \<Rightarrow> 'b::real_vector) \<Rightarrow> bool" where


451 
"linear f \<longleftrightarrow> (\<forall>x y. f(x + y) = f x + f y) \<and> (\<forall>c x. f(c *\<^sub>R x) = c *\<^sub>R f x)"


452 


453 
lemma linearI: assumes "\<And>x y. f (x + y) = f x + f y" "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"


454 
shows "linear f" using assms unfolding linear_def by auto


455 


456 
lemma linear_compose_cmul: "linear f ==> linear (\<lambda>x. c *\<^sub>R f x)"


457 
by (simp add: linear_def algebra_simps)


458 


459 
lemma linear_compose_neg: "linear f ==> linear (\<lambda>x. (f(x)))"


460 
by (simp add: linear_def)


461 


462 
lemma linear_compose_add: "linear f \<Longrightarrow> linear g ==> linear (\<lambda>x. f(x) + g(x))"


463 
by (simp add: linear_def algebra_simps)


464 


465 
lemma linear_compose_sub: "linear f \<Longrightarrow> linear g ==> linear (\<lambda>x. f x  g x)"


466 
by (simp add: linear_def algebra_simps)


467 


468 
lemma linear_compose: "linear f \<Longrightarrow> linear g ==> linear (g o f)"


469 
by (simp add: linear_def)


470 


471 
lemma linear_id: "linear id" by (simp add: linear_def id_def)


472 


473 
lemma linear_zero: "linear (\<lambda>x. 0)" by (simp add: linear_def)


474 


475 
lemma linear_compose_setsum:


476 
assumes fS: "finite S" and lS: "\<forall>a \<in> S. linear (f a)"


477 
shows "linear(\<lambda>x. setsum (\<lambda>a. f a x) S)"


478 
using lS


479 
apply (induct rule: finite_induct[OF fS])


480 
by (auto simp add: linear_zero intro: linear_compose_add)


481 


482 
lemma linear_0: "linear f \<Longrightarrow> f 0 = 0"


483 
unfolding linear_def


484 
apply clarsimp


485 
apply (erule allE[where x="0::'a"])


486 
apply simp


487 
done


488 


489 
lemma linear_cmul: "linear f ==> f(c *\<^sub>R x) = c *\<^sub>R f x" by (simp add: linear_def)


490 


491 
lemma linear_neg: "linear f ==> f (x) =  f x"


492 
using linear_cmul [where c="1"] by simp


493 


494 
lemma linear_add: "linear f ==> f(x + y) = f x + f y" by (metis linear_def)


495 


496 
lemma linear_sub: "linear f ==> f(x  y) = f x  f y"


497 
by (simp add: diff_minus linear_add linear_neg)


498 


499 
lemma linear_setsum:


500 
assumes lf: "linear f" and fS: "finite S"


501 
shows "f (setsum g S) = setsum (f o g) S"


502 
proof (induct rule: finite_induct[OF fS])


503 
case 1 thus ?case by (simp add: linear_0[OF lf])


504 
next


505 
case (2 x F)


506 
have "f (setsum g (insert x F)) = f (g x + setsum g F)" using "2.hyps"


507 
by simp


508 
also have "\<dots> = f (g x) + f (setsum g F)" using linear_add[OF lf] by simp


509 
also have "\<dots> = setsum (f o g) (insert x F)" using "2.hyps" by simp


510 
finally show ?case .


511 
qed


512 


513 
lemma linear_setsum_mul:


514 
assumes lf: "linear f" and fS: "finite S"


515 
shows "f (setsum (\<lambda>i. c i *\<^sub>R v i) S) = setsum (\<lambda>i. c i *\<^sub>R f (v i)) S"


516 
using linear_setsum[OF lf fS, of "\<lambda>i. c i *\<^sub>R v i" , unfolded o_def]


517 
linear_cmul[OF lf] by simp


518 


519 
lemma linear_injective_0:


520 
assumes lf: "linear f"


521 
shows "inj f \<longleftrightarrow> (\<forall>x. f x = 0 \<longrightarrow> x = 0)"


522 
proof


523 
have "inj f \<longleftrightarrow> (\<forall> x y. f x = f y \<longrightarrow> x = y)" by (simp add: inj_on_def)


524 
also have "\<dots> \<longleftrightarrow> (\<forall> x y. f x  f y = 0 \<longrightarrow> x  y = 0)" by simp


525 
also have "\<dots> \<longleftrightarrow> (\<forall> x y. f (x  y) = 0 \<longrightarrow> x  y = 0)"


526 
by (simp add: linear_sub[OF lf])


527 
also have "\<dots> \<longleftrightarrow> (\<forall> x. f x = 0 \<longrightarrow> x = 0)" by auto


528 
finally show ?thesis .


529 
qed


530 


531 
subsection{* Bilinear functions. *}


532 


533 
definition "bilinear f \<longleftrightarrow> (\<forall>x. linear(\<lambda>y. f x y)) \<and> (\<forall>y. linear(\<lambda>x. f x y))"


534 


535 
lemma bilinear_ladd: "bilinear h ==> h (x + y) z = (h x z) + (h y z)"


536 
by (simp add: bilinear_def linear_def)


537 
lemma bilinear_radd: "bilinear h ==> h x (y + z) = (h x y) + (h x z)"


538 
by (simp add: bilinear_def linear_def)


539 


540 
lemma bilinear_lmul: "bilinear h ==> h (c *\<^sub>R x) y = c *\<^sub>R (h x y)"


541 
by (simp add: bilinear_def linear_def)


542 


543 
lemma bilinear_rmul: "bilinear h ==> h x (c *\<^sub>R y) = c *\<^sub>R (h x y)"


544 
by (simp add: bilinear_def linear_def)


545 


546 
lemma bilinear_lneg: "bilinear h ==> h ( x) y = (h x y)"


547 
by (simp only: scaleR_minus1_left [symmetric] bilinear_lmul)


548 


549 
lemma bilinear_rneg: "bilinear h ==> h x ( y) =  h x y"


550 
by (simp only: scaleR_minus1_left [symmetric] bilinear_rmul)


551 


552 
lemma (in ab_group_add) eq_add_iff: "x = x + y \<longleftrightarrow> y = 0"


553 
using add_imp_eq[of x y 0] by auto


554 


555 
lemma bilinear_lzero:


556 
assumes bh: "bilinear h" shows "h 0 x = 0"


557 
using bilinear_ladd[OF bh, of 0 0 x]


558 
by (simp add: eq_add_iff field_simps)


559 


560 
lemma bilinear_rzero:


561 
assumes bh: "bilinear h" shows "h x 0 = 0"


562 
using bilinear_radd[OF bh, of x 0 0 ]


563 
by (simp add: eq_add_iff field_simps)


564 


565 
lemma bilinear_lsub: "bilinear h ==> h (x  y) z = h x z  h y z"


566 
by (simp add: diff_minus bilinear_ladd bilinear_lneg)


567 


568 
lemma bilinear_rsub: "bilinear h ==> h z (x  y) = h z x  h z y"


569 
by (simp add: diff_minus bilinear_radd bilinear_rneg)


570 


571 
lemma bilinear_setsum:


572 
assumes bh: "bilinear h" and fS: "finite S" and fT: "finite T"


573 
shows "h (setsum f S) (setsum g T) = setsum (\<lambda>(i,j). h (f i) (g j)) (S \<times> T) "


574 
proof


575 
have "h (setsum f S) (setsum g T) = setsum (\<lambda>x. h (f x) (setsum g T)) S"


576 
apply (rule linear_setsum[unfolded o_def])


577 
using bh fS by (auto simp add: bilinear_def)


578 
also have "\<dots> = setsum (\<lambda>x. setsum (\<lambda>y. h (f x) (g y)) T) S"


579 
apply (rule setsum_cong, simp)


580 
apply (rule linear_setsum[unfolded o_def])


581 
using bh fT by (auto simp add: bilinear_def)


582 
finally show ?thesis unfolding setsum_cartesian_product .


583 
qed


584 


585 
subsection{* Adjoints. *}


586 


587 
definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"


588 


589 
lemma adjoint_unique:


590 
assumes "\<forall>x y. inner (f x) y = inner x (g y)"


591 
shows "adjoint f = g"


592 
unfolding adjoint_def


593 
proof (rule some_equality)


594 
show "\<forall>x y. inner (f x) y = inner x (g y)" using assms .


595 
next


596 
fix h assume "\<forall>x y. inner (f x) y = inner x (h y)"


597 
hence "\<forall>x y. inner x (g y) = inner x (h y)" using assms by simp


598 
hence "\<forall>x y. inner x (g y  h y) = 0" by (simp add: inner_diff_right)


599 
hence "\<forall>y. inner (g y  h y) (g y  h y) = 0" by simp


600 
hence "\<forall>y. h y = g y" by simp


601 
thus "h = g" by (simp add: ext)


602 
qed


603 


604 
lemma choice_iff: "(\<forall>x. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x. P x (f x))" by metis


605 


606 
subsection{* Interlude: Some properties of real sets *}


607 


608 
lemma seq_mono_lemma: assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n" and "\<forall>n \<ge> m. e n <= e m"


609 
shows "\<forall>n \<ge> m. d n < e m"


610 
using assms apply auto


611 
apply (erule_tac x="n" in allE)


612 
apply (erule_tac x="n" in allE)


613 
apply auto


614 
done


615 


616 


617 
lemma infinite_enumerate: assumes fS: "infinite S"


618 
shows "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> S)"


619 
unfolding subseq_def


620 
using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto


621 


622 
lemma approachable_lt_le: "(\<exists>(d::real)>0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)"


623 
apply auto


624 
apply (rule_tac x="d/2" in exI)


625 
apply auto


626 
done


627 


628 


629 
lemma triangle_lemma:


630 
assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x^2 <= y^2 + z^2"


631 
shows "x <= y + z"


632 
proof


633 
have "y^2 + z^2 \<le> y^2 + 2*y*z + z^2" using z y by (simp add: mult_nonneg_nonneg)


634 
with xy have th: "x ^2 \<le> (y+z)^2" by (simp add: power2_eq_square field_simps)


635 
from y z have yz: "y + z \<ge> 0" by arith


636 
from power2_le_imp_le[OF th yz] show ?thesis .


637 
qed


638 


639 
text {* TODO: move to NthRoot *}


640 
lemma sqrt_add_le_add_sqrt:


641 
assumes x: "0 \<le> x" and y: "0 \<le> y"


642 
shows "sqrt (x + y) \<le> sqrt x + sqrt y"


643 
apply (rule power2_le_imp_le)


644 
apply (simp add: real_sum_squared_expand add_nonneg_nonneg x y)


645 
apply (simp add: mult_nonneg_nonneg x y)


646 
apply (simp add: add_nonneg_nonneg x y)


647 
done


648 


649 
subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *}


650 


651 
definition hull :: "'a set set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75) where


652 
"S hull s = Inter {t. t \<in> S \<and> s \<subseteq> t}"


653 


654 
lemma hull_same: "s \<in> S \<Longrightarrow> S hull s = s"


655 
unfolding hull_def by auto


656 


657 
lemma hull_in: "(\<And>T. T \<subseteq> S ==> Inter T \<in> S) ==> (S hull s) \<in> S"


658 
unfolding hull_def subset_iff by auto


659 


660 
lemma hull_eq: "(\<And>T. T \<subseteq> S ==> Inter T \<in> S) ==> (S hull s) = s \<longleftrightarrow> s \<in> S"


661 
using hull_same[of s S] hull_in[of S s] by metis


662 


663 


664 
lemma hull_hull: "S hull (S hull s) = S hull s"


665 
unfolding hull_def by blast


666 


667 
lemma hull_subset[intro]: "s \<subseteq> (S hull s)"


668 
unfolding hull_def by blast


669 


670 
lemma hull_mono: " s \<subseteq> t ==> (S hull s) \<subseteq> (S hull t)"


671 
unfolding hull_def by blast


672 


673 
lemma hull_antimono: "S \<subseteq> T ==> (T hull s) \<subseteq> (S hull s)"


674 
unfolding hull_def by blast


675 


676 
lemma hull_minimal: "s \<subseteq> t \<Longrightarrow> t \<in> S ==> (S hull s) \<subseteq> t"


677 
unfolding hull_def by blast


678 


679 
lemma subset_hull: "t \<in> S ==> S hull s \<subseteq> t \<longleftrightarrow> s \<subseteq> t"


680 
unfolding hull_def by blast


681 


682 
lemma hull_unique: "s \<subseteq> t \<Longrightarrow> t \<in> S \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> t' \<in> S ==> t \<subseteq> t')


683 
==> (S hull s = t)"


684 
unfolding hull_def by auto


685 


686 
lemma hull_induct: "(\<And>x. x\<in> S \<Longrightarrow> P x) \<Longrightarrow> Q {x. P x} \<Longrightarrow> \<forall>x\<in> Q hull S. P x"


687 
using hull_minimal[of S "{x. P x}" Q]


688 
by (auto simp add: subset_eq Collect_def mem_def)


689 


690 
lemma hull_inc: "x \<in> S \<Longrightarrow> x \<in> P hull S" by (metis hull_subset subset_eq)


691 


692 
lemma hull_union_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))"


693 
unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2)


694 


695 
lemma hull_union: assumes T: "\<And>T. T \<subseteq> S ==> Inter T \<in> S"


696 
shows "S hull (s \<union> t) = S hull (S hull s \<union> S hull t)"


697 
apply rule


698 
apply (rule hull_mono)


699 
unfolding Un_subset_iff


700 
apply (metis hull_subset Un_upper1 Un_upper2 subset_trans)


701 
apply (rule hull_minimal)


702 
apply (metis hull_union_subset)


703 
apply (metis hull_in T)


704 
done


705 


706 
lemma hull_redundant_eq: "a \<in> (S hull s) \<longleftrightarrow> (S hull (insert a s) = S hull s)"


707 
unfolding hull_def by blast


708 


709 
lemma hull_redundant: "a \<in> (S hull s) ==> (S hull (insert a s) = S hull s)"


710 
by (metis hull_redundant_eq)


711 


712 
text{* Archimedian properties and useful consequences. *}


713 


714 
lemma real_arch_simple: "\<exists>n. x <= real (n::nat)"


715 
using reals_Archimedean2[of x] apply auto by (rule_tac x="Suc n" in exI, auto)


716 
lemmas real_arch_lt = reals_Archimedean2


717 


718 
lemmas real_arch = reals_Archimedean3


719 


720 
lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"


721 
using reals_Archimedean


722 
apply (auto simp add: field_simps)


723 
apply (subgoal_tac "inverse (real n) > 0")


724 
apply arith


725 
apply simp


726 
done


727 


728 
lemma real_pow_lbound: "0 <= x ==> 1 + real n * x <= (1 + x) ^ n"


729 
proof(induct n)


730 
case 0 thus ?case by simp


731 
next


732 
case (Suc n)


733 
hence h: "1 + real n * x \<le> (1 + x) ^ n" by simp


734 
from h have p: "1 \<le> (1 + x) ^ n" using Suc.prems by simp


735 
from h have "1 + real n * x + x \<le> (1 + x) ^ n + x" by simp


736 
also have "\<dots> \<le> (1 + x) ^ Suc n" apply (subst diff_le_0_iff_le[symmetric])


737 
apply (simp add: field_simps)


738 
using mult_left_mono[OF p Suc.prems] by simp


739 
finally show ?case by (simp add: real_of_nat_Suc field_simps)


740 
qed


741 


742 
lemma real_arch_pow: assumes x: "1 < (x::real)" shows "\<exists>n. y < x^n"


743 
proof


744 
from x have x0: "x  1 > 0" by arith


745 
from real_arch[OF x0, rule_format, of y]


746 
obtain n::nat where n:"y < real n * (x  1)" by metis


747 
from x0 have x00: "x 1 \<ge> 0" by arith


748 
from real_pow_lbound[OF x00, of n] n


749 
have "y < x^n" by auto


750 
then show ?thesis by metis


751 
qed


752 


753 
lemma real_arch_pow2: "\<exists>n. (x::real) < 2^ n"


754 
using real_arch_pow[of 2 x] by simp


755 


756 
lemma real_arch_pow_inv: assumes y: "(y::real) > 0" and x1: "x < 1"


757 
shows "\<exists>n. x^n < y"


758 
proof


759 
{assume x0: "x > 0"


760 
from x0 x1 have ix: "1 < 1/x" by (simp add: field_simps)


761 
from real_arch_pow[OF ix, of "1/y"]


762 
obtain n where n: "1/y < (1/x)^n" by blast


763 
then


764 
have ?thesis using y x0 by (auto simp add: field_simps power_divide) }


765 
moreover


766 
{assume "\<not> x > 0" with y x1 have ?thesis apply auto by (rule exI[where x=1], auto)}


767 
ultimately show ?thesis by metis


768 
qed


769 


770 
lemma forall_pos_mono: "(\<And>d e::real. d < e \<Longrightarrow> P d ==> P e) \<Longrightarrow> (\<And>n::nat. n \<noteq> 0 ==> P(inverse(real n))) \<Longrightarrow> (\<And>e. 0 < e ==> P e)"


771 
by (metis real_arch_inv)


772 


773 
lemma forall_pos_mono_1: "(\<And>d e::real. d < e \<Longrightarrow> P d ==> P e) \<Longrightarrow> (\<And>n. P(inverse(real (Suc n)))) ==> 0 < e ==> P e"


774 
apply (rule forall_pos_mono)


775 
apply auto


776 
apply (atomize)


777 
apply (erule_tac x="n  1" in allE)


778 
apply auto


779 
done


780 


781 
lemma real_archimedian_rdiv_eq_0: assumes x0: "x \<ge> 0" and c: "c \<ge> 0" and xc: "\<forall>(m::nat)>0. real m * x \<le> c"


782 
shows "x = 0"


783 
proof


784 
{assume "x \<noteq> 0" with x0 have xp: "x > 0" by arith


785 
from real_arch[OF xp, rule_format, of c] obtain n::nat where n: "c < real n * x" by blast


786 
with xc[rule_format, of n] have "n = 0" by arith


787 
with n c have False by simp}


788 
then show ?thesis by blast


789 
qed


790 


791 
subsection {* Geometric progression *}


792 


793 
lemma sum_gp_basic: "((1::'a::{field})  x) * setsum (\<lambda>i. x^i) {0 .. n} = (1  x^(Suc n))"


794 
(is "?lhs = ?rhs")


795 
proof


796 
{assume x1: "x = 1" hence ?thesis by simp}


797 
moreover


798 
{assume x1: "x\<noteq>1"


799 
hence x1': "x  1 \<noteq> 0" "1  x \<noteq> 0" "x  1 =  (1  x)" " (1  x) \<noteq> 0" by auto


800 
from geometric_sum[OF x1, of "Suc n", unfolded x1']


801 
have "( (1  x)) * setsum (\<lambda>i. x^i) {0 .. n} =  (1  x^(Suc n))"


802 
unfolding atLeastLessThanSuc_atLeastAtMost


803 
using x1' apply (auto simp only: field_simps)


804 
apply (simp add: field_simps)


805 
done


806 
then have ?thesis by (simp add: field_simps) }


807 
ultimately show ?thesis by metis


808 
qed


809 


810 
lemma sum_gp_multiplied: assumes mn: "m <= n"


811 
shows "((1::'a::{field})  x) * setsum (op ^ x) {m..n} = x^m  x^ Suc n"


812 
(is "?lhs = ?rhs")


813 
proof


814 
let ?S = "{0..(n  m)}"


815 
from mn have mn': "n  m \<ge> 0" by arith


816 
let ?f = "op + m"


817 
have i: "inj_on ?f ?S" unfolding inj_on_def by auto


818 
have f: "?f ` ?S = {m..n}"


819 
using mn apply (auto simp add: image_iff Bex_def) by arith


820 
have th: "op ^ x o op + m = (\<lambda>i. x^m * x^i)"


821 
by (rule ext, simp add: power_add power_mult)


822 
from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]]


823 
have "?lhs = x^m * ((1  x) * setsum (op ^ x) {0..n  m})" by simp


824 
then show ?thesis unfolding sum_gp_basic using mn


825 
by (simp add: field_simps power_add[symmetric])


826 
qed


827 


828 
lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =


829 
(if n < m then 0 else if x = 1 then of_nat ((n + 1)  m)


830 
else (x^ m  x^ (Suc n)) / (1  x))"


831 
proof


832 
{assume nm: "n < m" hence ?thesis by simp}


833 
moreover


834 
{assume "\<not> n < m" hence nm: "m \<le> n" by arith


835 
{assume x: "x = 1" hence ?thesis by simp}


836 
moreover


837 
{assume x: "x \<noteq> 1" hence nz: "1  x \<noteq> 0" by simp


838 
from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}


839 
ultimately have ?thesis by metis


840 
}


841 
ultimately show ?thesis by metis


842 
qed


843 


844 
lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =


845 
(if x = 1 then of_nat n + 1 else x^m * (1  x^Suc n) / (1  x))"


846 
unfolding sum_gp[of x m "m + n"] power_Suc


847 
by (simp add: field_simps power_add)


848 


849 


850 
subsection{* A bit of linear algebra. *}


851 


852 
definition (in real_vector)


853 
subspace :: "'a set \<Rightarrow> bool" where


854 
"subspace S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>x\<in> S. \<forall>y \<in>S. x + y \<in> S) \<and> (\<forall>c. \<forall>x \<in>S. c *\<^sub>R x \<in>S )"


855 


856 
definition (in real_vector) "span S = (subspace hull S)"


857 
definition (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span(S  {a}))"


858 
abbreviation (in real_vector) "independent s == ~(dependent s)"


859 


860 
text {* Closure properties of subspaces. *}


861 


862 
lemma subspace_UNIV[simp]: "subspace(UNIV)" by (simp add: subspace_def)


863 


864 
lemma (in real_vector) subspace_0: "subspace S ==> 0 \<in> S" by (metis subspace_def)


865 


866 
lemma (in real_vector) subspace_add: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S ==> x + y \<in> S"


867 
by (metis subspace_def)


868 


869 
lemma (in real_vector) subspace_mul: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> c *\<^sub>R x \<in> S"


870 
by (metis subspace_def)


871 


872 
lemma subspace_neg: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow>  x \<in> S"


873 
by (metis scaleR_minus1_left subspace_mul)


874 


875 
lemma subspace_sub: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x  y \<in> S"


876 
by (metis diff_minus subspace_add subspace_neg)


877 


878 
lemma (in real_vector) subspace_setsum:


879 
assumes sA: "subspace A" and fB: "finite B"


880 
and f: "\<forall>x\<in> B. f x \<in> A"


881 
shows "setsum f B \<in> A"


882 
using fB f sA


883 
apply(induct rule: finite_induct[OF fB])


884 
by (simp add: subspace_def sA, auto simp add: sA subspace_add)


885 


886 
lemma subspace_linear_image:


887 
assumes lf: "linear f" and sS: "subspace S"


888 
shows "subspace(f ` S)"


889 
using lf sS linear_0[OF lf]


890 
unfolding linear_def subspace_def


891 
apply (auto simp add: image_iff)


892 
apply (rule_tac x="x + y" in bexI, auto)


893 
apply (rule_tac x="c *\<^sub>R x" in bexI, auto)


894 
done


895 


896 
lemma subspace_linear_preimage: "linear f ==> subspace S ==> subspace {x. f x \<in> S}"


897 
by (auto simp add: subspace_def linear_def linear_0[of f])


898 


899 
lemma subspace_trivial: "subspace {0}"


900 
by (simp add: subspace_def)


901 


902 
lemma (in real_vector) subspace_inter: "subspace A \<Longrightarrow> subspace B ==> subspace (A \<inter> B)"


903 
by (simp add: subspace_def)


904 


905 
lemma (in real_vector) span_mono: "A \<subseteq> B ==> span A \<subseteq> span B"


906 
by (metis span_def hull_mono)


907 


908 
lemma (in real_vector) subspace_span: "subspace(span S)"


909 
unfolding span_def


910 
apply (rule hull_in[unfolded mem_def])


911 
apply (simp only: subspace_def Inter_iff Int_iff subset_eq)


912 
apply auto


913 
apply (erule_tac x="X" in ballE)


914 
apply (simp add: mem_def)


915 
apply blast


916 
apply (erule_tac x="X" in ballE)


917 
apply (erule_tac x="X" in ballE)


918 
apply (erule_tac x="X" in ballE)


919 
apply (clarsimp simp add: mem_def)


920 
apply simp


921 
apply simp


922 
apply simp


923 
apply (erule_tac x="X" in ballE)


924 
apply (erule_tac x="X" in ballE)


925 
apply (simp add: mem_def)


926 
apply simp


927 
apply simp


928 
done


929 


930 
lemma (in real_vector) span_clauses:


931 
"a \<in> S ==> a \<in> span S"


932 
"0 \<in> span S"


933 
"x\<in> span S \<Longrightarrow> y \<in> span S ==> x + y \<in> span S"


934 
"x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S"


935 
by (metis span_def hull_subset subset_eq)


936 
(metis subspace_span subspace_def)+


937 


938 
lemma (in real_vector) span_induct: assumes SP: "\<And>x. x \<in> S ==> P x"


939 
and P: "subspace P" and x: "x \<in> span S" shows "P x"


940 
proof


941 
from SP have SP': "S \<subseteq> P" by (simp add: mem_def subset_eq)


942 
from P have P': "P \<in> subspace" by (simp add: mem_def)


943 
from x hull_minimal[OF SP' P', unfolded span_def[symmetric]]


944 
show "P x" by (metis mem_def subset_eq)


945 
qed


946 


947 
lemma span_empty[simp]: "span {} = {0}"


948 
apply (simp add: span_def)


949 
apply (rule hull_unique)


950 
apply (auto simp add: mem_def subspace_def)


951 
unfolding mem_def[of "0::'a", symmetric]


952 
apply simp


953 
done


954 


955 
lemma (in real_vector) independent_empty[intro]: "independent {}"


956 
by (simp add: dependent_def)


957 


958 
lemma dependent_single[simp]:


959 
"dependent {x} \<longleftrightarrow> x = 0"


960 
unfolding dependent_def by auto


961 


962 
lemma (in real_vector) independent_mono: "independent A \<Longrightarrow> B \<subseteq> A ==> independent B"


963 
apply (clarsimp simp add: dependent_def span_mono)


964 
apply (subgoal_tac "span (B  {a}) \<le> span (A  {a})")


965 
apply force


966 
apply (rule span_mono)


967 
apply auto


968 
done


969 


970 
lemma (in real_vector) span_subspace: "A \<subseteq> B \<Longrightarrow> B \<le> span A \<Longrightarrow> subspace B \<Longrightarrow> span A = B"


971 
by (metis order_antisym span_def hull_minimal mem_def)


972 


973 
lemma (in real_vector) span_induct': assumes SP: "\<forall>x \<in> S. P x"


974 
and P: "subspace P" shows "\<forall>x \<in> span S. P x"


975 
using span_induct SP P by blast


976 


977 
inductive (in real_vector) span_induct_alt_help for S:: "'a \<Rightarrow> bool"


978 
where


979 
span_induct_alt_help_0: "span_induct_alt_help S 0"


980 
 span_induct_alt_help_S: "x \<in> S \<Longrightarrow> span_induct_alt_help S z \<Longrightarrow> span_induct_alt_help S (c *\<^sub>R x + z)"


981 


982 
lemma span_induct_alt':


983 
assumes h0: "h 0" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)" shows "\<forall>x \<in> span S. h x"


984 
proof


985 
{fix x:: "'a" assume x: "span_induct_alt_help S x"


986 
have "h x"


987 
apply (rule span_induct_alt_help.induct[OF x])


988 
apply (rule h0)


989 
apply (rule hS, assumption, assumption)


990 
done}


991 
note th0 = this


992 
{fix x assume x: "x \<in> span S"


993 


994 
have "span_induct_alt_help S x"


995 
proof(rule span_induct[where x=x and S=S])


996 
show "x \<in> span S" using x .


997 
next


998 
fix x assume xS : "x \<in> S"


999 
from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1]


1000 
show "span_induct_alt_help S x" by simp


1001 
next


1002 
have "span_induct_alt_help S 0" by (rule span_induct_alt_help_0)


1003 
moreover


1004 
{fix x y assume h: "span_induct_alt_help S x" "span_induct_alt_help S y"


1005 
from h


1006 
have "span_induct_alt_help S (x + y)"


1007 
apply (induct rule: span_induct_alt_help.induct)


1008 
apply simp


1009 
unfolding add_assoc


1010 
apply (rule span_induct_alt_help_S)


1011 
apply assumption


1012 
apply simp


1013 
done}


1014 
moreover


1015 
{fix c x assume xt: "span_induct_alt_help S x"


1016 
then have "span_induct_alt_help S (c *\<^sub>R x)"


1017 
apply (induct rule: span_induct_alt_help.induct)


1018 
apply (simp add: span_induct_alt_help_0)


1019 
apply (simp add: scaleR_right_distrib)


1020 
apply (rule span_induct_alt_help_S)


1021 
apply assumption


1022 
apply simp


1023 
done


1024 
}


1025 
ultimately show "subspace (span_induct_alt_help S)"


1026 
unfolding subspace_def mem_def Ball_def by blast


1027 
qed}


1028 
with th0 show ?thesis by blast


1029 
qed


1030 


1031 
lemma span_induct_alt:


1032 
assumes h0: "h 0" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)" and x: "x \<in> span S"


1033 
shows "h x"


1034 
using span_induct_alt'[of h S] h0 hS x by blast


1035 


1036 
text {* Individual closure properties. *}


1037 


1038 
lemma span_span: "span (span A) = span A"


1039 
unfolding span_def hull_hull ..


1040 


1041 
lemma (in real_vector) span_superset: "x \<in> S ==> x \<in> span S" by (metis span_clauses(1))


1042 


1043 
lemma (in real_vector) span_0: "0 \<in> span S" by (metis subspace_span subspace_0)


1044 


1045 
lemma span_inc: "S \<subseteq> span S"


1046 
by (metis subset_eq span_superset)


1047 


1048 
lemma (in real_vector) dependent_0: assumes "0\<in>A" shows "dependent A"


1049 
unfolding dependent_def apply(rule_tac x=0 in bexI)


1050 
using assms span_0 by auto


1051 


1052 
lemma (in real_vector) span_add: "x \<in> span S \<Longrightarrow> y \<in> span S ==> x + y \<in> span S"


1053 
by (metis subspace_add subspace_span)


1054 


1055 
lemma (in real_vector) span_mul: "x \<in> span S ==> (c *\<^sub>R x) \<in> span S"


1056 
by (metis subspace_span subspace_mul)


1057 


1058 
lemma span_neg: "x \<in> span S ==>  x \<in> span S"


1059 
by (metis subspace_neg subspace_span)


1060 


1061 
lemma span_sub: "x \<in> span S \<Longrightarrow> y \<in> span S ==> x  y \<in> span S"


1062 
by (metis subspace_span subspace_sub)


1063 


1064 
lemma (in real_vector) span_setsum: "finite A \<Longrightarrow> \<forall>x \<in> A. f x \<in> span S ==> setsum f A \<in> span S"


1065 
by (rule subspace_setsum, rule subspace_span)


1066 


1067 
lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"


1068 
apply (auto simp only: span_add span_sub)


1069 
apply (subgoal_tac "(x + y)  x \<in> span S", simp)


1070 
by (simp only: span_add span_sub)


1071 


1072 
text {* Mapping under linear image. *}


1073 


1074 
lemma span_linear_image: assumes lf: "linear f"


1075 
shows "span (f ` S) = f ` (span S)"


1076 
proof


1077 
{fix x


1078 
assume x: "x \<in> span (f ` S)"


1079 
have "x \<in> f ` span S"


1080 
apply (rule span_induct[where x=x and S = "f ` S"])


1081 
apply (clarsimp simp add: image_iff)


1082 
apply (frule span_superset)


1083 
apply blast


1084 
apply (simp only: mem_def)


1085 
apply (rule subspace_linear_image[OF lf])


1086 
apply (rule subspace_span)


1087 
apply (rule x)


1088 
done}


1089 
moreover


1090 
{fix x assume x: "x \<in> span S"


1091 
have th0:"(\<lambda>a. f a \<in> span (f ` S)) = {x. f x \<in> span (f ` S)}" apply (rule set_eqI)


1092 
unfolding mem_def Collect_def ..


1093 
have "f x \<in> span (f ` S)"


1094 
apply (rule span_induct[where S=S])


1095 
apply (rule span_superset)


1096 
apply simp


1097 
apply (subst th0)


1098 
apply (rule subspace_linear_preimage[OF lf subspace_span, of "f ` S"])


1099 
apply (rule x)


1100 
done}


1101 
ultimately show ?thesis by blast


1102 
qed


1103 


1104 
text {* The key breakdown property. *}


1105 


1106 
lemma span_breakdown:


1107 
assumes bS: "b \<in> S" and aS: "a \<in> span S"


1108 
shows "\<exists>k. a  k *\<^sub>R b \<in> span (S  {b})" (is "?P a")


1109 
proof


1110 
{fix x assume xS: "x \<in> S"


1111 
{assume ab: "x = b"


1112 
then have "?P x"


1113 
apply simp


1114 
apply (rule exI[where x="1"], simp)


1115 
by (rule span_0)}


1116 
moreover


1117 
{assume ab: "x \<noteq> b"


1118 
then have "?P x" using xS


1119 
apply 


1120 
apply (rule exI[where x=0])


1121 
apply (rule span_superset)


1122 
by simp}


1123 
ultimately have "?P x" by blast}


1124 
moreover have "subspace ?P"


1125 
unfolding subspace_def


1126 
apply auto


1127 
apply (simp add: mem_def)


1128 
apply (rule exI[where x=0])


1129 
using span_0[of "S  {b}"]


1130 
apply (simp add: mem_def)


1131 
apply (clarsimp simp add: mem_def)


1132 
apply (rule_tac x="k + ka" in exI)


1133 
apply (subgoal_tac "x + y  (k + ka) *\<^sub>R b = (x  k*\<^sub>R b) + (y  ka *\<^sub>R b)")


1134 
apply (simp only: )


1135 
apply (rule span_add[unfolded mem_def])


1136 
apply assumption+


1137 
apply (simp add: algebra_simps)


1138 
apply (clarsimp simp add: mem_def)


1139 
apply (rule_tac x= "c*k" in exI)


1140 
apply (subgoal_tac "c *\<^sub>R x  (c * k) *\<^sub>R b = c*\<^sub>R (x  k*\<^sub>R b)")


1141 
apply (simp only: )


1142 
apply (rule span_mul[unfolded mem_def])


1143 
apply assumption


1144 
by (simp add: algebra_simps)


1145 
ultimately show "?P a" using aS span_induct[where S=S and P= "?P"] by metis


1146 
qed


1147 


1148 
lemma span_breakdown_eq:


1149 
"x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. (x  k *\<^sub>R a) \<in> span S)" (is "?lhs \<longleftrightarrow> ?rhs")


1150 
proof


1151 
{assume x: "x \<in> span (insert a S)"


1152 
from x span_breakdown[of "a" "insert a S" "x"]


1153 
have ?rhs apply clarsimp


1154 
apply (rule_tac x= "k" in exI)


1155 
apply (rule set_rev_mp[of _ "span (S  {a})" _])


1156 
apply assumption


1157 
apply (rule span_mono)


1158 
apply blast


1159 
done}


1160 
moreover


1161 
{ fix k assume k: "x  k *\<^sub>R a \<in> span S"


1162 
have eq: "x = (x  k *\<^sub>R a) + k *\<^sub>R a" by simp


1163 
have "(x  k *\<^sub>R a) + k *\<^sub>R a \<in> span (insert a S)"


1164 
apply (rule span_add)


1165 
apply (rule set_rev_mp[of _ "span S" _])


1166 
apply (rule k)


1167 
apply (rule span_mono)


1168 
apply blast


1169 
apply (rule span_mul)


1170 
apply (rule span_superset)


1171 
apply blast


1172 
done


1173 
then have ?lhs using eq by metis}


1174 
ultimately show ?thesis by blast


1175 
qed


1176 


1177 
text {* Hence some "reversal" results. *}


1178 


1179 
lemma in_span_insert:


1180 
assumes a: "a \<in> span (insert b S)" and na: "a \<notin> span S"


1181 
shows "b \<in> span (insert a S)"


1182 
proof


1183 
from span_breakdown[of b "insert b S" a, OF insertI1 a]


1184 
obtain k where k: "a  k*\<^sub>R b \<in> span (S  {b})" by auto


1185 
{assume k0: "k = 0"


1186 
with k have "a \<in> span S"


1187 
apply (simp)


1188 
apply (rule set_rev_mp)


1189 
apply assumption


1190 
apply (rule span_mono)


1191 
apply blast


1192 
done


1193 
with na have ?thesis by blast}


1194 
moreover


1195 
{assume k0: "k \<noteq> 0"


1196 
have eq: "b = (1/k) *\<^sub>R a  ((1/k) *\<^sub>R a  b)" by simp


1197 
from k0 have eq': "(1/k) *\<^sub>R (a  k*\<^sub>R b) = (1/k) *\<^sub>R a  b"


1198 
by (simp add: algebra_simps)


1199 
from k have "(1/k) *\<^sub>R (a  k*\<^sub>R b) \<in> span (S  {b})"


1200 
by (rule span_mul)


1201 
hence th: "(1/k) *\<^sub>R a  b \<in> span (S  {b})"


1202 
unfolding eq' .


1203 


1204 
from k


1205 
have ?thesis


1206 
apply (subst eq)


1207 
apply (rule span_sub)


1208 
apply (rule span_mul)


1209 
apply (rule span_superset)


1210 
apply blast


1211 
apply (rule set_rev_mp)


1212 
apply (rule th)


1213 
apply (rule span_mono)


1214 
using na by blast}


1215 
ultimately show ?thesis by blast


1216 
qed


1217 


1218 
lemma in_span_delete:


1219 
assumes a: "a \<in> span S"


1220 
and na: "a \<notin> span (S{b})"


1221 
shows "b \<in> span (insert a (S  {b}))"


1222 
apply (rule in_span_insert)


1223 
apply (rule set_rev_mp)


1224 
apply (rule a)


1225 
apply (rule span_mono)


1226 
apply blast


1227 
apply (rule na)


1228 
done


1229 


1230 
text {* Transitivity property. *}


1231 


1232 
lemma span_trans:


1233 
assumes x: "x \<in> span S" and y: "y \<in> span (insert x S)"


1234 
shows "y \<in> span S"


1235 
proof


1236 
from span_breakdown[of x "insert x S" y, OF insertI1 y]


1237 
obtain k where k: "y k*\<^sub>R x \<in> span (S  {x})" by auto


1238 
have eq: "y = (y  k *\<^sub>R x) + k *\<^sub>R x" by simp


1239 
show ?thesis


1240 
apply (subst eq)


1241 
apply (rule span_add)


1242 
apply (rule set_rev_mp)


1243 
apply (rule k)


1244 
apply (rule span_mono)


1245 
apply blast


1246 
apply (rule span_mul)


1247 
by (rule x)


1248 
qed


1249 


1250 
lemma span_insert_0[simp]: "span (insert 0 S) = span S"


1251 
using span_mono[of S "insert 0 S"] by (auto intro: span_trans span_0)


1252 


1253 
text {* An explicit expansion is sometimes needed. *}


1254 


1255 
lemma span_explicit:


1256 
"span P = {y. \<exists>S u. finite S \<and> S \<subseteq> P \<and> setsum (\<lambda>v. u v *\<^sub>R v) S = y}"


1257 
(is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \<exists>S u. ?Q S u y}")


1258 
proof


1259 
{fix x assume x: "x \<in> ?E"


1260 
then obtain S u where fS: "finite S" and SP: "S\<subseteq>P" and u: "setsum (\<lambda>v. u v *\<^sub>R v) S = x"


1261 
by blast


1262 
have "x \<in> span P"


1263 
unfolding u[symmetric]


1264 
apply (rule span_setsum[OF fS])


1265 
using span_mono[OF SP]


1266 
by (auto intro: span_superset span_mul)}


1267 
moreover


1268 
have "\<forall>x \<in> span P. x \<in> ?E"


1269 
unfolding mem_def Collect_def


1270 
proof(rule span_induct_alt')


1271 
show "?h 0"


1272 
apply (rule exI[where x="{}"]) by simp


1273 
next


1274 
fix c x y


1275 
assume x: "x \<in> P" and hy: "?h y"


1276 
from hy obtain S u where fS: "finite S" and SP: "S\<subseteq>P"


1277 
and u: "setsum (\<lambda>v. u v *\<^sub>R v) S = y" by blast


1278 
let ?S = "insert x S"


1279 
let ?u = "\<lambda>y. if y = x then (if x \<in> S then u y + c else c)


1280 
else u y"


1281 
from fS SP x have th0: "finite (insert x S)" "insert x S \<subseteq> P" by blast+


1282 
{assume xS: "x \<in> S"


1283 
have S1: "S = (S  {x}) \<union> {x}"


1284 
and Sss:"finite (S  {x})" "finite {x}" "(S {x}) \<inter> {x} = {}" using xS fS by auto


1285 
have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S =(\<Sum>v\<in>S  {x}. u v *\<^sub>R v) + (u x + c) *\<^sub>R x"


1286 
using xS


1287 
by (simp add: setsum_Un_disjoint[OF Sss, unfolded S1[symmetric]]


1288 
setsum_clauses(2)[OF fS] cong del: if_weak_cong)


1289 
also have "\<dots> = (\<Sum>v\<in>S. u v *\<^sub>R v) + c *\<^sub>R x"


1290 
apply (simp add: setsum_Un_disjoint[OF Sss, unfolded S1[symmetric]])


1291 
by (simp add: algebra_simps)


1292 
also have "\<dots> = c*\<^sub>R x + y"


1293 
by (simp add: add_commute u)


1294 
finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = c*\<^sub>R x + y" .


1295 
then have "?Q ?S ?u (c*\<^sub>R x + y)" using th0 by blast}


1296 
moreover


1297 
{assume xS: "x \<notin> S"


1298 
have th00: "(\<Sum>v\<in>S. (if v = x then c else u v) *\<^sub>R v) = y"


1299 
unfolding u[symmetric]


1300 
apply (rule setsum_cong2)


1301 
using xS by auto


1302 
have "?Q ?S ?u (c*\<^sub>R x + y)" using fS xS th0


1303 
by (simp add: th00 setsum_clauses add_commute cong del: if_weak_cong)}


1304 
ultimately have "?Q ?S ?u (c*\<^sub>R x + y)"


1305 
by (cases "x \<in> S", simp, simp)


1306 
then show "?h (c*\<^sub>R x + y)"


1307 
apply 


1308 
apply (rule exI[where x="?S"])


1309 
apply (rule exI[where x="?u"]) by metis


1310 
qed


1311 
ultimately show ?thesis by blast


1312 
qed


1313 


1314 
lemma dependent_explicit:


1315 
"dependent P \<longleftrightarrow> (\<exists>S u. finite S \<and> S \<subseteq> P \<and> (\<exists>v\<in>S. u v \<noteq> 0 \<and> setsum (\<lambda>v. u v *\<^sub>R v) S = 0))" (is "?lhs = ?rhs")


1316 
proof


1317 
{assume dP: "dependent P"


1318 
then obtain a S u where aP: "a \<in> P" and fS: "finite S"


1319 
and SP: "S \<subseteq> P  {a}" and ua: "setsum (\<lambda>v. u v *\<^sub>R v) S = a"


1320 
unfolding dependent_def span_explicit by blast


1321 
let ?S = "insert a S"


1322 
let ?u = "\<lambda>y. if y = a then  1 else u y"


1323 
let ?v = a


1324 
from aP SP have aS: "a \<notin> S" by blast


1325 
from fS SP aP have th0: "finite ?S" "?S \<subseteq> P" "?v \<in> ?S" "?u ?v \<noteq> 0" by auto


1326 
have s0: "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = 0"


1327 
using fS aS


1328 
apply (simp add: setsum_clauses field_simps)


1329 
apply (subst (2) ua[symmetric])


1330 
apply (rule setsum_cong2)


1331 
by auto


1332 
with th0 have ?rhs


1333 
apply 


1334 
apply (rule exI[where x= "?S"])


1335 
apply (rule exI[where x= "?u"])


1336 
by clarsimp}


1337 
moreover


1338 
{fix S u v assume fS: "finite S"


1339 
and SP: "S \<subseteq> P" and vS: "v \<in> S" and uv: "u v \<noteq> 0"


1340 
and u: "setsum (\<lambda>v. u v *\<^sub>R v) S = 0"


1341 
let ?a = v


1342 
let ?S = "S  {v}"


1343 
let ?u = "\<lambda>i. ( u i) / u v"


1344 
have th0: "?a \<in> P" "finite ?S" "?S \<subseteq> P" using fS SP vS by auto


1345 
have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = setsum (\<lambda>v. ( (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S  ?u v *\<^sub>R v"


1346 
using fS vS uv


1347 
by (simp add: setsum_diff1 divide_inverse field_simps)


1348 
also have "\<dots> = ?a"


1349 
unfolding scaleR_right.setsum [symmetric] u


1350 
using uv by simp


1351 
finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = ?a" .


1352 
with th0 have ?lhs


1353 
unfolding dependent_def span_explicit


1354 
apply 


1355 
apply (rule bexI[where x= "?a"])


1356 
apply (simp_all del: scaleR_minus_left)


1357 
apply (rule exI[where x= "?S"])


1358 
by (auto simp del: scaleR_minus_left)}


1359 
ultimately show ?thesis by blast

691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
