--- a/src/HOL/Library/Convex_Euclidean_Space.thy Fri Jun 12 16:23:07 2009 -0700
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy Fri Jun 12 22:20:36 2009 -0700
@@ -384,28 +384,28 @@
lemma convex_Int: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<inter> t)"
unfolding convex_def by auto
-lemma convex_halfspace_le: "convex {x. a \<bullet> x \<le> b}"
+lemma convex_halfspace_le: "convex {x. inner a x \<le> b}"
unfolding convex_def apply auto
- unfolding dot_radd dot_rmult [where 'a=real, unfolded smult_conv_scaleR]
+ unfolding inner_add inner_scaleR
by (metis real_convex_bound_le)
-lemma convex_halfspace_ge: "convex {x. a \<bullet> x \<ge> b}"
-proof- have *:"{x. a \<bullet> x \<ge> b} = {x. -a \<bullet> x \<le> -b}" by auto
+lemma convex_halfspace_ge: "convex {x. inner a x \<ge> b}"
+proof- have *:"{x. inner a x \<ge> b} = {x. inner (-a) x \<le> -b}" by auto
show ?thesis apply(unfold *) using convex_halfspace_le[of "-a" "-b"] by auto qed
-lemma convex_hyperplane: "convex {x. a \<bullet> x = b}"
+lemma convex_hyperplane: "convex {x. inner a x = b}"
proof-
- have *:"{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}" by auto
+ have *:"{x. inner a x = b} = {x. inner a x \<le> b} \<inter> {x. inner a x \<ge> b}" by auto
show ?thesis unfolding * apply(rule convex_Int)
using convex_halfspace_le convex_halfspace_ge by auto
qed
-lemma convex_halfspace_lt: "convex {x. a \<bullet> x < b}"
+lemma convex_halfspace_lt: "convex {x. inner a x < b}"
unfolding convex_def
- by(auto simp add: real_convex_bound_lt dot_radd dot_rmult [where 'a=real, unfolded smult_conv_scaleR])
-
-lemma convex_halfspace_gt: "convex {x. a \<bullet> x > b}"
- using convex_halfspace_lt[of "-a" "-b"] by(auto simp add: dot_lneg neg_less_iff_less)
+ by(auto simp add: real_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_positive_orthant: "convex {x::real^'n::finite. (\<forall>i. 0 \<le> x$i)}"
unfolding convex_def apply auto apply(erule_tac x=i in allE)+
@@ -1360,16 +1360,16 @@
fixes a b d :: "real ^ 'n::finite"
assumes "d \<noteq> 0"
shows "dist a (b + d) > dist a b \<or> dist a (b - d) > dist a b"
-proof(cases "a \<bullet> d - b \<bullet> d > 0")
- case True hence "0 < d \<bullet> d + (a \<bullet> d * 2 - b \<bullet> d * 2)"
+proof(cases "inner a d - inner b d > 0")
+ case True hence "0 < inner d d + (inner a d * 2 - inner b d * 2)"
apply(rule_tac add_pos_pos) using assms by auto
- thus ?thesis apply(rule_tac disjI2) unfolding dist_norm and real_vector_norm_def and real_sqrt_less_iff
- by(simp add: dot_rsub dot_radd dot_lsub dot_ladd dot_sym field_simps)
+ thus ?thesis apply(rule_tac disjI2) unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff
+ by (simp add: algebra_simps inner_commute)
next
- case False hence "0 < d \<bullet> d + (b \<bullet> d * 2 - a \<bullet> d * 2)"
+ case False hence "0 < inner d d + (inner b d * 2 - inner a d * 2)"
apply(rule_tac add_pos_nonneg) using assms by auto
- thus ?thesis apply(rule_tac disjI1) unfolding dist_norm and real_vector_norm_def and real_sqrt_less_iff
- by(simp add: dot_rsub dot_radd dot_lsub dot_ladd dot_sym field_simps)
+ thus ?thesis apply(rule_tac disjI1) unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff
+ by (simp add: algebra_simps inner_commute)
qed
lemma norm_increases_online:
@@ -1504,19 +1504,27 @@
"closed s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> (closest_point s x = x \<longleftrightarrow> x \<in> s)"
using closest_point_in_set[of s x] closest_point_self[of x s] by auto
+(* TODO: move *)
+lemma norm_lt: "norm x < norm y \<longleftrightarrow> inner x x < inner y y"
+ unfolding norm_eq_sqrt_inner by simp
+
+(* TODO: move *)
+lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> inner x x \<le> inner y y"
+ unfolding norm_eq_sqrt_inner by simp
+
lemma closer_points_lemma: fixes y::"real^'n::finite"
- assumes "y \<bullet> z > 0"
+ assumes "inner y z > 0"
shows "\<exists>u>0. \<forall>v>0. v \<le> u \<longrightarrow> norm(v *\<^sub>R z - y) < norm y"
-proof- have z:"z \<bullet> z > 0" unfolding dot_pos_lt using assms by auto
- thus ?thesis using assms apply(rule_tac x="(y \<bullet> z) / (z \<bullet> z)" in exI) apply(rule) defer proof(rule+)
- fix v assume "0<v" "v \<le> y \<bullet> z / (z \<bullet> z)"
+proof- have z:"inner z z > 0" unfolding inner_gt_zero_iff using assms by auto
+ thus ?thesis using assms apply(rule_tac x="inner y z / inner z z" in exI) apply(rule) defer proof(rule+)
+ fix v assume "0<v" "v \<le> inner y z / inner z z"
thus "norm (v *\<^sub>R z - y) < norm y" unfolding norm_lt using z and assms
- by (simp add: field_simps dot_sym mult_strict_left_mono[OF _ `0<v`] dot_rmult [where 'a=real, unfolded smult_conv_scaleR])
+ by (simp add: field_simps inner_diff inner_commute mult_strict_left_mono[OF _ `0<v`])
qed(rule divide_pos_pos, auto) qed
lemma closer_point_lemma:
fixes x y z :: "real ^ 'n::finite"
- assumes "(y - x) \<bullet> (z - x) > 0"
+ assumes "inner (y - x) (z - x) > 0"
shows "\<exists>u>0. u \<le> 1 \<and> dist (x + u *\<^sub>R (z - x)) y < dist x y"
proof- obtain u where "u>0" and u:"\<forall>v>0. v \<le> u \<longrightarrow> norm (v *\<^sub>R (z - x) - (y - x)) < norm (y - x)"
using closer_points_lemma[OF assms] by auto
@@ -1525,17 +1533,30 @@
lemma any_closest_point_dot:
assumes "convex s" "closed s" "x \<in> s" "y \<in> s" "\<forall>z\<in>s. dist a x \<le> dist a z"
- shows "(a - x) \<bullet> (y - x) \<le> 0"
-proof(rule ccontr) assume "\<not> (a - x) \<bullet> (y - x) \<le> 0"
+ shows "inner (a - x) (y - x) \<le> 0"
+proof(rule ccontr) assume "\<not> inner (a - x) (y - x) \<le> 0"
then obtain u where u:"u>0" "u\<le>1" "dist (x + u *\<^sub>R (y - x)) a < dist x a" using closer_point_lemma[of a x y] by auto
let ?z = "(1 - u) *\<^sub>R x + u *\<^sub>R y" have "?z \<in> s" using mem_convex[OF assms(1,3,4), of u] using u by auto
thus False using assms(5)[THEN bspec[where x="?z"]] and u(3) by (auto simp add: dist_commute algebra_simps) qed
+(* TODO: move *)
+lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> inner x x \<le> a\<twosuperior>"
+proof -
+ have "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> norm x \<le> a"
+ using norm_ge_zero [of x] by arith
+ also have "\<dots> \<longleftrightarrow> 0 \<le> a \<and> (norm x)\<twosuperior> \<le> a\<twosuperior>"
+ by (auto intro: power_mono dest: power2_le_imp_le)
+ also have "\<dots> \<longleftrightarrow> 0 \<le> a \<and> inner x x \<le> a\<twosuperior>"
+ unfolding power2_norm_eq_inner ..
+ finally show ?thesis .
+qed
+
lemma any_closest_point_unique:
assumes "convex s" "closed s" "x \<in> s" "y \<in> s"
"\<forall>z\<in>s. dist a x \<le> dist a z" "\<forall>z\<in>s. dist a y \<le> dist a z"
shows "x = y" using any_closest_point_dot[OF assms(1-4,5)] and any_closest_point_dot[OF assms(1-2,4,3,6)]
- unfolding norm_pths(1) and norm_le_square by auto
+ unfolding norm_pths(1) and norm_le_square
+ by (auto simp add: algebra_simps)
lemma closest_point_unique:
assumes "convex s" "closed s" "x \<in> s" "\<forall>z\<in>s. dist a x \<le> dist a z"
@@ -1545,7 +1566,7 @@
lemma closest_point_dot:
assumes "convex s" "closed s" "x \<in> s"
- shows "(a - closest_point s a) \<bullet> (x - closest_point s a) \<le> 0"
+ shows "inner (a - closest_point s a) (x - closest_point s a) \<le> 0"
apply(rule any_closest_point_dot[OF assms(1,2) _ assms(3)])
using closest_point_exists[OF assms(2)] and assms(3) by auto
@@ -1560,13 +1581,13 @@
assumes "convex s" "closed s" "s \<noteq> {}"
shows "dist (closest_point s x) (closest_point s y) \<le> dist x y"
proof-
- have "(x - closest_point s x) \<bullet> (closest_point s y - closest_point s x) \<le> 0"
- "(y - closest_point s y) \<bullet> (closest_point s x - closest_point s y) \<le> 0"
+ have "inner (x - closest_point s x) (closest_point s y - closest_point s x) \<le> 0"
+ "inner (y - closest_point s y) (closest_point s x - closest_point s y) \<le> 0"
apply(rule_tac[!] any_closest_point_dot[OF assms(1-2)])
using closest_point_exists[OF assms(2-3)] by auto
thus ?thesis unfolding dist_norm and norm_le
- using dot_pos_le[of "(x - closest_point s x) - (y - closest_point s y)"]
- by (auto simp add: dot_sym dot_ladd dot_radd) qed
+ using inner_ge_zero[of "(x - closest_point s x) - (y - closest_point s y)"]
+ by (simp add: inner_add inner_diff inner_commute) qed
lemma continuous_at_closest_point:
assumes "convex s" "closed s" "s \<noteq> {}"
@@ -1583,50 +1604,50 @@
lemma supporting_hyperplane_closed_point:
assumes "convex s" "closed s" "s \<noteq> {}" "z \<notin> s"
- shows "\<exists>a b. \<exists>y\<in>s. a \<bullet> z < b \<and> (a \<bullet> y = b) \<and> (\<forall>x\<in>s. a \<bullet> x \<ge> b)"
+ shows "\<exists>a b. \<exists>y\<in>s. inner a z < b \<and> (inner a y = b) \<and> (\<forall>x\<in>s. inner a x \<ge> b)"
proof-
from distance_attains_inf[OF assms(2-3)] obtain y where "y\<in>s" and y:"\<forall>x\<in>s. dist z y \<le> dist z x" by auto
- show ?thesis apply(rule_tac x="y - z" in exI, rule_tac x="(y - z) \<bullet> y" in exI, rule_tac x=y in bexI)
+ show ?thesis apply(rule_tac x="y - z" in exI, rule_tac x="inner (y - z) y" in exI, rule_tac x=y in bexI)
apply rule defer apply rule defer apply(rule, rule ccontr) using `y\<in>s` proof-
- show "(y - z) \<bullet> z < (y - z) \<bullet> y" apply(subst diff_less_iff(1)[THEN sym])
- unfolding dot_rsub[THEN sym] and dot_pos_lt using `y\<in>s` `z\<notin>s` by auto
+ show "inner (y - z) z < inner (y - z) y" apply(subst diff_less_iff(1)[THEN sym])
+ unfolding inner_diff_right[THEN sym] and inner_gt_zero_iff using `y\<in>s` `z\<notin>s` by auto
next
fix x assume "x\<in>s" have *:"\<forall>u. 0 \<le> u \<and> u \<le> 1 \<longrightarrow> dist z y \<le> dist z ((1 - u) *\<^sub>R y + u *\<^sub>R x)"
using assms(1)[unfolded convex_alt] and y and `x\<in>s` and `y\<in>s` by auto
- assume "\<not> (y - z) \<bullet> y \<le> (y - z) \<bullet> x" then obtain v where
- "v>0" "v\<le>1" "dist (y + v *\<^sub>R (x - y)) z < dist y z" using closer_point_lemma[of z y x] by auto
+ assume "\<not> inner (y - z) y \<le> inner (y - z) x" then obtain v where
+ "v>0" "v\<le>1" "dist (y + v *\<^sub>R (x - y)) z < dist y z" using closer_point_lemma[of z y x] apply - by (auto simp add: inner_diff)
thus False using *[THEN spec[where x=v]] by(auto simp add: dist_commute algebra_simps)
qed auto
qed
lemma separating_hyperplane_closed_point:
assumes "convex s" "closed s" "z \<notin> s"
- shows "\<exists>a b. a \<bullet> z < b \<and> (\<forall>x\<in>s. a \<bullet> x > b)"
+ shows "\<exists>a b. inner a z < b \<and> (\<forall>x\<in>s. inner a x > b)"
proof(cases "s={}")
case True thus ?thesis apply(rule_tac x="-z" in exI, rule_tac x=1 in exI)
- using less_le_trans[OF _ dot_pos_le[of z]] by auto
+ using less_le_trans[OF _ inner_ge_zero[of z]] by auto
next
case False obtain y where "y\<in>s" and y:"\<forall>x\<in>s. dist z y \<le> dist z x"
using distance_attains_inf[OF assms(2) False] by auto
- show ?thesis apply(rule_tac x="y - z" in exI, rule_tac x="(y - z) \<bullet> z + (norm(y - z))\<twosuperior> / 2" in exI)
+ show ?thesis apply(rule_tac x="y - z" in exI, rule_tac x="inner (y - z) z + (norm(y - z))\<twosuperior> / 2" in exI)
apply rule defer apply rule proof-
fix x assume "x\<in>s"
- have "\<not> 0 < (z - y) \<bullet> (x - y)" apply(rule_tac notI) proof(drule closer_point_lemma)
+ have "\<not> 0 < inner (z - y) (x - y)" apply(rule_tac notI) proof(drule closer_point_lemma)
assume "\<exists>u>0. u \<le> 1 \<and> dist (y + u *\<^sub>R (x - y)) z < dist y z"
then obtain u where "u>0" "u\<le>1" "dist (y + u *\<^sub>R (x - y)) z < dist y z" by auto
thus False using y[THEN bspec[where x="y + u *\<^sub>R (x - y)"]]
using assms(1)[unfolded convex_alt, THEN bspec[where x=y]]
using `x\<in>s` `y\<in>s` by (auto simp add: dist_commute algebra_simps) qed
moreover have "0 < norm (y - z) ^ 2" using `y\<in>s` `z\<notin>s` by auto
- hence "0 < (y - z) \<bullet> (y - z)" unfolding norm_pow_2 by simp
- ultimately show "(y - z) \<bullet> z + (norm (y - z))\<twosuperior> / 2 < (y - z) \<bullet> x"
- unfolding norm_pow_2 and dlo_simps(3) by (auto simp add: field_simps dot_sym)
+ hence "0 < inner (y - z) (y - z)" unfolding power2_norm_eq_inner by simp
+ ultimately show "inner (y - z) z + (norm (y - z))\<twosuperior> / 2 < inner (y - z) x"
+ unfolding power2_norm_eq_inner and not_less by (auto simp add: field_simps inner_commute inner_diff)
qed(insert `y\<in>s` `z\<notin>s`, auto)
qed
lemma separating_hyperplane_closed_0:
assumes "convex (s::(real^'n::finite) set)" "closed s" "0 \<notin> s"
- shows "\<exists>a b. a \<noteq> 0 \<and> 0 < b \<and> (\<forall>x\<in>s. a \<bullet> x > b)"
+ shows "\<exists>a b. a \<noteq> 0 \<and> 0 < b \<and> (\<forall>x\<in>s. inner a x > b)"
proof(cases "s={}") guess a using UNIV_witness[where 'a='n] ..
case True have "norm ((basis a)::real^'n::finite) = 1"
using norm_basis and dimindex_ge_1 by auto
@@ -1638,41 +1659,41 @@
lemma separating_hyperplane_closed_compact:
assumes "convex (s::(real^'n::finite) set)" "closed s" "convex t" "compact t" "t \<noteq> {}" "s \<inter> t = {}"
- shows "\<exists>a b. (\<forall>x\<in>s. a \<bullet> x < b) \<and> (\<forall>x\<in>t. a \<bullet> x > b)"
+ shows "\<exists>a b. (\<forall>x\<in>s. inner a x < b) \<and> (\<forall>x\<in>t. inner a x > b)"
proof(cases "s={}")
case True
obtain b where b:"b>0" "\<forall>x\<in>t. norm x \<le> b" using compact_imp_bounded[OF assms(4)] unfolding bounded_pos by auto
obtain z::"real^'n" where z:"norm z = b + 1" using vector_choose_size[of "b + 1"] and b(1) by auto
hence "z\<notin>t" using b(2)[THEN bspec[where x=z]] by auto
- then obtain a b where ab:"a \<bullet> z < b" "\<forall>x\<in>t. b < a \<bullet> x"
+ then obtain a b where ab:"inner a z < b" "\<forall>x\<in>t. b < inner a x"
using separating_hyperplane_closed_point[OF assms(3) compact_imp_closed[OF assms(4)], of z] by auto
thus ?thesis using True by auto
next
case False then obtain y where "y\<in>s" by auto
- obtain a b where "0 < b" "\<forall>x\<in>{x - y |x y. x \<in> s \<and> y \<in> t}. b < a \<bullet> x"
+ obtain a b where "0 < b" "\<forall>x\<in>{x - y |x y. x \<in> s \<and> y \<in> t}. b < inner a x"
using separating_hyperplane_closed_point[OF convex_differences[OF assms(1,3)], of 0]
using closed_compact_differences[OF assms(2,4)] using assms(6) by(auto, blast)
- hence ab:"\<forall>x\<in>s. \<forall>y\<in>t. b + a \<bullet> y < a \<bullet> x" apply- apply(rule,rule) apply(erule_tac x="x - y" in ballE) by auto
- def k \<equiv> "rsup ((\<lambda>x. a \<bullet> x) ` t)"
+ hence ab:"\<forall>x\<in>s. \<forall>y\<in>t. b + inner a y < inner a x" apply- apply(rule,rule) apply(erule_tac x="x - y" in ballE) by (auto simp add: inner_diff)
+ def k \<equiv> "rsup ((\<lambda>x. inner a x) ` t)"
show ?thesis apply(rule_tac x="-a" in exI, rule_tac x="-(k + b / 2)" in exI)
- apply(rule,rule) defer apply(rule) unfolding dot_lneg and neg_less_iff_less proof-
- from ab have "((\<lambda>x. a \<bullet> x) ` t) *<= (a \<bullet> y - b)"
+ apply(rule,rule) defer apply(rule) unfolding inner_minus_left and neg_less_iff_less proof-
+ from ab have "((\<lambda>x. inner a x) ` t) *<= (inner a y - b)"
apply(erule_tac x=y in ballE) apply(rule setleI) using `y\<in>s` by auto
- hence k:"isLub UNIV ((\<lambda>x. a \<bullet> x) ` t) k" unfolding k_def apply(rule_tac rsup) using assms(5) by auto
- fix x assume "x\<in>t" thus "a \<bullet> x < (k + b / 2)" using `0<b` and isLubD2[OF k, of "a \<bullet> x"] by auto
+ hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac rsup) using assms(5) by auto
+ fix x assume "x\<in>t" thus "inner a x < (k + b / 2)" using `0<b` and isLubD2[OF k, of "inner a x"] by auto
next
fix x assume "x\<in>s"
- hence "k \<le> a \<bullet> x - b" unfolding k_def apply(rule_tac rsup_le) using assms(5)
+ hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac rsup_le) using assms(5)
unfolding setle_def
using ab[THEN bspec[where x=x]] by auto
- thus "k + b / 2 < a \<bullet> x" using `0 < b` by auto
+ thus "k + b / 2 < inner a x" using `0 < b` by auto
qed
qed
lemma separating_hyperplane_compact_closed:
assumes "convex s" "compact s" "s \<noteq> {}" "convex t" "closed t" "s \<inter> t = {}"
- shows "\<exists>a b. (\<forall>x\<in>s. a \<bullet> x < b) \<and> (\<forall>x\<in>t. a \<bullet> x > b)"
-proof- obtain a b where "(\<forall>x\<in>t. a \<bullet> x < b) \<and> (\<forall>x\<in>s. b < a \<bullet> x)"
+ shows "\<exists>a b. (\<forall>x\<in>s. inner a x < b) \<and> (\<forall>x\<in>t. inner a x > b)"
+proof- obtain a b where "(\<forall>x\<in>t. inner a x < b) \<and> (\<forall>x\<in>s. b < inner a x)"
using separating_hyperplane_closed_compact[OF assms(4-5,1-2,3)] and assms(6) by auto
thus ?thesis apply(rule_tac x="-a" in exI, rule_tac x="-b" in exI) by auto qed
@@ -1680,33 +1701,33 @@
lemma separating_hyperplane_set_0:
assumes "convex s" "(0::real^'n::finite) \<notin> s"
- shows "\<exists>a. a \<noteq> 0 \<and> (\<forall>x\<in>s. 0 \<le> a \<bullet> x)"
-proof- let ?k = "\<lambda>c. {x::real^'n. 0 \<le> c \<bullet> x}"
+ shows "\<exists>a. a \<noteq> 0 \<and> (\<forall>x\<in>s. 0 \<le> inner a x)"
+proof- let ?k = "\<lambda>c. {x::real^'n. 0 \<le> inner c x}"
have "frontier (cball 0 1) \<inter> (\<Inter> (?k ` s)) \<noteq> {}"
apply(rule compact_imp_fip) apply(rule compact_frontier[OF compact_cball])
defer apply(rule,rule,erule conjE) proof-
fix f assume as:"f \<subseteq> ?k ` s" "finite f"
obtain c where c:"f = ?k ` c" "c\<subseteq>s" "finite c" using finite_subset_image[OF as(2,1)] by auto
- then obtain a b where ab:"a \<noteq> 0" "0 < b" "\<forall>x\<in>convex hull c. b < a \<bullet> x"
+ then obtain a b where ab:"a \<noteq> 0" "0 < b" "\<forall>x\<in>convex hull c. b < inner a x"
using separating_hyperplane_closed_0[OF convex_convex_hull, of c]
using finite_imp_compact_convex_hull[OF c(3), THEN compact_imp_closed] and assms(2)
using subset_hull[unfolded mem_def, of convex, OF assms(1), THEN sym, of c] by auto
- hence "\<exists>x. norm x = 1 \<and> (\<forall>y\<in>c. 0 \<le> y \<bullet> x)" apply(rule_tac x="inverse(norm a) *\<^sub>R a" in exI)
- using hull_subset[of c convex] unfolding subset_eq and dot_rmult [where 'a=real, unfolded smult_conv_scaleR]
+ hence "\<exists>x. norm x = 1 \<and> (\<forall>y\<in>c. 0 \<le> inner y x)" apply(rule_tac x="inverse(norm a) *\<^sub>R a" in exI)
+ using hull_subset[of c convex] unfolding subset_eq and inner_scaleR
apply- apply rule defer apply rule apply(rule mult_nonneg_nonneg)
- by(auto simp add: dot_sym elim!: ballE)
+ by(auto simp add: inner_commute elim!: ballE)
thus "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}" unfolding c(1) frontier_cball dist_norm by auto
qed(insert closed_halfspace_ge, auto)
then obtain x where "norm x = 1" "\<forall>y\<in>s. x\<in>?k y" unfolding frontier_cball dist_norm by auto
- thus ?thesis apply(rule_tac x=x in exI) by(auto simp add: dot_sym) qed
+ thus ?thesis apply(rule_tac x=x in exI) by(auto simp add: inner_commute) qed
lemma separating_hyperplane_sets:
assumes "convex s" "convex (t::(real^'n::finite) set)" "s \<noteq> {}" "t \<noteq> {}" "s \<inter> t = {}"
- shows "\<exists>a b. a \<noteq> 0 \<and> (\<forall>x\<in>s. a \<bullet> x \<le> b) \<and> (\<forall>x\<in>t. a \<bullet> x \<ge> b)"
+ shows "\<exists>a b. a \<noteq> 0 \<and> (\<forall>x\<in>s. inner a x \<le> b) \<and> (\<forall>x\<in>t. inner a x \<ge> b)"
proof- from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
- obtain a where "a\<noteq>0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> a \<bullet> x" using assms(3-5) by auto
- hence "\<forall>x\<in>t. \<forall>y\<in>s. a \<bullet> y \<le> a \<bullet> x" apply- apply(rule, rule) apply(erule_tac x="x - y" in ballE) by auto
- thus ?thesis apply(rule_tac x=a in exI, rule_tac x="rsup ((\<lambda>x. a \<bullet> x) ` s)" in exI) using `a\<noteq>0`
+ obtain a where "a\<noteq>0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x" using assms(3-5) by auto
+ hence "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x" apply- apply(rule, rule) apply(erule_tac x="x - y" in ballE) by (auto simp add: inner_diff)
+ thus ?thesis apply(rule_tac x=a in exI, rule_tac x="rsup ((\<lambda>x. inner a x) ` s)" in exI) using `a\<noteq>0`
apply(rule) apply(rule,rule) apply(rule rsup[THEN isLubD2]) prefer 4 apply(rule,rule rsup_le) unfolding setle_def
prefer 4 using assms(3-5) by blast+ qed
@@ -1769,10 +1790,10 @@
lemma convex_halfspace_intersection:
assumes "closed s" "convex s"
- shows "s = \<Inter> {h. s \<subseteq> h \<and> (\<exists>a b. h = {x. a \<bullet> x \<le> b})}"
+ shows "s = \<Inter> {h. s \<subseteq> h \<and> (\<exists>a b. h = {x. inner a x \<le> b})}"
apply(rule set_ext, rule) unfolding Inter_iff Ball_def mem_Collect_eq apply(rule,rule,erule conjE) proof-
- fix x assume "\<forall>xa. s \<subseteq> xa \<and> (\<exists>a b. xa = {x. a \<bullet> x \<le> b}) \<longrightarrow> x \<in> xa"
- hence "\<forall>a b. s \<subseteq> {x. a \<bullet> x \<le> b} \<longrightarrow> x \<in> {x. a \<bullet> x \<le> b}" by blast
+ fix x assume "\<forall>xa. s \<subseteq> xa \<and> (\<exists>a b. xa = {x. inner a x \<le> b}) \<longrightarrow> x \<in> xa"
+ hence "\<forall>a b. s \<subseteq> {x. inner a x \<le> b} \<longrightarrow> x \<in> {x. inner a x \<le> b}" by blast
thus "x\<in>s" apply(rule_tac ccontr) apply(drule separating_hyperplane_closed_point[OF assms(2,1)])
apply(erule exE)+ apply(erule_tac x="-a" in allE, erule_tac x="-b" in allE) by auto
qed auto
@@ -2217,10 +2238,10 @@
apply(rule,rule,rule,rule,erule conjE,rule ccontr) proof-
fix a b x assume as:"connected s" "a \<in> s" "b \<in> s" "dest_vec1 a \<le> dest_vec1 x" "dest_vec1 x \<le> dest_vec1 b" "x\<notin>s"
hence *:"dest_vec1 a < dest_vec1 x" "dest_vec1 x < dest_vec1 b" apply(rule_tac [!] ccontr) unfolding not_less by auto
- let ?halfl = "{z. basis 1 \<bullet> z < dest_vec1 x} " and ?halfr = "{z. basis 1 \<bullet> z > dest_vec1 x} "
+ let ?halfl = "{z. inner (basis 1) z < dest_vec1 x} " and ?halfr = "{z. inner (basis 1) z > dest_vec1 x} "
{ fix y assume "y \<in> s" have "y \<in> ?halfr \<union> ?halfl" apply(rule ccontr)
- using as(6) `y\<in>s` by (auto simp add: basis_component field_simps dest_vec1_eq[unfolded dest_vec1_def One_nat_def] dest_vec1_def) }
- moreover have "a\<in>?halfl" "b\<in>?halfr" using * by (auto simp add: basis_component field_simps dest_vec1_def)
+ using as(6) `y\<in>s` by (auto simp add: inner_vector_def dest_vec1_eq [unfolded dest_vec1_def] dest_vec1_def) }
+ moreover have "a\<in>?halfl" "b\<in>?halfr" using * by (auto simp add: inner_vector_def dest_vec1_def)
hence "?halfl \<inter> s \<noteq> {}" "?halfr \<inter> s \<noteq> {}" using as(2-3) by auto
ultimately show False apply(rule_tac notE[OF as(1)[unfolded connected_def]])
apply(rule_tac x="?halfl" in exI, rule_tac x="?halfr" in exI)
@@ -2667,8 +2688,8 @@
qed(insert as(2)[unfolded **], auto)
next fix x::"real^'n" assume as:"\<forall>i. 0 \<le> x $ i" "setsum (op $ x) ?D \<le> 1"
show "\<exists>u. (\<forall>x\<in>{basis i |i. i \<in> ?D}. 0 \<le> u x) \<and> setsum u {basis i |i. i \<in> ?D} \<le> 1 \<and> (\<Sum>x\<in>{basis i |i. i \<in> ?D}. u x *\<^sub>R x) = x"
- apply(rule_tac x="\<lambda>y. y \<bullet> x" in exI) apply(rule,rule) unfolding mem_Collect_eq apply(erule exE) using as(1) apply(erule_tac x=i in allE)
- unfolding sumbas using as(2) and basis_expansion_unique [where 'a=real, unfolded smult_conv_scaleR] by(auto simp add:dot_basis) qed qed
+ apply(rule_tac x="\<lambda>y. inner y x" in exI) apply(rule,rule) unfolding mem_Collect_eq apply(erule exE) using as(1) apply(erule_tac x=i in allE)
+ unfolding sumbas using as(2) and basis_expansion_unique [where 'a=real, unfolded smult_conv_scaleR] by(auto simp add:inner_basis) qed qed
lemma interior_std_simplex:
"interior (convex hull (insert 0 { basis i| i. i\<in>UNIV})) =
@@ -3203,18 +3224,18 @@
obtain \<psi> where \<psi>:"bij_betw \<psi> {1..CARD('n)} (UNIV::'n set)" using ex_bij_betw_nat_finite_1[OF finite_UNIV] by auto
let ?U = "UNIV::(real^'n) set" let ?u = "?U - {0}"
let ?basis = "\<lambda>k. basis (\<psi> k)"
- let ?A = "\<lambda>k. {x::real^'n. \<exists>i\<in>{1..k}. (basis (\<psi> i)) \<bullet> x \<noteq> 0}"
+ let ?A = "\<lambda>k. {x::real^'n. \<exists>i\<in>{1..k}. inner (basis (\<psi> i)) x \<noteq> 0}"
have "\<forall>k\<in>{2..CARD('n)}. path_connected (?A k)" proof
- have *:"\<And>k. ?A (Suc k) = {x. ?basis (Suc k) \<bullet> x < 0} \<union> {x. ?basis (Suc k) \<bullet> x > 0} \<union> ?A k" apply(rule set_ext,rule) defer
+ have *:"\<And>k. ?A (Suc k) = {x. inner (?basis (Suc k)) x < 0} \<union> {x. inner (?basis (Suc k)) x > 0} \<union> ?A k" apply(rule set_ext,rule) defer
apply(erule UnE)+ unfolding mem_Collect_eq apply(rule_tac[1-2] x="Suc k" in bexI)
by(auto elim!: ballE simp add: not_less le_Suc_eq)
fix k assume "k \<in> {2..CARD('n)}" thus "path_connected (?A k)" proof(induct k)
case (Suc k) show ?case proof(cases "k = 1")
case False from Suc have d:"k \<in> {1..CARD('n)}" "Suc k \<in> {1..CARD('n)}" by auto
hence "\<psi> k \<noteq> \<psi> (Suc k)" using \<psi>[unfolded bij_betw_def inj_on_def, THEN conjunct1, THEN bspec[where x=k]] by auto
- hence **:"?basis k + ?basis (Suc k) \<in> {x. 0 < ?basis (Suc k) \<bullet> x} \<inter> (?A k)"
- "?basis k - ?basis (Suc k) \<in> {x. 0 > ?basis (Suc k) \<bullet> x} \<inter> ({x. 0 < ?basis (Suc k) \<bullet> x} \<union> (?A k))" using d
- by(auto simp add: dot_basis vector_component_simps intro!:bexI[where x=k])
+ hence **:"?basis k + ?basis (Suc k) \<in> {x. 0 < inner (?basis (Suc k)) x} \<inter> (?A k)"
+ "?basis k - ?basis (Suc k) \<in> {x. 0 > inner (?basis (Suc k)) x} \<inter> ({x. 0 < inner (?basis (Suc k)) x} \<union> (?A k))" using d
+ by(auto simp add: inner_basis vector_component_simps intro!:bexI[where x=k])
show ?thesis unfolding * Un_assoc apply(rule path_connected_Un) defer apply(rule path_connected_Un)
prefer 5 apply(rule_tac[1-2] convex_imp_path_connected, rule convex_halfspace_lt, rule convex_halfspace_gt)
apply(rule Suc(1)) apply(rule_tac[2-3] ccontr) using d ** False by auto
@@ -3227,18 +3248,18 @@
apply(rule_tac[5] x=" ?basis 1 + ?basis 2" in nequals0I)
apply(rule_tac[6] x="-?basis 1 + ?basis 2" in nequals0I)
apply(rule_tac[7] x="-?basis 1 - ?basis 2" in nequals0I)
- using d unfolding *** by(auto intro!: convex_halfspace_gt convex_halfspace_lt, auto simp add:vector_component_simps dot_basis)
+ using d unfolding *** by(auto intro!: convex_halfspace_gt convex_halfspace_lt, auto simp add:vector_component_simps inner_basis)
qed qed auto qed note lem = this
- have ***:"\<And>x::real^'n. (\<exists>i\<in>{1..CARD('n)}. basis (\<psi> i) \<bullet> x \<noteq> 0) \<longleftrightarrow> (\<exists>i. basis i \<bullet> x \<noteq> 0)"
+ have ***:"\<And>x::real^'n. (\<exists>i\<in>{1..CARD('n)}. inner (basis (\<psi> i)) x \<noteq> 0) \<longleftrightarrow> (\<exists>i. inner (basis i) x \<noteq> 0)"
apply rule apply(erule bexE) apply(rule_tac x="\<psi> i" in exI) defer apply(erule exE) proof-
- fix x::"real^'n" and i assume as:"basis i \<bullet> x \<noteq> 0"
+ fix x::"real^'n" and i assume as:"inner (basis i) x \<noteq> 0"
have "i\<in>\<psi> ` {1..CARD('n)}" using \<psi>[unfolded bij_betw_def, THEN conjunct2] by auto
then obtain j where "j\<in>{1..CARD('n)}" "\<psi> j = i" by auto
- thus "\<exists>i\<in>{1..CARD('n)}. basis (\<psi> i) \<bullet> x \<noteq> 0" apply(rule_tac x=j in bexI) using as by auto qed auto
+ thus "\<exists>i\<in>{1..CARD('n)}. inner (basis (\<psi> i)) x \<noteq> 0" apply(rule_tac x=j in bexI) using as by auto qed auto
have *:"?U - {a} = (\<lambda>x. x + a) ` {x. x \<noteq> 0}" apply(rule set_ext) unfolding image_iff
apply rule apply(rule_tac x="x - a" in bexI) by auto
- have **:"\<And>x::real^'n. x\<noteq>0 \<longleftrightarrow> (\<exists>i. basis i \<bullet> x \<noteq> 0)" unfolding Cart_eq by(auto simp add: dot_basis)
+ have **:"\<And>x::real^'n. x\<noteq>0 \<longleftrightarrow> (\<exists>i. inner (basis i) x \<noteq> 0)" unfolding Cart_eq by(auto simp add: inner_basis)
show ?thesis unfolding * apply(rule path_connected_continuous_image) apply(rule continuous_on_intros)+
unfolding ** apply(rule lem[THEN bspec[where x="CARD('n)"], unfolded ***]) using assms by auto qed
--- a/src/HOL/Library/Euclidean_Space.thy Fri Jun 12 16:23:07 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy Fri Jun 12 22:20:36 2009 -0700
@@ -750,7 +750,7 @@
instantiation "^" :: (real_normed_vector, finite) real_normed_vector
begin
-definition vector_norm_def:
+definition norm_vector_def:
"norm (x::'a^'b) = setL2 (\<lambda>i. norm (x$i)) UNIV"
definition vector_sgn_def:
@@ -759,30 +759,30 @@
instance proof
fix a :: real and x y :: "'a ^ 'b"
show "0 \<le> norm x"
- unfolding vector_norm_def
+ unfolding norm_vector_def
by (rule setL2_nonneg)
show "norm x = 0 \<longleftrightarrow> x = 0"
- unfolding vector_norm_def
+ unfolding norm_vector_def
by (simp add: setL2_eq_0_iff Cart_eq)
show "norm (x + y) \<le> norm x + norm y"
- unfolding vector_norm_def
+ unfolding norm_vector_def
apply (rule order_trans [OF _ setL2_triangle_ineq])
apply (simp add: setL2_mono norm_triangle_ineq)
done
show "norm (scaleR a x) = \<bar>a\<bar> * norm x"
- unfolding vector_norm_def
+ unfolding norm_vector_def
by (simp add: setL2_right_distrib)
show "sgn x = scaleR (inverse (norm x)) x"
by (rule vector_sgn_def)
show "dist x y = norm (x - y)"
- unfolding dist_vector_def vector_norm_def
+ unfolding dist_vector_def norm_vector_def
by (simp add: dist_norm)
qed
end
lemma norm_nth_le: "norm (x $ i) \<le> norm x"
-unfolding vector_norm_def
+unfolding norm_vector_def
by (rule member_le_setL2) simp_all
interpretation Cart_nth: bounded_linear "\<lambda>x. x $ i"
@@ -799,28 +799,28 @@
instantiation "^" :: (real_inner, finite) real_inner
begin
-definition vector_inner_def:
+definition inner_vector_def:
"inner x y = setsum (\<lambda>i. inner (x$i) (y$i)) UNIV"
instance proof
fix r :: real and x y z :: "'a ^ 'b"
show "inner x y = inner y x"
- unfolding vector_inner_def
+ unfolding inner_vector_def
by (simp add: inner_commute)
show "inner (x + y) z = inner x z + inner y z"
- unfolding vector_inner_def
+ unfolding inner_vector_def
by (simp add: inner_add_left setsum_addf)
show "inner (scaleR r x) y = r * inner x y"
- unfolding vector_inner_def
+ unfolding inner_vector_def
by (simp add: setsum_right_distrib)
show "0 \<le> inner x x"
- unfolding vector_inner_def
+ unfolding inner_vector_def
by (simp add: setsum_nonneg)
show "inner x x = 0 \<longleftrightarrow> x = 0"
- unfolding vector_inner_def
+ unfolding inner_vector_def
by (simp add: Cart_eq setsum_nonneg_eq_0_iff)
show "norm x = sqrt (inner x x)"
- unfolding vector_inner_def vector_norm_def setL2_def
+ unfolding inner_vector_def norm_vector_def setL2_def
by (simp add: power2_norm_eq_inner)
qed
@@ -878,7 +878,7 @@
done
lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
- by (simp add: vector_norm_def UNIV_1)
+ by (simp add: norm_vector_def UNIV_1)
lemma norm_real: "norm(x::real ^ 1) = abs(x$1)"
by (simp add: norm_vector_1)
@@ -997,12 +997,12 @@
by (rule norm_zero)
lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x"
- by (simp add: vector_norm_def vector_component setL2_right_distrib
+ by (simp add: norm_vector_def vector_component setL2_right_distrib
abs_mult cong: strong_setL2_cong)
lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (x \<bullet> x = (0::real))"
- by (simp add: vector_norm_def dot_def setL2_def power2_eq_square)
+ by (simp add: norm_vector_def dot_def setL2_def power2_eq_square)
lemma real_vector_norm_def: "norm x = sqrt (x \<bullet> x)"
- by (simp add: vector_norm_def setL2_def dot_def power2_eq_square)
+ by (simp add: norm_vector_def setL2_def dot_def power2_eq_square)
lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"
by (simp add: real_vector_norm_def)
lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n::finite)" by (metis norm_eq_zero)
@@ -1078,7 +1078,7 @@
qed
lemma component_le_norm: "\<bar>x$i\<bar> <= norm (x::real ^ 'n::finite)"
- apply (simp add: vector_norm_def)
+ apply (simp add: norm_vector_def)
apply (rule member_le_setL2, simp_all)
done
@@ -1091,7 +1091,7 @@
by (metis component_le_norm basic_trans_rules(21))
lemma norm_le_l1: "norm (x:: real ^'n::finite) <= setsum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
- by (simp add: vector_norm_def setL2_le_setsum)
+ by (simp add: norm_vector_def setL2_le_setsum)
lemma real_abs_norm: "\<bar>norm x\<bar> = norm (x :: real ^ _)"
by (rule abs_norm_cancel)
@@ -1536,6 +1536,13 @@
shows "basis i \<bullet> x = x$i" "x \<bullet> (basis i :: 'a^'n::finite) = (x$i :: 'a::semiring_1)"
by (auto simp add: dot_def basis_def cond_application_beta cond_value_iff setsum_delta cong del: if_weak_cong)
+lemma inner_basis:
+ fixes x :: "'a::{real_inner, real_algebra_1} ^ 'n::finite"
+ shows "inner (basis i) x = inner 1 (x $ i)"
+ and "inner x (basis i) = inner (x $ i) 1"
+ unfolding inner_vector_def basis_def
+ by (auto simp add: cond_application_beta cond_value_iff setsum_delta cong del: if_weak_cong)
+
lemma basis_eq_0: "basis i = (0::'a::semiring_1^'n) \<longleftrightarrow> False"
by (auto simp add: Cart_eq)
@@ -2931,7 +2938,7 @@
done
lemma norm_pastecart: "norm (pastecart x y) <= norm x + norm y"
- unfolding vector_norm_def setL2_def setsum_UNIV_sum
+ unfolding norm_vector_def setL2_def setsum_UNIV_sum
by (simp add: sqrt_add_le_add_sqrt setsum_nonneg)
subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *}
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Fri Jun 12 16:23:07 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Fri Jun 12 22:20:36 2009 -0700
@@ -5168,59 +5168,64 @@
using continuous_at_dot
by auto
+lemma continuous_on_inner:
+ fixes s :: "(real ^ _) set"
+ shows "continuous_on s (inner a)"
+ unfolding continuous_on by (rule ballI) (intro tendsto_intros)
+
lemma closed_halfspace_le: fixes a::"real^'n::finite"
- shows "closed {x. a \<bullet> x \<le> b}"
+ shows "closed {x. inner a x \<le> b}"
proof-
- have *:"{x \<in> UNIV. (op \<bullet> a) x \<in> {r. \<exists>x. a \<bullet> x = r \<and> r \<le> b}} = {x. a \<bullet> x \<le> b}" by auto
+ have *:"{x \<in> UNIV. inner a x \<in> {r. \<exists>x. inner a x = r \<and> r \<le> b}} = {x. inner a x \<le> b}" by auto
let ?T = "{..b}"
have "closed ?T" by (rule closed_real_atMost)
- moreover have "{r. \<exists>x. a \<bullet> x = r \<and> r \<le> b} = range (op \<bullet> a) \<inter> ?T"
+ moreover have "{r. \<exists>x. inner a x = r \<and> r \<le> b} = range (inner a) \<inter> ?T"
unfolding image_def by auto
- ultimately have "\<exists>T. closed T \<and> {r. \<exists>x. a \<bullet> x = r \<and> r \<le> b} = range (op \<bullet> a) \<inter> T" by fast
- hence "closedin euclidean {x \<in> UNIV. (op \<bullet> a) x \<in> {r. \<exists>x. a \<bullet> x = r \<and> r \<le> b}}"
- using continuous_on_dot[of UNIV a, unfolded continuous_on_closed subtopology_UNIV] unfolding closedin_closed
- by (fast elim!: allE[where x="{r. (\<exists>x. a \<bullet> x = r \<and> r \<le> b)}"])
+ ultimately have "\<exists>T. closed T \<and> {r. \<exists>x. inner a x = r \<and> r \<le> b} = range (inner a) \<inter> T" by fast
+ hence "closedin euclidean {x \<in> UNIV. inner a x \<in> {r. \<exists>x. inner a x = r \<and> r \<le> b}}"
+ using continuous_on_inner[of UNIV a, unfolded continuous_on_closed subtopology_UNIV] unfolding closedin_closed
+ by (fast elim!: allE[where x="{r. (\<exists>x. inner a x = r \<and> r \<le> b)}"])
thus ?thesis unfolding closed_closedin[THEN sym] and * by auto
qed
-lemma closed_halfspace_ge: "closed {x::real^_. a \<bullet> x \<ge> b}"
- using closed_halfspace_le[of "-a" "-b"] unfolding dot_lneg by auto
-
-lemma closed_hyperplane: "closed {x::real^_. a \<bullet> x = b}"
+lemma closed_halfspace_ge: "closed {x::real^_. inner a x \<ge> b}"
+ using closed_halfspace_le[of "-a" "-b"] unfolding inner_minus_left by auto
+
+lemma closed_hyperplane: "closed {x::real^_. inner a x = b}"
proof-
- have "{x. a \<bullet> x = b} = {x. a \<bullet> x \<ge> b} \<inter> {x. a \<bullet> x \<le> b}" by auto
+ have "{x. inner a x = b} = {x. inner a x \<ge> b} \<inter> {x. inner a x \<le> b}" by auto
thus ?thesis using closed_halfspace_le[of a b] and closed_halfspace_ge[of b a] using closed_Int by auto
qed
lemma closed_halfspace_component_le:
shows "closed {x::real^'n::finite. x$i \<le> a}"
- using closed_halfspace_le[of "(basis i)::real^'n" a] unfolding dot_basis[OF assms] by auto
+ using closed_halfspace_le[of "(basis i)::real^'n" a] unfolding inner_basis[OF assms] by auto
lemma closed_halfspace_component_ge:
shows "closed {x::real^'n::finite. x$i \<ge> a}"
- using closed_halfspace_ge[of a "(basis i)::real^'n"] unfolding dot_basis[OF assms] by auto
+ using closed_halfspace_ge[of a "(basis i)::real^'n"] unfolding inner_basis[OF assms] by auto
text{* Openness of halfspaces. *}
-lemma open_halfspace_lt: "open {x::real^_. a \<bullet> x < b}"
+lemma open_halfspace_lt: "open {x::real^_. inner a x < b}"
proof-
- have "UNIV - {x. b \<le> a \<bullet> x} = {x. a \<bullet> x < b}" by auto
+ have "UNIV - {x. b \<le> inner a x} = {x. inner a x < b}" by auto
thus ?thesis using closed_halfspace_ge[unfolded closed_def Compl_eq_Diff_UNIV, of b a] by auto
qed
-lemma open_halfspace_gt: "open {x::real^_. a \<bullet> x > b}"
+lemma open_halfspace_gt: "open {x::real^_. inner a x > b}"
proof-
- have "UNIV - {x. b \<ge> a \<bullet> x} = {x. a \<bullet> x > b}" by auto
+ have "UNIV - {x. b \<ge> inner a x} = {x. inner a x > b}" by auto
thus ?thesis using closed_halfspace_le[unfolded closed_def Compl_eq_Diff_UNIV, of a b] by auto
qed
lemma open_halfspace_component_lt:
shows "open {x::real^'n::finite. x$i < a}"
- using open_halfspace_lt[of "(basis i)::real^'n" a] unfolding dot_basis[OF assms] by auto
+ using open_halfspace_lt[of "(basis i)::real^'n" a] unfolding inner_basis[OF assms] by auto
lemma open_halfspace_component_gt:
shows "open {x::real^'n::finite. x$i > a}"
- using open_halfspace_gt[of a "(basis i)::real^'n"] unfolding dot_basis[OF assms] by auto
+ using open_halfspace_gt[of a "(basis i)::real^'n"] unfolding inner_basis[OF assms] by auto
text{* This gives a simple derivation of limit component bounds. *}
@@ -5228,8 +5233,8 @@
assumes "(f ---> l) net" "\<not> (trivial_limit net)" "eventually (\<lambda>x. f(x)$i \<le> b) net"
shows "l$i \<le> b"
proof-
- { fix x have "x \<in> {x::real^'n. basis i \<bullet> x \<le> b} \<longleftrightarrow> x$i \<le> b" unfolding dot_basis by auto } note * = this
- show ?thesis using Lim_in_closed_set[of "{x. basis i \<bullet> x \<le> b}" f net l] unfolding *
+ { fix x have "x \<in> {x::real^'n. inner (basis i) x \<le> b} \<longleftrightarrow> x$i \<le> b" unfolding inner_basis by auto } note * = this
+ show ?thesis using Lim_in_closed_set[of "{x. inner (basis i) x \<le> b}" f net l] unfolding *
using closed_halfspace_le[of "(basis i)::real^'n" b] and assms(1,2,3) by auto
qed
@@ -5237,8 +5242,8 @@
assumes "(f ---> l) net" "\<not> (trivial_limit net)" "eventually (\<lambda>x. b \<le> (f x)$i) net"
shows "b \<le> l$i"
proof-
- { fix x have "x \<in> {x::real^'n. basis i \<bullet> x \<ge> b} \<longleftrightarrow> x$i \<ge> b" unfolding dot_basis by auto } note * = this
- show ?thesis using Lim_in_closed_set[of "{x. basis i \<bullet> x \<ge> b}" f net l] unfolding *
+ { fix x have "x \<in> {x::real^'n. inner (basis i) x \<ge> b} \<longleftrightarrow> x$i \<ge> b" unfolding inner_basis by auto } note * = this
+ show ?thesis using Lim_in_closed_set[of "{x. inner (basis i) x \<ge> b}" f net l] unfolding *
using closed_halfspace_ge[of b "(basis i)::real^'n"] and assms(1,2,3) by auto
qed
@@ -5293,12 +5298,12 @@
text{* Some more convenient intermediate-value theorem formulations. *}
lemma connected_ivt_hyperplane: fixes y :: "real^'n::finite"
- assumes "connected s" "x \<in> s" "y \<in> s" "a \<bullet> x \<le> b" "b \<le> a \<bullet> y"
- shows "\<exists>z \<in> s. a \<bullet> z = b"
+ assumes "connected s" "x \<in> s" "y \<in> s" "inner a x \<le> b" "b \<le> inner a y"
+ shows "\<exists>z \<in> s. inner a z = b"
proof(rule ccontr)
- assume as:"\<not> (\<exists>z\<in>s. a \<bullet> z = b)"
- let ?A = "{x::real^'n. a \<bullet> x < b}"
- let ?B = "{x::real^'n. a \<bullet> x > b}"
+ assume as:"\<not> (\<exists>z\<in>s. inner a z = b)"
+ let ?A = "{x::real^'n. inner a x < b}"
+ let ?B = "{x::real^'n. inner a x > b}"
have "open ?A" "open ?B" using open_halfspace_lt and open_halfspace_gt by auto
moreover have "?A \<inter> ?B = {}" by auto
moreover have "s \<subseteq> ?A \<union> ?B" using as by auto
@@ -5307,7 +5312,7 @@
lemma connected_ivt_component: fixes x::"real^'n::finite" shows
"connected s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x$k \<le> a \<Longrightarrow> a \<le> y$k \<Longrightarrow> (\<exists>z\<in>s. z$k = a)"
- using connected_ivt_hyperplane[of s x y "(basis k)::real^'n" a] by (auto simp add: dot_basis)
+ using connected_ivt_hyperplane[of s x y "(basis k)::real^'n" a] by (auto simp add: inner_basis)
text{* Also more convenient formulations of monotone convergence. *}
@@ -5594,16 +5599,16 @@
"closed {x::real^'n::finite. \<forall>i. P i --> x$i = 0}" (is "closed ?A")
proof-
let ?D = "{i. P i}"
- let ?Bs = "{{x::real^'n. basis i \<bullet> x = 0}| i. i \<in> ?D}"
+ let ?Bs = "{{x::real^'n. inner (basis i) x = 0}| i. i \<in> ?D}"
{ fix x
{ assume "x\<in>?A"
hence x:"\<forall>i\<in>?D. x $ i = 0" by auto
- hence "x\<in> \<Inter> ?Bs" by(auto simp add: dot_basis x) }
+ hence "x\<in> \<Inter> ?Bs" by(auto simp add: inner_basis x) }
moreover
{ assume x:"x\<in>\<Inter>?Bs"
{ fix i assume i:"i \<in> ?D"
- then obtain B where BB:"B \<in> ?Bs" and B:"B = {x::real^'n. basis i \<bullet> x = 0}" by auto
- hence "x $ i = 0" unfolding B using x unfolding dot_basis by auto }
+ then obtain B where BB:"B \<in> ?Bs" and B:"B = {x::real^'n. inner (basis i) x = 0}" by auto
+ hence "x $ i = 0" unfolding B using x unfolding inner_basis by auto }
hence "x\<in>?A" by auto }
ultimately have "x\<in>?A \<longleftrightarrow> x\<in> \<Inter>?Bs" by auto }
hence "?A = \<Inter> ?Bs" by auto