diff --git a/src/HOL/Analysis/Convex.thy b/src/HOL/Analysis/Convex.thy --- a/src/HOL/Analysis/Convex.thy +++ b/src/HOL/Analysis/Convex.thy @@ -1,4141 +1,4140 @@ (* Title: HOL/Analysis/Convex.thy Author: L C Paulson, University of Cambridge Author: Robert Himmelmann, TU Muenchen Author: Bogdan Grechuk, University of Edinburgh Author: Armin Heller, TU Muenchen Author: Johannes Hoelzl, TU Muenchen *) section \Convex Sets and Functions\ theory Convex imports Linear_Algebra "HOL-Library.Set_Algebras" begin subsection \Convexity\ definition\<^marker>\tag important\ convex :: "'a::real_vector set \ bool" where "convex s \ (\x\s. \y\s. \u\0. \v\0. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s)" lemma convexI: assumes "\x y u v. x \ s \ y \ s \ 0 \ u \ 0 \ v \ u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s" shows "convex s" using assms unfolding convex_def by fast lemma convexD: assumes "convex s" and "x \ s" and "y \ s" and "0 \ u" and "0 \ v" and "u + v = 1" shows "u *\<^sub>R x + v *\<^sub>R y \ s" using assms unfolding convex_def by fast lemma convex_alt: "convex s \ (\x\s. \y\s. \u. 0 \ u \ u \ 1 \ ((1 - u) *\<^sub>R x + u *\<^sub>R y) \ s)" (is "_ \ ?alt") proof show "convex s" if alt: ?alt proof - { fix x y and u v :: real assume mem: "x \ s" "y \ s" assume "0 \ u" "0 \ v" moreover assume "u + v = 1" then have "u = 1 - v" by auto ultimately have "u *\<^sub>R x + v *\<^sub>R y \ s" using alt [rule_format, OF mem] by auto } then show ?thesis unfolding convex_def by auto qed show ?alt if "convex s" using that by (auto simp: convex_def) qed lemma convexD_alt: assumes "convex s" "a \ s" "b \ s" "0 \ u" "u \ 1" shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \ s" using assms unfolding convex_alt by auto lemma mem_convex_alt: assumes "convex S" "x \ S" "y \ S" "u \ 0" "v \ 0" "u + v > 0" shows "((u/(u+v)) *\<^sub>R x + (v/(u+v)) *\<^sub>R y) \ S" apply (rule convexD) using assms apply (simp_all add: zero_le_divide_iff add_divide_distrib [symmetric]) done lemma convex_empty[intro,simp]: "convex {}" unfolding convex_def by simp lemma convex_singleton[intro,simp]: "convex {a}" unfolding convex_def by (auto simp: scaleR_left_distrib[symmetric]) lemma convex_UNIV[intro,simp]: "convex UNIV" unfolding convex_def by auto lemma convex_Inter: "(\s. s\f \ convex s) \ convex(\f)" unfolding convex_def by auto lemma convex_Int: "convex s \ convex t \ convex (s \ t)" unfolding convex_def by auto lemma convex_INT: "(\i. i \ A \ convex (B i)) \ convex (\i\A. B i)" unfolding convex_def by auto lemma convex_Times: "convex s \ convex t \ convex (s \ t)" unfolding convex_def by auto lemma convex_halfspace_le: "convex {x. inner a x \ b}" unfolding convex_def by (auto simp: inner_add intro!: convex_bound_le) lemma convex_halfspace_ge: "convex {x. inner a x \ b}" proof - have *: "{x. inner a x \ b} = {x. inner (-a) x \ -b}" by auto show ?thesis unfolding * using convex_halfspace_le[of "-a" "-b"] by auto qed lemma convex_halfspace_abs_le: "convex {x. \inner a x\ \ b}" proof - have *: "{x. \inner a x\ \ b} = {x. inner a x \ b} \ {x. -b \ inner a x}" by auto show ?thesis unfolding * by (simp add: convex_Int convex_halfspace_ge convex_halfspace_le) qed lemma convex_hyperplane: "convex {x. inner a x = b}" proof - have *: "{x. inner a x = b} = {x. inner a x \ b} \ {x. inner a x \ b}" by auto show ?thesis using convex_halfspace_le convex_halfspace_ge by (auto intro!: convex_Int simp: *) qed lemma convex_halfspace_lt: "convex {x. inner a x < b}" unfolding convex_def by (auto simp: convex_bound_lt inner_add) lemma convex_halfspace_gt: "convex {x. inner a x > b}" using convex_halfspace_lt[of "-a" "-b"] by auto lemma convex_halfspace_Re_ge: "convex {x. Re x \ b}" using convex_halfspace_ge[of b "1::complex"] by simp lemma convex_halfspace_Re_le: "convex {x. Re x \ b}" using convex_halfspace_le[of "1::complex" b] by simp lemma convex_halfspace_Im_ge: "convex {x. Im x \ b}" using convex_halfspace_ge[of b \] by simp lemma convex_halfspace_Im_le: "convex {x. Im x \ b}" using convex_halfspace_le[of \ b] by simp lemma convex_halfspace_Re_gt: "convex {x. Re x > b}" using convex_halfspace_gt[of b "1::complex"] by simp lemma convex_halfspace_Re_lt: "convex {x. Re x < b}" using convex_halfspace_lt[of "1::complex" b] by simp lemma convex_halfspace_Im_gt: "convex {x. Im x > b}" using convex_halfspace_gt[of b \] by simp lemma convex_halfspace_Im_lt: "convex {x. Im x < b}" using convex_halfspace_lt[of \ b] by simp lemma convex_real_interval [iff]: fixes a b :: "real" shows "convex {a..}" and "convex {..b}" and "convex {a<..}" and "convex {.. inner 1 x}" by auto then show 1: "convex {a..}" by (simp only: convex_halfspace_ge) have "{..b} = {x. inner 1 x \ b}" by auto then show 2: "convex {..b}" by (simp only: convex_halfspace_le) have "{a<..} = {x. a < inner 1 x}" by auto then show 3: "convex {a<..}" by (simp only: convex_halfspace_gt) have "{.. {..b}" by auto then show "convex {a..b}" by (simp only: convex_Int 1 2) have "{a<..b} = {a<..} \ {..b}" by auto then show "convex {a<..b}" by (simp only: convex_Int 3 2) have "{a.. {.. {.." by (simp add: convex_def scaleR_conv_of_real) subsection\<^marker>\tag unimportant\ \Explicit expressions for convexity in terms of arbitrary sums\ lemma convex_sum: fixes C :: "'a::real_vector set" assumes "finite s" and "convex C" and "(\ i \ s. a i) = 1" assumes "\i. i \ s \ a i \ 0" and "\i. i \ s \ y i \ C" shows "(\ j \ s. a j *\<^sub>R y j) \ C" using assms(1,3,4,5) proof (induct arbitrary: a set: finite) case empty then show ?case by simp next case (insert i s) note IH = this(3) have "a i + sum a s = 1" and "0 \ a i" and "\j\s. 0 \ a j" and "y i \ C" and "\j\s. y j \ C" using insert.hyps(1,2) insert.prems by simp_all then have "0 \ sum a s" by (simp add: sum_nonneg) have "a i *\<^sub>R y i + (\j\s. a j *\<^sub>R y j) \ C" proof (cases "sum a s = 0") case True with \a i + sum a s = 1\ have "a i = 1" by simp from sum_nonneg_0 [OF \finite s\ _ True] \\j\s. 0 \ a j\ have "\j\s. a j = 0" by simp show ?thesis using \a i = 1\ and \\j\s. a j = 0\ and \y i \ C\ by simp next case False with \0 \ sum a s\ have "0 < sum a s" by simp then have "(\j\s. (a j / sum a s) *\<^sub>R y j) \ C" using \\j\s. 0 \ a j\ and \\j\s. y j \ C\ by (simp add: IH sum_divide_distrib [symmetric]) from \convex C\ and \y i \ C\ and this and \0 \ a i\ and \0 \ sum a s\ and \a i + sum a s = 1\ have "a i *\<^sub>R y i + sum a s *\<^sub>R (\j\s. (a j / sum a s) *\<^sub>R y j) \ C" by (rule convexD) then show ?thesis by (simp add: scaleR_sum_right False) qed then show ?case using \finite s\ and \i \ s\ by simp qed lemma convex: "convex s \ (\(k::nat) u x. (\i. 1\i \ i\k \ 0 \ u i \ x i \s) \ (sum u {1..k} = 1) \ sum (\i. u i *\<^sub>R x i) {1..k} \ s)" proof safe fix k :: nat fix u :: "nat \ real" fix x assume "convex s" "\i. 1 \ i \ i \ k \ 0 \ u i \ x i \ s" "sum u {1..k} = 1" with convex_sum[of "{1 .. k}" s] show "(\j\{1 .. k}. u j *\<^sub>R x j) \ s" by auto next assume *: "\k u x. (\ i :: nat. 1 \ i \ i \ k \ 0 \ u i \ x i \ s) \ sum u {1..k} = 1 \ (\i = 1..k. u i *\<^sub>R (x i :: 'a)) \ s" { fix \ :: real fix x y :: 'a assume xy: "x \ s" "y \ s" assume mu: "\ \ 0" "\ \ 1" let ?u = "\i. if (i :: nat) = 1 then \ else 1 - \" let ?x = "\i. if (i :: nat) = 1 then x else y" have "{1 :: nat .. 2} \ - {x. x = 1} = {2}" by auto then have card: "card ({1 :: nat .. 2} \ - {x. x = 1}) = 1" by simp then have "sum ?u {1 .. 2} = 1" using sum.If_cases[of "{(1 :: nat) .. 2}" "\ x. x = 1" "\ x. \" "\ x. 1 - \"] by auto with *[rule_format, of "2" ?u ?x] have s: "(\j \ {1..2}. ?u j *\<^sub>R ?x j) \ s" using mu xy by auto have grarr: "(\j \ {Suc (Suc 0)..2}. ?u j *\<^sub>R ?x j) = (1 - \) *\<^sub>R y" using sum.atLeast_Suc_atMost[of "Suc (Suc 0)" 2 "\ j. (1 - \) *\<^sub>R y"] by auto from sum.atLeast_Suc_atMost[of "Suc 0" 2 "\ j. ?u j *\<^sub>R ?x j", simplified this] have "(\j \ {1..2}. ?u j *\<^sub>R ?x j) = \ *\<^sub>R x + (1 - \) *\<^sub>R y" by auto then have "(1 - \) *\<^sub>R y + \ *\<^sub>R x \ s" using s by (auto simp: add.commute) } then show "convex s" unfolding convex_alt by auto qed lemma convex_explicit: fixes s :: "'a::real_vector set" shows "convex s \ (\t u. finite t \ t \ s \ (\x\t. 0 \ u x) \ sum u t = 1 \ sum (\x. u x *\<^sub>R x) t \ s)" proof safe fix t fix u :: "'a \ real" assume "convex s" and "finite t" and "t \ s" "\x\t. 0 \ u x" "sum u t = 1" then show "(\x\t. u x *\<^sub>R x) \ s" using convex_sum[of t s u "\ x. x"] by auto next assume *: "\t. \ u. finite t \ t \ s \ (\x\t. 0 \ u x) \ sum u t = 1 \ (\x\t. u x *\<^sub>R x) \ s" show "convex s" unfolding convex_alt proof safe fix x y fix \ :: real assume **: "x \ s" "y \ s" "0 \ \" "\ \ 1" show "(1 - \) *\<^sub>R x + \ *\<^sub>R y \ s" proof (cases "x = y") case False then show ?thesis using *[rule_format, of "{x, y}" "\ z. if z = x then 1 - \ else \"] ** by auto next case True then show ?thesis using *[rule_format, of "{x, y}" "\ z. 1"] ** by (auto simp: field_simps real_vector.scale_left_diff_distrib) qed qed qed lemma convex_finite: assumes "finite s" shows "convex s \ (\u. (\x\s. 0 \ u x) \ sum u s = 1 \ sum (\x. u x *\<^sub>R x) s \ s)" unfolding convex_explicit apply safe subgoal for u by (erule allE [where x=s], erule allE [where x=u]) auto subgoal for t u proof - have if_distrib_arg: "\P f g x. (if P then f else g) x = (if P then f x else g x)" by simp assume sum: "\u. (\x\s. 0 \ u x) \ sum u s = 1 \ (\x\s. u x *\<^sub>R x) \ s" assume *: "\x\t. 0 \ u x" "sum u t = 1" assume "t \ s" then have "s \ t = t" by auto with sum[THEN spec[where x="\x. if x\t then u x else 0"]] * show "(\x\t. u x *\<^sub>R x) \ s" by (auto simp: assms sum.If_cases if_distrib if_distrib_arg) qed done subsection \Functions that are convex on a set\ definition\<^marker>\tag important\ convex_on :: "'a::real_vector set \ ('a \ real) \ bool" where "convex_on s f \ (\x\s. \y\s. \u\0. \v\0. u + v = 1 \ f (u *\<^sub>R x + v *\<^sub>R y) \ u * f x + v * f y)" lemma convex_onI [intro?]: assumes "\t x y. t > 0 \ t < 1 \ x \ A \ y \ A \ f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \ (1 - t) * f x + t * f y" shows "convex_on A f" unfolding convex_on_def proof clarify fix x y fix u v :: real assume A: "x \ A" "y \ A" "u \ 0" "v \ 0" "u + v = 1" from A(5) have [simp]: "v = 1 - u" by (simp add: algebra_simps) from A(1-4) show "f (u *\<^sub>R x + v *\<^sub>R y) \ u * f x + v * f y" using assms[of u y x] by (cases "u = 0 \ u = 1") (auto simp: algebra_simps) qed lemma convex_on_linorderI [intro?]: fixes A :: "('a::{linorder,real_vector}) set" assumes "\t x y. t > 0 \ t < 1 \ x \ A \ y \ A \ x < y \ f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \ (1 - t) * f x + t * f y" shows "convex_on A f" proof fix x y fix t :: real assume A: "x \ A" "y \ A" "t > 0" "t < 1" with assms [of t x y] assms [of "1 - t" y x] show "f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \ (1 - t) * f x + t * f y" by (cases x y rule: linorder_cases) (auto simp: algebra_simps) qed lemma convex_onD: assumes "convex_on A f" shows "\t x y. t \ 0 \ t \ 1 \ x \ A \ y \ A \ f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \ (1 - t) * f x + t * f y" using assms by (auto simp: convex_on_def) lemma convex_onD_Icc: assumes "convex_on {x..y} f" "x \ (y :: _ :: {real_vector,preorder})" shows "\t. t \ 0 \ t \ 1 \ f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \ (1 - t) * f x + t * f y" using assms(2) by (intro convex_onD [OF assms(1)]) simp_all lemma convex_on_subset: "convex_on t f \ s \ t \ convex_on s f" unfolding convex_on_def by auto lemma convex_on_add [intro]: assumes "convex_on s f" and "convex_on s g" shows "convex_on s (\x. f x + g x)" proof - { fix x y assume "x \ s" "y \ s" moreover fix u v :: real assume "0 \ u" "0 \ v" "u + v = 1" ultimately have "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \ (u * f x + v * f y) + (u * g x + v * g y)" using assms unfolding convex_on_def by (auto simp: add_mono) then have "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \ u * (f x + g x) + v * (f y + g y)" by (simp add: field_simps) } then show ?thesis unfolding convex_on_def by auto qed lemma convex_on_cmul [intro]: fixes c :: real assumes "0 \ c" and "convex_on s f" shows "convex_on s (\x. c * f x)" proof - have *: "u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" for u c fx v fy :: real by (simp add: field_simps) show ?thesis using assms(2) and mult_left_mono [OF _ assms(1)] unfolding convex_on_def and * by auto qed lemma convex_lower: assumes "convex_on s f" and "x \ s" and "y \ s" and "0 \ u" and "0 \ v" and "u + v = 1" shows "f (u *\<^sub>R x + v *\<^sub>R y) \ max (f x) (f y)" proof - let ?m = "max (f x) (f y)" have "u * f x + v * f y \ u * max (f x) (f y) + v * max (f x) (f y)" using assms(4,5) by (auto simp: mult_left_mono add_mono) also have "\ = max (f x) (f y)" using assms(6) by (simp add: distrib_right [symmetric]) finally show ?thesis using assms unfolding convex_on_def by fastforce qed lemma convex_on_dist [intro]: fixes s :: "'a::real_normed_vector set" shows "convex_on s (\x. dist a x)" proof (auto simp: convex_on_def dist_norm) fix x y assume "x \ s" "y \ s" fix u v :: real assume "0 \ u" assume "0 \ v" assume "u + v = 1" have "a = u *\<^sub>R a + v *\<^sub>R a" unfolding scaleR_left_distrib[symmetric] and \u + v = 1\ by simp then have *: "a - (u *\<^sub>R x + v *\<^sub>R y) = (u *\<^sub>R (a - x)) + (v *\<^sub>R (a - y))" by (auto simp: algebra_simps) show "norm (a - (u *\<^sub>R x + v *\<^sub>R y)) \ u * norm (a - x) + v * norm (a - y)" unfolding * using norm_triangle_ineq[of "u *\<^sub>R (a - x)" "v *\<^sub>R (a - y)"] using \0 \ u\ \0 \ v\ by auto qed subsection\<^marker>\tag unimportant\ \Arithmetic operations on sets preserve convexity\ lemma convex_linear_image: assumes "linear f" and "convex s" shows "convex (f ` s)" proof - interpret f: linear f by fact from \convex s\ show "convex (f ` s)" by (simp add: convex_def f.scaleR [symmetric] f.add [symmetric]) qed lemma convex_linear_vimage: assumes "linear f" and "convex s" shows "convex (f -` s)" proof - interpret f: linear f by fact from \convex s\ show "convex (f -` s)" by (simp add: convex_def f.add f.scaleR) qed lemma convex_scaling: assumes "convex s" shows "convex ((\x. c *\<^sub>R x) ` s)" proof - have "linear (\x. c *\<^sub>R x)" by (simp add: linearI scaleR_add_right) then show ?thesis using \convex s\ by (rule convex_linear_image) qed lemma convex_scaled: assumes "convex S" shows "convex ((\x. x *\<^sub>R c) ` S)" proof - have "linear (\x. x *\<^sub>R c)" by (simp add: linearI scaleR_add_left) then show ?thesis using \convex S\ by (rule convex_linear_image) qed lemma convex_negations: assumes "convex S" shows "convex ((\x. - x) ` S)" proof - have "linear (\x. - x)" by (simp add: linearI) then show ?thesis using \convex S\ by (rule convex_linear_image) qed lemma convex_sums: assumes "convex S" and "convex T" shows "convex (\x\ S. \y \ T. {x + y})" proof - have "linear (\(x, y). x + y)" by (auto intro: linearI simp: scaleR_add_right) with assms have "convex ((\(x, y). x + y) ` (S \ T))" by (intro convex_linear_image convex_Times) also have "((\(x, y). x + y) ` (S \ T)) = (\x\ S. \y \ T. {x + y})" by auto finally show ?thesis . qed lemma convex_differences: assumes "convex S" "convex T" shows "convex (\x\ S. \y \ T. {x - y})" proof - have "{x - y| x y. x \ S \ y \ T} = {x + y |x y. x \ S \ y \ uminus ` T}" by (auto simp: diff_conv_add_uminus simp del: add_uminus_conv_diff) then show ?thesis using convex_sums[OF assms(1) convex_negations[OF assms(2)]] by auto qed lemma convex_translation: "convex ((+) a ` S)" if "convex S" proof - have "(\ x\ {a}. \y \ S. {x + y}) = (+) a ` S" by auto then show ?thesis using convex_sums [OF convex_singleton [of a] that] by auto qed lemma convex_translation_subtract: "convex ((\b. b - a) ` S)" if "convex S" using convex_translation [of S "- a"] that by (simp cong: image_cong_simp) lemma convex_affinity: assumes "convex S" shows "convex ((\x. a + c *\<^sub>R x) ` S)" proof - have "(\x. a + c *\<^sub>R x) ` S = (+) a ` (*\<^sub>R) c ` S" by auto then show ?thesis using convex_translation[OF convex_scaling[OF assms], of a c] by auto qed lemma pos_is_convex: "convex {0 :: real <..}" unfolding convex_alt proof safe fix y x \ :: real assume *: "y > 0" "x > 0" "\ \ 0" "\ \ 1" { assume "\ = 0" then have "\ *\<^sub>R x + (1 - \) *\<^sub>R y = y" by simp then have "\ *\<^sub>R x + (1 - \) *\<^sub>R y > 0" using * by simp } moreover { assume "\ = 1" then have "\ *\<^sub>R x + (1 - \) *\<^sub>R y > 0" using * by simp } moreover { assume "\ \ 1" "\ \ 0" then have "\ > 0" "(1 - \) > 0" using * by auto then have "\ *\<^sub>R x + (1 - \) *\<^sub>R y > 0" using * by (auto simp: add_pos_pos) } ultimately show "(1 - \) *\<^sub>R y + \ *\<^sub>R x > 0" by fastforce qed lemma convex_on_sum: fixes a :: "'a \ real" and y :: "'a \ 'b::real_vector" and f :: "'b \ real" assumes "finite s" "s \ {}" and "convex_on C f" and "convex C" and "(\ i \ s. a i) = 1" and "\i. i \ s \ a i \ 0" and "\i. i \ s \ y i \ C" shows "f (\ i \ s. a i *\<^sub>R y i) \ (\ i \ s. a i * f (y i))" using assms proof (induct s arbitrary: a rule: finite_ne_induct) case (singleton i) then have ai: "a i = 1" by auto then show ?case by auto next case (insert i s) then have "convex_on C f" by simp from this[unfolded convex_on_def, rule_format] have conv: "\x y \. x \ C \ y \ C \ 0 \ \ \ \ \ 1 \ f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) \ \ * f x + (1 - \) * f y" by simp show ?case proof (cases "a i = 1") case True then have "(\ j \ s. a j) = 0" using insert by auto then have "\j. j \ s \ a j = 0" using insert by (fastforce simp: sum_nonneg_eq_0_iff) then show ?thesis using insert by auto next case False from insert have yai: "y i \ C" "a i \ 0" by auto have fis: "finite (insert i s)" using insert by auto then have ai1: "a i \ 1" using sum_nonneg_leq_bound[of "insert i s" a] insert by simp then have "a i < 1" using False by auto then have i0: "1 - a i > 0" by auto let ?a = "\j. a j / (1 - a i)" have a_nonneg: "?a j \ 0" if "j \ s" for j using i0 insert that by fastforce have "(\ j \ insert i s. a j) = 1" using insert by auto then have "(\ j \ s. a j) = 1 - a i" using sum.insert insert by fastforce then have "(\ j \ s. a j) / (1 - a i) = 1" using i0 by auto then have a1: "(\ j \ s. ?a j) = 1" unfolding sum_divide_distrib by simp have "convex C" using insert by auto then have asum: "(\ j \ s. ?a j *\<^sub>R y j) \ C" using insert convex_sum [OF \finite s\ \convex C\ a1 a_nonneg] by auto have asum_le: "f (\ j \ s. ?a j *\<^sub>R y j) \ (\ j \ s. ?a j * f (y j))" using a_nonneg a1 insert by blast have "f (\ j \ insert i s. a j *\<^sub>R y j) = f ((\ j \ s. a j *\<^sub>R y j) + a i *\<^sub>R y i)" using sum.insert[of s i "\ j. a j *\<^sub>R y j", OF \finite s\ \i \ s\] insert by (auto simp only: add.commute) also have "\ = f (((1 - a i) * inverse (1 - a i)) *\<^sub>R (\ j \ s. a j *\<^sub>R y j) + a i *\<^sub>R y i)" using i0 by auto also have "\ = f ((1 - a i) *\<^sub>R (\ j \ s. (a j * inverse (1 - a i)) *\<^sub>R y j) + a i *\<^sub>R y i)" using scaleR_right.sum[of "inverse (1 - a i)" "\ j. a j *\<^sub>R y j" s, symmetric] by (auto simp: algebra_simps) also have "\ = f ((1 - a i) *\<^sub>R (\ j \ s. ?a j *\<^sub>R y j) + a i *\<^sub>R y i)" by (auto simp: divide_inverse) also have "\ \ (1 - a i) *\<^sub>R f ((\ j \ s. ?a j *\<^sub>R y j)) + a i * f (y i)" using conv[of "y i" "(\ j \ s. ?a j *\<^sub>R y j)" "a i", OF yai(1) asum yai(2) ai1] by (auto simp: add.commute) also have "\ \ (1 - a i) * (\ j \ s. ?a j * f (y j)) + a i * f (y i)" using add_right_mono [OF mult_left_mono [of _ _ "1 - a i", OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp also have "\ = (\ j \ s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)" unfolding sum_distrib_left[of "1 - a i" "\ j. ?a j * f (y j)"] using i0 by auto also have "\ = (\ j \ s. a j * f (y j)) + a i * f (y i)" using i0 by auto also have "\ = (\ j \ insert i s. a j * f (y j))" using insert by auto finally show ?thesis by simp qed qed lemma convex_on_alt: fixes C :: "'a::real_vector set" assumes "convex C" shows "convex_on C f \ (\x \ C. \ y \ C. \ \ :: real. \ \ 0 \ \ \ 1 \ f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) \ \ * f x + (1 - \) * f y)" proof safe fix x y fix \ :: real assume *: "convex_on C f" "x \ C" "y \ C" "0 \ \" "\ \ 1" from this[unfolded convex_on_def, rule_format] have "0 \ u \ 0 \ v \ u + v = 1 \ f (u *\<^sub>R x + v *\<^sub>R y) \ u * f x + v * f y" for u v by auto from this [of "\" "1 - \", simplified] * show "f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) \ \ * f x + (1 - \) * f y" by auto next assume *: "\x\C. \y\C. \\. 0 \ \ \ \ \ 1 \ f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) \ \ * f x + (1 - \) * f y" { fix x y fix u v :: real assume **: "x \ C" "y \ C" "u \ 0" "v \ 0" "u + v = 1" then have[simp]: "1 - u = v" by auto from *[rule_format, of x y u] have "f (u *\<^sub>R x + v *\<^sub>R y) \ u * f x + v * f y" using ** by auto } then show "convex_on C f" unfolding convex_on_def by auto qed lemma convex_on_diff: fixes f :: "real \ real" assumes f: "convex_on I f" and I: "x \ I" "y \ I" and t: "x < t" "t < y" shows "(f x - f t) / (x - t) \ (f x - f y) / (x - y)" and "(f x - f y) / (x - y) \ (f t - f y) / (t - y)" proof - define a where "a \ (t - y) / (x - y)" with t have "0 \ a" "0 \ 1 - a" by (auto simp: field_simps) with f \x \ I\ \y \ I\ have cvx: "f (a * x + (1 - a) * y) \ a * f x + (1 - a) * f y" by (auto simp: convex_on_def) have "a * x + (1 - a) * y = a * (x - y) + y" by (simp add: field_simps) also have "\ = t" unfolding a_def using \x < t\ \t < y\ by simp finally have "f t \ a * f x + (1 - a) * f y" using cvx by simp also have "\ = a * (f x - f y) + f y" by (simp add: field_simps) finally have "f t - f y \ a * (f x - f y)" by simp with t show "(f x - f t) / (x - t) \ (f x - f y) / (x - y)" by (simp add: le_divide_eq divide_le_eq field_simps a_def) with t show "(f x - f y) / (x - y) \ (f t - f y) / (t - y)" by (simp add: le_divide_eq divide_le_eq field_simps) qed lemma pos_convex_function: fixes f :: "real \ real" assumes "convex C" and leq: "\x y. x \ C \ y \ C \ f' x * (y - x) \ f y - f x" shows "convex_on C f" unfolding convex_on_alt[OF assms(1)] using assms proof safe fix x y \ :: real let ?x = "\ *\<^sub>R x + (1 - \) *\<^sub>R y" assume *: "convex C" "x \ C" "y \ C" "\ \ 0" "\ \ 1" then have "1 - \ \ 0" by auto then have xpos: "?x \ C" using * unfolding convex_alt by fastforce have geq: "\ * (f x - f ?x) + (1 - \) * (f y - f ?x) \ \ * f' ?x * (x - ?x) + (1 - \) * f' ?x * (y - ?x)" using add_mono [OF mult_left_mono [OF leq [OF xpos *(2)] \\ \ 0\] mult_left_mono [OF leq [OF xpos *(3)] \1 - \ \ 0\]] by auto then have "\ * f x + (1 - \) * f y - f ?x \ 0" by (auto simp: field_simps) then show "f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) \ \ * f x + (1 - \) * f y" using convex_on_alt by auto qed lemma atMostAtLeast_subset_convex: fixes C :: "real set" assumes "convex C" and "x \ C" "y \ C" "x < y" shows "{x .. y} \ C" proof safe fix z assume z: "z \ {x .. y}" have less: "z \ C" if *: "x < z" "z < y" proof - let ?\ = "(y - z) / (y - x)" have "0 \ ?\" "?\ \ 1" using assms * by (auto simp: field_simps) then have comb: "?\ * x + (1 - ?\) * y \ C" using assms iffD1[OF convex_alt, rule_format, of C y x ?\] by (simp add: algebra_simps) have "?\ * x + (1 - ?\) * y = (y - z) * x / (y - x) + (1 - (y - z) / (y - x)) * y" by (auto simp: field_simps) also have "\ = ((y - z) * x + (y - x - (y - z)) * y) / (y - x)" using assms by (simp only: add_divide_distrib) (auto simp: field_simps) also have "\ = z" using assms by (auto simp: field_simps) finally show ?thesis using comb by auto qed show "z \ C" using z less assms by (auto simp: le_less) qed lemma f''_imp_f': fixes f :: "real \ real" assumes "convex C" and f': "\x. x \ C \ DERIV f x :> (f' x)" and f'': "\x. x \ C \ DERIV f' x :> (f'' x)" and pos: "\x. x \ C \ f'' x \ 0" and x: "x \ C" and y: "y \ C" shows "f' x * (y - x) \ f y - f x" using assms proof - have less_imp: "f y - f x \ f' x * (y - x)" "f' y * (x - y) \ f x - f y" if *: "x \ C" "y \ C" "y > x" for x y :: real proof - from * have ge: "y - x > 0" "y - x \ 0" by auto from * have le: "x - y < 0" "x - y \ 0" by auto then obtain z1 where z1: "z1 > x" "z1 < y" "f y - f x = (y - x) * f' z1" using subsetD[OF atMostAtLeast_subset_convex[OF \convex C\ \x \ C\ \y \ C\ \x < y\], THEN f', THEN MVT2[OF \x < y\, rule_format, unfolded atLeastAtMost_iff[symmetric]]] by auto then have "z1 \ C" using atMostAtLeast_subset_convex \convex C\ \x \ C\ \y \ C\ \x < y\ by fastforce from z1 have z1': "f x - f y = (x - y) * f' z1" by (simp add: field_simps) obtain z2 where z2: "z2 > x" "z2 < z1" "f' z1 - f' x = (z1 - x) * f'' z2" using subsetD[OF atMostAtLeast_subset_convex[OF \convex C\ \x \ C\ \z1 \ C\ \x < z1\], THEN f'', THEN MVT2[OF \x < z1\, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1 by auto obtain z3 where z3: "z3 > z1" "z3 < y" "f' y - f' z1 = (y - z1) * f'' z3" using subsetD[OF atMostAtLeast_subset_convex[OF \convex C\ \z1 \ C\ \y \ C\ \z1 < y\], THEN f'', THEN MVT2[OF \z1 < y\, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1 by auto have "f' y - (f x - f y) / (x - y) = f' y - f' z1" using * z1' by auto also have "\ = (y - z1) * f'' z3" using z3 by auto finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3" by simp have A': "y - z1 \ 0" using z1 by auto have "z3 \ C" using z3 * atMostAtLeast_subset_convex \convex C\ \x \ C\ \z1 \ C\ \x < z1\ by fastforce then have B': "f'' z3 \ 0" using assms by auto from A' B' have "(y - z1) * f'' z3 \ 0" by auto from cool' this have "f' y - (f x - f y) / (x - y) \ 0" by auto from mult_right_mono_neg[OF this le(2)] have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \ 0 * (x - y)" by (simp add: algebra_simps) then have "f' y * (x - y) - (f x - f y) \ 0" using le by auto then have res: "f' y * (x - y) \ f x - f y" by auto have "(f y - f x) / (y - x) - f' x = f' z1 - f' x" using * z1 by auto also have "\ = (z1 - x) * f'' z2" using z2 by auto finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2" by simp have A: "z1 - x \ 0" using z1 by auto have "z2 \ C" using z2 z1 * atMostAtLeast_subset_convex \convex C\ \z1 \ C\ \y \ C\ \z1 < y\ by fastforce then have B: "f'' z2 \ 0" using assms by auto from A B have "(z1 - x) * f'' z2 \ 0" by auto with cool have "(f y - f x) / (y - x) - f' x \ 0" by auto from mult_right_mono[OF this ge(2)] have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \ 0 * (y - x)" by (simp add: algebra_simps) then have "f y - f x - f' x * (y - x) \ 0" using ge by auto then show "f y - f x \ f' x * (y - x)" "f' y * (x - y) \ f x - f y" using res by auto qed show ?thesis proof (cases "x = y") case True with x y show ?thesis by auto next case False with less_imp x y show ?thesis by (auto simp: neq_iff) qed qed lemma f''_ge0_imp_convex: fixes f :: "real \ real" assumes conv: "convex C" and f': "\x. x \ C \ DERIV f x :> (f' x)" and f'': "\x. x \ C \ DERIV f' x :> (f'' x)" and pos: "\x. x \ C \ f'' x \ 0" shows "convex_on C f" using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastforce lemma minus_log_convex: fixes b :: real assumes "b > 1" shows "convex_on {0 <..} (\ x. - log b x)" proof - have "\z. z > 0 \ DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto then have f': "\z. z > 0 \ DERIV (\ z. - log b z) z :> - 1 / (ln b * z)" by (auto simp: DERIV_minus) have "\z::real. z > 0 \ DERIV inverse z :> - (inverse z ^ Suc (Suc 0))" using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto from this[THEN DERIV_cmult, of _ "- 1 / ln b"] have "\z::real. z > 0 \ DERIV (\ z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))" by auto then have f''0: "\z::real. z > 0 \ DERIV (\ z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)" unfolding inverse_eq_divide by (auto simp: mult.assoc) have f''_ge0: "\z::real. z > 0 \ 1 / (ln b * z * z) \ 0" using \b > 1\ by (auto intro!: less_imp_le) from f''_ge0_imp_convex[OF pos_is_convex, unfolded greaterThan_iff, OF f' f''0 f''_ge0] show ?thesis by auto qed subsection\<^marker>\tag unimportant\ \Convexity of real functions\ lemma convex_on_realI: assumes "connected A" and "\x. x \ A \ (f has_real_derivative f' x) (at x)" and "\x y. x \ A \ y \ A \ x \ y \ f' x \ f' y" shows "convex_on A f" proof (rule convex_on_linorderI) fix t x y :: real assume t: "t > 0" "t < 1" assume xy: "x \ A" "y \ A" "x < y" define z where "z = (1 - t) * x + t * y" with \connected A\ and xy have ivl: "{x..y} \ A" using connected_contains_Icc by blast from xy t have xz: "z > x" by (simp add: z_def algebra_simps) have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps) also from xy t have "\ > 0" by (intro mult_pos_pos) simp_all finally have yz: "z < y" by simp from assms xz yz ivl t have "\\. \ > x \ \ < z \ f z - f x = (z - x) * f' \" by (intro MVT2) (auto intro!: assms(2)) then obtain \ where \: "\ > x" "\ < z" "f' \ = (f z - f x) / (z - x)" by auto from assms xz yz ivl t have "\\. \ > z \ \ < y \ f y - f z = (y - z) * f' \" by (intro MVT2) (auto intro!: assms(2)) then obtain \ where \: "\ > z" "\ < y" "f' \ = (f y - f z) / (y - z)" by auto from \(3) have "(f y - f z) / (y - z) = f' \" .. also from \ \ ivl have "\ \ A" "\ \ A" by auto with \ \ have "f' \ \ f' \" by (intro assms(3)) auto also from \(3) have "f' \ = (f z - f x) / (z - x)" . finally have "(f y - f z) * (z - x) \ (f z - f x) * (y - z)" using xz yz by (simp add: field_simps) also have "z - x = t * (y - x)" by (simp add: z_def algebra_simps) also have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps) finally have "(f y - f z) * t \ (f z - f x) * (1 - t)" using xy by simp then show "(1 - t) * f x + t * f y \ f ((1 - t) *\<^sub>R x + t *\<^sub>R y)" by (simp add: z_def algebra_simps) qed lemma convex_on_inverse: assumes "A \ {0<..}" shows "convex_on A (inverse :: real \ real)" proof (rule convex_on_subset[OF _ assms], intro convex_on_realI[of _ _ "\x. -inverse (x^2)"]) fix u v :: real assume "u \ {0<..}" "v \ {0<..}" "u \ v" with assms show "-inverse (u^2) \ -inverse (v^2)" by (intro le_imp_neg_le le_imp_inverse_le power_mono) (simp_all) qed (insert assms, auto intro!: derivative_eq_intros simp: field_split_simps power2_eq_square) lemma convex_onD_Icc': assumes "convex_on {x..y} f" "c \ {x..y}" defines "d \ y - x" shows "f c \ (f y - f x) / d * (c - x) + f x" proof (cases x y rule: linorder_cases) case less then have d: "d > 0" by (simp add: d_def) from assms(2) less have A: "0 \ (c - x) / d" "(c - x) / d \ 1" by (simp_all add: d_def field_split_simps) have "f c = f (x + (c - x) * 1)" by simp also from less have "1 = ((y - x) / d)" by (simp add: d_def) also from d have "x + (c - x) * \ = (1 - (c - x) / d) *\<^sub>R x + ((c - x) / d) *\<^sub>R y" by (simp add: field_simps) also have "f \ \ (1 - (c - x) / d) * f x + (c - x) / d * f y" using assms less by (intro convex_onD_Icc) simp_all also from d have "\ = (f y - f x) / d * (c - x) + f x" by (simp add: field_simps) finally show ?thesis . qed (insert assms(2), simp_all) lemma convex_onD_Icc'': assumes "convex_on {x..y} f" "c \ {x..y}" defines "d \ y - x" shows "f c \ (f x - f y) / d * (y - c) + f y" proof (cases x y rule: linorder_cases) case less then have d: "d > 0" by (simp add: d_def) from assms(2) less have A: "0 \ (y - c) / d" "(y - c) / d \ 1" by (simp_all add: d_def field_split_simps) have "f c = f (y - (y - c) * 1)" by simp also from less have "1 = ((y - x) / d)" by (simp add: d_def) also from d have "y - (y - c) * \ = (1 - (1 - (y - c) / d)) *\<^sub>R x + (1 - (y - c) / d) *\<^sub>R y" by (simp add: field_simps) also have "f \ \ (1 - (1 - (y - c) / d)) * f x + (1 - (y - c) / d) * f y" using assms less by (intro convex_onD_Icc) (simp_all add: field_simps) also from d have "\ = (f x - f y) / d * (y - c) + f y" by (simp add: field_simps) finally show ?thesis . qed (insert assms(2), simp_all) lemma convex_translation_eq [simp]: "convex ((+) a ` s) \ convex s" by (metis convex_translation translation_galois) lemma convex_translation_subtract_eq [simp]: "convex ((\b. b - a) ` s) \ convex s" using convex_translation_eq [of "- a"] by (simp cong: image_cong_simp) lemma convex_linear_image_eq [simp]: fixes f :: "'a::real_vector \ 'b::real_vector" shows "\linear f; inj f\ \ convex (f ` s) \ convex s" by (metis (no_types) convex_linear_image convex_linear_vimage inj_vimage_image_eq) lemma fst_linear: "linear fst" unfolding linear_iff by (simp add: algebra_simps) lemma snd_linear: "linear snd" unfolding linear_iff by (simp add: algebra_simps) lemma fst_snd_linear: "linear (\(x,y). x + y)" unfolding linear_iff by (simp add: algebra_simps) lemma vector_choose_size: assumes "0 \ c" obtains x :: "'a::{real_normed_vector, perfect_space}" where "norm x = c" proof - obtain a::'a where "a \ 0" using UNIV_not_singleton UNIV_eq_I set_zero singletonI by fastforce then show ?thesis by (rule_tac x="scaleR (c / norm a) a" in that) (simp add: assms) qed lemma vector_choose_dist: assumes "0 \ c" obtains y :: "'a::{real_normed_vector, perfect_space}" where "dist x y = c" by (metis add_diff_cancel_left' assms dist_commute dist_norm vector_choose_size) lemma sum_delta_notmem: assumes "x \ s" shows "sum (\y. if (y = x) then P x else Q y) s = sum Q s" and "sum (\y. if (x = y) then P x else Q y) s = sum Q s" and "sum (\y. if (y = x) then P y else Q y) s = sum Q s" and "sum (\y. if (x = y) then P y else Q y) s = sum Q s" apply (rule_tac [!] sum.cong) using assms apply auto done lemma sum_delta'': fixes s::"'a::real_vector set" assumes "finite s" shows "(\x\s. (if y = x then f x else 0) *\<^sub>R x) = (if y\s then (f y) *\<^sub>R y else 0)" proof - have *: "\x y. (if y = x then f x else (0::real)) *\<^sub>R x = (if x=y then (f x) *\<^sub>R x else 0)" by auto show ?thesis unfolding * using sum.delta[OF assms, of y "\x. f x *\<^sub>R x"] by auto qed lemma if_smult: "(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)" by (fact if_distrib) lemma dist_triangle_eq: fixes x y z :: "'a::real_inner" shows "dist x z = dist x y + dist y z \ norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)" proof - have *: "x - y + (y - z) = x - z" by auto show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *] by (auto simp:norm_minus_commute) qed subsection \Affine set and affine hull\ definition\<^marker>\tag important\ affine :: "'a::real_vector set \ bool" where "affine s \ (\x\s. \y\s. \u v. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s)" lemma affine_alt: "affine s \ (\x\s. \y\s. \u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \ s)" unfolding affine_def by (metis eq_diff_eq') lemma affine_empty [iff]: "affine {}" unfolding affine_def by auto lemma affine_sing [iff]: "affine {x}" unfolding affine_alt by (auto simp: scaleR_left_distrib [symmetric]) lemma affine_UNIV [iff]: "affine UNIV" unfolding affine_def by auto lemma affine_Inter [intro]: "(\s. s\f \ affine s) \ affine (\f)" unfolding affine_def by auto lemma affine_Int[intro]: "affine s \ affine t \ affine (s \ t)" unfolding affine_def by auto lemma affine_scaling: "affine s \ affine (image (\x. c *\<^sub>R x) s)" apply (clarsimp simp add: affine_def) apply (rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in image_eqI) apply (auto simp: algebra_simps) done lemma affine_affine_hull [simp]: "affine(affine hull s)" unfolding hull_def using affine_Inter[of "{t. affine t \ s \ t}"] by auto lemma affine_hull_eq[simp]: "(affine hull s = s) \ affine s" by (metis affine_affine_hull hull_same) lemma affine_hyperplane: "affine {x. a \ x = b}" by (simp add: affine_def algebra_simps) (metis distrib_right mult.left_neutral) subsubsection\<^marker>\tag unimportant\ \Some explicit formulations\ text "Formalized by Lars Schewe." lemma affine: fixes V::"'a::real_vector set" shows "affine V \ (\S u. finite S \ S \ {} \ S \ V \ sum u S = 1 \ (\x\S. u x *\<^sub>R x) \ V)" proof - have "u *\<^sub>R x + v *\<^sub>R y \ V" if "x \ V" "y \ V" "u + v = (1::real)" and *: "\S u. \finite S; S \ {}; S \ V; sum u S = 1\ \ (\x\S. u x *\<^sub>R x) \ V" for x y u v proof (cases "x = y") case True then show ?thesis using that by (metis scaleR_add_left scaleR_one) next case False then show ?thesis using that *[of "{x,y}" "\w. if w = x then u else v"] by auto qed moreover have "(\x\S. u x *\<^sub>R x) \ V" if *: "\x y u v. \x\V; y\V; u + v = 1\ \ u *\<^sub>R x + v *\<^sub>R y \ V" and "finite S" "S \ {}" "S \ V" "sum u S = 1" for S u proof - define n where "n = card S" consider "card S = 0" | "card S = 1" | "card S = 2" | "card S > 2" by linarith then show "(\x\S. u x *\<^sub>R x) \ V" proof cases assume "card S = 1" then obtain a where "S={a}" by (auto simp: card_Suc_eq) then show ?thesis using that by simp next assume "card S = 2" then obtain a b where "S = {a, b}" by (metis Suc_1 card_1_singletonE card_Suc_eq) then show ?thesis using *[of a b] that by (auto simp: sum_clauses(2)) next assume "card S > 2" then show ?thesis using that n_def proof (induct n arbitrary: u S) case 0 then show ?case by auto next case (Suc n u S) have "sum u S = card S" if "\ (\x\S. u x \ 1)" using that unfolding card_eq_sum by auto with Suc.prems obtain x where "x \ S" and x: "u x \ 1" by force have c: "card (S - {x}) = card S - 1" by (simp add: Suc.prems(3) \x \ S\) have "sum u (S - {x}) = 1 - u x" by (simp add: Suc.prems sum_diff1 \x \ S\) with x have eq1: "inverse (1 - u x) * sum u (S - {x}) = 1" by auto have inV: "(\y\S - {x}. (inverse (1 - u x) * u y) *\<^sub>R y) \ V" proof (cases "card (S - {x}) > 2") case True then have S: "S - {x} \ {}" "card (S - {x}) = n" using Suc.prems c by force+ show ?thesis proof (rule Suc.hyps) show "(\a\S - {x}. inverse (1 - u x) * u a) = 1" by (auto simp: eq1 sum_distrib_left[symmetric]) qed (use S Suc.prems True in auto) next case False then have "card (S - {x}) = Suc (Suc 0)" using Suc.prems c by auto then obtain a b where ab: "(S - {x}) = {a, b}" "a\b" unfolding card_Suc_eq by auto then show ?thesis using eq1 \S \ V\ by (auto simp: sum_distrib_left distrib_left intro!: Suc.prems(2)[of a b]) qed have "u x + (1 - u x) = 1 \ u x *\<^sub>R x + (1 - u x) *\<^sub>R ((\y\S - {x}. u y *\<^sub>R y) /\<^sub>R (1 - u x)) \ V" by (rule Suc.prems) (use \x \ S\ Suc.prems inV in \auto simp: scaleR_right.sum\) moreover have "(\a\S. u a *\<^sub>R a) = u x *\<^sub>R x + (\a\S - {x}. u a *\<^sub>R a)" by (meson Suc.prems(3) sum.remove \x \ S\) ultimately show "(\x\S. u x *\<^sub>R x) \ V" by (simp add: x) qed qed (use \S\{}\ \finite S\ in auto) qed ultimately show ?thesis unfolding affine_def by meson qed lemma affine_hull_explicit: "affine hull p = {y. \S u. finite S \ S \ {} \ S \ p \ sum u S = 1 \ sum (\v. u v *\<^sub>R v) S = y}" (is "_ = ?rhs") proof (rule hull_unique) show "p \ ?rhs" proof (intro subsetI CollectI exI conjI) show "\x. sum (\z. 1) {x} = 1" by auto qed auto show "?rhs \ T" if "p \ T" "affine T" for T using that unfolding affine by blast show "affine ?rhs" unfolding affine_def proof clarify fix u v :: real and sx ux sy uy assume uv: "u + v = 1" and x: "finite sx" "sx \ {}" "sx \ p" "sum ux sx = (1::real)" and y: "finite sy" "sy \ {}" "sy \ p" "sum uy sy = (1::real)" have **: "(sx \ sy) \ sx = sx" "(sx \ sy) \ sy = sy" by auto show "\S w. finite S \ S \ {} \ S \ p \ sum w S = 1 \ (\v\S. w v *\<^sub>R v) = u *\<^sub>R (\v\sx. ux v *\<^sub>R v) + v *\<^sub>R (\v\sy. uy v *\<^sub>R v)" proof (intro exI conjI) show "finite (sx \ sy)" using x y by auto show "sum (\i. (if i\sx then u * ux i else 0) + (if i\sy then v * uy i else 0)) (sx \ sy) = 1" using x y uv by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric] sum_distrib_left [symmetric] **) have "(\i\sx \ sy. ((if i \ sx then u * ux i else 0) + (if i \ sy then v * uy i else 0)) *\<^sub>R i) = (\i\sx. (u * ux i) *\<^sub>R i) + (\i\sy. (v * uy i) *\<^sub>R i)" using x y unfolding scaleR_left_distrib scaleR_zero_left if_smult by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric] **) also have "\ = u *\<^sub>R (\v\sx. ux v *\<^sub>R v) + v *\<^sub>R (\v\sy. uy v *\<^sub>R v)" unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] by blast finally show "(\i\sx \ sy. ((if i \ sx then u * ux i else 0) + (if i \ sy then v * uy i else 0)) *\<^sub>R i) = u *\<^sub>R (\v\sx. ux v *\<^sub>R v) + v *\<^sub>R (\v\sy. uy v *\<^sub>R v)" . qed (use x y in auto) qed qed lemma affine_hull_finite: assumes "finite S" shows "affine hull S = {y. \u. sum u S = 1 \ sum (\v. u v *\<^sub>R v) S = y}" proof - have *: "\h. sum h S = 1 \ (\v\S. h v *\<^sub>R v) = x" if "F \ S" "finite F" "F \ {}" and sum: "sum u F = 1" and x: "(\v\F. u v *\<^sub>R v) = x" for x F u proof - have "S \ F = F" using that by auto show ?thesis proof (intro exI conjI) show "(\x\S. if x \ F then u x else 0) = 1" by (metis (mono_tags, lifting) \S \ F = F\ assms sum.inter_restrict sum) show "(\v\S. (if v \ F then u v else 0) *\<^sub>R v) = x" by (simp add: if_smult cong: if_cong) (metis (no_types) \S \ F = F\ assms sum.inter_restrict x) qed qed show ?thesis unfolding affine_hull_explicit using assms by (fastforce dest: *) qed subsubsection\<^marker>\tag unimportant\ \Stepping theorems and hence small special cases\ lemma affine_hull_empty[simp]: "affine hull {} = {}" by simp lemma affine_hull_finite_step: fixes y :: "'a::real_vector" shows "finite S \ (\u. sum u (insert a S) = w \ sum (\x. u x *\<^sub>R x) (insert a S) = y) \ (\v u. sum u S = w - v \ sum (\x. u x *\<^sub>R x) S = y - v *\<^sub>R a)" (is "_ \ ?lhs = ?rhs") proof - assume fin: "finite S" show "?lhs = ?rhs" proof assume ?lhs then obtain u where u: "sum u (insert a S) = w \ (\x\insert a S. u x *\<^sub>R x) = y" by auto show ?rhs proof (cases "a \ S") case True then show ?thesis using u by (simp add: insert_absorb) (metis diff_zero real_vector.scale_zero_left) next case False show ?thesis by (rule exI [where x="u a"]) (use u fin False in auto) qed next assume ?rhs then obtain v u where vu: "sum u S = w - v" "(\x\S. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto have *: "\x M. (if x = a then v else M) *\<^sub>R x = (if x = a then v *\<^sub>R x else M *\<^sub>R x)" by auto show ?lhs proof (cases "a \ S") case True show ?thesis by (rule exI [where x="\x. (if x=a then v else 0) + u x"]) (simp add: True scaleR_left_distrib sum.distrib sum_clauses fin vu * cong: if_cong) next case False then show ?thesis apply (rule_tac x="\x. if x=a then v else u x" in exI) apply (simp add: vu sum_clauses(2)[OF fin] *) by (simp add: sum_delta_notmem(3) vu) qed qed qed lemma affine_hull_2: fixes a b :: "'a::real_vector" shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs") proof - have *: "\x y z. z = x - y \ y + z = (x::real)" "\x y z. z = x - y \ y + z = (x::'a)" by auto have "?lhs = {y. \u. sum u {a, b} = 1 \ (\v\{a, b}. u v *\<^sub>R v) = y}" using affine_hull_finite[of "{a,b}"] by auto also have "\ = {y. \v u. u b = 1 - v \ u b *\<^sub>R b = y - v *\<^sub>R a}" by (simp add: affine_hull_finite_step[of "{b}" a]) also have "\ = ?rhs" unfolding * by auto finally show ?thesis by auto qed lemma affine_hull_3: fixes a b c :: "'a::real_vector" shows "affine hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" proof - have *: "\x y z. z = x - y \ y + z = (x::real)" "\x y z. z = x - y \ y + z = (x::'a)" by auto show ?thesis apply (simp add: affine_hull_finite affine_hull_finite_step) unfolding * apply safe apply (metis add.assoc) apply (rule_tac x=u in exI, force) done qed lemma mem_affine: assumes "affine S" "x \ S" "y \ S" "u + v = 1" shows "u *\<^sub>R x + v *\<^sub>R y \ S" using assms affine_def[of S] by auto lemma mem_affine_3: assumes "affine S" "x \ S" "y \ S" "z \ S" "u + v + w = 1" shows "u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z \ S" proof - have "u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z \ affine hull {x, y, z}" using affine_hull_3[of x y z] assms by auto moreover have "affine hull {x, y, z} \ affine hull S" using hull_mono[of "{x, y, z}" "S"] assms by auto moreover have "affine hull S = S" using assms affine_hull_eq[of S] by auto ultimately show ?thesis by auto qed lemma mem_affine_3_minus: assumes "affine S" "x \ S" "y \ S" "z \ S" shows "x + v *\<^sub>R (y-z) \ S" using mem_affine_3[of S x y z 1 v "-v"] assms by (simp add: algebra_simps) corollary mem_affine_3_minus2: "\affine S; x \ S; y \ S; z \ S\ \ x - v *\<^sub>R (y-z) \ S" by (metis add_uminus_conv_diff mem_affine_3_minus real_vector.scale_minus_left) subsubsection\<^marker>\tag unimportant\ \Some relations between affine hull and subspaces\ lemma affine_hull_insert_subset_span: "affine hull (insert a S) \ {a + v| v . v \ span {x - a | x . x \ S}}" proof - have "\v T u. x = a + v \ (finite T \ T \ {x - a |x. x \ S} \ (\v\T. u v *\<^sub>R v) = v)" if "finite F" "F \ {}" "F \ insert a S" "sum u F = 1" "(\v\F. u v *\<^sub>R v) = x" for x F u proof - have *: "(\x. x - a) ` (F - {a}) \ {x - a |x. x \ S}" using that by auto show ?thesis proof (intro exI conjI) show "finite ((\x. x - a) ` (F - {a}))" by (simp add: that(1)) show "(\v\(\x. x - a) ` (F - {a}). u(v+a) *\<^sub>R v) = x-a" by (simp add: sum.reindex[unfolded inj_on_def] algebra_simps sum_subtractf scaleR_left.sum[symmetric] sum_diff1 that) qed (use \F \ insert a S\ in auto) qed then show ?thesis unfolding affine_hull_explicit span_explicit by blast qed lemma affine_hull_insert_span: assumes "a \ S" shows "affine hull (insert a S) = {a + v | v . v \ span {x - a | x. x \ S}}" proof - have *: "\G u. finite G \ G \ {} \ G \ insert a S \ sum u G = 1 \ (\v\G. u v *\<^sub>R v) = y" if "v \ span {x - a |x. x \ S}" "y = a + v" for y v proof - from that obtain T u where u: "finite T" "T \ {x - a |x. x \ S}" "a + (\v\T. u v *\<^sub>R v) = y" unfolding span_explicit by auto define F where "F = (\x. x + a) ` T" have F: "finite F" "F \ S" "(\v\F. u (v - a) *\<^sub>R (v - a)) = y - a" unfolding F_def using u by (auto simp: sum.reindex[unfolded inj_on_def]) have *: "F \ {a} = {}" "F \ - {a} = F" using F assms by auto show "\G u. finite G \ G \ {} \ G \ insert a S \ sum u G = 1 \ (\v\G. u v *\<^sub>R v) = y" apply (rule_tac x = "insert a F" in exI) apply (rule_tac x = "\x. if x=a then 1 - sum (\x. u (x - a)) F else u (x - a)" in exI) using assms F apply (auto simp: sum_clauses sum.If_cases if_smult sum_subtractf scaleR_left.sum algebra_simps *) done qed show ?thesis by (intro subset_antisym affine_hull_insert_subset_span) (auto simp: affine_hull_explicit dest!: *) qed lemma affine_hull_span: assumes "a \ S" shows "affine hull S = {a + v | v. v \ span {x - a | x. x \ S - {a}}}" using affine_hull_insert_span[of a "S - {a}", unfolded insert_Diff[OF assms]] by auto subsubsection\<^marker>\tag unimportant\ \Parallel affine sets\ definition affine_parallel :: "'a::real_vector set \ 'a::real_vector set \ bool" where "affine_parallel S T \ (\a. T = (\x. a + x) ` S)" lemma affine_parallel_expl_aux: fixes S T :: "'a::real_vector set" assumes "\x. x \ S \ a + x \ T" shows "T = (\x. a + x) ` S" proof - have "x \ ((\x. a + x) ` S)" if "x \ T" for x using that by (simp add: image_iff) (metis add.commute diff_add_cancel assms) moreover have "T \ (\x. a + x) ` S" using assms by auto ultimately show ?thesis by auto qed lemma affine_parallel_expl: "affine_parallel S T \ (\a. \x. x \ S \ a + x \ T)" by (auto simp add: affine_parallel_def) (use affine_parallel_expl_aux [of S _ T] in blast) lemma affine_parallel_reflex: "affine_parallel S S" unfolding affine_parallel_def using image_add_0 by blast lemma affine_parallel_commut: assumes "affine_parallel A B" shows "affine_parallel B A" proof - from assms obtain a where B: "B = (\x. a + x) ` A" unfolding affine_parallel_def by auto have [simp]: "(\x. x - a) = plus (- a)" by (simp add: fun_eq_iff) from B show ?thesis using translation_galois [of B a A] unfolding affine_parallel_def by blast qed lemma affine_parallel_assoc: assumes "affine_parallel A B" and "affine_parallel B C" shows "affine_parallel A C" proof - from assms obtain ab where "B = (\x. ab + x) ` A" unfolding affine_parallel_def by auto moreover from assms obtain bc where "C = (\x. bc + x) ` B" unfolding affine_parallel_def by auto ultimately show ?thesis using translation_assoc[of bc ab A] unfolding affine_parallel_def by auto qed lemma affine_translation_aux: fixes a :: "'a::real_vector" assumes "affine ((\x. a + x) ` S)" shows "affine S" proof - { fix x y u v assume xy: "x \ S" "y \ S" "(u :: real) + v = 1" then have "(a + x) \ ((\x. a + x) ` S)" "(a + y) \ ((\x. a + x) ` S)" by auto then have h1: "u *\<^sub>R (a + x) + v *\<^sub>R (a + y) \ (\x. a + x) ` S" using xy assms unfolding affine_def by auto have "u *\<^sub>R (a + x) + v *\<^sub>R (a + y) = (u + v) *\<^sub>R a + (u *\<^sub>R x + v *\<^sub>R y)" by (simp add: algebra_simps) also have "\ = a + (u *\<^sub>R x + v *\<^sub>R y)" using \u + v = 1\ by auto ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) \ (\x. a + x) ` S" using h1 by auto then have "u *\<^sub>R x + v *\<^sub>R y \ S" by auto } then show ?thesis unfolding affine_def by auto qed lemma affine_translation: "affine S \ affine ((+) a ` S)" for a :: "'a::real_vector" proof show "affine ((+) a ` S)" if "affine S" using that translation_assoc [of "- a" a S] by (auto intro: affine_translation_aux [of "- a" "((+) a ` S)"]) show "affine S" if "affine ((+) a ` S)" using that by (rule affine_translation_aux) qed lemma parallel_is_affine: fixes S T :: "'a::real_vector set" assumes "affine S" "affine_parallel S T" shows "affine T" proof - from assms obtain a where "T = (\x. a + x) ` S" unfolding affine_parallel_def by auto then show ?thesis using affine_translation assms by auto qed lemma subspace_imp_affine: "subspace s \ affine s" unfolding subspace_def affine_def by auto subsubsection\<^marker>\tag unimportant\ \Subspace parallel to an affine set\ lemma subspace_affine: "subspace S \ affine S \ 0 \ S" proof - have h0: "subspace S \ affine S \ 0 \ S" using subspace_imp_affine[of S] subspace_0 by auto { assume assm: "affine S \ 0 \ S" { fix c :: real fix x assume x: "x \ S" have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto moreover have "(1 - c) *\<^sub>R 0 + c *\<^sub>R x \ S" using affine_alt[of S] assm x by auto ultimately have "c *\<^sub>R x \ S" by auto } then have h1: "\c. \x \ S. c *\<^sub>R x \ S" by auto { fix x y assume xy: "x \ S" "y \ S" define u where "u = (1 :: real)/2" have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)" by auto moreover have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y" by (simp add: algebra_simps) moreover have "(1 - u) *\<^sub>R x + u *\<^sub>R y \ S" using affine_alt[of S] assm xy by auto ultimately have "(1/2) *\<^sub>R (x+y) \ S" using u_def by auto moreover have "x + y = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))" by auto ultimately have "x + y \ S" using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto } then have "\x \ S. \y \ S. x + y \ S" by auto then have "subspace S" using h1 assm unfolding subspace_def by auto } then show ?thesis using h0 by metis qed lemma affine_diffs_subspace: assumes "affine S" "a \ S" shows "subspace ((\x. (-a)+x) ` S)" proof - have [simp]: "(\x. x - a) = plus (- a)" by (simp add: fun_eq_iff) have "affine ((\x. (-a)+x) ` S)" using affine_translation assms by blast moreover have "0 \ ((\x. (-a)+x) ` S)" using assms exI[of "(\x. x\S \ -a+x = 0)" a] by auto ultimately show ?thesis using subspace_affine by auto qed lemma affine_diffs_subspace_subtract: "subspace ((\x. x - a) ` S)" if "affine S" "a \ S" using that affine_diffs_subspace [of _ a] by simp lemma parallel_subspace_explicit: assumes "affine S" and "a \ S" assumes "L \ {y. \x \ S. (-a) + x = y}" shows "subspace L \ affine_parallel S L" proof - from assms have "L = plus (- a) ` S" by auto then have par: "affine_parallel S L" unfolding affine_parallel_def .. then have "affine L" using assms parallel_is_affine by auto moreover have "0 \ L" using assms by auto ultimately show ?thesis using subspace_affine par by auto qed lemma parallel_subspace_aux: assumes "subspace A" and "subspace B" and "affine_parallel A B" shows "A \ B" proof - from assms obtain a where a: "\x. x \ A \ a + x \ B" using affine_parallel_expl[of A B] by auto then have "-a \ A" using assms subspace_0[of B] by auto then have "a \ A" using assms subspace_neg[of A "-a"] by auto then show ?thesis using assms a unfolding subspace_def by auto qed lemma parallel_subspace: assumes "subspace A" and "subspace B" and "affine_parallel A B" shows "A = B" proof show "A \ B" using assms parallel_subspace_aux by auto show "A \ B" using assms parallel_subspace_aux[of B A] affine_parallel_commut by auto qed lemma affine_parallel_subspace: assumes "affine S" "S \ {}" shows "\!L. subspace L \ affine_parallel S L" proof - have ex: "\L. subspace L \ affine_parallel S L" using assms parallel_subspace_explicit by auto { fix L1 L2 assume ass: "subspace L1 \ affine_parallel S L1" "subspace L2 \ affine_parallel S L2" then have "affine_parallel L1 L2" using affine_parallel_commut[of S L1] affine_parallel_assoc[of L1 S L2] by auto then have "L1 = L2" using ass parallel_subspace by auto } then show ?thesis using ex by auto qed subsection \Cones\ definition\<^marker>\tag important\ cone :: "'a::real_vector set \ bool" where "cone s \ (\x\s. \c\0. c *\<^sub>R x \ s)" lemma cone_empty[intro, simp]: "cone {}" unfolding cone_def by auto lemma cone_univ[intro, simp]: "cone UNIV" unfolding cone_def by auto lemma cone_Inter[intro]: "\s\f. cone s \ cone (\f)" unfolding cone_def by auto lemma subspace_imp_cone: "subspace S \ cone S" by (simp add: cone_def subspace_scale) subsubsection \Conic hull\ lemma cone_cone_hull: "cone (cone hull s)" unfolding hull_def by auto lemma cone_hull_eq: "cone hull s = s \ cone s" apply (rule hull_eq) using cone_Inter unfolding subset_eq apply auto done lemma mem_cone: assumes "cone S" "x \ S" "c \ 0" shows "c *\<^sub>R x \ S" using assms cone_def[of S] by auto lemma cone_contains_0: assumes "cone S" shows "S \ {} \ 0 \ S" proof - { assume "S \ {}" then obtain a where "a \ S" by auto then have "0 \ S" using assms mem_cone[of S a 0] by auto } then show ?thesis by auto qed lemma cone_0: "cone {0}" unfolding cone_def by auto lemma cone_Union[intro]: "(\s\f. cone s) \ cone (\f)" unfolding cone_def by blast lemma cone_iff: assumes "S \ {}" shows "cone S \ 0 \ S \ (\c. c > 0 \ ((*\<^sub>R) c) ` S = S)" proof - { assume "cone S" { fix c :: real assume "c > 0" { fix x assume "x \ S" then have "x \ ((*\<^sub>R) c) ` S" unfolding image_def using \cone S\ \c>0\ mem_cone[of S x "1/c"] exI[of "(\t. t \ S \ x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"] by auto } moreover { fix x assume "x \ ((*\<^sub>R) c) ` S" then have "x \ S" using \cone S\ \c > 0\ unfolding cone_def image_def \c > 0\ by auto } ultimately have "((*\<^sub>R) c) ` S = S" by blast } then have "0 \ S \ (\c. c > 0 \ ((*\<^sub>R) c) ` S = S)" using \cone S\ cone_contains_0[of S] assms by auto } moreover { assume a: "0 \ S \ (\c. c > 0 \ ((*\<^sub>R) c) ` S = S)" { fix x assume "x \ S" fix c1 :: real assume "c1 \ 0" then have "c1 = 0 \ c1 > 0" by auto then have "c1 *\<^sub>R x \ S" using a \x \ S\ by auto } then have "cone S" unfolding cone_def by auto } ultimately show ?thesis by blast qed lemma cone_hull_empty: "cone hull {} = {}" by (metis cone_empty cone_hull_eq) lemma cone_hull_empty_iff: "S = {} \ cone hull S = {}" by (metis bot_least cone_hull_empty hull_subset xtrans(5)) lemma cone_hull_contains_0: "S \ {} \ 0 \ cone hull S" using cone_cone_hull[of S] cone_contains_0[of "cone hull S"] cone_hull_empty_iff[of S] by auto lemma mem_cone_hull: assumes "x \ S" "c \ 0" shows "c *\<^sub>R x \ cone hull S" by (metis assms cone_cone_hull hull_inc mem_cone) proposition cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \ 0 \ x \ S}" (is "?lhs = ?rhs") proof - { fix x assume "x \ ?rhs" then obtain cx :: real and xx where x: "x = cx *\<^sub>R xx" "cx \ 0" "xx \ S" by auto fix c :: real assume c: "c \ 0" then have "c *\<^sub>R x = (c * cx) *\<^sub>R xx" using x by (simp add: algebra_simps) moreover have "c * cx \ 0" using c x by auto ultimately have "c *\<^sub>R x \ ?rhs" using x by auto } then have "cone ?rhs" unfolding cone_def by auto then have "?rhs \ Collect cone" unfolding mem_Collect_eq by auto { fix x assume "x \ S" then have "1 *\<^sub>R x \ ?rhs" apply auto apply (rule_tac x = 1 in exI, auto) done then have "x \ ?rhs" by auto } then have "S \ ?rhs" by auto then have "?lhs \ ?rhs" using \?rhs \ Collect cone\ hull_minimal[of S "?rhs" "cone"] by auto moreover { fix x assume "x \ ?rhs" then obtain cx :: real and xx where x: "x = cx *\<^sub>R xx" "cx \ 0" "xx \ S" by auto then have "xx \ cone hull S" using hull_subset[of S] by auto then have "x \ ?lhs" using x cone_cone_hull[of S] cone_def[of "cone hull S"] by auto } ultimately show ?thesis by auto qed subsection \Affine dependence and consequential theorems\ text "Formalized by Lars Schewe." definition\<^marker>\tag important\ affine_dependent :: "'a::real_vector set \ bool" where "affine_dependent s \ (\x\s. x \ affine hull (s - {x}))" lemma affine_dependent_subset: "\affine_dependent s; s \ t\ \ affine_dependent t" apply (simp add: affine_dependent_def Bex_def) apply (blast dest: hull_mono [OF Diff_mono [OF _ subset_refl]]) done lemma affine_independent_subset: shows "\\ affine_dependent t; s \ t\ \ \ affine_dependent s" by (metis affine_dependent_subset) lemma affine_independent_Diff: "\ affine_dependent s \ \ affine_dependent(s - t)" by (meson Diff_subset affine_dependent_subset) proposition affine_dependent_explicit: "affine_dependent p \ (\S u. finite S \ S \ p \ sum u S = 0 \ (\v\S. u v \ 0) \ sum (\v. u v *\<^sub>R v) S = 0)" proof - have "\S u. finite S \ S \ p \ sum u S = 0 \ (\v\S. u v \ 0) \ (\w\S. u w *\<^sub>R w) = 0" if "(\w\S. u w *\<^sub>R w) = x" "x \ p" "finite S" "S \ {}" "S \ p - {x}" "sum u S = 1" for x S u proof (intro exI conjI) have "x \ S" using that by auto then show "(\v \ insert x S. if v = x then - 1 else u v) = 0" using that by (simp add: sum_delta_notmem) show "(\w \ insert x S. (if w = x then - 1 else u w) *\<^sub>R w) = 0" using that \x \ S\ by (simp add: if_smult sum_delta_notmem cong: if_cong) qed (use that in auto) moreover have "\x\p. \S u. finite S \ S \ {} \ S \ p - {x} \ sum u S = 1 \ (\v\S. u v *\<^sub>R v) = x" if "(\v\S. u v *\<^sub>R v) = 0" "finite S" "S \ p" "sum u S = 0" "v \ S" "u v \ 0" for S u v proof (intro bexI exI conjI) have "S \ {v}" using that by auto then show "S - {v} \ {}" using that by auto show "(\x \ S - {v}. - (1 / u v) * u x) = 1" unfolding sum_distrib_left[symmetric] sum_diff1[OF \finite S\] by (simp add: that) show "(\x\S - {v}. (- (1 / u v) * u x) *\<^sub>R x) = v" unfolding sum_distrib_left [symmetric] scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] sum_diff1[OF \finite S\] using that by auto show "S - {v} \ p - {v}" using that by auto qed (use that in auto) ultimately show ?thesis unfolding affine_dependent_def affine_hull_explicit by auto qed lemma affine_dependent_explicit_finite: fixes S :: "'a::real_vector set" assumes "finite S" shows "affine_dependent S \ (\u. sum u S = 0 \ (\v\S. u v \ 0) \ sum (\v. u v *\<^sub>R v) S = 0)" (is "?lhs = ?rhs") proof have *: "\vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else 0::'a)" by auto assume ?lhs then obtain t u v where "finite t" "t \ S" "sum u t = 0" "v\t" "u v \ 0" "(\v\t. u v *\<^sub>R v) = 0" unfolding affine_dependent_explicit by auto then show ?rhs apply (rule_tac x="\x. if x\t then u x else 0" in exI) apply (auto simp: * sum.inter_restrict[OF assms, symmetric] Int_absorb1[OF \t\S\]) done next assume ?rhs then obtain u v where "sum u S = 0" "v\S" "u v \ 0" "(\v\S. u v *\<^sub>R v) = 0" by auto then show ?lhs unfolding affine_dependent_explicit using assms by auto qed subsection\<^marker>\tag unimportant\ \Connectedness of convex sets\ lemma connectedD: "connected S \ open A \ open B \ S \ A \ B \ A \ B \ S = {} \ A \ S = {} \ B \ S = {}" by (rule Topological_Spaces.topological_space_class.connectedD) lemma convex_connected: fixes S :: "'a::real_normed_vector set" assumes "convex S" shows "connected S" proof (rule connectedI) fix A B assume "open A" "open B" "A \ B \ S = {}" "S \ A \ B" moreover assume "A \ S \ {}" "B \ S \ {}" then obtain a b where a: "a \ A" "a \ S" and b: "b \ B" "b \ S" by auto define f where [abs_def]: "f u = u *\<^sub>R a + (1 - u) *\<^sub>R b" for u then have "continuous_on {0 .. 1} f" by (auto intro!: continuous_intros) then have "connected (f ` {0 .. 1})" by (auto intro!: connected_continuous_image) note connectedD[OF this, of A B] moreover have "a \ A \ f ` {0 .. 1}" using a by (auto intro!: image_eqI[of _ _ 1] simp: f_def) moreover have "b \ B \ f ` {0 .. 1}" using b by (auto intro!: image_eqI[of _ _ 0] simp: f_def) moreover have "f ` {0 .. 1} \ S" using \convex S\ a b unfolding convex_def f_def by auto ultimately show False by auto qed corollary connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)" by (simp add: convex_connected) lemma convex_prod: assumes "\i. i \ Basis \ convex {x. P i x}" shows "convex {x. \i\Basis. P i (x\i)}" using assms unfolding convex_def by (auto simp: inner_add_left) lemma convex_positive_orthant: "convex {x::'a::euclidean_space. (\i\Basis. 0 \ x\i)}" by (rule convex_prod) (simp add: atLeast_def[symmetric] convex_real_interval) subsection \Convex hull\ lemma convex_convex_hull [iff]: "convex (convex hull s)" unfolding hull_def using convex_Inter[of "{t. convex t \ s \ t}"] by auto lemma convex_hull_subset: "s \ convex hull t \ convex hull s \ convex hull t" by (simp add: convex_convex_hull subset_hull) lemma convex_hull_eq: "convex hull s = s \ convex s" by (metis convex_convex_hull hull_same) subsubsection\<^marker>\tag unimportant\ \Convex hull is "preserved" by a linear function\ lemma convex_hull_linear_image: assumes f: "linear f" shows "f ` (convex hull s) = convex hull (f ` s)" proof show "convex hull (f ` s) \ f ` (convex hull s)" by (intro hull_minimal image_mono hull_subset convex_linear_image assms convex_convex_hull) show "f ` (convex hull s) \ convex hull (f ` s)" proof (unfold image_subset_iff_subset_vimage, rule hull_minimal) show "s \ f -` (convex hull (f ` s))" by (fast intro: hull_inc) show "convex (f -` (convex hull (f ` s)))" by (intro convex_linear_vimage [OF f] convex_convex_hull) qed qed lemma in_convex_hull_linear_image: assumes "linear f" and "x \ convex hull s" shows "f x \ convex hull (f ` s)" using convex_hull_linear_image[OF assms(1)] assms(2) by auto lemma convex_hull_Times: "convex hull (s \ t) = (convex hull s) \ (convex hull t)" proof show "convex hull (s \ t) \ (convex hull s) \ (convex hull t)" by (intro hull_minimal Sigma_mono hull_subset convex_Times convex_convex_hull) have "(x, y) \ convex hull (s \ t)" if x: "x \ convex hull s" and y: "y \ convex hull t" for x y proof (rule hull_induct [OF x], rule hull_induct [OF y]) fix x y assume "x \ s" and "y \ t" then show "(x, y) \ convex hull (s \ t)" by (simp add: hull_inc) next fix x let ?S = "((\y. (0, y)) -` (\p. (- x, 0) + p) ` (convex hull s \ t))" have "convex ?S" by (intro convex_linear_vimage convex_translation convex_convex_hull, simp add: linear_iff) also have "?S = {y. (x, y) \ convex hull (s \ t)}" by (auto simp: image_def Bex_def) finally show "convex {y. (x, y) \ convex hull (s \ t)}" . next show "convex {x. (x, y) \ convex hull s \ t}" proof - fix y let ?S = "((\x. (x, 0)) -` (\p. (0, - y) + p) ` (convex hull s \ t))" have "convex ?S" by (intro convex_linear_vimage convex_translation convex_convex_hull, simp add: linear_iff) also have "?S = {x. (x, y) \ convex hull (s \ t)}" by (auto simp: image_def Bex_def) finally show "convex {x. (x, y) \ convex hull (s \ t)}" . qed qed then show "(convex hull s) \ (convex hull t) \ convex hull (s \ t)" unfolding subset_eq split_paired_Ball_Sigma by blast qed subsubsection\<^marker>\tag unimportant\ \Stepping theorems for convex hulls of finite sets\ lemma convex_hull_empty[simp]: "convex hull {} = {}" by (rule hull_unique) auto lemma convex_hull_singleton[simp]: "convex hull {a} = {a}" by (rule hull_unique) auto lemma convex_hull_insert: fixes S :: "'a::real_vector set" assumes "S \ {}" shows "convex hull (insert a S) = {x. \u\0. \v\0. \b. (u + v = 1) \ b \ (convex hull S) \ (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "_ = ?hull") proof (intro equalityI hull_minimal subsetI) fix x assume "x \ insert a S" then have "\u\0. \v\0. u + v = 1 \ (\b. b \ convex hull S \ x = u *\<^sub>R a + v *\<^sub>R b)" unfolding insert_iff proof assume "x = a" then show ?thesis by (rule_tac x=1 in exI) (use assms hull_subset in fastforce) next assume "x \ S" with hull_subset[of S convex] show ?thesis by force qed then show "x \ ?hull" by simp next fix x assume "x \ ?hull" then obtain u v b where obt: "u\0" "v\0" "u + v = 1" "b \ convex hull S" "x = u *\<^sub>R a + v *\<^sub>R b" by auto have "a \ convex hull insert a S" "b \ convex hull insert a S" using hull_mono[of S "insert a S" convex] hull_mono[of "{a}" "insert a S" convex] and obt(4) by auto then show "x \ convex hull insert a S" unfolding obt(5) using obt(1-3) by (rule convexD [OF convex_convex_hull]) next show "convex ?hull" proof (rule convexI) fix x y u v assume as: "(0::real) \ u" "0 \ v" "u + v = 1" and x: "x \ ?hull" and y: "y \ ?hull" from x obtain u1 v1 b1 where obt1: "u1\0" "v1\0" "u1 + v1 = 1" "b1 \ convex hull S" and xeq: "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto from y obtain u2 v2 b2 where obt2: "u2\0" "v2\0" "u2 + v2 = 1" "b2 \ convex hull S" and yeq: "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto have *: "\(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp: algebra_simps) have "\b \ convex hull S. u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)" proof (cases "u * v1 + v * v2 = 0") case True have *: "\(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp: algebra_simps) have eq0: "u * v1 = 0" "v * v2 = 0" using True mult_nonneg_nonneg[OF \u\0\ \v1\0\] mult_nonneg_nonneg[OF \v\0\ \v2\0\] by arith+ then have "u * u1 + v * u2 = 1" using as(3) obt1(3) obt2(3) by auto then show ?thesis using "*" eq0 as obt1(4) xeq yeq by auto next case False have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)" using as(3) obt1(3) obt2(3) by (auto simp: field_simps) also have "\ = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)" using as(3) obt1(3) obt2(3) by (auto simp: field_simps) also have "\ = u * v1 + v * v2" by simp finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto let ?b = "((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" have zeroes: "0 \ u * v1 + v * v2" "0 \ u * v1" "0 \ u * v1 + v * v2" "0 \ v * v2" using as(1,2) obt1(1,2) obt2(1,2) by auto show ?thesis proof show "u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (?b - (u * u1) *\<^sub>R ?b - (v * u2) *\<^sub>R ?b)" unfolding xeq yeq * ** using False by (auto simp: scaleR_left_distrib scaleR_right_distrib) show "?b \ convex hull S" using False zeroes obt1(4) obt2(4) by (auto simp: convexD [OF convex_convex_hull] scaleR_left_distrib scaleR_right_distrib add_divide_distrib[symmetric] zero_le_divide_iff) qed qed then obtain b where b: "b \ convex hull S" "u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)" .. have u1: "u1 \ 1" unfolding obt1(3)[symmetric] and not_le using obt1(2) by auto have u2: "u2 \ 1" unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto have "u1 * u + u2 * v \ max u1 u2 * u + max u1 u2 * v" proof (rule add_mono) show "u1 * u \ max u1 u2 * u" "u2 * v \ max u1 u2 * v" by (simp_all add: as mult_right_mono) qed also have "\ \ 1" unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto finally have le1: "u1 * u + u2 * v \ 1" . show "u *\<^sub>R x + v *\<^sub>R y \ ?hull" proof (intro CollectI exI conjI) show "0 \ u * u1 + v * u2" by (simp add: as(1) as(2) obt1(1) obt2(1)) show "0 \ 1 - u * u1 - v * u2" by (simp add: le1 diff_diff_add mult.commute) qed (use b in \auto simp: algebra_simps\) qed qed lemma convex_hull_insert_alt: "convex hull (insert a S) = (if S = {} then {a} else {(1 - u) *\<^sub>R a + u *\<^sub>R x |x u. 0 \ u \ u \ 1 \ x \ convex hull S})" apply (auto simp: convex_hull_insert) using diff_eq_eq apply fastforce by (metis add.group_left_neutral add_le_imp_le_diff diff_add_cancel) subsubsection\<^marker>\tag unimportant\ \Explicit expression for convex hull\ proposition convex_hull_indexed: fixes S :: "'a::real_vector set" shows "convex hull S = {y. \k u x. (\i\{1::nat .. k}. 0 \ u i \ x i \ S) \ (sum u {1..k} = 1) \ (\i = 1..k. u i *\<^sub>R x i) = y}" (is "?xyz = ?hull") proof (rule hull_unique [OF _ convexI]) show "S \ ?hull" by (clarsimp, rule_tac x=1 in exI, rule_tac x="\x. 1" in exI, auto) next fix T assume "S \ T" "convex T" then show "?hull \ T" by (blast intro: convex_sum) next fix x y u v assume uv: "0 \ u" "0 \ v" "u + v = (1::real)" assume xy: "x \ ?hull" "y \ ?hull" from xy obtain k1 u1 x1 where x [rule_format]: "\i\{1::nat..k1}. 0\u1 i \ x1 i \ S" "sum u1 {Suc 0..k1} = 1" "(\i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x" by auto from xy obtain k2 u2 x2 where y [rule_format]: "\i\{1::nat..k2}. 0\u2 i \ x2 i \ S" "sum u2 {Suc 0..k2} = 1" "(\i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y" by auto have *: "\P (x::'a) y s t i. (if P i then s else t) *\<^sub>R (if P i then x else y) = (if P i then s *\<^sub>R x else t *\<^sub>R y)" "{1..k1 + k2} \ {1..k1} = {1..k1}" "{1..k1 + k2} \ - {1..k1} = (\i. i + k1) ` {1..k2}" by auto have inj: "inj_on (\i. i + k1) {1..k2}" unfolding inj_on_def by auto let ?uu = "\i. if i \ {1..k1} then u * u1 i else v * u2 (i - k1)" let ?xx = "\i. if i \ {1..k1} then x1 i else x2 (i - k1)" show "u *\<^sub>R x + v *\<^sub>R y \ ?hull" proof (intro CollectI exI conjI ballI) show "0 \ ?uu i" "?xx i \ S" if "i \ {1..k1+k2}" for i using that by (auto simp add: le_diff_conv uv(1) x(1) uv(2) y(1)) show "(\i = 1..k1 + k2. ?uu i) = 1" "(\i = 1..k1 + k2. ?uu i *\<^sub>R ?xx i) = u *\<^sub>R x + v *\<^sub>R y" unfolding * sum.If_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] sum.reindex[OF inj] Collect_mem_eq o_def unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] sum_distrib_left[symmetric] by (simp_all add: sum_distrib_left[symmetric] x(2,3) y(2,3) uv(3)) qed qed lemma convex_hull_finite: fixes S :: "'a::real_vector set" assumes "finite S" shows "convex hull S = {y. \u. (\x\S. 0 \ u x) \ sum u S = 1 \ sum (\x. u x *\<^sub>R x) S = y}" (is "?HULL = _") proof (rule hull_unique [OF _ convexI]; clarify) fix x assume "x \ S" then show "\u. (\x\S. 0 \ u x) \ sum u S = 1 \ (\x\S. u x *\<^sub>R x) = x" by (rule_tac x="\y. if x=y then 1 else 0" in exI) (auto simp: sum.delta'[OF assms] sum_delta''[OF assms]) next fix u v :: real assume uv: "0 \ u" "0 \ v" "u + v = 1" fix ux assume ux [rule_format]: "\x\S. 0 \ ux x" "sum ux S = (1::real)" fix uy assume uy [rule_format]: "\x\S. 0 \ uy x" "sum uy S = (1::real)" have "0 \ u * ux x + v * uy x" if "x\S" for x by (simp add: that uv ux(1) uy(1)) moreover have "(\x\S. u * ux x + v * uy x) = 1" unfolding sum.distrib and sum_distrib_left[symmetric] ux(2) uy(2) using uv(3) by auto moreover have "(\x\S. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\x\S. ux x *\<^sub>R x) + v *\<^sub>R (\x\S. uy x *\<^sub>R x)" unfolding scaleR_left_distrib sum.distrib scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] by auto ultimately show "\uc. (\x\S. 0 \ uc x) \ sum uc S = 1 \ (\x\S. uc x *\<^sub>R x) = u *\<^sub>R (\x\S. ux x *\<^sub>R x) + v *\<^sub>R (\x\S. uy x *\<^sub>R x)" by (rule_tac x="\x. u * ux x + v * uy x" in exI, auto) qed (use assms in \auto simp: convex_explicit\) subsubsection\<^marker>\tag unimportant\ \Another formulation\ text "Formalized by Lars Schewe." lemma convex_hull_explicit: fixes p :: "'a::real_vector set" shows "convex hull p = {y. \S u. finite S \ S \ p \ (\x\S. 0 \ u x) \ sum u S = 1 \ sum (\v. u v *\<^sub>R v) S = y}" (is "?lhs = ?rhs") proof - { fix x assume "x\?lhs" then obtain k u y where obt: "\i\{1::nat..k}. 0 \ u i \ y i \ p" "sum u {1..k} = 1" "(\i = 1..k. u i *\<^sub>R y i) = x" unfolding convex_hull_indexed by auto have fin: "finite {1..k}" by auto have fin': "\v. finite {i \ {1..k}. y i = v}" by auto { fix j assume "j\{1..k}" then have "y j \ p" "0 \ sum u {i. Suc 0 \ i \ i \ k \ y i = y j}" using obt(1)[THEN bspec[where x=j]] and obt(2) apply simp apply (rule sum_nonneg) using obt(1) apply auto done } moreover have "(\v\y ` {1..k}. sum u {i \ {1..k}. y i = v}) = 1" unfolding sum.image_gen[OF fin, symmetric] using obt(2) by auto moreover have "(\v\y ` {1..k}. sum u {i \ {1..k}. y i = v} *\<^sub>R v) = x" using sum.image_gen[OF fin, of "\i. u i *\<^sub>R y i" y, symmetric] unfolding scaleR_left.sum using obt(3) by auto ultimately have "\S u. finite S \ S \ p \ (\x\S. 0 \ u x) \ sum u S = 1 \ (\v\S. u v *\<^sub>R v) = x" apply (rule_tac x="y ` {1..k}" in exI) apply (rule_tac x="\v. sum u {i\{1..k}. y i = v}" in exI, auto) done then have "x\?rhs" by auto } moreover { fix y assume "y\?rhs" then obtain S u where obt: "finite S" "S \ p" "\x\S. 0 \ u x" "sum u S = 1" "(\v\S. u v *\<^sub>R v) = y" by auto obtain f where f: "inj_on f {1..card S}" "f ` {1..card S} = S" using ex_bij_betw_nat_finite_1[OF obt(1)] unfolding bij_betw_def by auto { fix i :: nat assume "i\{1..card S}" then have "f i \ S" using f(2) by blast then have "0 \ u (f i)" "f i \ p" using obt(2,3) by auto } moreover have *: "finite {1..card S}" by auto { fix y assume "y\S" then obtain i where "i\{1..card S}" "f i = y" using f using image_iff[of y f "{1..card S}"] by auto then have "{x. Suc 0 \ x \ x \ card S \ f x = y} = {i}" apply auto using f(1)[unfolded inj_on_def] by (metis One_nat_def atLeastAtMost_iff) then have "card {x. Suc 0 \ x \ x \ card S \ f x = y} = 1" by auto then have "(\x\{x \ {1..card S}. f x = y}. u (f x)) = u y" "(\x\{x \ {1..card S}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y" by (auto simp: sum_constant_scaleR) } then have "(\x = 1..card S. u (f x)) = 1" "(\i = 1..card S. u (f i) *\<^sub>R f i) = y" unfolding sum.image_gen[OF *(1), of "\x. u (f x) *\<^sub>R f x" f] and sum.image_gen[OF *(1), of "\x. u (f x)" f] unfolding f using sum.cong [of S S "\y. (\x\{x \ {1..card S}. f x = y}. u (f x) *\<^sub>R f x)" "\v. u v *\<^sub>R v"] using sum.cong [of S S "\y. (\x\{x \ {1..card S}. f x = y}. u (f x))" u] unfolding obt(4,5) by auto ultimately have "\k u x. (\i\{1..k}. 0 \ u i \ x i \ p) \ sum u {1..k} = 1 \ (\i::nat = 1..k. u i *\<^sub>R x i) = y" apply (rule_tac x="card S" in exI) apply (rule_tac x="u \ f" in exI) apply (rule_tac x=f in exI, fastforce) done then have "y \ ?lhs" unfolding convex_hull_indexed by auto } ultimately show ?thesis unfolding set_eq_iff by blast qed subsubsection\<^marker>\tag unimportant\ \A stepping theorem for that expansion\ lemma convex_hull_finite_step: fixes S :: "'a::real_vector set" assumes "finite S" shows "(\u. (\x\insert a S. 0 \ u x) \ sum u (insert a S) = w \ sum (\x. u x *\<^sub>R x) (insert a S) = y) \ (\v\0. \u. (\x\S. 0 \ u x) \ sum u S = w - v \ sum (\x. u x *\<^sub>R x) S = y - v *\<^sub>R a)" (is "?lhs = ?rhs") proof (rule, case_tac[!] "a\S") assume "a \ S" then have *: "insert a S = S" by auto assume ?lhs then show ?rhs unfolding * by (rule_tac x=0 in exI, auto) next assume ?lhs then obtain u where u: "\x\insert a S. 0 \ u x" "sum u (insert a S) = w" "(\x\insert a S. u x *\<^sub>R x) = y" by auto assume "a \ S" then show ?rhs apply (rule_tac x="u a" in exI) using u(1)[THEN bspec[where x=a]] apply simp apply (rule_tac x=u in exI) using u[unfolded sum_clauses(2)[OF assms]] and \a\S\ apply auto done next assume "a \ S" then have *: "insert a S = S" by auto have fin: "finite (insert a S)" using assms by auto assume ?rhs then obtain v u where uv: "v\0" "\x\S. 0 \ u x" "sum u S = w - v" "(\x\S. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto show ?lhs apply (rule_tac x = "\x. (if a = x then v else 0) + u x" in exI) unfolding scaleR_left_distrib and sum.distrib and sum_delta''[OF fin] and sum.delta'[OF fin] unfolding sum_clauses(2)[OF assms] using uv and uv(2)[THEN bspec[where x=a]] and \a\S\ apply auto done next assume ?rhs then obtain v u where uv: "v\0" "\x\S. 0 \ u x" "sum u S = w - v" "(\x\S. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto moreover assume "a \ S" moreover have "(\x\S. if a = x then v else u x) = sum u S" "(\x\S. (if a = x then v else u x) *\<^sub>R x) = (\x\S. u x *\<^sub>R x)" using \a \ S\ by (auto simp: intro!: sum.cong) ultimately show ?lhs by (rule_tac x="\x. if a = x then v else u x" in exI) (auto simp: sum_clauses(2)[OF assms]) qed subsubsection\<^marker>\tag unimportant\ \Hence some special cases\ lemma convex_hull_2: "convex hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b | u v. 0 \ u \ 0 \ v \ u + v = 1}" proof - have *: "\u. (\x\{a, b}. 0 \ u x) \ 0 \ u a \ 0 \ u b" by auto have **: "finite {b}" by auto show ?thesis apply (simp add: convex_hull_finite) unfolding convex_hull_finite_step[OF **, of a 1, unfolded * conj_assoc] apply auto apply (rule_tac x=v in exI) apply (rule_tac x="1 - v" in exI, simp) apply (rule_tac x=u in exI, simp) apply (rule_tac x="\x. v" in exI, simp) done qed lemma convex_hull_2_alt: "convex hull {a,b} = {a + u *\<^sub>R (b - a) | u. 0 \ u \ u \ 1}" unfolding convex_hull_2 proof (rule Collect_cong) have *: "\x y ::real. x + y = 1 \ x = 1 - y" by auto fix x show "(\v u. x = v *\<^sub>R a + u *\<^sub>R b \ 0 \ v \ 0 \ u \ v + u = 1) \ (\u. x = a + u *\<^sub>R (b - a) \ 0 \ u \ u \ 1)" unfolding * apply auto apply (rule_tac[!] x=u in exI) apply (auto simp: algebra_simps) done qed lemma convex_hull_3: "convex hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c | u v w. 0 \ u \ 0 \ v \ 0 \ w \ u + v + w = 1}" proof - have fin: "finite {a,b,c}" "finite {b,c}" "finite {c}" by auto have *: "\x y z ::real. x + y + z = 1 \ x = 1 - y - z" by (auto simp: field_simps) show ?thesis unfolding convex_hull_finite[OF fin(1)] and convex_hull_finite_step[OF fin(2)] and * unfolding convex_hull_finite_step[OF fin(3)] apply (rule Collect_cong, simp) apply auto apply (rule_tac x=va in exI) apply (rule_tac x="u c" in exI, simp) apply (rule_tac x="1 - v - w" in exI, simp) apply (rule_tac x=v in exI, simp) apply (rule_tac x="\x. w" in exI, simp) done qed lemma convex_hull_3_alt: "convex hull {a,b,c} = {a + u *\<^sub>R (b - a) + v *\<^sub>R (c - a) | u v. 0 \ u \ 0 \ v \ u + v \ 1}" proof - have *: "\x y z ::real. x + y + z = 1 \ x = 1 - y - z" by auto show ?thesis unfolding convex_hull_3 apply (auto simp: *) apply (rule_tac x=v in exI) apply (rule_tac x=w in exI) apply (simp add: algebra_simps) apply (rule_tac x=u in exI) apply (rule_tac x=v in exI) apply (simp add: algebra_simps) done qed subsection\<^marker>\tag unimportant\ \Relations among closure notions and corresponding hulls\ lemma affine_imp_convex: "affine s \ convex s" unfolding affine_def convex_def by auto lemma convex_affine_hull [simp]: "convex (affine hull S)" by (simp add: affine_imp_convex) lemma subspace_imp_convex: "subspace s \ convex s" using subspace_imp_affine affine_imp_convex by auto lemma affine_hull_subset_span: "(affine hull s) \ (span s)" by (metis hull_minimal span_superset subspace_imp_affine subspace_span) lemma convex_hull_subset_span: "(convex hull s) \ (span s)" by (metis hull_minimal span_superset subspace_imp_convex subspace_span) lemma convex_hull_subset_affine_hull: "(convex hull s) \ (affine hull s)" by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset) lemma affine_dependent_imp_dependent: "affine_dependent s \ dependent s" unfolding affine_dependent_def dependent_def using affine_hull_subset_span by auto lemma dependent_imp_affine_dependent: assumes "dependent {x - a| x . x \ s}" and "a \ s" shows "affine_dependent (insert a s)" proof - from assms(1)[unfolded dependent_explicit] obtain S u v where obt: "finite S" "S \ {x - a |x. x \ s}" "v\S" "u v \ 0" "(\v\S. u v *\<^sub>R v) = 0" by auto define t where "t = (\x. x + a) ` S" have inj: "inj_on (\x. x + a) S" unfolding inj_on_def by auto have "0 \ S" using obt(2) assms(2) unfolding subset_eq by auto have fin: "finite t" and "t \ s" unfolding t_def using obt(1,2) by auto then have "finite (insert a t)" and "insert a t \ insert a s" by auto moreover have *: "\P Q. (\x\t. (if x = a then P x else Q x)) = (\x\t. Q x)" apply (rule sum.cong) using \a\s\ \t\s\ apply auto done have "(\x\insert a t. if x = a then - (\x\t. u (x - a)) else u (x - a)) = 0" unfolding sum_clauses(2)[OF fin] * using \a\s\ \t\s\ by auto moreover have "\v\insert a t. (if v = a then - (\x\t. u (x - a)) else u (v - a)) \ 0" using obt(3,4) \0\S\ by (rule_tac x="v + a" in bexI) (auto simp: t_def) moreover have *: "\P Q. (\x\t. (if x = a then P x else Q x) *\<^sub>R x) = (\x\t. Q x *\<^sub>R x)" using \a\s\ \t\s\ by (auto intro!: sum.cong) have "(\x\t. u (x - a)) *\<^sub>R a = (\v\t. u (v - a) *\<^sub>R v)" unfolding scaleR_left.sum unfolding t_def and sum.reindex[OF inj] and o_def using obt(5) by (auto simp: sum.distrib scaleR_right_distrib) then have "(\v\insert a t. (if v = a then - (\x\t. u (x - a)) else u (v - a)) *\<^sub>R v) = 0" unfolding sum_clauses(2)[OF fin] using \a\s\ \t\s\ by (auto simp: *) ultimately show ?thesis unfolding affine_dependent_explicit apply (rule_tac x="insert a t" in exI, auto) done qed lemma convex_cone: "convex s \ cone s \ (\x\s. \y\s. (x + y) \ s) \ (\x\s. \c\0. (c *\<^sub>R x) \ s)" (is "?lhs = ?rhs") proof - { fix x y assume "x\s" "y\s" and ?lhs then have "2 *\<^sub>R x \s" "2 *\<^sub>R y \ s" unfolding cone_def by auto then have "x + y \ s" using \?lhs\[unfolded convex_def, THEN conjunct1] apply (erule_tac x="2*\<^sub>R x" in ballE) apply (erule_tac x="2*\<^sub>R y" in ballE) apply (erule_tac x="1/2" in allE, simp) apply (erule_tac x="1/2" in allE, auto) done } then show ?thesis unfolding convex_def cone_def by blast qed lemma affine_dependent_biggerset: fixes s :: "'a::euclidean_space set" assumes "finite s" "card s \ DIM('a) + 2" shows "affine_dependent s" proof - have "s \ {}" using assms by auto then obtain a where "a\s" by auto have *: "{x - a |x. x \ s - {a}} = (\x. x - a) ` (s - {a})" by auto have "card {x - a |x. x \ s - {a}} = card (s - {a})" unfolding * by (simp add: card_image inj_on_def) also have "\ > DIM('a)" using assms(2) unfolding card_Diff_singleton[OF assms(1) \a\s\] by auto finally show ?thesis apply (subst insert_Diff[OF \a\s\, symmetric]) apply (rule dependent_imp_affine_dependent) apply (rule dependent_biggerset, auto) done qed lemma affine_dependent_biggerset_general: assumes "finite (S :: 'a::euclidean_space set)" and "card S \ dim S + 2" shows "affine_dependent S" proof - from assms(2) have "S \ {}" by auto then obtain a where "a\S" by auto have *: "{x - a |x. x \ S - {a}} = (\x. x - a) ` (S - {a})" by auto have **: "card {x - a |x. x \ S - {a}} = card (S - {a})" by (metis (no_types, lifting) "*" card_image diff_add_cancel inj_on_def) have "dim {x - a |x. x \ S - {a}} \ dim S" using \a\S\ by (auto simp: span_base span_diff intro: subset_le_dim) also have "\ < dim S + 1" by auto also have "\ \ card (S - {a})" using assms using card_Diff_singleton[OF assms(1) \a\S\] by auto finally show ?thesis apply (subst insert_Diff[OF \a\S\, symmetric]) apply (rule dependent_imp_affine_dependent) apply (rule dependent_biggerset_general) unfolding ** apply auto done qed subsection\<^marker>\tag unimportant\ \Some Properties of Affine Dependent Sets\ lemma affine_independent_0 [simp]: "\ affine_dependent {}" by (simp add: affine_dependent_def) lemma affine_independent_1 [simp]: "\ affine_dependent {a}" by (simp add: affine_dependent_def) lemma affine_independent_2 [simp]: "\ affine_dependent {a,b}" by (simp add: affine_dependent_def insert_Diff_if hull_same) lemma affine_hull_translation: "affine hull ((\x. a + x) ` S) = (\x. a + x) ` (affine hull S)" proof - have "affine ((\x. a + x) ` (affine hull S))" using affine_translation affine_affine_hull by blast moreover have "(\x. a + x) ` S \ (\x. a + x) ` (affine hull S)" using hull_subset[of S] by auto ultimately have h1: "affine hull ((\x. a + x) ` S) \ (\x. a + x) ` (affine hull S)" by (metis hull_minimal) have "affine((\x. -a + x) ` (affine hull ((\x. a + x) ` S)))" using affine_translation affine_affine_hull by blast moreover have "(\x. -a + x) ` (\x. a + x) ` S \ (\x. -a + x) ` (affine hull ((\x. a + x) ` S))" using hull_subset[of "(\x. a + x) ` S"] by auto moreover have "S = (\x. -a + x) ` (\x. a + x) ` S" using translation_assoc[of "-a" a] by auto ultimately have "(\x. -a + x) ` (affine hull ((\x. a + x) ` S)) >= (affine hull S)" by (metis hull_minimal) then have "affine hull ((\x. a + x) ` S) >= (\x. a + x) ` (affine hull S)" by auto then show ?thesis using h1 by auto qed lemma affine_dependent_translation: assumes "affine_dependent S" shows "affine_dependent ((\x. a + x) ` S)" proof - obtain x where x: "x \ S \ x \ affine hull (S - {x})" using assms affine_dependent_def by auto have "(+) a ` (S - {x}) = (+) a ` S - {a + x}" by auto then have "a + x \ affine hull ((\x. a + x) ` S - {a + x})" using affine_hull_translation[of a "S - {x}"] x by auto moreover have "a + x \ (\x. a + x) ` S" using x by auto ultimately show ?thesis unfolding affine_dependent_def by auto qed lemma affine_dependent_translation_eq: "affine_dependent S \ affine_dependent ((\x. a + x) ` S)" proof - { assume "affine_dependent ((\x. a + x) ` S)" then have "affine_dependent S" using affine_dependent_translation[of "((\x. a + x) ` S)" "-a"] translation_assoc[of "-a" a] by auto } then show ?thesis using affine_dependent_translation by auto qed lemma affine_hull_0_dependent: assumes "0 \ affine hull S" shows "dependent S" proof - obtain s u where s_u: "finite s \ s \ {} \ s \ S \ sum u s = 1 \ (\v\s. u v *\<^sub>R v) = 0" using assms affine_hull_explicit[of S] by auto - then have "\v\s. u v \ 0" - using sum_not_0[of "u" "s"] by auto + then have "\v\s. u v \ 0" by auto then have "finite s \ s \ S \ (\v\s. u v \ 0 \ (\v\s. u v *\<^sub>R v) = 0)" using s_u by auto then show ?thesis unfolding dependent_explicit[of S] by auto qed lemma affine_dependent_imp_dependent2: assumes "affine_dependent (insert 0 S)" shows "dependent S" proof - obtain x where x: "x \ insert 0 S \ x \ affine hull (insert 0 S - {x})" using affine_dependent_def[of "(insert 0 S)"] assms by blast then have "x \ span (insert 0 S - {x})" using affine_hull_subset_span by auto moreover have "span (insert 0 S - {x}) = span (S - {x})" using insert_Diff_if[of "0" S "{x}"] span_insert_0[of "S-{x}"] by auto ultimately have "x \ span (S - {x})" by auto then have "x \ 0 \ dependent S" using x dependent_def by auto moreover { assume "x = 0" then have "0 \ affine hull S" using x hull_mono[of "S - {0}" S] by auto then have "dependent S" using affine_hull_0_dependent by auto } ultimately show ?thesis by auto qed lemma affine_dependent_iff_dependent: assumes "a \ S" shows "affine_dependent (insert a S) \ dependent ((\x. -a + x) ` S)" proof - have "((+) (- a) ` S) = {x - a| x . x \ S}" by auto then show ?thesis using affine_dependent_translation_eq[of "(insert a S)" "-a"] affine_dependent_imp_dependent2 assms dependent_imp_affine_dependent[of a S] by (auto simp del: uminus_add_conv_diff) qed lemma affine_dependent_iff_dependent2: assumes "a \ S" shows "affine_dependent S \ dependent ((\x. -a + x) ` (S-{a}))" proof - have "insert a (S - {a}) = S" using assms by auto then show ?thesis using assms affine_dependent_iff_dependent[of a "S-{a}"] by auto qed lemma affine_hull_insert_span_gen: "affine hull (insert a s) = (\x. a + x) ` span ((\x. - a + x) ` s)" proof - have h1: "{x - a |x. x \ s} = ((\x. -a+x) ` s)" by auto { assume "a \ s" then have ?thesis using affine_hull_insert_span[of a s] h1 by auto } moreover { assume a1: "a \ s" have "\x. x \ s \ -a+x=0" apply (rule exI[of _ a]) using a1 apply auto done then have "insert 0 ((\x. -a+x) ` (s - {a})) = (\x. -a+x) ` s" by auto then have "span ((\x. -a+x) ` (s - {a}))=span ((\x. -a+x) ` s)" using span_insert_0[of "(+) (- a) ` (s - {a})"] by (auto simp del: uminus_add_conv_diff) moreover have "{x - a |x. x \ (s - {a})} = ((\x. -a+x) ` (s - {a}))" by auto moreover have "insert a (s - {a}) = insert a s" by auto ultimately have ?thesis using affine_hull_insert_span[of "a" "s-{a}"] by auto } ultimately show ?thesis by auto qed lemma affine_hull_span2: assumes "a \ s" shows "affine hull s = (\x. a+x) ` span ((\x. -a+x) ` (s-{a}))" using affine_hull_insert_span_gen[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto lemma affine_hull_span_gen: assumes "a \ affine hull s" shows "affine hull s = (\x. a+x) ` span ((\x. -a+x) ` s)" proof - have "affine hull (insert a s) = affine hull s" using hull_redundant[of a affine s] assms by auto then show ?thesis using affine_hull_insert_span_gen[of a "s"] by auto qed lemma affine_hull_span_0: assumes "0 \ affine hull S" shows "affine hull S = span S" using affine_hull_span_gen[of "0" S] assms by auto lemma extend_to_affine_basis_nonempty: fixes S V :: "'n::euclidean_space set" assumes "\ affine_dependent S" "S \ V" "S \ {}" shows "\T. \ affine_dependent T \ S \ T \ T \ V \ affine hull T = affine hull V" proof - obtain a where a: "a \ S" using assms by auto then have h0: "independent ((\x. -a + x) ` (S-{a}))" using affine_dependent_iff_dependent2 assms by auto obtain B where B: "(\x. -a+x) ` (S - {a}) \ B \ B \ (\x. -a+x) ` V \ independent B \ (\x. -a+x) ` V \ span B" using assms by (blast intro: maximal_independent_subset_extend[OF _ h0, of "(\x. -a + x) ` V"]) define T where "T = (\x. a+x) ` insert 0 B" then have "T = insert a ((\x. a+x) ` B)" by auto then have "affine hull T = (\x. a+x) ` span B" using affine_hull_insert_span_gen[of a "((\x. a+x) ` B)"] translation_assoc[of "-a" a B] by auto then have "V \ affine hull T" using B assms translation_inverse_subset[of a V "span B"] by auto moreover have "T \ V" using T_def B a assms by auto ultimately have "affine hull T = affine hull V" by (metis Int_absorb1 Int_absorb2 hull_hull hull_mono) moreover have "S \ T" using T_def B translation_inverse_subset[of a "S-{a}" B] by auto moreover have "\ affine_dependent T" using T_def affine_dependent_translation_eq[of "insert 0 B"] affine_dependent_imp_dependent2 B by auto ultimately show ?thesis using \T \ V\ by auto qed lemma affine_basis_exists: fixes V :: "'n::euclidean_space set" shows "\B. B \ V \ \ affine_dependent B \ affine hull V = affine hull B" proof (cases "V = {}") case True then show ?thesis using affine_independent_0 by auto next case False then obtain x where "x \ V" by auto then show ?thesis using affine_dependent_def[of "{x}"] extend_to_affine_basis_nonempty[of "{x}" V] by auto qed proposition extend_to_affine_basis: fixes S V :: "'n::euclidean_space set" assumes "\ affine_dependent S" "S \ V" obtains T where "\ affine_dependent T" "S \ T" "T \ V" "affine hull T = affine hull V" proof (cases "S = {}") case True then show ?thesis using affine_basis_exists by (metis empty_subsetI that) next case False then show ?thesis by (metis assms extend_to_affine_basis_nonempty that) qed subsection \Affine Dimension of a Set\ definition\<^marker>\tag important\ aff_dim :: "('a::euclidean_space) set \ int" where "aff_dim V = (SOME d :: int. \B. affine hull B = affine hull V \ \ affine_dependent B \ of_nat (card B) = d + 1)" lemma aff_dim_basis_exists: fixes V :: "('n::euclidean_space) set" shows "\B. affine hull B = affine hull V \ \ affine_dependent B \ of_nat (card B) = aff_dim V + 1" proof - obtain B where "\ affine_dependent B \ affine hull B = affine hull V" using affine_basis_exists[of V] by auto then show ?thesis unfolding aff_dim_def some_eq_ex[of "\d. \B. affine hull B = affine hull V \ \ affine_dependent B \ of_nat (card B) = d + 1"] apply auto apply (rule exI[of _ "int (card B) - (1 :: int)"]) apply (rule exI[of _ "B"], auto) done qed lemma affine_hull_nonempty: "S \ {} \ affine hull S \ {}" proof - have "S = {} \ affine hull S = {}" using affine_hull_empty by auto moreover have "affine hull S = {} \ S = {}" unfolding hull_def by auto ultimately show ?thesis by blast qed lemma aff_dim_parallel_subspace_aux: fixes B :: "'n::euclidean_space set" assumes "\ affine_dependent B" "a \ B" shows "finite B \ ((card B) - 1 = dim (span ((\x. -a+x) ` (B-{a}))))" proof - have "independent ((\x. -a + x) ` (B-{a}))" using affine_dependent_iff_dependent2 assms by auto then have fin: "dim (span ((\x. -a+x) ` (B-{a}))) = card ((\x. -a + x) ` (B-{a}))" "finite ((\x. -a + x) ` (B - {a}))" using indep_card_eq_dim_span[of "(\x. -a+x) ` (B-{a})"] by auto show ?thesis proof (cases "(\x. -a + x) ` (B - {a}) = {}") case True have "B = insert a ((\x. a + x) ` (\x. -a + x) ` (B - {a}))" using translation_assoc[of "a" "-a" "(B - {a})"] assms by auto then have "B = {a}" using True by auto then show ?thesis using assms fin by auto next case False then have "card ((\x. -a + x) ` (B - {a})) > 0" using fin by auto moreover have h1: "card ((\x. -a + x) ` (B-{a})) = card (B-{a})" by (rule card_image) (use translate_inj_on in blast) ultimately have "card (B-{a}) > 0" by auto then have *: "finite (B - {a})" using card_gt_0_iff[of "(B - {a})"] by auto then have "card (B - {a}) = card B - 1" using card_Diff_singleton assms by auto with * show ?thesis using fin h1 by auto qed qed lemma aff_dim_parallel_subspace: fixes V L :: "'n::euclidean_space set" assumes "V \ {}" and "subspace L" and "affine_parallel (affine hull V) L" shows "aff_dim V = int (dim L)" proof - obtain B where B: "affine hull B = affine hull V \ \ affine_dependent B \ int (card B) = aff_dim V + 1" using aff_dim_basis_exists by auto then have "B \ {}" using assms B affine_hull_nonempty[of V] affine_hull_nonempty[of B] by auto then obtain a where a: "a \ B" by auto define Lb where "Lb = span ((\x. -a+x) ` (B-{a}))" moreover have "affine_parallel (affine hull B) Lb" using Lb_def B assms affine_hull_span2[of a B] a affine_parallel_commut[of "Lb" "(affine hull B)"] unfolding affine_parallel_def by auto moreover have "subspace Lb" using Lb_def subspace_span by auto moreover have "affine hull B \ {}" using assms B affine_hull_nonempty[of V] by auto ultimately have "L = Lb" using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B by auto then have "dim L = dim Lb" by auto moreover have "card B - 1 = dim Lb" and "finite B" using Lb_def aff_dim_parallel_subspace_aux a B by auto ultimately show ?thesis using B \B \ {}\ card_gt_0_iff[of B] by auto qed lemma aff_independent_finite: fixes B :: "'n::euclidean_space set" assumes "\ affine_dependent B" shows "finite B" proof - { assume "B \ {}" then obtain a where "a \ B" by auto then have ?thesis using aff_dim_parallel_subspace_aux assms by auto } then show ?thesis by auto qed lemmas independent_finite = independent_imp_finite lemma span_substd_basis: assumes d: "d \ Basis" shows "span d = {x. \i\Basis. i \ d \ x\i = 0}" (is "_ = ?B") proof - have "d \ ?B" using d by (auto simp: inner_Basis) moreover have s: "subspace ?B" using subspace_substandard[of "\i. i \ d"] . ultimately have "span d \ ?B" using span_mono[of d "?B"] span_eq_iff[of "?B"] by blast moreover have *: "card d \ dim (span d)" using independent_card_le_dim[of d "span d"] independent_substdbasis[OF assms] span_superset[of d] by auto moreover from * have "dim ?B \ dim (span d)" using dim_substandard[OF assms] by auto ultimately show ?thesis using s subspace_dim_equal[of "span d" "?B"] subspace_span[of d] by auto qed lemma basis_to_substdbasis_subspace_isomorphism: fixes B :: "'a::euclidean_space set" assumes "independent B" shows "\f d::'a set. card d = card B \ linear f \ f ` B = d \ f ` span B = {x. \i\Basis. i \ d \ x \ i = 0} \ inj_on f (span B) \ d \ Basis" proof - have B: "card B = dim B" using dim_unique[of B B "card B"] assms span_superset[of B] by auto have "dim B \ card (Basis :: 'a set)" using dim_subset_UNIV[of B] by simp from ex_card[OF this] obtain d :: "'a set" where d: "d \ Basis" and t: "card d = dim B" by auto let ?t = "{x::'a::euclidean_space. \i\Basis. i \ d \ x\i = 0}" have "\f. linear f \ f ` B = d \ f ` span B = ?t \ inj_on f (span B)" proof (intro basis_to_basis_subspace_isomorphism subspace_span subspace_substandard span_superset) show "d \ {x. \i\Basis. i \ d \ x \ i = 0}" using d inner_not_same_Basis by blast qed (auto simp: span_substd_basis independent_substdbasis dim_substandard d t B assms) with t \card B = dim B\ d show ?thesis by auto qed lemma aff_dim_empty: fixes S :: "'n::euclidean_space set" shows "S = {} \ aff_dim S = -1" proof - obtain B where *: "affine hull B = affine hull S" and "\ affine_dependent B" and "int (card B) = aff_dim S + 1" using aff_dim_basis_exists by auto moreover from * have "S = {} \ B = {}" using affine_hull_nonempty[of B] affine_hull_nonempty[of S] by auto ultimately show ?thesis using aff_independent_finite[of B] card_gt_0_iff[of B] by auto qed lemma aff_dim_empty_eq [simp]: "aff_dim ({}::'a::euclidean_space set) = -1" by (simp add: aff_dim_empty [symmetric]) lemma aff_dim_affine_hull [simp]: "aff_dim (affine hull S) = aff_dim S" unfolding aff_dim_def using hull_hull[of _ S] by auto lemma aff_dim_affine_hull2: assumes "affine hull S = affine hull T" shows "aff_dim S = aff_dim T" unfolding aff_dim_def using assms by auto lemma aff_dim_unique: fixes B V :: "'n::euclidean_space set" assumes "affine hull B = affine hull V \ \ affine_dependent B" shows "of_nat (card B) = aff_dim V + 1" proof (cases "B = {}") case True then have "V = {}" using affine_hull_nonempty[of V] affine_hull_nonempty[of B] assms by auto then have "aff_dim V = (-1::int)" using aff_dim_empty by auto then show ?thesis using \B = {}\ by auto next case False then obtain a where a: "a \ B" by auto define Lb where "Lb = span ((\x. -a+x) ` (B-{a}))" have "affine_parallel (affine hull B) Lb" using Lb_def affine_hull_span2[of a B] a affine_parallel_commut[of "Lb" "(affine hull B)"] unfolding affine_parallel_def by auto moreover have "subspace Lb" using Lb_def subspace_span by auto ultimately have "aff_dim B = int(dim Lb)" using aff_dim_parallel_subspace[of B Lb] \B \ {}\ by auto moreover have "(card B) - 1 = dim Lb" "finite B" using Lb_def aff_dim_parallel_subspace_aux a assms by auto ultimately have "of_nat (card B) = aff_dim B + 1" using \B \ {}\ card_gt_0_iff[of B] by auto then show ?thesis using aff_dim_affine_hull2 assms by auto qed lemma aff_dim_affine_independent: fixes B :: "'n::euclidean_space set" assumes "\ affine_dependent B" shows "of_nat (card B) = aff_dim B + 1" using aff_dim_unique[of B B] assms by auto lemma affine_independent_iff_card: fixes s :: "'a::euclidean_space set" shows "\ affine_dependent s \ finite s \ aff_dim s = int(card s) - 1" apply (rule iffI) apply (simp add: aff_dim_affine_independent aff_independent_finite) by (metis affine_basis_exists [of s] aff_dim_unique card_subset_eq diff_add_cancel of_nat_eq_iff) lemma aff_dim_sing [simp]: fixes a :: "'n::euclidean_space" shows "aff_dim {a} = 0" using aff_dim_affine_independent[of "{a}"] affine_independent_1 by auto lemma aff_dim_2 [simp]: "aff_dim {a,b} = (if a = b then 0 else 1)" proof (clarsimp) assume "a \ b" then have "aff_dim{a,b} = card{a,b} - 1" using affine_independent_2 [of a b] aff_dim_affine_independent by fastforce also have "\ = 1" using \a \ b\ by simp finally show "aff_dim {a, b} = 1" . qed lemma aff_dim_inner_basis_exists: fixes V :: "('n::euclidean_space) set" shows "\B. B \ V \ affine hull B = affine hull V \ \ affine_dependent B \ of_nat (card B) = aff_dim V + 1" proof - obtain B where B: "\ affine_dependent B" "B \ V" "affine hull B = affine hull V" using affine_basis_exists[of V] by auto then have "of_nat(card B) = aff_dim V+1" using aff_dim_unique by auto with B show ?thesis by auto qed lemma aff_dim_le_card: fixes V :: "'n::euclidean_space set" assumes "finite V" shows "aff_dim V \ of_nat (card V) - 1" proof - obtain B where B: "B \ V" "of_nat (card B) = aff_dim V + 1" using aff_dim_inner_basis_exists[of V] by auto then have "card B \ card V" using assms card_mono by auto with B show ?thesis by auto qed lemma aff_dim_parallel_eq: fixes S T :: "'n::euclidean_space set" assumes "affine_parallel (affine hull S) (affine hull T)" shows "aff_dim S = aff_dim T" proof - { assume "T \ {}" "S \ {}" then obtain L where L: "subspace L \ affine_parallel (affine hull T) L" using affine_parallel_subspace[of "affine hull T"] affine_affine_hull[of T] affine_hull_nonempty by auto then have "aff_dim T = int (dim L)" using aff_dim_parallel_subspace \T \ {}\ by auto moreover have *: "subspace L \ affine_parallel (affine hull S) L" using L affine_parallel_assoc[of "affine hull S" "affine hull T" L] assms by auto moreover from * have "aff_dim S = int (dim L)" using aff_dim_parallel_subspace \S \ {}\ by auto ultimately have ?thesis by auto } moreover { assume "S = {}" then have "S = {}" and "T = {}" using assms affine_hull_nonempty unfolding affine_parallel_def by auto then have ?thesis using aff_dim_empty by auto } moreover { assume "T = {}" then have "S = {}" and "T = {}" using assms affine_hull_nonempty unfolding affine_parallel_def by auto then have ?thesis using aff_dim_empty by auto } ultimately show ?thesis by blast qed lemma aff_dim_translation_eq: "aff_dim ((+) a ` S) = aff_dim S" for a :: "'n::euclidean_space" proof - have "affine_parallel (affine hull S) (affine hull ((\x. a + x) ` S))" unfolding affine_parallel_def apply (rule exI[of _ "a"]) using affine_hull_translation[of a S] apply auto done then show ?thesis using aff_dim_parallel_eq[of S "(\x. a + x) ` S"] by auto qed lemma aff_dim_translation_eq_subtract: "aff_dim ((\x. x - a) ` S) = aff_dim S" for a :: "'n::euclidean_space" using aff_dim_translation_eq [of "- a"] by (simp cong: image_cong_simp) lemma aff_dim_affine: fixes S L :: "'n::euclidean_space set" assumes "S \ {}" and "affine S" and "subspace L" and "affine_parallel S L" shows "aff_dim S = int (dim L)" proof - have *: "affine hull S = S" using assms affine_hull_eq[of S] by auto then have "affine_parallel (affine hull S) L" using assms by (simp add: *) then show ?thesis using assms aff_dim_parallel_subspace[of S L] by blast qed lemma dim_affine_hull: fixes S :: "'n::euclidean_space set" shows "dim (affine hull S) = dim S" proof - have "dim (affine hull S) \ dim S" using dim_subset by auto moreover have "dim (span S) \ dim (affine hull S)" using dim_subset affine_hull_subset_span by blast moreover have "dim (span S) = dim S" using dim_span by auto ultimately show ?thesis by auto qed lemma aff_dim_subspace: fixes S :: "'n::euclidean_space set" assumes "subspace S" shows "aff_dim S = int (dim S)" proof (cases "S={}") case True with assms show ?thesis by (simp add: subspace_affine) next case False with aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S] subspace_affine show ?thesis by auto qed lemma aff_dim_zero: fixes S :: "'n::euclidean_space set" assumes "0 \ affine hull S" shows "aff_dim S = int (dim S)" proof - have "subspace (affine hull S)" using subspace_affine[of "affine hull S"] affine_affine_hull assms by auto then have "aff_dim (affine hull S) = int (dim (affine hull S))" using assms aff_dim_subspace[of "affine hull S"] by auto then show ?thesis using aff_dim_affine_hull[of S] dim_affine_hull[of S] by auto qed lemma aff_dim_eq_dim: "aff_dim S = int (dim ((+) (- a) ` S))" if "a \ affine hull S" for S :: "'n::euclidean_space set" proof - have "0 \ affine hull (+) (- a) ` S" unfolding affine_hull_translation using that by (simp add: ac_simps) with aff_dim_zero show ?thesis by (metis aff_dim_translation_eq) qed lemma aff_dim_eq_dim_subtract: "aff_dim S = int (dim ((\x. x - a) ` S))" if "a \ affine hull S" for S :: "'n::euclidean_space set" using aff_dim_eq_dim [of a] that by (simp cong: image_cong_simp) lemma aff_dim_UNIV [simp]: "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))" using aff_dim_subspace[of "(UNIV :: 'n::euclidean_space set)"] dim_UNIV[where 'a="'n::euclidean_space"] by auto lemma aff_dim_geq: fixes V :: "'n::euclidean_space set" shows "aff_dim V \ -1" proof - obtain B where "affine hull B = affine hull V" and "\ affine_dependent B" and "int (card B) = aff_dim V + 1" using aff_dim_basis_exists by auto then show ?thesis by auto qed lemma aff_dim_negative_iff [simp]: fixes S :: "'n::euclidean_space set" shows "aff_dim S < 0 \S = {}" by (metis aff_dim_empty aff_dim_geq diff_0 eq_iff zle_diff1_eq) lemma aff_lowdim_subset_hyperplane: fixes S :: "'a::euclidean_space set" assumes "aff_dim S < DIM('a)" obtains a b where "a \ 0" "S \ {x. a \ x = b}" proof (cases "S={}") case True moreover have "(SOME b. b \ Basis) \ 0" by (metis norm_some_Basis norm_zero zero_neq_one) ultimately show ?thesis using that by blast next case False then obtain c S' where "c \ S'" "S = insert c S'" by (meson equals0I mk_disjoint_insert) have "dim ((+) (-c) ` S) < DIM('a)" by (metis \S = insert c S'\ aff_dim_eq_dim assms hull_inc insertI1 of_nat_less_imp_less) then obtain a where "a \ 0" "span ((+) (-c) ` S) \ {x. a \ x = 0}" using lowdim_subset_hyperplane by blast moreover have "a \ w = a \ c" if "span ((+) (- c) ` S) \ {x. a \ x = 0}" "w \ S" for w proof - have "w-c \ span ((+) (- c) ` S)" by (simp add: span_base \w \ S\) with that have "w-c \ {x. a \ x = 0}" by blast then show ?thesis by (auto simp: algebra_simps) qed ultimately have "S \ {x. a \ x = a \ c}" by blast then show ?thesis by (rule that[OF \a \ 0\]) qed lemma affine_independent_card_dim_diffs: fixes S :: "'a :: euclidean_space set" assumes "\ affine_dependent S" "a \ S" shows "card S = dim {x - a|x. x \ S} + 1" proof - have 1: "{b - a|b. b \ (S - {a})} \ {x - a|x. x \ S}" by auto have 2: "x - a \ span {b - a |b. b \ S - {a}}" if "x \ S" for x proof (cases "x = a") case True then show ?thesis by (simp add: span_clauses) next case False then show ?thesis using assms by (blast intro: span_base that) qed have "\ affine_dependent (insert a S)" by (simp add: assms insert_absorb) then have 3: "independent {b - a |b. b \ S - {a}}" using dependent_imp_affine_dependent by fastforce have "{b - a |b. b \ S - {a}} = (\b. b-a) ` (S - {a})" by blast then have "card {b - a |b. b \ S - {a}} = card ((\b. b-a) ` (S - {a}))" by simp also have "\ = card (S - {a})" by (metis (no_types, lifting) card_image diff_add_cancel inj_onI) also have "\ = card S - 1" by (simp add: aff_independent_finite assms) finally have 4: "card {b - a |b. b \ S - {a}} = card S - 1" . have "finite S" by (meson assms aff_independent_finite) with \a \ S\ have "card S \ 0" by auto moreover have "dim {x - a |x. x \ S} = card S - 1" using 2 by (blast intro: dim_unique [OF 1 _ 3 4]) ultimately show ?thesis by auto qed lemma independent_card_le_aff_dim: fixes B :: "'n::euclidean_space set" assumes "B \ V" assumes "\ affine_dependent B" shows "int (card B) \ aff_dim V + 1" proof - obtain T where T: "\ affine_dependent T \ B \ T \ T \ V \ affine hull T = affine hull V" by (metis assms extend_to_affine_basis[of B V]) then have "of_nat (card T) = aff_dim V + 1" using aff_dim_unique by auto then show ?thesis using T card_mono[of T B] aff_independent_finite[of T] by auto qed lemma aff_dim_subset: fixes S T :: "'n::euclidean_space set" assumes "S \ T" shows "aff_dim S \ aff_dim T" proof - obtain B where B: "\ affine_dependent B" "B \ S" "affine hull B = affine hull S" "of_nat (card B) = aff_dim S + 1" using aff_dim_inner_basis_exists[of S] by auto then have "int (card B) \ aff_dim T + 1" using assms independent_card_le_aff_dim[of B T] by auto with B show ?thesis by auto qed lemma aff_dim_le_DIM: fixes S :: "'n::euclidean_space set" shows "aff_dim S \ int (DIM('n))" proof - have "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))" using aff_dim_UNIV by auto then show "aff_dim (S:: 'n::euclidean_space set) \ int(DIM('n))" using aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto qed lemma affine_dim_equal: fixes S :: "'n::euclidean_space set" assumes "affine S" "affine T" "S \ {}" "S \ T" "aff_dim S = aff_dim T" shows "S = T" proof - obtain a where "a \ S" using assms by auto then have "a \ T" using assms by auto define LS where "LS = {y. \x \ S. (-a) + x = y}" then have ls: "subspace LS" "affine_parallel S LS" using assms parallel_subspace_explicit[of S a LS] \a \ S\ by auto then have h1: "int(dim LS) = aff_dim S" using assms aff_dim_affine[of S LS] by auto have "T \ {}" using assms by auto define LT where "LT = {y. \x \ T. (-a) + x = y}" then have lt: "subspace LT \ affine_parallel T LT" using assms parallel_subspace_explicit[of T a LT] \a \ T\ by auto then have "int(dim LT) = aff_dim T" using assms aff_dim_affine[of T LT] \T \ {}\ by auto then have "dim LS = dim LT" using h1 assms by auto moreover have "LS \ LT" using LS_def LT_def assms by auto ultimately have "LS = LT" using subspace_dim_equal[of LS LT] ls lt by auto moreover have "S = {x. \y \ LS. a+y=x}" using LS_def by auto moreover have "T = {x. \y \ LT. a+y=x}" using LT_def by auto ultimately show ?thesis by auto qed lemma aff_dim_eq_0: fixes S :: "'a::euclidean_space set" shows "aff_dim S = 0 \ (\a. S = {a})" proof (cases "S = {}") case True then show ?thesis by auto next case False then obtain a where "a \ S" by auto show ?thesis proof safe assume 0: "aff_dim S = 0" have "\ {a,b} \ S" if "b \ a" for b by (metis "0" aff_dim_2 aff_dim_subset not_one_le_zero that) then show "\a. S = {a}" using \a \ S\ by blast qed auto qed lemma affine_hull_UNIV: fixes S :: "'n::euclidean_space set" assumes "aff_dim S = int(DIM('n))" shows "affine hull S = (UNIV :: ('n::euclidean_space) set)" proof - have "S \ {}" using assms aff_dim_empty[of S] by auto have h0: "S \ affine hull S" using hull_subset[of S _] by auto have h1: "aff_dim (UNIV :: ('n::euclidean_space) set) = aff_dim S" using aff_dim_UNIV assms by auto then have h2: "aff_dim (affine hull S) \ aff_dim (UNIV :: ('n::euclidean_space) set)" using aff_dim_le_DIM[of "affine hull S"] assms h0 by auto have h3: "aff_dim S \ aff_dim (affine hull S)" using h0 aff_dim_subset[of S "affine hull S"] assms by auto then have h4: "aff_dim (affine hull S) = aff_dim (UNIV :: ('n::euclidean_space) set)" using h0 h1 h2 by auto then show ?thesis using affine_dim_equal[of "affine hull S" "(UNIV :: ('n::euclidean_space) set)"] affine_affine_hull[of S] affine_UNIV assms h4 h0 \S \ {}\ by auto qed lemma disjoint_affine_hull: fixes s :: "'n::euclidean_space set" assumes "\ affine_dependent s" "t \ s" "u \ s" "t \ u = {}" shows "(affine hull t) \ (affine hull u) = {}" proof - have "finite s" using assms by (simp add: aff_independent_finite) then have "finite t" "finite u" using assms finite_subset by blast+ { fix y assume yt: "y \ affine hull t" and yu: "y \ affine hull u" then obtain a b where a1 [simp]: "sum a t = 1" and [simp]: "sum (\v. a v *\<^sub>R v) t = y" and [simp]: "sum b u = 1" "sum (\v. b v *\<^sub>R v) u = y" by (auto simp: affine_hull_finite \finite t\ \finite u\) define c where "c x = (if x \ t then a x else if x \ u then -(b x) else 0)" for x have [simp]: "s \ t = t" "s \ - t \ u = u" using assms by auto have "sum c s = 0" by (simp add: c_def comm_monoid_add_class.sum.If_cases \finite s\ sum_negf) moreover have "\ (\v\s. c v = 0)" - by (metis (no_types) IntD1 \s \ t = t\ a1 c_def sum_not_0 zero_neq_one) + by (metis (no_types) IntD1 \s \ t = t\ a1 c_def sum.neutral zero_neq_one) moreover have "(\v\s. c v *\<^sub>R v) = 0" by (simp add: c_def if_smult sum_negf comm_monoid_add_class.sum.If_cases \finite s\) ultimately have False using assms \finite s\ by (auto simp: affine_dependent_explicit) } then show ?thesis by blast qed lemma aff_dim_convex_hull: fixes S :: "'n::euclidean_space set" shows "aff_dim (convex hull S) = aff_dim S" using aff_dim_affine_hull[of S] convex_hull_subset_affine_hull[of S] hull_subset[of S "convex"] aff_dim_subset[of S "convex hull S"] aff_dim_subset[of "convex hull S" "affine hull S"] by auto subsection \Caratheodory's theorem\ lemma convex_hull_caratheodory_aff_dim: fixes p :: "('a::euclidean_space) set" shows "convex hull p = {y. \s u. finite s \ s \ p \ card s \ aff_dim p + 1 \ (\x\s. 0 \ u x) \ sum u s = 1 \ sum (\v. u v *\<^sub>R v) s = y}" unfolding convex_hull_explicit set_eq_iff mem_Collect_eq proof (intro allI iffI) fix y let ?P = "\n. \s u. finite s \ card s = n \ s \ p \ (\x\s. 0 \ u x) \ sum u s = 1 \ (\v\s. u v *\<^sub>R v) = y" assume "\s u. finite s \ s \ p \ (\x\s. 0 \ u x) \ sum u s = 1 \ (\v\s. u v *\<^sub>R v) = y" then obtain N where "?P N" by auto then have "\n\N. (\k ?P k) \ ?P n" apply (rule_tac ex_least_nat_le, auto) done then obtain n where "?P n" and smallest: "\k ?P k" by blast then obtain s u where obt: "finite s" "card s = n" "s\p" "\x\s. 0 \ u x" "sum u s = 1" "(\v\s. u v *\<^sub>R v) = y" by auto have "card s \ aff_dim p + 1" proof (rule ccontr, simp only: not_le) assume "aff_dim p + 1 < card s" then have "affine_dependent s" using affine_dependent_biggerset[OF obt(1)] independent_card_le_aff_dim not_less obt(3) by blast then obtain w v where wv: "sum w s = 0" "v\s" "w v \ 0" "(\v\s. w v *\<^sub>R v) = 0" using affine_dependent_explicit_finite[OF obt(1)] by auto define i where "i = (\v. (u v) / (- w v)) ` {v\s. w v < 0}" define t where "t = Min i" have "\x\s. w x < 0" proof (rule ccontr, simp add: not_less) assume as:"\x\s. 0 \ w x" then have "sum w (s - {v}) \ 0" apply (rule_tac sum_nonneg, auto) done then have "sum w s > 0" unfolding sum.remove[OF obt(1) \v\s\] using as[THEN bspec[where x=v]] \v\s\ \w v \ 0\ by auto then show False using wv(1) by auto qed then have "i \ {}" unfolding i_def by auto then have "t \ 0" using Min_ge_iff[of i 0 ] and obt(1) unfolding t_def i_def using obt(4)[unfolded le_less] by (auto simp: divide_le_0_iff) have t: "\v\s. u v + t * w v \ 0" proof fix v assume "v \ s" then have v: "0 \ u v" using obt(4)[THEN bspec[where x=v]] by auto show "0 \ u v + t * w v" proof (cases "w v < 0") case False thus ?thesis using v \t\0\ by auto next case True then have "t \ u v / (- w v)" using \v\s\ unfolding t_def i_def apply (rule_tac Min_le) using obt(1) apply auto done then show ?thesis unfolding real_0_le_add_iff using pos_le_divide_eq[OF True[unfolded neg_0_less_iff_less[symmetric]]] by auto qed qed obtain a where "a \ s" and "t = (\v. (u v) / (- w v)) a" and "w a < 0" using Min_in[OF _ \i\{}\] and obt(1) unfolding i_def t_def by auto then have a: "a \ s" "u a + t * w a = 0" by auto have *: "\f. sum f (s - {a}) = sum f s - ((f a)::'b::ab_group_add)" unfolding sum.remove[OF obt(1) \a\s\] by auto have "(\v\s. u v + t * w v) = 1" unfolding sum.distrib wv(1) sum_distrib_left[symmetric] obt(5) by auto moreover have "(\v\s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y" unfolding sum.distrib obt(6) scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] wv(4) using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]] by simp ultimately have "?P (n - 1)" apply (rule_tac x="(s - {a})" in exI) apply (rule_tac x="\v. u v + t * w v" in exI) using obt(1-3) and t and a apply (auto simp: * scaleR_left_distrib) done then show False using smallest[THEN spec[where x="n - 1"]] by auto qed then show "\s u. finite s \ s \ p \ card s \ aff_dim p + 1 \ (\x\s. 0 \ u x) \ sum u s = 1 \ (\v\s. u v *\<^sub>R v) = y" using obt by auto qed auto lemma caratheodory_aff_dim: fixes p :: "('a::euclidean_space) set" shows "convex hull p = {x. \s. finite s \ s \ p \ card s \ aff_dim p + 1 \ x \ convex hull s}" (is "?lhs = ?rhs") proof show "?lhs \ ?rhs" apply (subst convex_hull_caratheodory_aff_dim, clarify) apply (rule_tac x=s in exI) apply (simp add: hull_subset convex_explicit [THEN iffD1, OF convex_convex_hull]) done next show "?rhs \ ?lhs" using hull_mono by blast qed lemma convex_hull_caratheodory: fixes p :: "('a::euclidean_space) set" shows "convex hull p = {y. \s u. finite s \ s \ p \ card s \ DIM('a) + 1 \ (\x\s. 0 \ u x) \ sum u s = 1 \ sum (\v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs") proof (intro set_eqI iffI) fix x assume "x \ ?lhs" then show "x \ ?rhs" apply (simp only: convex_hull_caratheodory_aff_dim Set.mem_Collect_eq) apply (erule ex_forward)+ using aff_dim_le_DIM [of p] apply simp done next fix x assume "x \ ?rhs" then show "x \ ?lhs" by (auto simp: convex_hull_explicit) qed theorem caratheodory: "convex hull p = {x::'a::euclidean_space. \s. finite s \ s \ p \ card s \ DIM('a) + 1 \ x \ convex hull s}" proof safe fix x assume "x \ convex hull p" then obtain s u where "finite s" "s \ p" "card s \ DIM('a) + 1" "\x\s. 0 \ u x" "sum u s = 1" "(\v\s. u v *\<^sub>R v) = x" unfolding convex_hull_caratheodory by auto then show "\s. finite s \ s \ p \ card s \ DIM('a) + 1 \ x \ convex hull s" apply (rule_tac x=s in exI) using hull_subset[of s convex] using convex_convex_hull[simplified convex_explicit, of s, THEN spec[where x=s], THEN spec[where x=u]] apply auto done next fix x s assume "finite s" "s \ p" "card s \ DIM('a) + 1" "x \ convex hull s" then show "x \ convex hull p" using hull_mono[OF \s\p\] by auto qed subsection\<^marker>\tag unimportant\\Some Properties of subset of standard basis\ lemma affine_hull_substd_basis: assumes "d \ Basis" shows "affine hull (insert 0 d) = {x::'a::euclidean_space. \i\Basis. i \ d \ x\i = 0}" (is "affine hull (insert 0 ?A) = ?B") proof - have *: "\A. (+) (0::'a) ` A = A" "\A. (+) (- (0::'a)) ` A = A" by auto show ?thesis unfolding affine_hull_insert_span_gen span_substd_basis[OF assms,symmetric] * .. qed lemma affine_hull_convex_hull [simp]: "affine hull (convex hull S) = affine hull S" by (metis Int_absorb1 Int_absorb2 convex_hull_subset_affine_hull hull_hull hull_mono hull_subset) subsection\<^marker>\tag unimportant\ \Moving and scaling convex hulls\ lemma convex_hull_set_plus: "convex hull (S + T) = convex hull S + convex hull T" unfolding set_plus_image apply (subst convex_hull_linear_image [symmetric]) apply (simp add: linear_iff scaleR_right_distrib) apply (simp add: convex_hull_Times) done lemma translation_eq_singleton_plus: "(\x. a + x) ` T = {a} + T" unfolding set_plus_def by auto lemma convex_hull_translation: "convex hull ((\x. a + x) ` S) = (\x. a + x) ` (convex hull S)" unfolding translation_eq_singleton_plus by (simp only: convex_hull_set_plus convex_hull_singleton) lemma convex_hull_scaling: "convex hull ((\x. c *\<^sub>R x) ` S) = (\x. c *\<^sub>R x) ` (convex hull S)" using linear_scaleR by (rule convex_hull_linear_image [symmetric]) lemma convex_hull_affinity: "convex hull ((\x. a + c *\<^sub>R x) ` S) = (\x. a + c *\<^sub>R x) ` (convex hull S)" by(simp only: image_image[symmetric] convex_hull_scaling convex_hull_translation) subsection\<^marker>\tag unimportant\ \Convexity of cone hulls\ lemma convex_cone_hull: assumes "convex S" shows "convex (cone hull S)" proof (rule convexI) fix x y assume xy: "x \ cone hull S" "y \ cone hull S" then have "S \ {}" using cone_hull_empty_iff[of S] by auto fix u v :: real assume uv: "u \ 0" "v \ 0" "u + v = 1" then have *: "u *\<^sub>R x \ cone hull S" "v *\<^sub>R y \ cone hull S" using cone_cone_hull[of S] xy cone_def[of "cone hull S"] by auto from * obtain cx :: real and xx where x: "u *\<^sub>R x = cx *\<^sub>R xx" "cx \ 0" "xx \ S" using cone_hull_expl[of S] by auto from * obtain cy :: real and yy where y: "v *\<^sub>R y = cy *\<^sub>R yy" "cy \ 0" "yy \ S" using cone_hull_expl[of S] by auto { assume "cx + cy \ 0" then have "u *\<^sub>R x = 0" and "v *\<^sub>R y = 0" using x y by auto then have "u *\<^sub>R x + v *\<^sub>R y = 0" by auto then have "u *\<^sub>R x + v *\<^sub>R y \ cone hull S" using cone_hull_contains_0[of S] \S \ {}\ by auto } moreover { assume "cx + cy > 0" then have "(cx / (cx + cy)) *\<^sub>R xx + (cy / (cx + cy)) *\<^sub>R yy \ S" using assms mem_convex_alt[of S xx yy cx cy] x y by auto then have "cx *\<^sub>R xx + cy *\<^sub>R yy \ cone hull S" using mem_cone_hull[of "(cx/(cx+cy)) *\<^sub>R xx + (cy/(cx+cy)) *\<^sub>R yy" S "cx+cy"] \cx+cy>0\ by (auto simp: scaleR_right_distrib) then have "u *\<^sub>R x + v *\<^sub>R y \ cone hull S" using x y by auto } moreover have "cx + cy \ 0 \ cx + cy > 0" by auto ultimately show "u *\<^sub>R x + v *\<^sub>R y \ cone hull S" by blast qed lemma cone_convex_hull: assumes "cone S" shows "cone (convex hull S)" proof (cases "S = {}") case True then show ?thesis by auto next case False then have *: "0 \ S \ (\c. c > 0 \ (*\<^sub>R) c ` S = S)" using cone_iff[of S] assms by auto { fix c :: real assume "c > 0" then have "(*\<^sub>R) c ` (convex hull S) = convex hull ((*\<^sub>R) c ` S)" using convex_hull_scaling[of _ S] by auto also have "\ = convex hull S" using * \c > 0\ by auto finally have "(*\<^sub>R) c ` (convex hull S) = convex hull S" by auto } then have "0 \ convex hull S" "\c. c > 0 \ ((*\<^sub>R) c ` (convex hull S)) = (convex hull S)" using * hull_subset[of S convex] by auto then show ?thesis using \S \ {}\ cone_iff[of "convex hull S"] by auto qed subsection \Radon's theorem\ text "Formalized by Lars Schewe." lemma Radon_ex_lemma: assumes "finite c" "affine_dependent c" shows "\u. sum u c = 0 \ (\v\c. u v \ 0) \ sum (\v. u v *\<^sub>R v) c = 0" proof - from assms(2)[unfolded affine_dependent_explicit] obtain s u where "finite s" "s \ c" "sum u s = 0" "\v\s. u v \ 0" "(\v\s. u v *\<^sub>R v) = 0" by blast then show ?thesis apply (rule_tac x="\v. if v\s then u v else 0" in exI) unfolding if_smult scaleR_zero_left and sum.inter_restrict[OF assms(1), symmetric] apply (auto simp: Int_absorb1) done qed lemma Radon_s_lemma: assumes "finite s" and "sum f s = (0::real)" shows "sum f {x\s. 0 < f x} = - sum f {x\s. f x < 0}" proof - have *: "\x. (if f x < 0 then f x else 0) + (if 0 < f x then f x else 0) = f x" by auto show ?thesis unfolding add_eq_0_iff[symmetric] and sum.inter_filter[OF assms(1)] and sum.distrib[symmetric] and * using assms(2) by assumption qed lemma Radon_v_lemma: assumes "finite s" and "sum f s = 0" and "\x. g x = (0::real) \ f x = (0::'a::euclidean_space)" shows "(sum f {x\s. 0 < g x}) = - sum f {x\s. g x < 0}" proof - have *: "\x. (if 0 < g x then f x else 0) + (if g x < 0 then f x else 0) = f x" using assms(3) by auto show ?thesis unfolding eq_neg_iff_add_eq_0 and sum.inter_filter[OF assms(1)] and sum.distrib[symmetric] and * using assms(2) apply assumption done qed lemma Radon_partition: assumes "finite c" "affine_dependent c" shows "\m p. m \ p = {} \ m \ p = c \ (convex hull m) \ (convex hull p) \ {}" proof - obtain u v where uv: "sum u c = 0" "v\c" "u v \ 0" "(\v\c. u v *\<^sub>R v) = 0" using Radon_ex_lemma[OF assms] by auto have fin: "finite {x \ c. 0 < u x}" "finite {x \ c. 0 > u x}" using assms(1) by auto define z where "z = inverse (sum u {x\c. u x > 0}) *\<^sub>R sum (\x. u x *\<^sub>R x) {x\c. u x > 0}" have "sum u {x \ c. 0 < u x} \ 0" proof (cases "u v \ 0") case False then have "u v < 0" by auto then show ?thesis proof (cases "\w\{x \ c. 0 < u x}. u w > 0") case True then show ?thesis using sum_nonneg_eq_0_iff[of _ u, OF fin(1)] by auto next case False then have "sum u c \ sum (\x. if x=v then u v else 0) c" apply (rule_tac sum_mono, auto) done then show ?thesis unfolding sum.delta[OF assms(1)] using uv(2) and \u v < 0\ and uv(1) by auto qed qed (insert sum_nonneg_eq_0_iff[of _ u, OF fin(1)] uv(2-3), auto) then have *: "sum u {x\c. u x > 0} > 0" unfolding less_le apply (rule_tac conjI) apply (rule_tac sum_nonneg, auto) done moreover have "sum u ({x \ c. 0 < u x} \ {x \ c. u x < 0}) = sum u c" "(\x\{x \ c. 0 < u x} \ {x \ c. u x < 0}. u x *\<^sub>R x) = (\x\c. u x *\<^sub>R x)" using assms(1) apply (rule_tac[!] sum.mono_neutral_left, auto) done then have "sum u {x \ c. 0 < u x} = - sum u {x \ c. 0 > u x}" "(\x\{x \ c. 0 < u x}. u x *\<^sub>R x) = - (\x\{x \ c. 0 > u x}. u x *\<^sub>R x)" unfolding eq_neg_iff_add_eq_0 using uv(1,4) by (auto simp: sum.union_inter_neutral[OF fin, symmetric]) moreover have "\x\{v \ c. u v < 0}. 0 \ inverse (sum u {x \ c. 0 < u x}) * - u x" apply rule apply (rule mult_nonneg_nonneg) using * apply auto done ultimately have "z \ convex hull {v \ c. u v \ 0}" unfolding convex_hull_explicit mem_Collect_eq apply (rule_tac x="{v \ c. u v < 0}" in exI) apply (rule_tac x="\y. inverse (sum u {x\c. u x > 0}) * - u y" in exI) using assms(1) unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] and z_def apply (auto simp: sum_negf sum_distrib_left[symmetric]) done moreover have "\x\{v \ c. 0 < u v}. 0 \ inverse (sum u {x \ c. 0 < u x}) * u x" apply rule apply (rule mult_nonneg_nonneg) using * apply auto done then have "z \ convex hull {v \ c. u v > 0}" unfolding convex_hull_explicit mem_Collect_eq apply (rule_tac x="{v \ c. 0 < u v}" in exI) apply (rule_tac x="\y. inverse (sum u {x\c. u x > 0}) * u y" in exI) using assms(1) unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] and z_def using * apply (auto simp: sum_negf sum_distrib_left[symmetric]) done ultimately show ?thesis apply (rule_tac x="{v\c. u v \ 0}" in exI) apply (rule_tac x="{v\c. u v > 0}" in exI, auto) done qed theorem Radon: assumes "affine_dependent c" obtains m p where "m \ c" "p \ c" "m \ p = {}" "(convex hull m) \ (convex hull p) \ {}" proof - from assms[unfolded affine_dependent_explicit] obtain s u where "finite s" "s \ c" "sum u s = 0" "\v\s. u v \ 0" "(\v\s. u v *\<^sub>R v) = 0" by blast then have *: "finite s" "affine_dependent s" and s: "s \ c" unfolding affine_dependent_explicit by auto from Radon_partition[OF *] obtain m p where "m \ p = {}" "m \ p = s" "convex hull m \ convex hull p \ {}" by blast then show ?thesis apply (rule_tac that[of p m]) using s apply auto done qed subsection \Helly's theorem\ lemma Helly_induct: fixes f :: "'a::euclidean_space set set" assumes "card f = n" and "n \ DIM('a) + 1" and "\s\f. convex s" "\t\f. card t = DIM('a) + 1 \ \t \ {}" shows "\f \ {}" using assms proof (induction n arbitrary: f) case 0 then show ?case by auto next case (Suc n) have "finite f" using \card f = Suc n\ by (auto intro: card_ge_0_finite) show "\f \ {}" proof (cases "n = DIM('a)") case True then show ?thesis by (simp add: Suc.prems(1) Suc.prems(4)) next case False have "\(f - {s}) \ {}" if "s \ f" for s proof (rule Suc.IH[rule_format]) show "card (f - {s}) = n" by (simp add: Suc.prems(1) \finite f\ that) show "DIM('a) + 1 \ n" using False Suc.prems(2) by linarith show "\t. \t \ f - {s}; card t = DIM('a) + 1\ \ \t \ {}" by (simp add: Suc.prems(4) subset_Diff_insert) qed (use Suc in auto) then have "\s\f. \x. x \ \(f - {s})" by blast then obtain X where X: "\s. s\f \ X s \ \(f - {s})" by metis show ?thesis proof (cases "inj_on X f") case False then obtain s t where "s\t" and st: "s\f" "t\f" "X s = X t" unfolding inj_on_def by auto then have *: "\f = \(f - {s}) \ \(f - {t})" by auto show ?thesis by (metis "*" X disjoint_iff_not_equal st) next case True then obtain m p where mp: "m \ p = {}" "m \ p = X ` f" "convex hull m \ convex hull p \ {}" using Radon_partition[of "X ` f"] and affine_dependent_biggerset[of "X ` f"] unfolding card_image[OF True] and \card f = Suc n\ using Suc(3) \finite f\ and False by auto have "m \ X ` f" "p \ X ` f" using mp(2) by auto then obtain g h where gh:"m = X ` g" "p = X ` h" "g \ f" "h \ f" unfolding subset_image_iff by auto then have "f \ (g \ h) = f" by auto then have f: "f = g \ h" using inj_on_Un_image_eq_iff[of X f "g \ h"] and True unfolding mp(2)[unfolded image_Un[symmetric] gh] by auto have *: "g \ h = {}" using mp(1) unfolding gh using inj_on_image_Int[OF True gh(3,4)] by auto have "convex hull (X ` h) \ \g" "convex hull (X ` g) \ \h" by (rule hull_minimal; use X * f in \auto simp: Suc.prems(3) convex_Inter\)+ then show ?thesis unfolding f using mp(3)[unfolded gh] by blast qed qed qed theorem Helly: fixes f :: "'a::euclidean_space set set" assumes "card f \ DIM('a) + 1" "\s\f. convex s" and "\t. \t\f; card t = DIM('a) + 1\ \ \t \ {}" shows "\f \ {}" apply (rule Helly_induct) using assms apply auto done subsection \Epigraphs of convex functions\ definition\<^marker>\tag important\ "epigraph S (f :: _ \ real) = {xy. fst xy \ S \ f (fst xy) \ snd xy}" lemma mem_epigraph: "(x, y) \ epigraph S f \ x \ S \ f x \ y" unfolding epigraph_def by auto lemma convex_epigraph: "convex (epigraph S f) \ convex_on S f \ convex S" proof safe assume L: "convex (epigraph S f)" then show "convex_on S f" by (auto simp: convex_def convex_on_def epigraph_def) show "convex S" using L apply (clarsimp simp: convex_def convex_on_def epigraph_def) apply (erule_tac x=x in allE) apply (erule_tac x="f x" in allE, safe) apply (erule_tac x=y in allE) apply (erule_tac x="f y" in allE) apply (auto simp: ) done next assume "convex_on S f" "convex S" then show "convex (epigraph S f)" unfolding convex_def convex_on_def epigraph_def apply safe apply (rule_tac [2] y="u * f a + v * f aa" in order_trans) apply (auto intro!:mult_left_mono add_mono) done qed lemma convex_epigraphI: "convex_on S f \ convex S \ convex (epigraph S f)" unfolding convex_epigraph by auto lemma convex_epigraph_convex: "convex S \ convex_on S f \ convex(epigraph S f)" by (simp add: convex_epigraph) subsubsection\<^marker>\tag unimportant\ \Use this to derive general bound property of convex function\ lemma convex_on: assumes "convex S" shows "convex_on S f \ (\k u x. (\i\{1..k::nat}. 0 \ u i \ x i \ S) \ sum u {1..k} = 1 \ f (sum (\i. u i *\<^sub>R x i) {1..k}) \ sum (\i. u i * f(x i)) {1..k})" unfolding convex_epigraph_convex[OF assms] convex epigraph_def Ball_def mem_Collect_eq unfolding fst_sum snd_sum fst_scaleR snd_scaleR apply safe apply (drule_tac x=k in spec) apply (drule_tac x=u in spec) apply (drule_tac x="\i. (x i, f (x i))" in spec) apply simp using assms[unfolded convex] apply simp apply (rule_tac y="\i = 1..k. u i * f (fst (x i))" in order_trans, force) apply (rule sum_mono) apply (erule_tac x=i in allE) unfolding real_scaleR_def apply (rule mult_left_mono) using assms[unfolded convex] apply auto done subsection\<^marker>\tag unimportant\ \A bound within a convex hull\ lemma convex_on_convex_hull_bound: assumes "convex_on (convex hull s) f" and "\x\s. f x \ b" shows "\x\ convex hull s. f x \ b" proof fix x assume "x \ convex hull s" then obtain k u v where obt: "\i\{1..k::nat}. 0 \ u i \ v i \ s" "sum u {1..k} = 1" "(\i = 1..k. u i *\<^sub>R v i) = x" unfolding convex_hull_indexed mem_Collect_eq by auto have "(\i = 1..k. u i * f (v i)) \ b" using sum_mono[of "{1..k}" "\i. u i * f (v i)" "\i. u i * b"] unfolding sum_distrib_right[symmetric] obt(2) mult_1 apply (drule_tac meta_mp) apply (rule mult_left_mono) using assms(2) obt(1) apply auto done then show "f x \ b" using assms(1)[unfolded convex_on[OF convex_convex_hull], rule_format, of k u v] unfolding obt(2-3) using obt(1) and hull_subset[unfolded subset_eq, rule_format, of _ s] by auto qed lemma inner_sum_Basis[simp]: "i \ Basis \ (\Basis) \ i = 1" by (simp add: inner_sum_left sum.If_cases inner_Basis) lemma convex_set_plus: assumes "convex S" and "convex T" shows "convex (S + T)" proof - have "convex (\x\ S. \y \ T. {x + y})" using assms by (rule convex_sums) moreover have "(\x\ S. \y \ T. {x + y}) = S + T" unfolding set_plus_def by auto finally show "convex (S + T)" . qed lemma convex_set_sum: assumes "\i. i \ A \ convex (B i)" shows "convex (\i\A. B i)" proof (cases "finite A") case True then show ?thesis using assms by induct (auto simp: convex_set_plus) qed auto lemma finite_set_sum: assumes "finite A" and "\i\A. finite (B i)" shows "finite (\i\A. B i)" using assms by (induct set: finite, simp, simp add: finite_set_plus) lemma box_eq_set_sum_Basis: shows "{x. \i\Basis. x\i \ B i} = (\i\Basis. image (\x. x *\<^sub>R i) (B i))" apply (subst set_sum_alt [OF finite_Basis], safe) apply (fast intro: euclidean_representation [symmetric]) apply (subst inner_sum_left) apply (rename_tac f) apply (subgoal_tac "(\x\Basis. f x \ i) = f i \ i") apply (drule (1) bspec) apply clarsimp apply (frule sum.remove [OF finite_Basis]) apply (erule trans, simp) apply (rule sum.neutral, clarsimp) apply (frule_tac x=i in bspec, assumption) apply (drule_tac x=x in bspec, assumption, clarsimp) apply (cut_tac u=x and v=i in inner_Basis, assumption+) apply (rule ccontr, simp) done lemma convex_hull_set_sum: "convex hull (\i\A. B i) = (\i\A. convex hull (B i))" proof (cases "finite A") assume "finite A" then show ?thesis by (induct set: finite, simp, simp add: convex_hull_set_plus) qed simp end \ No newline at end of file diff --git a/src/HOL/Analysis/Linear_Algebra.thy b/src/HOL/Analysis/Linear_Algebra.thy --- a/src/HOL/Analysis/Linear_Algebra.thy +++ b/src/HOL/Analysis/Linear_Algebra.thy @@ -1,1975 +1,1972 @@ (* Title: HOL/Analysis/Linear_Algebra.thy Author: Amine Chaieb, University of Cambridge *) section \Elementary Linear Algebra on Euclidean Spaces\ theory Linear_Algebra imports Euclidean_Space "HOL-Library.Infinite_Set" begin lemma linear_simps: assumes "bounded_linear f" shows "f (a + b) = f a + f b" "f (a - b) = f a - f b" "f 0 = 0" "f (- a) = - f a" "f (s *\<^sub>R v) = s *\<^sub>R (f v)" proof - interpret f: bounded_linear f by fact show "f (a + b) = f a + f b" by (rule f.add) show "f (a - b) = f a - f b" by (rule f.diff) show "f 0 = 0" by (rule f.zero) show "f (- a) = - f a" by (rule f.neg) show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scale) qed lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x \ (UNIV::'a::finite set)}" using finite finite_image_set by blast lemma substdbasis_expansion_unique: includes inner_syntax assumes d: "d \ Basis" shows "(\i\d. f i *\<^sub>R i) = (x::'a::euclidean_space) \ (\i\Basis. (i \ d \ f i = x \ i) \ (i \ d \ x \ i = 0))" proof - have *: "\x a b P. x * (if P then a else b) = (if P then x * a else x * b)" by auto have **: "finite d" by (auto intro: finite_subset[OF assms]) have ***: "\i. i \ Basis \ (\i\d. f i *\<^sub>R i) \ i = (\x\d. if x = i then f x else 0)" using d by (auto intro!: sum.cong simp: inner_Basis inner_sum_left) show ?thesis unfolding euclidean_eq_iff[where 'a='a] by (auto simp: sum.delta[OF **] ***) qed lemma independent_substdbasis: "d \ Basis \ independent d" by (rule independent_mono[OF independent_Basis]) -lemma sum_not_0: "sum f A \ 0 \ \a \ A. f a \ 0" - by (rule ccontr) auto - lemma subset_translation_eq [simp]: fixes a :: "'a::real_vector" shows "(+) a ` s \ (+) a ` t \ s \ t" by auto lemma translate_inj_on: fixes A :: "'a::ab_group_add set" shows "inj_on (\x. a + x) A" unfolding inj_on_def by auto lemma translation_assoc: fixes a b :: "'a::ab_group_add" shows "(\x. b + x) ` ((\x. a + x) ` S) = (\x. (a + b) + x) ` S" by auto lemma translation_invert: fixes a :: "'a::ab_group_add" assumes "(\x. a + x) ` A = (\x. a + x) ` B" shows "A = B" proof - have "(\x. -a + x) ` ((\x. a + x) ` A) = (\x. - a + x) ` ((\x. a + x) ` B)" using assms by auto then show ?thesis using translation_assoc[of "-a" a A] translation_assoc[of "-a" a B] by auto qed lemma translation_galois: fixes a :: "'a::ab_group_add" shows "T = ((\x. a + x) ` S) \ S = ((\x. (- a) + x) ` T)" using translation_assoc[of "-a" a S] apply auto using translation_assoc[of a "-a" T] apply auto done lemma translation_inverse_subset: assumes "((\x. - a + x) ` V) \ (S :: 'n::ab_group_add set)" shows "V \ ((\x. a + x) ` S)" proof - { fix x assume "x \ V" then have "x-a \ S" using assms by auto then have "x \ {a + v |v. v \ S}" apply auto apply (rule exI[of _ "x-a"], simp) done then have "x \ ((\x. a+x) ` S)" by auto } then show ?thesis by auto qed subsection\<^marker>\tag unimportant\ \More interesting properties of the norm\ unbundle inner_syntax text\Equality of vectors in terms of \<^term>\(\)\ products.\ lemma linear_componentwise: fixes f:: "'a::euclidean_space \ 'b::real_inner" assumes lf: "linear f" shows "(f x) \ j = (\i\Basis. (x\i) * (f i\j))" (is "?lhs = ?rhs") proof - interpret linear f by fact have "?rhs = (\i\Basis. (x\i) *\<^sub>R (f i))\j" by (simp add: inner_sum_left) then show ?thesis by (simp add: euclidean_representation sum[symmetric] scale[symmetric]) qed 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 then have "x \ (x - y) = 0 \ y \ (x - y) = 0" by (simp add: inner_diff inner_commute) then have "(x - y) \ (x - y) = 0" by (simp add: field_simps inner_diff inner_commute) then show "x = y" by simp qed lemma norm_triangle_half_r: "norm (y - x1) < e / 2 \ norm (y - x2) < e / 2 \ norm (x1 - x2) < e" using dist_triangle_half_r unfolding dist_norm[symmetric] by auto lemma norm_triangle_half_l: assumes "norm (x - y) < e / 2" and "norm (x' - y) < e / 2" shows "norm (x - x') < e" using dist_triangle_half_l[OF assms[unfolded dist_norm[symmetric]]] unfolding dist_norm[symmetric] . lemma abs_triangle_half_r: fixes y :: "'a::linordered_field" shows "abs (y - x1) < e / 2 \ abs (y - x2) < e / 2 \ abs (x1 - x2) < e" by linarith lemma abs_triangle_half_l: fixes y :: "'a::linordered_field" assumes "abs (x - y) < e / 2" and "abs (x' - y) < e / 2" shows "abs (x - x') < e" using assms by linarith lemma sum_clauses: shows "sum f {} = 0" and "finite S \ sum f (insert x S) = (if x \ S then sum f S else f x + sum f S)" by (auto simp add: insert_absorb) lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = z" proof assume "\x. x \ y = x \ z" then have "\x. x \ (y - z) = 0" by (simp add: inner_diff) then have "(y - z) \ (y - z) = 0" .. then show "y = z" by simp qed simp lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ x = y" proof assume "\z. x \ z = y \ z" then have "\z. (x - y) \ z = 0" by (simp add: inner_diff) then have "(x - y) \ (x - y) = 0" .. then show "x = y" by simp qed simp subsection \Substandard Basis\ lemma ex_card: assumes "n \ card A" shows "\S\A. card S = n" proof (cases "finite A") case True from ex_bij_betw_nat_finite[OF this] obtain f where f: "bij_betw f {0..n \ card A\ have "{..< n} \ {..< card A}" "inj_on f {..< n}" by (auto simp: bij_betw_def intro: subset_inj_on) ultimately have "f ` {..< n} \ A" "card (f ` {..< n}) = n" by (auto simp: bij_betw_def card_image) then show ?thesis by blast next case False with \n \ card A\ show ?thesis by force qed lemma subspace_substandard: "subspace {x::'a::euclidean_space. (\i\Basis. P i \ x\i = 0)}" by (auto simp: subspace_def inner_add_left) lemma dim_substandard: assumes d: "d \ Basis" shows "dim {x::'a::euclidean_space. \i\Basis. i \ d \ x\i = 0} = card d" (is "dim ?A = _") proof (rule dim_unique) from d show "d \ ?A" by (auto simp: inner_Basis) from d show "independent d" by (rule independent_mono [OF independent_Basis]) have "x \ span d" if "\i\Basis. i \ d \ x \ i = 0" for x proof - have "finite d" by (rule finite_subset [OF d finite_Basis]) then have "(\i\d. (x \ i) *\<^sub>R i) \ span d" by (simp add: span_sum span_clauses) also have "(\i\d. (x \ i) *\<^sub>R i) = (\i\Basis. (x \ i) *\<^sub>R i)" by (rule sum.mono_neutral_cong_left [OF finite_Basis d]) (auto simp: that) finally show "x \ span d" by (simp only: euclidean_representation) qed then show "?A \ span d" by auto qed simp subsection \Orthogonality\ definition\<^marker>\tag important\ (in real_inner) "orthogonal x y \ x \ y = 0" context real_inner begin lemma orthogonal_self: "orthogonal x x \ x = 0" by (simp add: orthogonal_def) 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_add inner_diff by auto end lemma orthogonal_commute: "orthogonal x y \ orthogonal y x" by (simp add: orthogonal_def inner_commute) lemma orthogonal_scaleR [simp]: "c \ 0 \ orthogonal (c *\<^sub>R x) = orthogonal x" by (rule ext) (simp add: orthogonal_def) lemma pairwise_ortho_scaleR: "pairwise (\i j. orthogonal (f i) (g j)) B \ pairwise (\i j. orthogonal (a i *\<^sub>R f i) (a j *\<^sub>R g j)) B" by (auto simp: pairwise_def orthogonal_clauses) lemma orthogonal_rvsum: "\finite s; \y. y \ s \ orthogonal x (f y)\ \ orthogonal x (sum f s)" by (induction s rule: finite_induct) (auto simp: orthogonal_clauses) lemma orthogonal_lvsum: "\finite s; \x. x \ s \ orthogonal (f x) y\ \ orthogonal (sum f s) y" by (induction s rule: finite_induct) (auto simp: orthogonal_clauses) lemma norm_add_Pythagorean: assumes "orthogonal a b" shows "norm(a + b) ^ 2 = norm a ^ 2 + norm b ^ 2" proof - from assms have "(a - (0 - b)) \ (a - (0 - b)) = a \ a - (0 - b \ b)" by (simp add: algebra_simps orthogonal_def inner_commute) then show ?thesis by (simp add: power2_norm_eq_inner) qed lemma norm_sum_Pythagorean: assumes "finite I" "pairwise (\i j. orthogonal (f i) (f j)) I" shows "(norm (sum f I))\<^sup>2 = (\i\I. (norm (f i))\<^sup>2)" using assms proof (induction I rule: finite_induct) case empty then show ?case by simp next case (insert x I) then have "orthogonal (f x) (sum f I)" by (metis pairwise_insert orthogonal_rvsum) with insert show ?case by (simp add: pairwise_insert norm_add_Pythagorean) qed subsection \Orthogonality of a transformation\ definition\<^marker>\tag important\ "orthogonal_transformation f \ linear f \ (\v w. f v \ f w = v \ w)" lemma\<^marker>\tag unimportant\ orthogonal_transformation: "orthogonal_transformation f \ linear f \ (\v. norm (f v) = norm v)" unfolding orthogonal_transformation_def apply auto apply (erule_tac x=v in allE)+ apply (simp add: norm_eq_sqrt_inner) apply (simp add: dot_norm linear_add[symmetric]) done lemma\<^marker>\tag unimportant\ orthogonal_transformation_id [simp]: "orthogonal_transformation (\x. x)" by (simp add: linear_iff orthogonal_transformation_def) lemma\<^marker>\tag unimportant\ orthogonal_orthogonal_transformation: "orthogonal_transformation f \ orthogonal (f x) (f y) \ orthogonal x y" by (simp add: orthogonal_def orthogonal_transformation_def) lemma\<^marker>\tag unimportant\ orthogonal_transformation_compose: "\orthogonal_transformation f; orthogonal_transformation g\ \ orthogonal_transformation(f \ g)" by (auto simp: orthogonal_transformation_def linear_compose) lemma\<^marker>\tag unimportant\ orthogonal_transformation_neg: "orthogonal_transformation(\x. -(f x)) \ orthogonal_transformation f" by (auto simp: orthogonal_transformation_def dest: linear_compose_neg) lemma\<^marker>\tag unimportant\ orthogonal_transformation_scaleR: "orthogonal_transformation f \ f (c *\<^sub>R v) = c *\<^sub>R f v" by (simp add: linear_iff orthogonal_transformation_def) lemma\<^marker>\tag unimportant\ orthogonal_transformation_linear: "orthogonal_transformation f \ linear f" by (simp add: orthogonal_transformation_def) lemma\<^marker>\tag unimportant\ orthogonal_transformation_inj: "orthogonal_transformation f \ inj f" unfolding orthogonal_transformation_def inj_on_def by (metis vector_eq) lemma\<^marker>\tag unimportant\ orthogonal_transformation_surj: "orthogonal_transformation f \ surj f" for f :: "'a::euclidean_space \ 'a::euclidean_space" by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear) lemma\<^marker>\tag unimportant\ orthogonal_transformation_bij: "orthogonal_transformation f \ bij f" for f :: "'a::euclidean_space \ 'a::euclidean_space" by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj) lemma\<^marker>\tag unimportant\ orthogonal_transformation_inv: "orthogonal_transformation f \ orthogonal_transformation (inv f)" for f :: "'a::euclidean_space \ 'a::euclidean_space" by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj) lemma\<^marker>\tag unimportant\ orthogonal_transformation_norm: "orthogonal_transformation f \ norm (f x) = norm x" by (metis orthogonal_transformation) subsection \Bilinear functions\ definition\<^marker>\tag important\ bilinear :: "('a::real_vector \ 'b::real_vector \ 'c::real_vector) \ bool" where "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_iff) lemma bilinear_radd: "bilinear h \ h x (y + z) = h x y + h x z" by (simp add: bilinear_def linear_iff) lemma bilinear_times: fixes c::"'a::real_algebra" shows "bilinear (\x y::'a. x*y)" by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI) lemma bilinear_lmul: "bilinear h \ h (c *\<^sub>R x) y = c *\<^sub>R h x y" by (simp add: bilinear_def linear_iff) lemma bilinear_rmul: "bilinear h \ h x (c *\<^sub>R y) = c *\<^sub>R h x y" by (simp add: bilinear_def linear_iff) lemma bilinear_lneg: "bilinear h \ h (- x) y = - h x y" by (drule bilinear_lmul [of _ "- 1"]) simp lemma bilinear_rneg: "bilinear h \ h x (- y) = - h x y" by (drule bilinear_rmul [of _ _ "- 1"]) simp lemma (in ab_group_add) eq_add_iff: "x = x + y \ y = 0" using add_left_imp_eq[of x y 0] by auto lemma bilinear_lzero: assumes "bilinear h" shows "h 0 x = 0" using bilinear_ladd [OF assms, of 0 0 x] by (simp add: eq_add_iff field_simps) lemma bilinear_rzero: assumes "bilinear h" shows "h x 0 = 0" using bilinear_radd [OF assms, of x 0 0 ] by (simp add: eq_add_iff field_simps) lemma bilinear_lsub: "bilinear h \ h (x - y) z = h x z - h y z" using bilinear_ladd [of h x "- y"] by (simp add: bilinear_lneg) lemma bilinear_rsub: "bilinear h \ h z (x - y) = h z x - h z y" using bilinear_radd [of h _ x "- y"] by (simp add: bilinear_rneg) lemma bilinear_sum: assumes "bilinear h" shows "h (sum f S) (sum g T) = sum (\(i,j). h (f i) (g j)) (S \ T) " proof - interpret l: linear "\x. h x y" for y using assms by (simp add: bilinear_def) interpret r: linear "\y. h x y" for x using assms by (simp add: bilinear_def) have "h (sum f S) (sum g T) = sum (\x. h (f x) (sum g T)) S" by (simp add: l.sum) also have "\ = sum (\x. sum (\y. h (f x) (g y)) T) S" by (rule sum.cong) (simp_all add: r.sum) finally show ?thesis unfolding sum.cartesian_product . qed subsection \Adjoints\ definition\<^marker>\tag important\ adjoint :: "(('a::real_inner) \ ('b::real_inner)) \ 'b \ 'a" where "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)" by (rule assms) next fix h assume "\x y. inner (f x) y = inner x (h y)" then have "\x y. inner x (g y) = inner x (h y)" using assms by simp then have "\x y. inner x (g y - h y) = 0" by (simp add: inner_diff_right) then have "\y. inner (g y - h y) (g y - h y) = 0" by simp then have "\y. h y = g y" by simp then show "h = g" by (simp add: ext) qed text \TODO: The following lemmas about adjoints should hold for any Hilbert space (i.e. complete inner product space). (see \<^url>\https://en.wikipedia.org/wiki/Hermitian_adjoint\) \ lemma adjoint_works: fixes f :: "'n::euclidean_space \ 'm::euclidean_space" assumes lf: "linear f" shows "x \ adjoint f y = f x \ y" proof - interpret linear f by fact have "\y. \w. \x. f x \ y = x \ w" proof (intro allI exI) fix y :: "'m" and x let ?w = "(\i\Basis. (f i \ y) *\<^sub>R i) :: 'n" have "f x \ y = f (\i\Basis. (x \ i) *\<^sub>R i) \ y" by (simp add: euclidean_representation) also have "\ = (\i\Basis. (x \ i) *\<^sub>R f i) \ y" by (simp add: sum scale) finally show "f x \ y = x \ ?w" by (simp add: inner_sum_left inner_sum_right mult.commute) qed then show ?thesis unfolding adjoint_def choice_iff by (intro someI2_ex[where Q="\f'. x \ f' y = f x \ y"]) auto qed lemma adjoint_clauses: fixes f :: "'n::euclidean_space \ 'm::euclidean_space" assumes lf: "linear f" shows "x \ adjoint f y = f x \ y" and "adjoint f y \ x = y \ f x" by (simp_all add: adjoint_works[OF lf] inner_commute) lemma adjoint_linear: fixes f :: "'n::euclidean_space \ 'm::euclidean_space" assumes lf: "linear f" shows "linear (adjoint f)" by (simp add: lf linear_iff euclidean_eq_iff[where 'a='n] euclidean_eq_iff[where 'a='m] adjoint_clauses[OF lf] inner_distrib) lemma adjoint_adjoint: fixes f :: "'n::euclidean_space \ 'm::euclidean_space" assumes lf: "linear f" shows "adjoint (adjoint f) = f" by (rule adjoint_unique, simp add: adjoint_clauses [OF lf]) subsection \Archimedean properties and useful consequences\ text\Bernoulli's inequality\ proposition Bernoulli_inequality: fixes x :: real assumes "-1 \ x" shows "1 + n * x \ (1 + x) ^ n" proof (induct n) case 0 then show ?case by simp next case (Suc n) have "1 + Suc n * x \ 1 + (Suc n)*x + n * x^2" by (simp add: algebra_simps) also have "... = (1 + x) * (1 + n*x)" by (auto simp: power2_eq_square algebra_simps of_nat_Suc) also have "... \ (1 + x) ^ Suc n" using Suc.hyps assms mult_left_mono by fastforce finally show ?case . qed corollary Bernoulli_inequality_even: fixes x :: real assumes "even n" shows "1 + n * x \ (1 + x) ^ n" proof (cases "-1 \ x \ n=0") case True then show ?thesis by (auto simp: Bernoulli_inequality) next case False then have "real n \ 1" by simp with False have "n * x \ -1" by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one) then have "1 + n * x \ 0" by auto also have "... \ (1 + x) ^ n" using assms using zero_le_even_power by blast finally show ?thesis . qed corollary real_arch_pow: fixes x :: real assumes x: "1 < x" shows "\n. y < x^n" proof - from x have x0: "x - 1 > 0" by arith from reals_Archimedean3[OF x0, rule_format, of y] obtain n :: nat where n: "y < real n * (x - 1)" by metis from x0 have x00: "x- 1 \ -1" by arith from Bernoulli_inequality[OF x00, of n] n have "y < x^n" by auto then show ?thesis by metis qed corollary real_arch_pow_inv: fixes x y :: real assumes y: "y > 0" and x1: "x < 1" shows "\n. x^n < y" proof (cases "x > 0") case True with x1 have ix: "1 < 1/x" by (simp add: field_simps) from real_arch_pow[OF ix, of "1/y"] obtain n where n: "1/y < (1/x)^n" by blast then show ?thesis using y \x > 0\ by (auto simp add: field_simps) next case False with y x1 show ?thesis by (metis less_le_trans not_less power_one_right) 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_inverse) 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 (metis Suc_pred of_nat_Suc) done subsection\<^marker>\tag unimportant\ \Euclidean Spaces as Typeclass\ lemma independent_Basis: "independent Basis" by (rule independent_Basis) lemma span_Basis [simp]: "span Basis = UNIV" by (rule span_Basis) lemma in_span_Basis: "x \ span Basis" unfolding span_Basis .. subsection\<^marker>\tag unimportant\ \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 interpret linear f by fact let ?B = "\b\Basis. norm (f b)" show "\x. norm (f x) \ ?B * norm x" proof fix x :: 'a let ?g = "\b. (x \ b) *\<^sub>R f b" have "norm (f x) = norm (f (\b\Basis. (x \ b) *\<^sub>R b))" unfolding euclidean_representation .. also have "\ = norm (sum ?g Basis)" by (simp add: sum scale) finally have th0: "norm (f x) = norm (sum ?g Basis)" . have th: "norm (?g i) \ norm (f i) * norm x" if "i \ Basis" for i proof - from Basis_le_norm[OF that, of x] show "norm (?g i) \ norm (f i) * norm x" unfolding norm_scaleR by (metis mult.commute mult_left_mono norm_ge_zero) qed from sum_norm_le[of _ ?g, OF th] show "norm (f x) \ ?B * norm x" unfolding th0 sum_distrib_right by metis qed 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" then interpret f: linear f . show "bounded_linear f" proof have "\B. \x. norm (f x) \ B * norm x" using \linear f\ by (rule linear_bounded) then show "\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" .. qed lemmas linear_linear = linear_conv_bounded_linear[symmetric] lemma inj_linear_imp_inv_bounded_linear: fixes f::"'a::euclidean_space \ 'a" shows "\bounded_linear f; inj f\ \ bounded_linear (inv f)" by (simp add: inj_linear_imp_inv_linear linear_linear) lemma linear_bounded_pos: fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" assumes lf: "linear f" obtains B where "B > 0" "\x. norm (f x) \ B * norm x" proof - have "\B > 0. \x. norm (f x) \ norm x * B" using lf unfolding linear_conv_bounded_linear by (rule bounded_linear.pos_bounded) with that show ?thesis by (auto simp: mult.commute) qed lemma linear_invertible_bounded_below_pos: fixes f :: "'a::real_normed_vector \ 'b::euclidean_space" assumes "linear f" "linear g" "g \ f = id" obtains B where "B > 0" "\x. B * norm x \ norm(f x)" proof - obtain B where "B > 0" and B: "\x. norm (g x) \ B * norm x" using linear_bounded_pos [OF \linear g\] by blast show thesis proof show "0 < 1/B" by (simp add: \B > 0\) show "1/B * norm x \ norm (f x)" for x proof - have "1/B * norm x = 1/B * norm (g (f x))" using assms by (simp add: pointfree_idE) also have "\ \ norm (f x)" using B [of "f x"] by (simp add: \B > 0\ mult.commute pos_divide_le_eq) finally show ?thesis . qed qed qed lemma linear_inj_bounded_below_pos: fixes f :: "'a::real_normed_vector \ 'b::euclidean_space" assumes "linear f" "inj f" obtains B where "B > 0" "\x. B * norm x \ norm(f x)" using linear_injective_left_inverse [OF assms] linear_invertible_bounded_below_pos assms by blast lemma bounded_linearI': fixes f ::"'a::euclidean_space \ 'b::real_normed_vector" assumes "\x y. f (x + y) = f x + f y" and "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" shows "bounded_linear f" using assms linearI linear_conv_bounded_linear by blast 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 (clarify intro!: exI[of _ "\i\Basis. \j\Basis. norm (h i j)"]) fix x :: 'm fix y :: 'n have "norm (h x y) = norm (h (sum (\i. (x \ i) *\<^sub>R i) Basis) (sum (\i. (y \ i) *\<^sub>R i) Basis))" by (simp add: euclidean_representation) also have "\ = norm (sum (\ (i,j). h ((x \ i) *\<^sub>R i) ((y \ j) *\<^sub>R j)) (Basis \ Basis))" unfolding bilinear_sum[OF bh] .. finally have th: "norm (h x y) = \" . have "\i j. \i \ Basis; j \ Basis\ \ \x \ i\ * (\y \ j\ * norm (h i j)) \ norm x * (norm y * norm (h i j))" by (auto simp add: zero_le_mult_iff Basis_le_norm mult_mono) then show "norm (h x y) \ (\i\Basis. \j\Basis. norm (h i j)) * norm x * norm y" unfolding sum_distrib_right th sum.cartesian_product by (clarsimp simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] field_simps simp del: scaleR_scaleR intro!: sum_norm_le) 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_iff 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_iff by simp next show "h (scaleR r x) y = scaleR r (h x y)" "h x (scaleR r y) = scaleR r (h x y)" for r x y using \bilinear h\ unfolding bilinear_def linear_iff by simp_all next have "\B. \x y. norm (h x y) \ B * norm x * norm y" using \bilinear h\ by (rule bilinear_bounded) then show "\K. \x y. norm (h x y) \ norm x * norm y * K" by (simp add: ac_simps) 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 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 - have "\B > 0. \x y. norm (h x y) \ norm x * norm y * B" using bh [unfolded bilinear_conv_bounded_bilinear] by (rule bounded_bilinear.pos_bounded) then show ?thesis by (simp only: ac_simps) qed lemma bounded_linear_imp_has_derivative: "bounded_linear f \ (f has_derivative f) net" by (auto simp add: has_derivative_def linear_diff linear_linear linear_def dest: bounded_linear.linear) lemma linear_imp_has_derivative: fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" shows "linear f \ (f has_derivative f) net" by (simp add: bounded_linear_imp_has_derivative linear_conv_bounded_linear) lemma bounded_linear_imp_differentiable: "bounded_linear f \ f differentiable net" using bounded_linear_imp_has_derivative differentiable_def by blast lemma linear_imp_differentiable: fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" shows "linear f \ f differentiable net" by (metis linear_imp_has_derivative differentiable_def) subsection\<^marker>\tag unimportant\ \We continue\ lemma independent_bound: fixes S :: "'a::euclidean_space set" shows "independent S \ finite S \ card S \ DIM('a)" by (metis dim_subset_UNIV finiteI_independent dim_span_eq_card_independent) lemmas independent_imp_finite = finiteI_independent corollary fixes S :: "'a::euclidean_space set" assumes "independent S" shows independent_card_le:"card S \ DIM('a)" using assms independent_bound by auto lemma dependent_biggerset: fixes S :: "'a::euclidean_space set" shows "(finite S \ card S > DIM('a)) \ dependent S" by (metis independent_bound not_less) text \Picking an orthogonal replacement for a spanning set.\ lemma vector_sub_project_orthogonal: fixes b x :: "'a::euclidean_space" shows "b \ (x - ((b \ x) / (b \ b)) *\<^sub>R b) = 0" unfolding inner_simps by auto lemma pairwise_orthogonal_insert: assumes "pairwise orthogonal S" and "\y. y \ S \ orthogonal x y" shows "pairwise orthogonal (insert x S)" using assms unfolding pairwise_def by (auto simp add: orthogonal_commute) lemma basis_orthogonal: fixes B :: "'a::real_inner 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") using fB proof (induct rule: finite_induct) case empty then show ?case apply (rule exI[where x="{}"]) apply (auto simp add: pairwise_def) done next case (insert 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 - sum (\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_scale) apply (rule span_sum) apply (rule span_scale) apply (rule span_base) apply assumption done } then have SC: "span ?C = span (insert a B)" unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto { fix y assume yC: "y \ C" then have Cy: "C = insert y (C - {y})" by blast have fth: "finite (C - {y})" using C by simp have "orthogonal ?a y" unfolding orthogonal_def unfolding inner_diff inner_sum_left right_minus_eq unfolding sum.remove [OF \finite C\ \y \ C\] apply (clarsimp simp add: inner_commute[of y a]) apply (rule sum.neutral) apply clarsimp apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format]) using \y \ C\ by auto } with \pairwise orthogonal C\ have CPO: "pairwise orthogonal ?C" by (rule pairwise_orthogonal_insert) 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 force 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_superset 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 ultimately have CdV: "card C = dim V" using C(1) by simp from C B CSV CdV iC show ?thesis by auto qed 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 - sum (\b. (a \ b / (b \ b)) *\<^sub>R b) B" have "sum (\b. (a \ b / (b \ b)) *\<^sub>R b) B \ span S" unfolding sSB apply (rule span_sum) apply (rule span_scale) apply (rule span_base) apply assumption done with a have a0:"?a \ 0" by auto have "?a \ x = 0" if "x\span B" for x proof (rule span_induct [OF that]) show "subspace {x. ?a \ x = 0}" by (auto simp add: subspace_def inner_add) 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 sum_clauses(2)[OF fth] apply simp unfolding inner_simps apply (clarsimp simp add: inner_add inner_sum_left) apply (rule sum.neutral, rule ballI) apply (simp only: inner_commute) apply (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format]) done } then show "?a \ x = 0" if "x \ B" for x using that by blast qed with a0 show ?thesis unfolding sSB by (auto intro: exI[where x="?a"]) qed lemma span_not_univ_subset_hyperplane: fixes S :: "'a::euclidean_space set" assumes SU: "span S \ UNIV" 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" then have "dim (span S) = dim (UNIV :: ('a) set)" by simp then have "dim S = DIM('a)" by (metis Euclidean_Space.dim_UNIV dim_span) with d have False by arith } then have th: "span S \ UNIV" by blast from span_not_univ_subset_hyperplane[OF th] show ?thesis . qed lemma linear_eq_stdbasis: fixes f :: "'a::euclidean_space \ _" assumes lf: "linear f" and lg: "linear g" and fg: "\b. b \ Basis \ f b = g b" shows "f = g" using linear_eq_on_span[OF lf lg, of Basis] fg by auto 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 "x\S" "y\T" and fg: "\x y. \x \ B; y\ C\ \ f x y = g x y" shows "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_iff subspace_def bf bg by (auto simp add: span_zero bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf]) have sfg: "\x. x \ B \ subspace {a. f x a = g x a}" apply (auto simp add: subspace_def) using bf bg unfolding bilinear_def linear_iff apply (auto simp add: span_zero bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf]) done have "\y\ span C. f x y = g x y" if "x \ span B" for x apply (rule span_induct [OF that sp]) using fg sfg span_induct by blast then show ?thesis using SB TC assms by auto qed lemma bilinear_eq_stdbasis: fixes f :: "'a::euclidean_space \ 'b::euclidean_space \ _" assumes bf: "bilinear f" and bg: "bilinear g" and fg: "\i j. i \ Basis \ j \ Basis \ f i j = g i j" shows "f = g" using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis]] fg by blast subsection \Infinity norm\ definition\<^marker>\tag important\ "infnorm (x::'a::euclidean_space) = Sup {\x \ b\ |b. b \ Basis}" lemma infnorm_set_image: fixes x :: "'a::euclidean_space" shows "{\x \ i\ |i. i \ Basis} = (\i. \x \ i\) ` Basis" by blast lemma infnorm_Max: fixes x :: "'a::euclidean_space" shows "infnorm x = Max ((\i. \x \ i\) ` Basis)" by (simp add: infnorm_def infnorm_set_image cSup_eq_Max) lemma infnorm_set_lemma: fixes x :: "'a::euclidean_space" shows "finite {\x \ i\ |i. i \ Basis}" and "{\x \ i\ |i. i \ Basis} \ {}" unfolding infnorm_set_image by auto lemma infnorm_pos_le: fixes x :: "'a::euclidean_space" shows "0 \ infnorm x" by (simp add: infnorm_Max Max_ge_iff ex_in_conv) lemma infnorm_triangle: fixes x :: "'a::euclidean_space" shows "infnorm (x + y) \ infnorm x + infnorm y" proof - have *: "\a b c d :: real. \a\ \ c \ \b\ \ d \ \a + b\ \ c + d" by simp show ?thesis by (auto simp: infnorm_Max inner_add_left intro!: *) qed lemma infnorm_eq_0: fixes x :: "'a::euclidean_space" shows "infnorm x = 0 \ x = 0" proof - have "infnorm x \ 0 \ x = 0" unfolding infnorm_Max by (simp add: euclidean_all_zero_iff) then show ?thesis using infnorm_pos_le[of x] by simp qed lemma infnorm_0: "infnorm 0 = 0" by (simp add: infnorm_eq_0) lemma infnorm_neg: "infnorm (- x) = infnorm x" unfolding infnorm_def by simp lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)" by (metis infnorm_neg minus_diff_eq) lemma absdiff_infnorm: "\infnorm x - infnorm y\ \ infnorm (x - y)" proof - have *: "\(nx::real) n ny. nx \ n + ny \ ny \ n + nx \ \nx - ny\ \ n" by arith show ?thesis proof (rule *) from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"] show "infnorm x \ infnorm (x - y) + infnorm y" "infnorm y \ infnorm (x - y) + infnorm x" by (simp_all add: field_simps infnorm_neg) qed qed lemma real_abs_infnorm: "\infnorm x\ = infnorm x" using infnorm_pos_le[of x] by arith lemma Basis_le_infnorm: fixes x :: "'a::euclidean_space" shows "b \ Basis \ \x \ b\ \ infnorm x" by (simp add: infnorm_Max) lemma infnorm_mul: "infnorm (a *\<^sub>R x) = \a\ * infnorm x" unfolding infnorm_Max proof (safe intro!: Max_eqI) let ?B = "(\i. \x \ i\) ` Basis" { fix b :: 'a assume "b \ Basis" then show "\a *\<^sub>R x \ b\ \ \a\ * Max ?B" by (simp add: abs_mult mult_left_mono) next from Max_in[of ?B] obtain b where "b \ Basis" "Max ?B = \x \ b\" by (auto simp del: Max_in) then show "\a\ * Max ((\i. \x \ i\) ` Basis) \ (\i. \a *\<^sub>R x \ i\) ` Basis" by (intro image_eqI[where x=b]) (auto simp: abs_mult) } qed simp lemma infnorm_mul_lemma: "infnorm (a *\<^sub>R x) \ \a\ * infnorm x" unfolding infnorm_mul .. 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" by (simp add: Basis_le_norm infnorm_Max) lemma norm_le_infnorm: fixes x :: "'a::euclidean_space" shows "norm x \ sqrt DIM('a) * infnorm x" unfolding norm_eq_sqrt_inner id_def proof (rule real_le_lsqrt[OF inner_ge_zero]) show "sqrt DIM('a) * infnorm x \ 0" by (simp add: zero_le_mult_iff infnorm_pos_le) have "x \ x \ (\b\Basis. x \ b * (x \ b))" by (metis euclidean_inner order_refl) also have "... \ DIM('a) * \infnorm x\\<^sup>2" by (rule sum_bounded_above) (metis Basis_le_infnorm abs_le_square_iff power2_eq_square real_abs_infnorm) also have "... \ (sqrt DIM('a) * infnorm x)\<^sup>2" by (simp add: power_mult_distrib) finally show "x \ x \ (sqrt DIM('a) * infnorm x)\<^sup>2" . qed lemma tendsto_infnorm [tendsto_intros]: assumes "(f \ a) F" shows "((\x. infnorm (f x)) \ infnorm a) F" proof (rule tendsto_compose [OF LIM_I assms]) fix r :: real assume "r > 0" then show "\s>0. \x. x \ a \ norm (x - a) < s \ norm (infnorm x - infnorm a) < r" by (metis real_norm_def le_less_trans absdiff_infnorm infnorm_le_norm) 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 (cases "x=0") case True then show ?thesis by auto next case False 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 False unfolding inner_simps by (auto simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps) also have "\ \ (2 * norm x * norm y * (norm x * norm y - x \ y) = 0)" using False by (simp add: field_simps inner_commute) also have "\ \ ?lhs" using False by auto finally show ?thesis by metis qed lemma norm_cauchy_schwarz_abs_eq: "\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 \ \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 (cases "x = 0 \ y = 0") case True then show ?thesis by force next case False then have n: "norm x > 0" "norm y > 0" by auto have "norm (x + y) = norm x + norm y \ (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2" by simp 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 show ?thesis . qed subsection \Collinearity\ definition\<^marker>\tag important\ collinear :: "'a::real_vector set \ bool" where "collinear S \ (\u. \x \ S. \ y \ S. \c. x - y = c *\<^sub>R u)" lemma collinear_alt: "collinear S \ (\u v. \x \ S. \c. x = u + c *\<^sub>R v)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs unfolding collinear_def by (metis Groups.add_ac(2) diff_add_cancel) next assume ?rhs then obtain u v where *: "\x. x \ S \ \c. x = u + c *\<^sub>R v" by (auto simp: ) have "\c. x - y = c *\<^sub>R v" if "x \ S" "y \ S" for x y by (metis *[OF \x \ S\] *[OF \y \ S\] scaleR_left.diff add_diff_cancel_left) then show ?lhs using collinear_def by blast qed lemma collinear: fixes S :: "'a::{perfect_space,real_vector} set" shows "collinear S \ (\u. u \ 0 \ (\x \ S. \ y \ S. \c. x - y = c *\<^sub>R u))" proof - have "\v. v \ 0 \ (\x\S. \y\S. \c. x - y = c *\<^sub>R v)" if "\x\S. \y\S. \c. x - y = c *\<^sub>R u" "u=0" for u proof - have "\x\S. \y\S. x = y" using that by auto moreover obtain v::'a where "v \ 0" using UNIV_not_singleton [of 0] by auto ultimately have "\x\S. \y\S. \c. x - y = c *\<^sub>R v" by auto then show ?thesis using \v \ 0\ by blast qed then show ?thesis apply (clarsimp simp: collinear_def) by (metis scaleR_zero_right vector_fraction_eq_iff) qed lemma collinear_subset: "\collinear T; S \ T\ \ collinear S" by (meson collinear_def subsetCE) lemma collinear_empty [iff]: "collinear {}" by (simp add: collinear_def) lemma collinear_sing [iff]: "collinear {x}" by (simp add: collinear_def) lemma collinear_2 [iff]: "collinear {x, y}" apply (simp add: collinear_def) apply (rule exI[where x="x - y"]) by (metis minus_diff_eq scaleR_left.minus scaleR_one) lemma collinear_lemma: "collinear {0, x, y} \ x = 0 \ y = 0 \ (\c. y = c *\<^sub>R x)" (is "?lhs \ ?rhs") proof (cases "x = 0 \ y = 0") case True then show ?thesis by (auto simp: insert_commute) next case False show ?thesis proof 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 cy False have cx0: "cx \ 0" and cy0: "cy \ 0" by auto let ?d = "cy / cx" from cx cy cx0 have "y = ?d *\<^sub>R x" by simp then show ?rhs using False by blast next assume h: "?rhs" then obtain c where c: "y = c *\<^sub>R x" using False by blast show ?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 qed qed lemma norm_cauchy_schwarz_equal: "\x \ y\ = norm x * norm y \ collinear {0, x, y}" proof (cases "x=0") case True then show ?thesis by (auto simp: insert_commute) next case False then have nnz: "norm x \ 0" by auto show ?thesis proof assume "\x \ y\ = norm x * norm y" then show "collinear {0, x, y}" unfolding norm_cauchy_schwarz_abs_eq collinear_lemma by (meson eq_vector_fraction_iff nnz) next assume "collinear {0, x, y}" with False show "\x \ y\ = norm x * norm y" unfolding norm_cauchy_schwarz_abs_eq collinear_lemma by (auto simp: abs_if) qed qed subsection\Properties of special hyperplanes\ lemma subspace_hyperplane: "subspace {x. a \ x = 0}" by (simp add: subspace_def inner_right_distrib) lemma subspace_hyperplane2: "subspace {x. x \ a = 0}" by (simp add: inner_commute inner_right_distrib subspace_def) lemma special_hyperplane_span: fixes S :: "'n::euclidean_space set" assumes "k \ Basis" shows "{x. k \ x = 0} = span (Basis - {k})" proof - have *: "x \ span (Basis - {k})" if "k \ x = 0" for x proof - have "x = (\b\Basis. (x \ b) *\<^sub>R b)" by (simp add: euclidean_representation) also have "... = (\b \ Basis - {k}. (x \ b) *\<^sub>R b)" by (auto simp: sum.remove [of _ k] inner_commute assms that) finally have "x = (\b\Basis - {k}. (x \ b) *\<^sub>R b)" . then show ?thesis by (simp add: span_finite) qed show ?thesis apply (rule span_subspace [symmetric]) using assms apply (auto simp: inner_not_same_Basis intro: * subspace_hyperplane) done qed lemma dim_special_hyperplane: fixes k :: "'n::euclidean_space" shows "k \ Basis \ dim {x. k \ x = 0} = DIM('n) - 1" apply (simp add: special_hyperplane_span) apply (rule dim_unique [OF subset_refl]) apply (auto simp: independent_substdbasis) apply (metis member_remove remove_def span_base) done proposition dim_hyperplane: fixes a :: "'a::euclidean_space" assumes "a \ 0" shows "dim {x. a \ x = 0} = DIM('a) - 1" proof - have span0: "span {x. a \ x = 0} = {x. a \ x = 0}" by (rule span_unique) (auto simp: subspace_hyperplane) then obtain B where "independent B" and Bsub: "B \ {x. a \ x = 0}" and subspB: "{x. a \ x = 0} \ span B" and card0: "(card B = dim {x. a \ x = 0})" and ortho: "pairwise orthogonal B" using orthogonal_basis_exists by metis with assms have "a \ span B" by (metis (mono_tags, lifting) span_eq inner_eq_zero_iff mem_Collect_eq span0) then have ind: "independent (insert a B)" by (simp add: \independent B\ independent_insert) have "finite B" using \independent B\ independent_bound by blast have "UNIV \ span (insert a B)" proof fix y::'a obtain r z where z: "y = r *\<^sub>R a + z" "a \ z = 0" apply (rule_tac r="(a \ y) / (a \ a)" and z = "y - ((a \ y) / (a \ a)) *\<^sub>R a" in that) using assms by (auto simp: algebra_simps) show "y \ span (insert a B)" by (metis (mono_tags, lifting) z Bsub span_eq_iff add_diff_cancel_left' mem_Collect_eq span0 span_breakdown_eq span_subspace subspB) qed then have dima: "DIM('a) = dim(insert a B)" by (metis independent_Basis span_Basis dim_eq_card top.extremum_uniqueI) then show ?thesis by (metis (mono_tags, lifting) Bsub Diff_insert_absorb \a \ span B\ ind card0 card_Diff_singleton dim_span indep_card_eq_dim_span insertI1 subsetCE subspB) qed lemma lowdim_eq_hyperplane: fixes S :: "'a::euclidean_space set" assumes "dim S = DIM('a) - 1" obtains a where "a \ 0" and "span S = {x. a \ x = 0}" proof - have dimS: "dim S < DIM('a)" by (simp add: assms) then obtain b where b: "b \ 0" "span S \ {a. b \ a = 0}" using lowdim_subset_hyperplane [of S] by fastforce show ?thesis apply (rule that[OF b(1)]) apply (rule subspace_dim_equal) by (auto simp: assms b dim_hyperplane dim_span subspace_hyperplane subspace_span) qed lemma dim_eq_hyperplane: fixes S :: "'n::euclidean_space set" shows "dim S = DIM('n) - 1 \ (\a. a \ 0 \ span S = {x. a \ x = 0})" by (metis One_nat_def dim_hyperplane dim_span lowdim_eq_hyperplane) subsection\ Orthogonal bases, Gram-Schmidt process, and related theorems\ lemma pairwise_orthogonal_independent: assumes "pairwise orthogonal S" and "0 \ S" shows "independent S" proof - have 0: "\x y. \x \ y; x \ S; y \ S\ \ x \ y = 0" using assms by (simp add: pairwise_def orthogonal_def) have "False" if "a \ S" and a: "a \ span (S - {a})" for a proof - obtain T U where "T \ S - {a}" "a = (\v\T. U v *\<^sub>R v)" using a by (force simp: span_explicit) then have "a \ a = a \ (\v\T. U v *\<^sub>R v)" by simp also have "... = 0" apply (simp add: inner_sum_right) apply (rule comm_monoid_add_class.sum.neutral) by (metis "0" DiffE \T \ S - {a}\ mult_not_zero singletonI subsetCE \a \ S\) finally show ?thesis using \0 \ S\ \a \ S\ by auto qed then show ?thesis by (force simp: dependent_def) qed lemma pairwise_orthogonal_imp_finite: fixes S :: "'a::euclidean_space set" assumes "pairwise orthogonal S" shows "finite S" proof - have "independent (S - {0})" apply (rule pairwise_orthogonal_independent) apply (metis Diff_iff assms pairwise_def) by blast then show ?thesis by (meson independent_imp_finite infinite_remove) qed lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}" by (simp add: subspace_def orthogonal_clauses) lemma subspace_orthogonal_to_vectors: "subspace {y. \x \ S. orthogonal x y}" by (simp add: subspace_def orthogonal_clauses) lemma orthogonal_to_span: assumes a: "a \ span S" and x: "\y. y \ S \ orthogonal x y" shows "orthogonal x a" by (metis a orthogonal_clauses(1,2,4) span_induct_alt x) proposition Gram_Schmidt_step: fixes S :: "'a::euclidean_space set" assumes S: "pairwise orthogonal S" and x: "x \ span S" shows "orthogonal x (a - (\b\S. (b \ a / (b \ b)) *\<^sub>R b))" proof - have "finite S" by (simp add: S pairwise_orthogonal_imp_finite) have "orthogonal (a - (\b\S. (b \ a / (b \ b)) *\<^sub>R b)) x" if "x \ S" for x proof - have "a \ x = (\y\S. if y = x then y \ a else 0)" by (simp add: \finite S\ inner_commute sum.delta that) also have "... = (\b\S. b \ a * (b \ x) / (b \ b))" apply (rule sum.cong [OF refl], simp) by (meson S orthogonal_def pairwise_def that) finally show ?thesis by (simp add: orthogonal_def algebra_simps inner_sum_left) qed then show ?thesis using orthogonal_to_span orthogonal_commute x by blast qed lemma orthogonal_extension_aux: fixes S :: "'a::euclidean_space set" assumes "finite T" "finite S" "pairwise orthogonal S" shows "\U. pairwise orthogonal (S \ U) \ span (S \ U) = span (S \ T)" using assms proof (induction arbitrary: S) case empty then show ?case by simp (metis sup_bot_right) next case (insert a T) have 0: "\x y. \x \ y; x \ S; y \ S\ \ x \ y = 0" using insert by (simp add: pairwise_def orthogonal_def) define a' where "a' = a - (\b\S. (b \ a / (b \ b)) *\<^sub>R b)" obtain U where orthU: "pairwise orthogonal (S \ insert a' U)" and spanU: "span (insert a' S \ U) = span (insert a' S \ T)" by (rule exE [OF insert.IH [of "insert a' S"]]) (auto simp: Gram_Schmidt_step a'_def insert.prems orthogonal_commute pairwise_orthogonal_insert span_clauses) have orthS: "\x. x \ S \ a' \ x = 0" apply (simp add: a'_def) using Gram_Schmidt_step [OF \pairwise orthogonal S\] apply (force simp: orthogonal_def inner_commute span_superset [THEN subsetD]) done have "span (S \ insert a' U) = span (insert a' (S \ T))" using spanU by simp also have "... = span (insert a (S \ T))" apply (rule eq_span_insert_eq) apply (simp add: a'_def span_neg span_sum span_base span_mul) done also have "... = span (S \ insert a T)" by simp finally show ?case by (rule_tac x="insert a' U" in exI) (use orthU in auto) qed proposition orthogonal_extension: fixes S :: "'a::euclidean_space set" assumes S: "pairwise orthogonal S" obtains U where "pairwise orthogonal (S \ U)" "span (S \ U) = span (S \ T)" proof - obtain B where "finite B" "span B = span T" using basis_subspace_exists [of "span T"] subspace_span by metis with orthogonal_extension_aux [of B S] obtain U where "pairwise orthogonal (S \ U)" "span (S \ U) = span (S \ B)" using assms pairwise_orthogonal_imp_finite by auto with \span B = span T\ show ?thesis by (rule_tac U=U in that) (auto simp: span_Un) qed corollary\<^marker>\tag unimportant\ orthogonal_extension_strong: fixes S :: "'a::euclidean_space set" assumes S: "pairwise orthogonal S" obtains U where "U \ (insert 0 S) = {}" "pairwise orthogonal (S \ U)" "span (S \ U) = span (S \ T)" proof - obtain U where "pairwise orthogonal (S \ U)" "span (S \ U) = span (S \ T)" using orthogonal_extension assms by blast then show ?thesis apply (rule_tac U = "U - (insert 0 S)" in that) apply blast apply (force simp: pairwise_def) apply (metis Un_Diff_cancel Un_insert_left span_redundant span_zero) done qed subsection\Decomposing a vector into parts in orthogonal subspaces\ text\existence of orthonormal basis for a subspace.\ lemma orthogonal_spanningset_subspace: fixes S :: "'a :: euclidean_space set" assumes "subspace S" obtains B where "B \ S" "pairwise orthogonal B" "span B = S" proof - obtain B where "B \ S" "independent B" "S \ span B" "card B = dim S" using basis_exists by blast with orthogonal_extension [of "{}" B] show ?thesis by (metis Un_empty_left assms pairwise_empty span_superset span_subspace that) qed lemma orthogonal_basis_subspace: fixes S :: "'a :: euclidean_space set" assumes "subspace S" obtains B where "0 \ B" "B \ S" "pairwise orthogonal B" "independent B" "card B = dim S" "span B = S" proof - obtain B where "B \ S" "pairwise orthogonal B" "span B = S" using assms orthogonal_spanningset_subspace by blast then show ?thesis apply (rule_tac B = "B - {0}" in that) apply (auto simp: indep_card_eq_dim_span pairwise_subset pairwise_orthogonal_independent elim: pairwise_subset) done qed proposition orthonormal_basis_subspace: fixes S :: "'a :: euclidean_space set" assumes "subspace S" obtains B where "B \ S" "pairwise orthogonal B" and "\x. x \ B \ norm x = 1" and "independent B" "card B = dim S" "span B = S" proof - obtain B where "0 \ B" "B \ S" and orth: "pairwise orthogonal B" and "independent B" "card B = dim S" "span B = S" by (blast intro: orthogonal_basis_subspace [OF assms]) have 1: "(\x. x /\<^sub>R norm x) ` B \ S" using \span B = S\ span_superset span_mul by fastforce have 2: "pairwise orthogonal ((\x. x /\<^sub>R norm x) ` B)" using orth by (force simp: pairwise_def orthogonal_clauses) have 3: "\x. x \ (\x. x /\<^sub>R norm x) ` B \ norm x = 1" by (metis (no_types, lifting) \0 \ B\ image_iff norm_sgn sgn_div_norm) have 4: "independent ((\x. x /\<^sub>R norm x) ` B)" by (metis "2" "3" norm_zero pairwise_orthogonal_independent zero_neq_one) have "inj_on (\x. x /\<^sub>R norm x) B" proof fix x y assume "x \ B" "y \ B" "x /\<^sub>R norm x = y /\<^sub>R norm y" moreover have "\i. i \ B \ norm (i /\<^sub>R norm i) = 1" using 3 by blast ultimately show "x = y" by (metis norm_eq_1 orth orthogonal_clauses(7) orthogonal_commute orthogonal_def pairwise_def zero_neq_one) qed then have 5: "card ((\x. x /\<^sub>R norm x) ` B) = dim S" by (metis \card B = dim S\ card_image) have 6: "span ((\x. x /\<^sub>R norm x) ` B) = S" by (metis "1" "4" "5" assms card_eq_dim independent_imp_finite span_subspace) show ?thesis by (rule that [OF 1 2 3 4 5 6]) qed proposition\<^marker>\tag unimportant\ orthogonal_to_subspace_exists_gen: fixes S :: "'a :: euclidean_space set" assumes "span S \ span T" obtains x where "x \ 0" "x \ span T" "\y. y \ span S \ orthogonal x y" proof - obtain B where "B \ span S" and orthB: "pairwise orthogonal B" and "\x. x \ B \ norm x = 1" and "independent B" "card B = dim S" "span B = span S" by (rule orthonormal_basis_subspace [of "span S", OF subspace_span]) (auto simp: dim_span) with assms obtain u where spanBT: "span B \ span T" and "u \ span B" "u \ span T" by auto obtain C where orthBC: "pairwise orthogonal (B \ C)" and spanBC: "span (B \ C) = span (B \ {u})" by (blast intro: orthogonal_extension [OF orthB]) show thesis proof (cases "C \ insert 0 B") case True then have "C \ span B" using span_eq by (metis span_insert_0 subset_trans) moreover have "u \ span (B \ C)" using \span (B \ C) = span (B \ {u})\ span_superset by force ultimately show ?thesis using True \u \ span B\ by (metis Un_insert_left span_insert_0 sup.orderE) next case False then obtain x where "x \ C" "x \ 0" "x \ B" by blast then have "x \ span T" by (metis (no_types, lifting) Un_insert_right Un_upper2 \u \ span T\ spanBT spanBC \u \ span T\ insert_subset span_superset span_mono span_span subsetCE subset_trans sup_bot.comm_neutral) moreover have "orthogonal x y" if "y \ span B" for y using that proof (rule span_induct) show "subspace {a. orthogonal x a}" by (simp add: subspace_orthogonal_to_vector) show "\b. b \ B \ orthogonal x b" by (metis Un_iff \x \ C\ \x \ B\ orthBC pairwise_def) qed ultimately show ?thesis using \x \ 0\ that \span B = span S\ by auto qed qed corollary\<^marker>\tag unimportant\ orthogonal_to_subspace_exists: fixes S :: "'a :: euclidean_space set" assumes "dim S < DIM('a)" obtains x where "x \ 0" "\y. y \ span S \ orthogonal x y" proof - have "span S \ UNIV" by (metis (mono_tags) UNIV_I assms inner_eq_zero_iff less_le lowdim_subset_hyperplane mem_Collect_eq top.extremum_strict top.not_eq_extremum) with orthogonal_to_subspace_exists_gen [of S UNIV] that show ?thesis by (auto simp: span_UNIV) qed corollary\<^marker>\tag unimportant\ orthogonal_to_vector_exists: fixes x :: "'a :: euclidean_space" assumes "2 \ DIM('a)" obtains y where "y \ 0" "orthogonal x y" proof - have "dim {x} < DIM('a)" using assms by auto then show thesis by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that) qed proposition\<^marker>\tag unimportant\ orthogonal_subspace_decomp_exists: fixes S :: "'a :: euclidean_space set" obtains y z where "y \ span S" and "\w. w \ span S \ orthogonal z w" and "x = y + z" proof - obtain T where "0 \ T" "T \ span S" "pairwise orthogonal T" "independent T" "card T = dim (span S)" "span T = span S" using orthogonal_basis_subspace subspace_span by blast let ?a = "\b\T. (b \ x / (b \ b)) *\<^sub>R b" have orth: "orthogonal (x - ?a) w" if "w \ span S" for w by (simp add: Gram_Schmidt_step \pairwise orthogonal T\ \span T = span S\ orthogonal_commute that) show ?thesis apply (rule_tac y = "?a" and z = "x - ?a" in that) apply (meson \T \ span S\ span_scale span_sum subsetCE) apply (fact orth, simp) done qed lemma orthogonal_subspace_decomp_unique: fixes S :: "'a :: euclidean_space set" assumes "x + y = x' + y'" and ST: "x \ span S" "x' \ span S" "y \ span T" "y' \ span T" and orth: "\a b. \a \ S; b \ T\ \ orthogonal a b" shows "x = x' \ y = y'" proof - have "x + y - y' = x'" by (simp add: assms) moreover have "\a b. \a \ span S; b \ span T\ \ orthogonal a b" by (meson orth orthogonal_commute orthogonal_to_span) ultimately have "0 = x' - x" by (metis (full_types) add_diff_cancel_left' ST diff_right_commute orthogonal_clauses(10) orthogonal_clauses(5) orthogonal_self) with assms show ?thesis by auto qed lemma vector_in_orthogonal_spanningset: fixes a :: "'a::euclidean_space" obtains S where "a \ S" "pairwise orthogonal S" "span S = UNIV" by (metis UNIV_I Un_iff empty_iff insert_subset orthogonal_extension pairwise_def pairwise_orthogonal_insert span_UNIV subsetI subset_antisym) lemma vector_in_orthogonal_basis: fixes a :: "'a::euclidean_space" assumes "a \ 0" obtains S where "a \ S" "0 \ S" "pairwise orthogonal S" "independent S" "finite S" "span S = UNIV" "card S = DIM('a)" proof - obtain S where S: "a \ S" "pairwise orthogonal S" "span S = UNIV" using vector_in_orthogonal_spanningset . show thesis proof show "pairwise orthogonal (S - {0})" using pairwise_mono S(2) by blast show "independent (S - {0})" by (simp add: \pairwise orthogonal (S - {0})\ pairwise_orthogonal_independent) show "finite (S - {0})" using \independent (S - {0})\ independent_imp_finite by blast show "card (S - {0}) = DIM('a)" using span_delete_0 [of S] S by (simp add: \independent (S - {0})\ indep_card_eq_dim_span dim_UNIV) qed (use S \a \ 0\ in auto) qed lemma vector_in_orthonormal_basis: fixes a :: "'a::euclidean_space" assumes "norm a = 1" obtains S where "a \ S" "pairwise orthogonal S" "\x. x \ S \ norm x = 1" "independent S" "card S = DIM('a)" "span S = UNIV" proof - have "a \ 0" using assms by auto then obtain S where "a \ S" "0 \ S" "finite S" and S: "pairwise orthogonal S" "independent S" "span S = UNIV" "card S = DIM('a)" by (metis vector_in_orthogonal_basis) let ?S = "(\x. x /\<^sub>R norm x) ` S" show thesis proof show "a \ ?S" using \a \ S\ assms image_iff by fastforce next show "pairwise orthogonal ?S" using \pairwise orthogonal S\ by (auto simp: pairwise_def orthogonal_def) show "\x. x \ (\x. x /\<^sub>R norm x) ` S \ norm x = 1" using \0 \ S\ by (auto simp: field_split_simps) then show "independent ?S" by (metis \pairwise orthogonal ((\x. x /\<^sub>R norm x) ` S)\ norm_zero pairwise_orthogonal_independent zero_neq_one) have "inj_on (\x. x /\<^sub>R norm x) S" unfolding inj_on_def by (metis (full_types) S(1) \0 \ S\ inverse_nonzero_iff_nonzero norm_eq_zero orthogonal_scaleR orthogonal_self pairwise_def) then show "card ?S = DIM('a)" by (simp add: card_image S) show "span ?S = UNIV" by (metis (no_types) \0 \ S\ \finite S\ \span S = UNIV\ field_class.field_inverse_zero inverse_inverse_eq less_irrefl span_image_scale zero_less_norm_iff) qed qed proposition dim_orthogonal_sum: fixes A :: "'a::euclidean_space set" assumes "\x y. \x \ A; y \ B\ \ x \ y = 0" shows "dim(A \ B) = dim A + dim B" proof - have 1: "\x y. \x \ span A; y \ B\ \ x \ y = 0" by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms) have "\x y. \x \ span A; y \ span B\ \ x \ y = 0" using 1 by (simp add: span_induct [OF _ subspace_hyperplane]) then have 0: "\x y. \x \ span A; y \ span B\ \ x \ y = 0" by simp have "dim(A \ B) = dim (span (A \ B))" by (simp add: dim_span) also have "span (A \ B) = ((\(a, b). a + b) ` (span A \ span B))" by (auto simp add: span_Un image_def) also have "dim \ = dim {x + y |x y. x \ span A \ y \ span B}" by (auto intro!: arg_cong [where f=dim]) also have "... = dim {x + y |x y. x \ span A \ y \ span B} + dim(span A \ span B)" by (auto simp: dest: 0) also have "... = dim (span A) + dim (span B)" by (rule dim_sums_Int) (auto simp: subspace_span) also have "... = dim A + dim B" by (simp add: dim_span) finally show ?thesis . qed lemma dim_subspace_orthogonal_to_vectors: fixes A :: "'a::euclidean_space set" assumes "subspace A" "subspace B" "A \ B" shows "dim {y \ B. \x \ A. orthogonal x y} + dim A = dim B" proof - have "dim (span ({y \ B. \x\A. orthogonal x y} \ A)) = dim (span B)" proof (rule arg_cong [where f=dim, OF subset_antisym]) show "span ({y \ B. \x\A. orthogonal x y} \ A) \ span B" by (simp add: \A \ B\ Collect_restrict span_mono) next have *: "x \ span ({y \ B. \x\A. orthogonal x y} \ A)" if "x \ B" for x proof - obtain y z where "x = y + z" "y \ span A" and orth: "\w. w \ span A \ orthogonal z w" using orthogonal_subspace_decomp_exists [of A x] that by auto have "y \ span B" using \y \ span A\ assms(3) span_mono by blast then have "z \ {a \ B. \x. x \ A \ orthogonal x a}" apply simp using \x = y + z\ assms(1) assms(2) orth orthogonal_commute span_add_eq span_eq_iff that by blast then have z: "z \ span {y \ B. \x\A. orthogonal x y}" by (meson span_superset subset_iff) then show ?thesis apply (auto simp: span_Un image_def \x = y + z\ \y \ span A\) using \y \ span A\ add.commute by blast qed show "span B \ span ({y \ B. \x\A. orthogonal x y} \ A)" by (rule span_minimal) (auto intro: * span_minimal simp: subspace_span) qed then show ?thesis by (metis (no_types, lifting) dim_orthogonal_sum dim_span mem_Collect_eq orthogonal_commute orthogonal_def) qed subsection\Linear functions are (uniformly) continuous on any set\ subsection\<^marker>\tag unimportant\ \Topological properties of linear functions\ lemma linear_lim_0: assumes "bounded_linear f" shows "(f \ 0) (at (0))" proof - interpret f: bounded_linear f by fact have "(f \ f 0) (at 0)" using tendsto_ident_at by (rule f.tendsto) then show ?thesis unfolding f.zero . qed lemma linear_continuous_at: assumes "bounded_linear f" shows "continuous (at a) f" unfolding continuous_at using assms apply (rule bounded_linear.tendsto) apply (rule tendsto_ident_at) done lemma linear_continuous_within: "bounded_linear f \ continuous (at x within s) f" using continuous_at_imp_continuous_at_within linear_continuous_at by blast lemma linear_continuous_on: "bounded_linear f \ continuous_on s f" using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto lemma Lim_linear: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" and h :: "'b \ 'c::real_normed_vector" assumes "(f \ l) F" "linear h" shows "((\x. h(f x)) \ h l) F" proof - obtain B where B: "B > 0" "\x. norm (h x) \ B * norm x" using linear_bounded_pos [OF \linear h\] by blast show ?thesis unfolding tendsto_iff proof (intro allI impI) show "\\<^sub>F x in F. dist (h (f x)) (h l) < e" if "e > 0" for e proof - have "\\<^sub>F x in F. dist (f x) l < e/B" by (simp add: \0 < B\ assms(1) tendstoD that) then show ?thesis unfolding dist_norm proof (rule eventually_mono) show "norm (h (f x) - h l) < e" if "norm (f x - l) < e / B" for x using that B apply (simp add: field_split_simps) by (metis \linear h\ le_less_trans linear_diff mult.commute) qed qed qed qed lemma linear_continuous_compose: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" and g :: "'b \ 'c::real_normed_vector" assumes "continuous F f" "linear g" shows "continuous F (\x. g(f x))" using assms unfolding continuous_def by (rule Lim_linear) lemma linear_continuous_on_compose: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" and g :: "'b \ 'c::real_normed_vector" assumes "continuous_on S f" "linear g" shows "continuous_on S (\x. g(f x))" using assms by (simp add: continuous_on_eq_continuous_within linear_continuous_compose) text\Also bilinear functions, in composition form\ lemma bilinear_continuous_compose: fixes h :: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector" assumes "continuous F f" "continuous F g" "bilinear h" shows "continuous F (\x. h (f x) (g x))" using assms bilinear_conv_bounded_bilinear bounded_bilinear.continuous by blast lemma bilinear_continuous_on_compose: fixes h :: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector" and f :: "'d::t2_space \ 'a" assumes "continuous_on S f" "continuous_on S g" "bilinear h" shows "continuous_on S (\x. h (f x) (g x))" using assms by (simp add: continuous_on_eq_continuous_within bilinear_continuous_compose) end