--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Dec 14 14:46:01 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Dec 14 15:46:01 2012 +0100
@@ -101,56 +101,22 @@
lemma span_eq[simp]: "(span s = s) <-> subspace s"
unfolding span_def by (rule hull_eq, rule subspace_Inter)
-lemma basis_inj_on: "d \<subseteq> {..<DIM('n)} \<Longrightarrow> inj_on (basis :: nat => 'n::euclidean_space) d"
- by (auto simp add: inj_on_def euclidean_eq[where 'a='n])
-
-lemma finite_substdbasis: "finite {basis i ::'n::euclidean_space |i. i : (d:: nat set)}" (is "finite ?S")
-proof -
- have eq: "?S = basis ` d" by blast
- show ?thesis
- unfolding eq
- apply (rule finite_subset[OF _ range_basis_finite])
- apply auto
- done
-qed
-
-lemma card_substdbasis:
- assumes "d \<subseteq> {..<DIM('n::euclidean_space)}"
- shows "card {basis i ::'n::euclidean_space | i. i : d} = card d" (is "card ?S = _")
-proof -
- have eq: "?S = basis ` d" by blast
- show ?thesis
- unfolding eq
- using card_image[OF basis_inj_on[of d]] assms by auto
-qed
-
lemma substdbasis_expansion_unique:
- assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
- shows "setsum (%i. f i *\<^sub>R basis i) d = (x::'a::euclidean_space)
- <-> (!i<DIM('a). (i:d --> f i = x$$i) & (i ~: d --> x $$ i = 0))"
+ assumes d: "d \<subseteq> Basis"
+ shows "(\<Sum>i\<in>d. f i *\<^sub>R i) = (x::'a::euclidean_space)
+ \<longleftrightarrow> (\<forall>i\<in>Basis. (i \<in> d \<longrightarrow> f i = x \<bullet> i) \<and> (i \<notin> d \<longrightarrow> x \<bullet> i = 0))"
proof -
have *: "\<And>x a b P. x * (if P then a else b) = (if P then x*a else x*b)" by auto
- have **: "finite d" apply(rule finite_subset[OF assms]) by fastforce
- have ***: "\<And>i. (setsum (%i. f i *\<^sub>R ((basis i)::'a)) d) $$ i = (\<Sum>x\<in>d. if x = i then f x else 0)"
- unfolding euclidean_component_setsum euclidean_component_scaleR basis_component *
- apply (rule setsum_cong2)
- using assms apply auto
- done
+ have **: "finite d" by (auto intro: finite_subset[OF assms])
+ have ***: "\<And>i. i \<in> Basis \<Longrightarrow> (\<Sum>i\<in>d. f i *\<^sub>R i) \<bullet> i = (\<Sum>x\<in>d. if x = i then f x else 0)"
+ using d
+ by (auto intro!: setsum_cong simp: inner_Basis inner_setsum_left)
show ?thesis
- unfolding euclidean_eq[where 'a='a] *** setsum_delta[OF **] using assms by auto
-qed
-
-lemma independent_substdbasis:
- assumes "d \<subseteq> {..<DIM('a::euclidean_space)}"
- shows "independent {basis i ::'a::euclidean_space |i. i : (d :: nat set)}"
- (is "independent ?A")
-proof -
- have *: "{basis i |i. i < DIM('a)} = basis ` {..<DIM('a)}" by auto
- show ?thesis
- apply(intro independent_mono[of "{basis i ::'a |i. i : {..<DIM('a::euclidean_space)}}" "?A"] )
- using independent_basis[where 'a='a] assms apply (auto simp: *)
- done
-qed
+ unfolding euclidean_eq_iff[where 'a='a] by (auto simp: setsum_delta[OF **] ***)
+qed
+
+lemma independent_substdbasis: "d \<subseteq> Basis \<Longrightarrow> independent d"
+ by (rule independent_mono[OF independent_Basis])
lemma dim_cball:
assumes "0<e"
@@ -321,8 +287,8 @@
lemma vector_choose_size:
"0 <= c ==> \<exists>(x::'a::euclidean_space). norm x = c"
- apply (rule exI[where x="c *\<^sub>R basis 0 ::'a"])
- using DIM_positive[where 'a='a] apply auto
+ apply (rule exI[where x="c *\<^sub>R (SOME i. i \<in> Basis)"])
+ apply (auto simp: SOME_Basis)
done
lemma setsum_delta_notmem:
@@ -1291,11 +1257,12 @@
text {* Balls, being convex, are connected. *}
lemma convex_box: fixes a::"'a::euclidean_space"
- assumes "\<And>i. i<DIM('a) \<Longrightarrow> convex {x. P i x}"
- shows "convex {x. \<forall>i<DIM('a). P i (x$$i)}"
- using assms unfolding convex_def by auto
-
-lemma convex_positive_orthant: "convex {x::'a::euclidean_space. (\<forall>i<DIM('a). 0 \<le> x$$i)}"
+ assumes "\<And>i. i\<in>Basis \<Longrightarrow> convex {x. P i x}"
+ shows "convex {x. \<forall>i\<in>Basis. P i (x\<bullet>i)}"
+ using assms unfolding convex_def
+ by (auto simp: inner_add_left)
+
+lemma convex_positive_orthant: "convex {x::'a::euclidean_space. (\<forall>i\<in>Basis. 0 \<le> x\<bullet>i)}"
by (rule convex_box) (simp add: atLeast_def[symmetric] convex_real_interval)
lemma convex_local_global_minimum:
@@ -2073,40 +2040,39 @@
from this show ?thesis using assms `span B=S` by auto
qed
-lemma span_substd_basis: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
- shows "(span {basis i | i. i : d}) = {x::'a::euclidean_space. (!i<DIM('a). i ~: d --> x$$i = 0)}"
- (is "span ?A = ?B")
+lemma span_substd_basis:
+ assumes d: "d \<subseteq> Basis"
+ shows "span d = {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}" (is "_ = ?B")
proof-
-have "?A <= ?B" by auto
+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 ?A <= ?B" using span_mono[of "?A" "?B"] span_eq[of "?B"] by blast
-moreover have "card d <= dim (span ?A)" using independent_card_le_dim[of "?A" "span ?A"]
- independent_substdbasis[OF assms] card_substdbasis[OF assms] span_inc[of "?A"] by auto
-moreover hence "dim ?B <= dim (span ?A)" using dim_substandard[OF assms] by auto
-ultimately show ?thesis using s subspace_dim_equal[of "span ?A" "?B"]
- subspace_span[of "?A"] by auto
+ultimately have "span d <= ?B" using span_mono[of d "?B"] span_eq[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_inc[of d] by auto
+moreover hence "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 "EX f d. card d = card B & linear f & f ` B = {basis i::'a |i. i : (d :: nat set)} &
- f ` span B = {x. ALL i<DIM('a). i ~: d --> x $$ i = (0::real)} & inj_on f (span B) \<and> d\<subseteq>{..<DIM('a)}"
+shows "EX f (d::'a set). card d = card B \<and> linear f \<and> f ` B = d \<and>
+ f ` span B = {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} \<and> inj_on f (span B) \<and> d \<subseteq> Basis"
proof-
have B:"card B=dim B" using dim_unique[of B B "card B"] assms span_inc[of B] by auto
- def d \<equiv> "{..<dim B}" have t:"card d = dim B" unfolding d_def by auto
- have "dim B <= DIM('a)" using dim_subset_UNIV[of B] by auto
- hence d:"d\<subseteq>{..<DIM('a)}" unfolding d_def by auto
- let ?t = "{x::'a::euclidean_space. !i<DIM('a). i ~: d --> x$$i = 0}"
- have "EX f. linear f & f ` B = {basis i |i. i : d} &
- f ` span B = ?t & inj_on f (span B)"
- apply (rule basis_to_basis_subspace_isomorphism[of "span B" ?t B "{basis i |i. i : d}"])
+ have "dim B \<le> card (Basis :: 'a set)" using dim_subset_UNIV[of B] by simp
+ from ex_card[OF this] obtain d :: "'a set" where d: "d \<subseteq> Basis" and t: "card d = dim B" by auto
+ let ?t = "{x::'a::euclidean_space. \<forall>i\<in>Basis. i ~: d --> x\<bullet>i = 0}"
+ have "EX f. linear f & f ` B = d & f ` span B = ?t & inj_on f (span B)"
+ apply (rule basis_to_basis_subspace_isomorphism[of "span B" ?t B "d"])
apply(rule subspace_span) apply(rule subspace_substandard) defer
apply(rule span_inc) apply(rule assms) defer unfolding dim_span[of B] apply(rule B)
- unfolding span_substd_basis[OF d,symmetric] card_substdbasis[OF d] apply(rule span_inc)
+ unfolding span_substd_basis[OF d, symmetric]
+ apply(rule span_inc)
apply(rule independent_substdbasis[OF d]) apply(rule,assumption)
unfolding t[symmetric] span_substd_basis[OF d] dim_substandard[OF d] by auto
- from this t `card B=dim B` show ?thesis using d by auto
+ with t `card B = dim B` d show ?thesis by auto
qed
lemma aff_dim_empty:
@@ -2492,7 +2458,7 @@
using as affine_affine_hull[of S] mem_affine[of "affine hull S" y x "(1 / e)" "-((1 - e) / e)"] by (simp add: algebra_simps)
have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
unfolding dist_norm unfolding norm_scaleR[symmetric] apply(rule arg_cong[where f=norm]) using `e>0`
- by(auto simp add:euclidean_eq[where 'a='a] field_simps)
+ by(auto simp add:euclidean_eq_iff[where 'a='a] field_simps inner_simps)
also have "... = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
also have "... < d" using as[unfolded dist_norm] and `e>0`
by(auto simp add:pos_divide_less_eq[OF `e>0`] mult_commute)
@@ -2770,9 +2736,9 @@
subsection{* Some Properties of subset of standard basis *}
-lemma affine_hull_substd_basis: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
- shows "affine hull (insert 0 {basis i | i. i : d}) =
- {x::'a::euclidean_space. (!i<DIM('a). i ~: d --> x$$i = 0)}"
+lemma affine_hull_substd_basis: assumes "d\<subseteq>Basis"
+ shows "affine hull (insert 0 d) =
+ {x::'a::euclidean_space. (\<forall>i\<in>Basis. i ~: d --> x\<bullet>i = 0)}"
(is "affine hull (insert 0 ?A) = ?B")
proof- have *:"\<And>A. op + (0\<Colon>'a) ` A = A" "\<And>A. op + (- (0\<Colon>'a)) ` A = A" by auto
show ?thesis unfolding affine_hull_insert_span_gen span_substd_basis[OF assms,symmetric] * ..
@@ -3230,10 +3196,10 @@
assumes "convex (s::('a::euclidean_space) set)" "closed s" "0 \<notin> s"
shows "\<exists>a b. a \<noteq> 0 \<and> 0 < b \<and> (\<forall>x\<in>s. inner a x > b)"
proof(cases "s={}")
- case True have "norm ((basis 0)::'a) = 1" by auto
- hence "norm ((basis 0)::'a) = 1" "basis 0 \<noteq> (0::'a)" defer
- apply(subst norm_le_zero_iff[symmetric]) by auto
- thus ?thesis apply(rule_tac x="basis 0" in exI, rule_tac x=1 in exI)
+ case True
+ have "norm ((SOME i. i\<in>Basis)::'a) = 1" "(SOME i. i\<in>Basis) \<noteq> (0::'a)" defer
+ apply(subst norm_le_zero_iff[symmetric]) by (auto simp: SOME_Basis)
+ thus ?thesis apply(rule_tac x="SOME i. i\<in>Basis" in exI, rule_tac x=1 in exI)
using True using DIM_positive[where 'a='a] by auto
next case False thus ?thesis using False using separating_hyperplane_closed_point[OF assms]
apply - apply(erule exE)+ unfolding inner_zero_right apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
@@ -3703,10 +3669,10 @@
case False thus ?thesis apply (intro continuous_intros)
using cont_surfpi unfolding continuous_on_eq_continuous_at[OF open_delete[OF open_UNIV]] o_def by auto
next obtain B where B:"\<forall>x\<in>s. norm x \<le> B" using compact_imp_bounded[OF assms(1)] unfolding bounded_iff by auto
- hence "B > 0" using assms(2) unfolding subset_eq apply(erule_tac x="basis 0" in ballE) defer
- apply(erule_tac x="basis 0" in ballE)
+ hence "B > 0" using assms(2) unfolding subset_eq apply(erule_tac x="SOME i. i\<in>Basis" in ballE) defer
+ apply(erule_tac x="SOME i. i\<in>Basis" in ballE)
unfolding Ball_def mem_cball dist_norm using DIM_positive[where 'a='a]
- by auto
+ by (auto simp: SOME_Basis)
case True show ?thesis unfolding True continuous_at Lim_at apply(rule,rule) apply(rule_tac x="e / B" in exI)
apply(rule) apply(rule divide_pos_pos) prefer 3 apply(rule,rule,erule conjE)
unfolding norm_zero scaleR_zero_left dist_norm diff_0_right norm_scaleR abs_norm_cancel proof-
@@ -3849,7 +3815,8 @@
hence "a < b" unfolding * using as(4) apply(rule_tac mult_left_less_imp_less) by(auto simp add: field_simps)
hence "u * a + v * b \<le> b" unfolding ** using **(2) as(3) by(auto simp add: field_simps intro!:mult_right_mono) }
ultimately show "u *\<^sub>R x + v *\<^sub>R y \<in> s" apply- apply(rule assms[unfolded is_interval_def, rule_format, OF as(1,2)])
- using as(3-) DIM_positive[where 'a='a] by auto qed
+ using as(3-) DIM_positive[where 'a='a] by (auto simp: inner_simps)
+qed
lemma is_interval_connected:
fixes s :: "('a::euclidean_space) set"
@@ -3892,8 +3859,8 @@
subsection {* Another intermediate value theorem formulation *}
lemma ivt_increasing_component_on_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
- assumes "a \<le> b" "continuous_on {a .. b} f" "(f a)$$k \<le> y" "y \<le> (f b)$$k"
- shows "\<exists>x\<in>{a..b}. (f x)$$k = y"
+ assumes "a \<le> b" "continuous_on {a .. b} f" "(f a)\<bullet>k \<le> y" "y \<le> (f b)\<bullet>k"
+ shows "\<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
proof- have "f a \<in> f ` {a..b}" "f b \<in> f ` {a..b}" apply(rule_tac[!] imageI)
using assms(1) by auto
thus ?thesis using connected_ivt_component[of "f ` {a..b}" "f a" "f b" k y]
@@ -3902,20 +3869,20 @@
lemma ivt_increasing_component_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
- \<Longrightarrow> f a$$k \<le> y \<Longrightarrow> y \<le> f b$$k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)$$k = y"
+ \<Longrightarrow> f a\<bullet>k \<le> y \<Longrightarrow> y \<le> f b\<bullet>k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
by(rule ivt_increasing_component_on_1)
(auto simp add: continuous_at_imp_continuous_on)
lemma ivt_decreasing_component_on_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
- assumes "a \<le> b" "continuous_on {a .. b} f" "(f b)$$k \<le> y" "y \<le> (f a)$$k"
- shows "\<exists>x\<in>{a..b}. (f x)$$k = y"
+ assumes "a \<le> b" "continuous_on {a .. b} f" "(f b)\<bullet>k \<le> y" "y \<le> (f a)\<bullet>k"
+ shows "\<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
apply(subst neg_equal_iff_equal[symmetric])
using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"]
using assms using continuous_on_minus by auto
lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
- \<Longrightarrow> f b$$k \<le> y \<Longrightarrow> y \<le> f a$$k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)$$k = y"
+ \<Longrightarrow> f b\<bullet>k \<le> y \<Longrightarrow> y \<le> f a\<bullet>k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
by(rule ivt_decreasing_component_on_1)
(auto simp: continuous_at_imp_continuous_on)
@@ -3933,104 +3900,127 @@
thus "f x \<le> 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_setsum_Basis[simp]: "\<And>i. i \<in> Basis \<Longrightarrow> (\<Sum>Basis) \<bullet> i = 1"
+ by (simp add: One_def inner_setsum_left setsum_cases inner_Basis)
+
lemma unit_interval_convex_hull:
- "{0::'a::ordered_euclidean_space .. (\<chi>\<chi> i. 1)} = convex hull {x. \<forall>i<DIM('a). (x$$i = 0) \<or> (x$$i = 1)}"
+ defines "One \<equiv> (\<Sum>Basis)"
+ shows "{0::'a::ordered_euclidean_space .. One} =
+ convex hull {x. \<forall>i\<in>Basis. (x\<bullet>i = 0) \<or> (x\<bullet>i = 1)}"
(is "?int = convex hull ?points")
-proof- have 01:"{0,(\<chi>\<chi> i. 1)} \<subseteq> convex hull ?points" apply rule apply(rule_tac hull_subset[unfolded subset_eq, rule_format]) by auto
- { fix n x assume "x\<in>{0::'a::ordered_euclidean_space .. \<chi>\<chi> i. 1}" "n \<le> DIM('a)" "card {i. i<DIM('a) \<and> x$$i \<noteq> 0} \<le> n"
+proof -
+ have One[simp]: "\<And>i. i \<in> Basis \<Longrightarrow> One \<bullet> i = 1"
+ by (simp add: One_def inner_setsum_left setsum_cases inner_Basis)
+ have 01:"{0,One} \<subseteq> convex hull ?points"
+ apply rule apply(rule_tac hull_subset[unfolded subset_eq, rule_format]) by auto
+ { fix n x assume "x\<in>{0::'a::ordered_euclidean_space .. One}" "n \<le> DIM('a)" "card {i. i\<in>Basis \<and> x\<bullet>i \<noteq> 0} \<le> n"
hence "x\<in>convex hull ?points" proof(induct n arbitrary: x)
- case 0 hence "x = 0" apply(subst euclidean_eq) apply rule by auto
+ case 0 hence "x = 0" apply(subst euclidean_eq_iff) apply rule by auto
thus "x\<in>convex hull ?points" using 01 by auto
next
- case (Suc n) show "x\<in>convex hull ?points" proof(cases "{i. i<DIM('a) \<and> x$$i \<noteq> 0} = {}")
- case True hence "x = 0" apply(subst euclidean_eq) by auto
+ case (Suc n) show "x\<in>convex hull ?points" proof(cases "{i. i\<in>Basis \<and> x\<bullet>i \<noteq> 0} = {}")
+ case True hence "x = 0" apply(subst euclidean_eq_iff) by auto
thus "x\<in>convex hull ?points" using 01 by auto
next
- case False def xi \<equiv> "Min ((\<lambda>i. x$$i) ` {i. i<DIM('a) \<and> x$$i \<noteq> 0})"
- have "xi \<in> (\<lambda>i. x$$i) ` {i. i<DIM('a) \<and> x$$i \<noteq> 0}" unfolding xi_def apply(rule Min_in) using False by auto
- then obtain i where i':"x$$i = xi" "x$$i \<noteq> 0" "i<DIM('a)" by auto
- have i:"\<And>j. j<DIM('a) \<Longrightarrow> x$$j > 0 \<Longrightarrow> x$$i \<le> x$$j"
+ case False def xi \<equiv> "Min ((\<lambda>i. x\<bullet>i) ` {i. i\<in>Basis \<and> x\<bullet>i \<noteq> 0})"
+ have "xi \<in> (\<lambda>i. x\<bullet>i) ` {i. i\<in>Basis \<and> x\<bullet>i \<noteq> 0}" unfolding xi_def apply(rule Min_in) using False by auto
+ then obtain i where i':"x\<bullet>i = xi" "x\<bullet>i \<noteq> 0" "i\<in>Basis" by auto
+ have i:"\<And>j. j\<in>Basis \<Longrightarrow> x\<bullet>j > 0 \<Longrightarrow> x\<bullet>i \<le> x\<bullet>j"
unfolding i'(1) xi_def apply(rule_tac Min_le) unfolding image_iff
defer apply(rule_tac x=j in bexI) using i' by auto
- have i01:"x$$i \<le> 1" "x$$i > 0" using Suc(2)[unfolded mem_interval,rule_format,of i]
- using i'(2-) `x$$i \<noteq> 0` by auto
- show ?thesis proof(cases "x$$i=1")
- case True have "\<forall>j\<in>{i. i<DIM('a) \<and> x$$i \<noteq> 0}. x$$j = 1" apply(rule, rule ccontr) unfolding mem_Collect_eq
- proof(erule conjE) fix j assume as:"x $$ j \<noteq> 0" "x $$ j \<noteq> 1" "j<DIM('a)"
- hence j:"x$$j \<in> {0<..<1}" using Suc(2) by(auto simp add: eucl_le[where 'a='a] elim!:allE[where x=j])
- hence "x$$j \<in> op $$ x ` {i. i<DIM('a) \<and> x $$ i \<noteq> 0}" using as(3) by auto
- hence "x$$j \<ge> x$$i" unfolding i'(1) xi_def apply(rule_tac Min_le) by auto
+ have i01:"x\<bullet>i \<le> 1" "x\<bullet>i > 0" using Suc(2)[unfolded mem_interval,rule_format,of i]
+ using i'(2-) `x\<bullet>i \<noteq> 0` by auto
+ show ?thesis proof(cases "x\<bullet>i=1")
+ case True have "\<forall>j\<in>{i. i\<in>Basis \<and> x\<bullet>i \<noteq> 0}. x\<bullet>j = 1" apply(rule, rule ccontr) unfolding mem_Collect_eq
+ proof(erule conjE) fix j assume as:"x \<bullet> j \<noteq> 0" "x \<bullet> j \<noteq> 1" "j\<in>Basis"
+ hence j:"x\<bullet>j \<in> {0<..<1}" using Suc(2)
+ by (auto simp add: eucl_le[where 'a='a] elim!:allE[where x=j])
+ hence "x\<bullet>j \<in> op \<bullet> x ` {i. i\<in>Basis \<and> x \<bullet> i \<noteq> 0}" using as(3) by auto
+ hence "x\<bullet>j \<ge> x\<bullet>i" unfolding i'(1) xi_def apply(rule_tac Min_le) by auto
thus False using True Suc(2) j by(auto simp add: elim!:ballE[where x=j]) qed
thus "x\<in>convex hull ?points" apply(rule_tac hull_subset[unfolded subset_eq, rule_format])
by auto
- next let ?y = "\<lambda>j. if x$$j = 0 then 0 else (x$$j - x$$i) / (1 - x$$i)"
- case False hence *:"x = x$$i *\<^sub>R (\<chi>\<chi> j. if x$$j = 0 then 0 else 1) + (1 - x$$i) *\<^sub>R (\<chi>\<chi> j. ?y j)"
- apply(subst euclidean_eq) by(auto simp add: field_simps)
- { fix j assume j:"j<DIM('a)"
- have "x$$j \<noteq> 0 \<Longrightarrow> 0 \<le> (x $$ j - x $$ i) / (1 - x $$ i)" "(x $$ j - x $$ i) / (1 - x $$ i) \<le> 1"
+ next
+ let ?y = "\<Sum>j\<in>Basis. (if x\<bullet>j = 0 then 0 else (x\<bullet>j - x\<bullet>i) / (1 - x\<bullet>i)) *\<^sub>R j"
+ case False
+ then have *: "x = (x\<bullet>i) *\<^sub>R (\<Sum>j\<in>Basis. (if x\<bullet>j = 0 then 0 else 1) *\<^sub>R j) + (1 - x\<bullet>i) *\<^sub>R ?y"
+ by (subst euclidean_eq_iff) (simp add: inner_simps)
+ { fix j :: 'a assume j:"j\<in>Basis"
+ have "x\<bullet>j \<noteq> 0 \<Longrightarrow> 0 \<le> (x \<bullet> j - x \<bullet> i) / (1 - x \<bullet> i)" "(x \<bullet> j - x \<bullet> i) / (1 - x \<bullet> i) \<le> 1"
apply(rule_tac divide_nonneg_pos) using i(1)[of j] using False i01
using Suc(2)[unfolded mem_interval, rule_format, of j] using j
- by(auto simp add:field_simps)
- hence "0 \<le> ?y j \<and> ?y j \<le> 1" by auto }
- moreover have "i\<in>{j. j<DIM('a) \<and> x$$j \<noteq> 0} - {j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0}"
+ by(auto simp add: field_simps)
+ with j have "0 \<le> ?y \<bullet> j \<and> ?y \<bullet> j \<le> 1" by (auto simp: inner_simps) }
+ moreover have "i\<in>{j. j\<in>Basis \<and> x\<bullet>j \<noteq> 0} - {j. j\<in>Basis \<and> ?y \<bullet> j \<noteq> 0}"
using i01 using i'(3) by auto
- hence "{j. j<DIM('a) \<and> x$$j \<noteq> 0} \<noteq> {j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0}" using i'(3) by blast
- hence **:"{j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0} \<subset> {j. j<DIM('a) \<and> x$$j \<noteq> 0}" apply - apply rule
+ hence "{j. j\<in>Basis \<and> x\<bullet>j \<noteq> 0} \<noteq> {j. j\<in>Basis \<and> ?y \<bullet> j \<noteq> 0}" using i'(3) by blast
+ hence **:"{j. j\<in>Basis \<and> ?y \<bullet> j \<noteq> 0} \<subset> {j. j\<in>Basis \<and> x\<bullet>j \<noteq> 0}"
by auto
- have "card {j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0} \<le> n"
+ have "card {j. j\<in>Basis \<and> ?y \<bullet> j \<noteq> 0} \<le> n"
using less_le_trans[OF psubset_card_mono[OF _ **] Suc(4)] by auto
- ultimately show ?thesis apply(subst *) apply(rule convex_convex_hull[unfolded convex_def, rule_format])
- apply(rule_tac hull_subset[unfolded subset_eq, rule_format]) defer apply(rule Suc(1))
- unfolding mem_interval using i01 Suc(3) by auto
- qed qed qed } note * = this
- have **:"DIM('a) = card {..<DIM('a)}" by auto
- show ?thesis apply rule defer apply(rule hull_minimal) unfolding subset_eq prefer 3 apply rule
- apply(rule_tac n2="DIM('a)" in *) prefer 3 apply(subst(2) **)
+ ultimately show ?thesis
+ apply(subst *)
+ apply(rule convex_convex_hull[unfolded convex_def, rule_format])
+ apply(rule_tac hull_subset[unfolded subset_eq, rule_format])
+ defer
+ apply(rule Suc(1))
+ unfolding mem_interval
+ using i01 Suc(3)
+ by auto
+ qed
+ qed
+ qed } note * = this
+ show ?thesis
+ apply rule defer apply(rule hull_minimal) unfolding subset_eq prefer 3 apply rule
+ apply(rule_tac n2="DIM('a)" in *) prefer 3
apply(rule card_mono) using 01 and convex_interval(1) prefer 5 apply - apply rule
- unfolding mem_interval apply rule unfolding mem_Collect_eq apply(erule_tac x=i in allE)
- by auto qed
+ unfolding mem_interval apply rule unfolding mem_Collect_eq apply(erule_tac x=i in ballE)
+ by auto
+qed
text {* And this is a finite set of vertices. *}
-lemma unit_cube_convex_hull: obtains s where "finite s" "{0 .. (\<chi>\<chi> i. 1)::'a::ordered_euclidean_space} = convex hull s"
- apply(rule that[of "{x::'a. \<forall>i<DIM('a). x$$i=0 \<or> x$$i=1}"])
- apply(rule finite_subset[of _ "(\<lambda>s. (\<chi>\<chi> i. if i\<in>s then 1::real else 0)::'a) ` Pow {..<DIM('a)}"])
+lemma unit_cube_convex_hull:
+ obtains s :: "'a::ordered_euclidean_space set" where "finite s" "{0 .. \<Sum>Basis} = convex hull s"
+ apply(rule that[of "{x::'a. \<forall>i\<in>Basis. x\<bullet>i=0 \<or> x\<bullet>i=1}"])
+ apply(rule finite_subset[of _ "(\<lambda>s. (\<Sum>i\<in>Basis. (if i\<in>s then 1 else 0) *\<^sub>R i)::'a) ` Pow Basis"])
prefer 3 apply(rule unit_interval_convex_hull) apply rule unfolding mem_Collect_eq proof-
- fix x::"'a" assume as:"\<forall>i<DIM('a). x $$ i = 0 \<or> x $$ i = 1"
- show "x \<in> (\<lambda>s. \<chi>\<chi> i. if i \<in> s then 1 else 0) ` Pow {..<DIM('a)}"
- apply(rule image_eqI[where x="{i. i<DIM('a) \<and> x$$i = 1}"])
- using as apply(subst euclidean_eq) by auto qed auto
+ fix x::"'a" assume as:"\<forall>i\<in>Basis. x \<bullet> i = 0 \<or> x \<bullet> i = 1"
+ show "x \<in> (\<lambda>s. \<Sum>i\<in>Basis. (if i\<in>s then 1 else 0) *\<^sub>R i) ` Pow Basis"
+ apply(rule image_eqI[where x="{i. i\<in>Basis \<and> x\<bullet>i = 1}"])
+ using as apply(subst euclidean_eq_iff) by (auto simp: inner_setsum_left_Basis)
+qed auto
text {* Hence any cube (could do any nonempty interval). *}
lemma cube_convex_hull:
assumes "0 < d" obtains s::"('a::ordered_euclidean_space) set" where
- "finite s" "{x - (\<chi>\<chi> i. d) .. x + (\<chi>\<chi> i. d)} = convex hull s" proof-
- let ?d = "(\<chi>\<chi> i. d)::'a"
- have *:"{x - ?d .. x + ?d} = (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` {0 .. \<chi>\<chi> i. 1}" apply(rule set_eqI, rule)
+ "finite s" "{x - (\<Sum>i\<in>Basis. d*\<^sub>Ri) .. x + (\<Sum>i\<in>Basis. d*\<^sub>Ri)} = convex hull s" proof-
+ let ?d = "(\<Sum>i\<in>Basis. d*\<^sub>Ri)::'a"
+ have *:"{x - ?d .. x + ?d} = (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` {0 .. \<Sum>Basis}" apply(rule set_eqI, rule)
unfolding image_iff defer apply(erule bexE) proof-
fix y assume as:"y\<in>{x - ?d .. x + ?d}"
- { fix i assume i:"i<DIM('a)" have "x $$ i \<le> d + y $$ i" "y $$ i \<le> d + x $$ i"
- using as[unfolded mem_interval, THEN spec[where x=i]] i
- by auto
- hence "1 \<ge> inverse d * (x $$ i - y $$ i)" "1 \<ge> inverse d * (y $$ i - x $$ i)"
+ { fix i :: 'a assume i:"i\<in>Basis" have "x \<bullet> i \<le> d + y \<bullet> i" "y \<bullet> i \<le> d + x \<bullet> i"
+ using as[unfolded mem_interval, THEN bspec[where x=i]] i
+ by (auto simp: inner_simps)
+ hence "1 \<ge> inverse d * (x \<bullet> i - y \<bullet> i)" "1 \<ge> inverse d * (y \<bullet> i - x \<bullet> i)"
apply(rule_tac[!] mult_left_le_imp_le[OF _ assms]) unfolding mult_assoc[symmetric]
using assms by(auto simp add: field_simps)
- hence "inverse d * (x $$ i * 2) \<le> 2 + inverse d * (y $$ i * 2)"
- "inverse d * (y $$ i * 2) \<le> 2 + inverse d * (x $$ i * 2)" by(auto simp add:field_simps) }
- hence "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> {0..\<chi>\<chi> i.1}" unfolding mem_interval using assms
- by(auto simp add: field_simps)
- thus "\<exists>z\<in>{0..\<chi>\<chi> i.1}. y = x - ?d + (2 * d) *\<^sub>R z" apply- apply(rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
+ hence "inverse d * (x \<bullet> i * 2) \<le> 2 + inverse d * (y \<bullet> i * 2)"
+ "inverse d * (y \<bullet> i * 2) \<le> 2 + inverse d * (x \<bullet> i * 2)" by(auto simp add:field_simps) }
+ hence "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> {0..\<Sum>Basis}" unfolding mem_interval using assms
+ by(auto simp add: field_simps inner_simps)
+ thus "\<exists>z\<in>{0..\<Sum>Basis}. y = x - ?d + (2 * d) *\<^sub>R z" apply- apply(rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
using assms by auto
next
- fix y z assume as:"z\<in>{0..\<chi>\<chi> i.1}" "y = x - ?d + (2*d) *\<^sub>R z"
- have "\<And>i. i<DIM('a) \<Longrightarrow> 0 \<le> d * z $$ i \<and> d * z $$ i \<le> d"
- using assms as(1)[unfolded mem_interval] apply(erule_tac x=i in allE)
+ fix y z assume as:"z\<in>{0..\<Sum>Basis}" "y = x - ?d + (2*d) *\<^sub>R z"
+ have "\<And>i. i\<in>Basis \<Longrightarrow> 0 \<le> d * (z \<bullet> i) \<and> d * (z \<bullet> i) \<le> d"
+ using assms as(1)[unfolded mem_interval] apply(erule_tac x=i in ballE)
apply rule apply(rule mult_nonneg_nonneg) prefer 3 apply(rule mult_right_le_one_le)
using assms by auto
thus "y \<in> {x - ?d..x + ?d}" unfolding as(2) mem_interval apply- apply rule using as(1)[unfolded mem_interval]
- apply(erule_tac x=i in allE) using assms by auto qed
- obtain s where "finite s" "{0::'a..\<chi>\<chi> i.1} = convex hull s" using unit_cube_convex_hull by auto
+ apply(erule_tac x=i in ballE) using assms by (auto simp: inner_simps) qed
+ obtain s where "finite s" "{0::'a..\<Sum>Basis} = convex hull s" using unit_cube_convex_hull by auto
thus ?thesis apply(rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` s"]) unfolding * and convex_hull_affinity by auto qed
subsection {* Bounded convex function on open set is continuous *}
@@ -4103,6 +4093,9 @@
subsubsection {* Hence a convex function on an open set is continuous *}
+lemma real_of_nat_ge_one_iff: "1 \<le> real (n::nat) \<longleftrightarrow> 1 \<le> n"
+ by auto
+
lemma convex_on_continuous:
assumes "open (s::('a::ordered_euclidean_space) set)" "convex_on s f"
(* FIXME: generalize to euclidean_space *)
@@ -4113,29 +4106,40 @@
then obtain e where e:"cball x e \<subseteq> s" "e>0" using assms(1) unfolding open_contains_cball by auto
def d \<equiv> "e / real DIM('a)"
have "0 < d" unfolding d_def using `e>0` dimge1 by(rule_tac divide_pos_pos, auto)
- let ?d = "(\<chi>\<chi> i. d)::'a"
+ let ?d = "(\<Sum>i\<in>Basis. d *\<^sub>R i)::'a"
obtain c where c:"finite c" "{x - ?d..x + ?d} = convex hull c" using cube_convex_hull[OF `d>0`, of x] by auto
- have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by auto
+ have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by (auto simp: inner_setsum_left_Basis inner_simps)
hence "c\<noteq>{}" using c by auto
def k \<equiv> "Max (f ` c)"
- have "convex_on {x - ?d..x + ?d} f" apply(rule convex_on_subset[OF assms(2)])
- apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof
+ have "convex_on {x - ?d..x + ?d} f"
+ apply(rule convex_on_subset[OF assms(2)])
+ apply(rule subset_trans[OF _ e(1)])
+ unfolding subset_eq mem_cball
+ proof
fix z assume z:"z\<in>{x - ?d..x + ?d}"
- have e:"e = setsum (\<lambda>i. d) {..<DIM('a)}" unfolding setsum_constant d_def using dimge1
+ have e:"e = setsum (\<lambda>i::'a. d) Basis" unfolding setsum_constant d_def using dimge1
unfolding real_eq_of_nat by auto
show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
- using z[unfolded mem_interval] apply(erule_tac x=i in allE) by auto qed
+ using z[unfolded mem_interval] apply(erule_tac x=b in ballE) by (auto simp: inner_simps)
+ qed
hence k:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption
unfolding k_def apply(rule, rule Max_ge) using c(1) by auto
- have "d \<le> e" unfolding d_def apply(rule mult_imp_div_pos_le) using `e>0` dimge1 unfolding mult_le_cancel_left1 by auto
+ have "d \<le> e"
+ unfolding d_def
+ apply(rule mult_imp_div_pos_le)
+ using `e>0`
+ unfolding mult_le_cancel_left1
+ apply (auto simp: real_of_nat_ge_one_iff Suc_le_eq DIM_positive)
+ done
hence dsube:"cball x d \<subseteq> cball x e" unfolding subset_eq Ball_def mem_cball by auto
have conv:"convex_on (cball x d) f" apply(rule convex_on_subset, rule convex_on_subset[OF assms(2)]) apply(rule e(1)) using dsube by auto
hence "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)" apply(rule_tac convex_bounds_lemma) apply assumption proof
fix y assume y:"y\<in>cball x d"
- { fix i assume "i<DIM('a)" hence "x $$ i - d \<le> y $$ i" "y $$ i \<le> x $$ i + d"
- using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by auto }
+ { fix i :: 'a assume "i\<in>Basis" hence "x \<bullet> i - d \<le> y \<bullet> i" "y \<bullet> i \<le> x \<bullet> i + d"
+ using order_trans[OF Basis_le_norm y[unfolded mem_cball dist_norm], of i] by (auto simp: inner_diff_left) }
thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm
- by auto qed
+ by (auto simp: inner_simps)
+ qed
hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous)
apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball)
apply force
@@ -4266,25 +4270,26 @@
have "norm (a - x) / norm (a - b) \<le> 1" unfolding divide_le_eq_1_pos[OF Fal2]
unfolding as[unfolded dist_norm] norm_ge_zero by auto
thus "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" apply(rule_tac x="dist a x / dist a b" in exI)
- unfolding dist_norm apply(subst euclidean_eq) apply rule defer apply(rule, rule divide_nonneg_pos) prefer 4
- proof(rule,rule) fix i assume i:"i<DIM('a)"
- have "((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $$ i =
- ((norm (a - b) - norm (a - x)) * (a $$ i) + norm (a - x) * (b $$ i)) / norm (a - b)"
- using Fal by(auto simp add: field_simps)
- also have "\<dots> = x$$i" apply(rule divide_eq_imp[OF Fal])
+ unfolding dist_norm apply(subst euclidean_eq_iff) apply rule defer apply(rule, rule divide_nonneg_pos) prefer 4
+ proof(rule) fix i :: 'a assume i:"i\<in>Basis"
+ have "((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) \<bullet> i =
+ ((norm (a - b) - norm (a - x)) * (a \<bullet> i) + norm (a - x) * (b \<bullet> i)) / norm (a - b)"
+ using Fal by(auto simp add: field_simps inner_simps)
+ also have "\<dots> = x\<bullet>i" apply(rule divide_eq_imp[OF Fal])
unfolding as[unfolded dist_norm] using as[unfolded dist_triangle_eq] apply-
- apply(subst (asm) euclidean_eq) using i apply(erule_tac x=i in allE) by(auto simp add:field_simps)
- finally show "x $$ i = ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $$ i"
+ apply(subst (asm) euclidean_eq_iff) using i apply(erule_tac x=i in ballE) by(auto simp add:field_simps inner_simps)
+ finally show "x \<bullet> i = ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) \<bullet> i"
by auto
- qed(insert Fal2, auto) qed qed
+ qed(insert Fal2, auto) qed
+qed
lemma between_midpoint: fixes a::"'a::euclidean_space" shows
"between (a,b) (midpoint a b)" (is ?t1)
"between (b,a) (midpoint a b)" (is ?t2)
proof- have *:"\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y" by auto
show ?t1 ?t2 unfolding between midpoint_def dist_norm apply(rule_tac[!] *)
- unfolding euclidean_eq[where 'a='a]
- by(auto simp add:field_simps) qed
+ unfolding euclidean_eq_iff[where 'a='a]
+ by(auto simp add:field_simps inner_simps) qed
lemma between_mem_convex_hull:
"between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}"
@@ -4303,7 +4308,7 @@
have *:"y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using `e>0` by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
unfolding dist_norm unfolding norm_scaleR[symmetric] apply(rule arg_cong[where f=norm]) using `e>0`
- by(auto simp add: euclidean_eq[where 'a='a] field_simps)
+ by(auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
also have "\<dots> = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
also have "\<dots> < d" using as[unfolded dist_norm] and `e>0`
by(auto simp add:pos_divide_less_eq[OF `e>0`] mult_commute)
@@ -4347,236 +4352,237 @@
apply(rule_tac x=u in exI) defer apply(rule_tac x="\<lambda>x. if x = 0 then 1 - setsum u s else u x" in exI) using assms(2)
unfolding if_smult and setsum_delta_notmem[OF assms(2)] by auto
-lemma substd_simplex: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
- shows "convex hull (insert 0 { basis i | i. i : d}) =
- {x::'a::euclidean_space . (!i<DIM('a). 0 <= x$$i) & setsum (%i. x$$i) d <= 1 &
- (!i<DIM('a). i ~: d --> x$$i = 0)}"
+lemma substd_simplex:
+ assumes d: "d \<subseteq> Basis"
+ shows "convex hull (insert 0 d) = {x. (\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> (\<Sum>i\<in>d. x\<bullet>i) \<le> 1 \<and> (\<forall>i\<in>Basis. i \<notin> d --> x\<bullet>i = 0)}"
(is "convex hull (insert 0 ?p) = ?s")
-(* Proof is a modified copy of the proof of similar lemma std_simplex in Convex_Euclidean_Space.thy *)
-proof- let ?D = d (*"{..<DIM('a::euclidean_space)}"*)
+proof- let ?D = d
have "0 ~: ?p" using assms by (auto simp: image_def)
- have "{(basis i)::'n::euclidean_space |i. i \<in> ?D} = basis ` ?D" by auto
- note sumbas = this setsum_reindex[OF basis_inj_on[of d], unfolded o_def, OF assms]
- show ?thesis unfolding simplex[OF finite_substdbasis `0 ~: ?p`]
+ from d have "finite d" by (blast intro: finite_subset finite_Basis)
+ show ?thesis unfolding simplex[OF `finite d` `0 ~: ?p`]
apply(rule set_eqI) unfolding mem_Collect_eq apply rule
apply(erule exE, (erule conjE)+) apply(erule_tac[2] conjE)+ proof-
- fix x::"'a::euclidean_space" and u assume as: "\<forall>x\<in>{basis i |i. i \<in>?D}. 0 \<le> u x"
- "setsum u {basis i |i. i \<in> ?D} \<le> 1" "(\<Sum>x\<in>{basis i |i. i \<in>?D}. u x *\<^sub>R x) = x"
- have *:"\<forall>i<DIM('a). i:d --> u (basis i) = x$$i" and "(!i<DIM('a). i ~: d --> x $$ i = 0)" using as(3)
- unfolding sumbas unfolding substdbasis_expansion_unique[OF assms] by auto
- hence **:"setsum u {basis i |i. i \<in> ?D} = setsum (op $$ x) ?D" unfolding sumbas
+ fix x::"'a::euclidean_space" and u assume as: "\<forall>x\<in>?D. 0 \<le> u x"
+ "setsum u ?D \<le> 1" "(\<Sum>x\<in>?D. u x *\<^sub>R x) = x"
+ have *:"\<forall>i\<in>Basis. i:d --> u i = x\<bullet>i" and "(\<forall>i\<in>Basis. i ~: d --> x \<bullet> i = 0)" using as(3)
+ unfolding substdbasis_expansion_unique[OF assms] by auto
+ hence **:"setsum u ?D = setsum (op \<bullet> x) ?D"
apply-apply(rule setsum_cong2) using assms by auto
- have " (\<forall>i<DIM('a). 0 \<le> x$$i) \<and> setsum (op $$ x) ?D \<le> 1"
- apply - proof(rule,rule,rule)
- fix i assume i:"i<DIM('a)" have "i : d ==> 0 \<le> x$$i" unfolding *[rule_format,OF i,symmetric]
+ have " (\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> setsum (op \<bullet> x) ?D \<le> 1"
+ apply - proof(rule,rule)
+ fix i :: 'a assume i:"i\<in>Basis" have "i : d ==> 0 \<le> x\<bullet>i" unfolding *[rule_format,OF i,symmetric]
apply(rule_tac as(1)[rule_format]) by auto
- moreover have "i ~: d ==> 0 \<le> x$$i"
- using `(!i<DIM('a). i ~: d --> x $$ i = 0)`[rule_format, OF i] by auto
- ultimately show "0 \<le> x$$i" by auto
+ moreover have "i ~: d ==> 0 \<le> x\<bullet>i"
+ using `(\<forall>i\<in>Basis. i ~: d --> x \<bullet> i = 0)`[rule_format, OF i] by auto
+ ultimately show "0 \<le> x\<bullet>i" by auto
qed(insert as(2)[unfolded **], auto)
- from this show " (\<forall>i<DIM('a). 0 \<le> x$$i) \<and> setsum (op $$ x) ?D \<le> 1 & (!i<DIM('a). i ~: d --> x $$ i = 0)"
- using `(!i<DIM('a). i ~: d --> x $$ i = 0)` by auto
- next fix x::"'a::euclidean_space" assume as:"\<forall>i<DIM('a). 0 \<le> x $$ i" "setsum (op $$ x) ?D \<le> 1"
- "(!i<DIM('a). i ~: d --> x $$ i = 0)"
- 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. 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 apply safe unfolding not_less basis_zero
- unfolding substdbasis_expansion_unique[OF assms] euclidean_component_def[symmetric]
- using as(2,3) by(auto simp add:dot_basis not_less)
- qed qed
+ from this show " (\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> setsum (op \<bullet> x) ?D \<le> 1 & (\<forall>i\<in>Basis. i ~: d --> x \<bullet> i = 0)"
+ using `(\<forall>i\<in>Basis. i ~: d --> x \<bullet> i = 0)` by auto
+ next fix x::"'a::euclidean_space" assume as:"\<forall>i\<in>Basis. 0 \<le> x \<bullet> i" "setsum (op \<bullet> x) ?D \<le> 1"
+ "(\<forall>i\<in>Basis. i ~: d --> x \<bullet> i = 0)"
+ show "\<exists>u. (\<forall>x\<in>?D. 0 \<le> u x) \<and> setsum u ?D \<le> 1 \<and> (\<Sum>x\<in>?D. u x *\<^sub>R x) = x"
+ using as d unfolding substdbasis_expansion_unique[OF assms]
+ by (rule_tac x="inner x" in exI) auto
+ qed
+qed
lemma std_simplex:
- "convex hull (insert 0 { basis i | i. i<DIM('a)}) =
- {x::'a::euclidean_space . (\<forall>i<DIM('a). 0 \<le> x$$i) \<and> setsum (\<lambda>i. x$$i) {..<DIM('a)} \<le> 1 }"
- using substd_simplex[of "{..<DIM('a)}"] by auto
+ "convex hull (insert 0 Basis) =
+ {x::'a::euclidean_space . (\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> setsum (\<lambda>i. x\<bullet>i) Basis \<le> 1 }"
+ using substd_simplex[of Basis] by auto
lemma interior_std_simplex:
- "interior (convex hull (insert 0 { basis i| i. i<DIM('a)})) =
- {x::'a::euclidean_space. (\<forall>i<DIM('a). 0 < x$$i) \<and> setsum (\<lambda>i. x$$i) {..<DIM('a)} < 1 }"
+ "interior (convex hull (insert 0 Basis)) =
+ {x::'a::euclidean_space. (\<forall>i\<in>Basis. 0 < x\<bullet>i) \<and> setsum (\<lambda>i. x\<bullet>i) Basis < 1 }"
apply(rule set_eqI) unfolding mem_interior std_simplex unfolding subset_eq mem_Collect_eq Ball_def mem_ball
unfolding Ball_def[symmetric] apply rule apply(erule exE, (erule conjE)+) defer apply(erule conjE) proof-
- fix x::"'a" and e assume "0<e" and as:"\<forall>xa. dist x xa < e \<longrightarrow> (\<forall>x<DIM('a). 0 \<le> xa $$ x) \<and> setsum (op $$ xa) {..<DIM('a)} \<le> 1"
- show "(\<forall>xa<DIM('a). 0 < x $$ xa) \<and> setsum (op $$ x) {..<DIM('a)} < 1" apply(safe) proof-
- fix i assume i:"i<DIM('a)" thus "0 < x $$ i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R basis i"]] and `e>0`
- unfolding dist_norm by (auto elim!:allE[where x=i])
- next have **:"dist x (x + (e / 2) *\<^sub>R basis 0) < e" using `e>0`
- unfolding dist_norm by(auto intro!: mult_strict_left_mono)
- have "\<And>i. i<DIM('a) \<Longrightarrow> (x + (e / 2) *\<^sub>R basis 0) $$ i = x$$i + (if i = 0 then e/2 else 0)"
- by auto
- hence *:"setsum (op $$ (x + (e / 2) *\<^sub>R basis 0)) {..<DIM('a)} = setsum (\<lambda>i. x$$i + (if 0 = i then e/2 else 0)) {..<DIM('a)}"
+ fix x::"'a" and e assume "0<e" and as:"\<forall>xa. dist x xa < e \<longrightarrow> (\<forall>x\<in>Basis. 0 \<le> xa \<bullet> x) \<and> setsum (op \<bullet> xa) Basis \<le> 1"
+ show "(\<forall>xa\<in>Basis. 0 < x \<bullet> xa) \<and> setsum (op \<bullet> x) Basis < 1" apply(safe) proof-
+ fix i :: 'a assume i:"i\<in>Basis" thus "0 < x \<bullet> i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R i"]] and `e>0`
+ unfolding dist_norm
+ by (auto elim!:ballE[where x=i] simp: inner_simps)
+ next have **:"dist x (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis)) < e" using `e>0`
+ unfolding dist_norm by(auto intro!: mult_strict_left_mono simp: SOME_Basis)
+ have "\<And>i. i\<in>Basis \<Longrightarrow> (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis)) \<bullet> i = x\<bullet>i + (if i = (SOME i. i\<in>Basis) then e/2 else 0)"
+ by (auto simp: SOME_Basis inner_Basis inner_simps)
+ hence *:"setsum (op \<bullet> (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis))) Basis = setsum (\<lambda>i. x\<bullet>i + (if (SOME i. i\<in>Basis) = i then e/2 else 0)) Basis"
apply(rule_tac setsum_cong) by auto
- have "setsum (op $$ x) {..<DIM('a)} < setsum (op $$ (x + (e / 2) *\<^sub>R basis 0)) {..<DIM('a)}" unfolding * setsum_addf
- using `0<e` DIM_positive[where 'a='a] apply(subst setsum_delta') by auto
+ have "setsum (op \<bullet> x) Basis < setsum (op \<bullet> (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis))) Basis" unfolding * setsum_addf
+ using `0<e` DIM_positive[where 'a='a] apply(subst setsum_delta') by (auto simp: SOME_Basis)
also have "\<dots> \<le> 1" using ** apply(drule_tac as[rule_format]) by auto
- finally show "setsum (op $$ x) {..<DIM('a)} < 1" by auto qed
-next fix x::"'a" assume as:"\<forall>i<DIM('a). 0 < x $$ i" "setsum (op $$ x) {..<DIM('a)} < 1"
+ finally show "setsum (op \<bullet> x) Basis < 1" by auto qed
+next fix x::"'a" assume as:"\<forall>i\<in>Basis. 0 < x \<bullet> i" "setsum (op \<bullet> x) Basis < 1"
guess a using UNIV_witness[where 'a='b] ..
- let ?d = "(1 - setsum (op $$ x) {..<DIM('a)}) / real (DIM('a))"
- have "Min ((op $$ x) ` {..<DIM('a)}) > 0" apply(rule Min_grI) using as(1) by auto
- moreover have"?d > 0" apply(rule divide_pos_pos) using as(2) by(auto simp add: Suc_le_eq)
- ultimately show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> (\<forall>i<DIM('a). 0 \<le> y $$ i) \<and> setsum (op $$ y) {..<DIM('a)} \<le> 1"
- apply(rule_tac x="min (Min ((op $$ x) ` {..<DIM('a)})) ?D" in exI) apply rule defer apply(rule,rule) proof-
- fix y assume y:"dist x y < min (Min (op $$ x ` {..<DIM('a)})) ?d"
- have "setsum (op $$ y) {..<DIM('a)} \<le> setsum (\<lambda>i. x$$i + ?d) {..<DIM('a)}" proof(rule setsum_mono)
- fix i assume "i\<in>{..<DIM('a)}" hence "abs (y$$i - x$$i) < ?d" apply-apply(rule le_less_trans)
- using component_le_norm[of "y - x" i]
- using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add: norm_minus_commute)
- thus "y $$ i \<le> x $$ i + ?d" by auto qed
+ let ?d = "(1 - setsum (op \<bullet> x) Basis) / real (DIM('a))"
+ have "Min ((op \<bullet> x) ` Basis) > 0" apply(rule Min_grI) using as(1) by auto
+ moreover have"?d > 0" apply(rule divide_pos_pos) using as(2) by (auto simp add: Suc_le_eq DIM_positive)
+ ultimately show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> (\<forall>i\<in>Basis. 0 \<le> y \<bullet> i) \<and> setsum (op \<bullet> y) Basis \<le> 1"
+ apply(rule_tac x="min (Min ((op \<bullet> x) ` Basis)) ?D" in exI) apply rule defer apply(rule,rule) proof-
+ fix y assume y:"dist x y < min (Min (op \<bullet> x ` Basis)) ?d"
+ have "setsum (op \<bullet> y) Basis \<le> setsum (\<lambda>i. x\<bullet>i + ?d) Basis" proof(rule setsum_mono)
+ fix i :: 'a assume i: "i\<in>Basis" hence "abs (y\<bullet>i - x\<bullet>i) < ?d" apply-apply(rule le_less_trans)
+ using Basis_le_norm[OF i, of "y - x"]
+ using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add: norm_minus_commute inner_diff_left)
+ thus "y \<bullet> i \<le> x \<bullet> i + ?d" by auto qed
also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant real_eq_of_nat by(auto simp add: Suc_le_eq)
- finally show "(\<forall>i<DIM('a). 0 \<le> y $$ i) \<and> setsum (op $$ y) {..<DIM('a)} \<le> 1"
- proof safe fix i assume i:"i<DIM('a)"
- have "norm (x - y) < x$$i" apply(rule less_le_trans)
+ finally show "(\<forall>i\<in>Basis. 0 \<le> y \<bullet> i) \<and> setsum (op \<bullet> y) Basis \<le> 1"
+ proof safe fix i :: 'a assume i:"i\<in>Basis"
+ have "norm (x - y) < x\<bullet>i" apply(rule less_le_trans)
apply(rule y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]) using i by auto
- thus "0 \<le> y$$i" using component_le_norm[of "x - y" i] and as(1)[rule_format, of i] by auto
+ thus "0 \<le> y\<bullet>i" using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format, OF i]
+ by (auto simp: inner_simps)
qed qed auto qed
lemma interior_std_simplex_nonempty: obtains a::"'a::euclidean_space" where
- "a \<in> interior(convex hull (insert 0 {basis i | i . i<DIM('a)}))" proof-
- let ?D = "{..<DIM('a)}" let ?a = "setsum (\<lambda>b::'a. inverse (2 * real DIM('a)) *\<^sub>R b) {(basis i) | i. i<DIM('a)}"
- have *:"{basis i :: 'a | i. i<DIM('a)} = basis ` ?D" by auto
- { fix i assume i:"i<DIM('a)" have "?a $$ i = inverse (2 * real DIM('a))"
- unfolding euclidean_component_setsum * and setsum_reindex[OF basis_inj] and o_def
- apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real DIM('a)) else 0) ?D"]) apply(rule setsum_cong2)
- defer apply(subst setsum_delta') unfolding euclidean_component_def using i by(auto simp add:dot_basis) }
+ "a \<in> interior(convex hull (insert 0 Basis))" proof-
+ let ?D = "Basis :: 'a set" let ?a = "setsum (\<lambda>b::'a. inverse (2 * real DIM('a)) *\<^sub>R b) Basis"
+ { fix i :: 'a assume i:"i\<in>Basis" have "?a \<bullet> i = inverse (2 * real DIM('a))"
+ by (rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real DIM('a)) else 0) ?D"])
+ (simp_all add: setsum_cases i) }
note ** = this
show ?thesis apply(rule that[of ?a]) unfolding interior_std_simplex mem_Collect_eq proof safe
- fix i assume i:"i<DIM('a)" show "0 < ?a $$ i" unfolding **[OF i] by(auto simp add: Suc_le_eq)
- next have "setsum (op $$ ?a) ?D = setsum (\<lambda>i. inverse (2 * real DIM('a))) ?D" apply(rule setsum_cong2, rule **) by auto
+ fix i :: 'a assume i:"i\<in>Basis" show "0 < ?a \<bullet> i" unfolding **[OF i] by(auto simp add: Suc_le_eq DIM_positive)
+ next have "setsum (op \<bullet> ?a) ?D = setsum (\<lambda>i. inverse (2 * real DIM('a))) ?D" apply(rule setsum_cong2, rule **) by auto
also have "\<dots> < 1" unfolding setsum_constant real_eq_of_nat divide_inverse[symmetric] by (auto simp add:field_simps)
- finally show "setsum (op $$ ?a) ?D < 1" by auto qed qed
-
-lemma rel_interior_substd_simplex: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
- shows "rel_interior (convex hull (insert 0 { basis i| i. i : d})) =
- {x::'a::euclidean_space. (\<forall>i\<in>d. 0 < x$$i) & setsum (%i. x$$i) d < 1 & (!i<DIM('a). i ~: d --> x$$i = 0)}"
+ finally show "setsum (op \<bullet> ?a) ?D < 1" by auto qed qed
+
+lemma rel_interior_substd_simplex: assumes d: "d\<subseteq>Basis"
+ shows "rel_interior (convex hull (insert 0 d)) =
+ {x::'a::euclidean_space. (\<forall>i\<in>d. 0 < x\<bullet>i) \<and> (\<Sum>i\<in>d. x\<bullet>i) < 1 \<and> (\<forall>i\<in>Basis. i ~: d --> x\<bullet>i = 0)}"
(is "rel_interior (convex hull (insert 0 ?p)) = ?s")
(* Proof is a modified copy of the proof of similar lemma interior_std_simplex in Convex_Euclidean_Space.thy *)
proof-
have "finite d" apply(rule finite_subset) using assms by auto
-{ assume "d={}" hence ?thesis using rel_interior_sing using euclidean_eq[of _ 0] by auto }
+{ assume "d={}" hence ?thesis using rel_interior_sing using euclidean_eq_iff[of _ 0] by auto }
moreover
{ assume "d~={}"
-have h0: "affine hull (convex hull (insert 0 ?p))={x::'a::euclidean_space. (!i<DIM('a). i ~: d --> x$$i = 0)}"
+have h0: "affine hull (convex hull (insert 0 ?p))={x::'a::euclidean_space. (\<forall>i\<in>Basis. i ~: d --> x\<bullet>i = 0)}"
using affine_hull_convex_hull affine_hull_substd_basis assms by auto
-have aux: "!x::'n::euclidean_space. !i. ((! i:d. 0 <= x$$i) & (!i. i ~: d --> x$$i = 0))--> 0 <= x$$i" by auto
+have aux: "!!x::'a. \<forall>i\<in>Basis. ((\<forall>i\<in>d. 0 \<le> x\<bullet>i) \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)) \<longrightarrow> 0 \<le> x\<bullet>i"
+ by auto
{ fix x::"'a::euclidean_space" assume x_def: "x : rel_interior (convex hull (insert 0 ?p))"
from this obtain e where e0: "e>0" and
- "ball x e Int {xa. (!i<DIM('a). i ~: d --> xa$$i = 0)} <= convex hull (insert 0 ?p)"
+ "ball x e Int {xa. (\<forall>i\<in>Basis. i ~: d --> xa\<bullet>i = 0)} <= convex hull (insert 0 ?p)"
using mem_rel_interior_ball[of x "convex hull (insert 0 ?p)"] h0 by auto
- hence as: "ALL xa. (dist x xa < e & (!i<DIM('a). i ~: d --> xa$$i = 0)) -->
- (!i : d. 0 <= xa $$ i) & setsum (op $$ xa) d <= 1"
+ hence as: "ALL xa. (dist x xa < e & (\<forall>i\<in>Basis. i ~: d --> xa\<bullet>i = 0)) -->
+ (!i : d. 0 <= xa \<bullet> i) & setsum (op \<bullet> xa) d <= 1"
unfolding ball_def unfolding substd_simplex[OF assms] using assms by auto
- have x0: "(!i<DIM('a). i ~: d --> x$$i = 0)"
+ have x0: "(\<forall>i\<in>Basis. i ~: d --> x\<bullet>i = 0)"
using x_def rel_interior_subset substd_simplex[OF assms] by auto
- have "(!i : d. 0 < x $$ i) & setsum (op $$ x) d < 1 & (!i<DIM('a). i ~: d --> x$$i = 0)" apply(rule,rule)
+ have "(\<forall>i\<in>d. 0 < x \<bullet> i) & setsum (op \<bullet> x) d < 1 & (\<forall>i\<in>Basis. i ~: d --> x\<bullet>i = 0)" apply(rule,rule)
proof-
- fix i::nat assume "i:d"
- hence "\<forall>ia\<in>d. 0 \<le> (x - (e / 2) *\<^sub>R basis i) $$ ia" apply-apply(rule as[rule_format,THEN conjunct1])
- unfolding dist_norm using assms `e>0` x0 by auto
- thus "0 < x $$ i" apply(erule_tac x=i in ballE) using `e>0` `i\<in>d` assms by auto
+ fix i::'a assume "i\<in>d"
+ hence "\<forall>ia\<in>d. 0 \<le> (x - (e / 2) *\<^sub>R i) \<bullet> ia" apply-apply(rule as[rule_format,THEN conjunct1])
+ unfolding dist_norm using d `e>0` x0 by (auto simp: inner_simps inner_Basis)
+ thus "0 < x \<bullet> i" apply(erule_tac x=i in ballE) using `e>0` `i\<in>d` d
+ by (auto simp: inner_simps inner_Basis)
next obtain a where a:"a:d" using `d ~= {}` by auto
- have **:"dist x (x + (e / 2) *\<^sub>R basis a) < e"
- using `e>0` and Euclidean_Space.norm_basis[of a]
+ then have **:"dist x (x + (e / 2) *\<^sub>R a) < e"
+ using `e>0` norm_Basis[of a] d
unfolding dist_norm by auto
- have "\<And>i. (x + (e / 2) *\<^sub>R basis a) $$ i = x$$i + (if i = a then e/2 else 0)"
- unfolding euclidean_simps using a assms by auto
- hence *:"setsum (op $$ (x + (e / 2) *\<^sub>R basis a)) d =
- setsum (\<lambda>i. x$$i + (if a = i then e/2 else 0)) d" by(rule_tac setsum_cong, auto)
- have h1: "(ALL i<DIM('a). i ~: d --> (x + (e / 2) *\<^sub>R basis a) $$ i = 0)"
- using as[THEN spec[where x="x + (e / 2) *\<^sub>R basis a"]] `a:d` using x0
- by(auto elim:allE[where x=a])
- have "setsum (op $$ x) d < setsum (op $$ (x + (e / 2) *\<^sub>R basis a)) d" unfolding * setsum_addf
+ have "\<And>i. i\<in>Basis \<Longrightarrow> (x + (e / 2) *\<^sub>R a) \<bullet> i = x\<bullet>i + (if i = a then e/2 else 0)"
+ using a d by (auto simp: inner_simps inner_Basis)
+ hence *:"setsum (op \<bullet> (x + (e / 2) *\<^sub>R a)) d =
+ setsum (\<lambda>i. x\<bullet>i + (if a = i then e/2 else 0)) d" using d by (intro setsum_cong) auto
+ have "a \<in> Basis" using `a \<in> d` d by auto
+ then have h1: "(\<forall>i\<in>Basis. i ~: d --> (x + (e / 2) *\<^sub>R a) \<bullet> i = 0)"
+ using x0 d `a\<in>d` by (auto simp add: inner_add_left inner_Basis)
+ have "setsum (op \<bullet> x) d < setsum (op \<bullet> (x + (e / 2) *\<^sub>R a)) d" unfolding * setsum_addf
using `0<e` `a:d` using `finite d` by(auto simp add: setsum_delta')
- also have "\<dots> \<le> 1" using ** h1 as[rule_format, of "x + (e / 2) *\<^sub>R basis a"] by auto
- finally show "setsum (op $$ x) d < 1 & (!i<DIM('a). i ~: d --> x$$i = 0)" using x0 by auto
+ also have "\<dots> \<le> 1" using ** h1 as[rule_format, of "x + (e / 2) *\<^sub>R a"] by auto
+ finally show "setsum (op \<bullet> x) d < 1 & (\<forall>i\<in>Basis. i ~: d --> x\<bullet>i = 0)" using x0 by auto
qed
}
moreover
{
fix x::"'a::euclidean_space" assume as: "x : ?s"
- have "!i. ((0<x$$i) | (0=x$$i) --> 0<=x$$i)" by auto
+ have "!i. ((0<x\<bullet>i) | (0=x\<bullet>i) --> 0<=x\<bullet>i)" by auto
moreover have "!i. (i:d) | (i ~: d)" by auto
ultimately
- have "!i. ( (ALL i:d. 0 < x$$i) & (ALL i. i ~: d --> x$$i = 0) ) --> 0 <= x$$i" by metis
+ have "!i. ( (ALL i:d. 0 < x\<bullet>i) & (ALL i. i ~: d --> x\<bullet>i = 0) ) --> 0 <= x\<bullet>i" by metis
hence h2: "x : convex hull (insert 0 ?p)" using as assms
unfolding substd_simplex[OF assms] by fastforce
obtain a where a:"a:d" using `d ~= {}` by auto
- let ?d = "(1 - setsum (op $$ x) d) / real (card d)"
+ let ?d = "(1 - setsum (op \<bullet> x) d) / real (card d)"
have "0 < card d" using `d ~={}` `finite d` by (simp add: card_gt_0_iff)
- have "Min ((op $$ x) ` d) > 0" using as `d \<noteq> {}` `finite d` by (simp add: Min_grI)
+ have "Min ((op \<bullet> x) ` d) > 0" using as `d \<noteq> {}` `finite d` by (simp add: Min_grI)
moreover have "?d > 0" apply(rule divide_pos_pos) using as using `0 < card d` by auto
- ultimately have h3: "min (Min ((op $$ x) ` d)) ?d > 0" by auto
+ ultimately have h3: "min (Min ((op \<bullet> x) ` d)) ?d > 0" by auto
have "x : rel_interior (convex hull (insert 0 ?p))"
unfolding rel_interior_ball mem_Collect_eq h0 apply(rule,rule h2)
unfolding substd_simplex[OF assms]
- apply(rule_tac x="min (Min ((op $$ x) ` d)) ?d" in exI) apply(rule,rule h3) apply safe unfolding mem_ball
- proof- fix y::'a assume y:"dist x y < min (Min (op $$ x ` d)) ?d" and y2:"(!i<DIM('a). i ~: d --> y$$i = 0)"
- have "setsum (op $$ y) d \<le> setsum (\<lambda>i. x$$i + ?d) d" proof(rule setsum_mono)
- fix i assume i:"i\<in>d"
- have "abs (y$$i - x$$i) < ?d" apply(rule le_less_trans) using component_le_norm[of "y - x" i]
+ apply(rule_tac x="min (Min ((op \<bullet> x) ` d)) ?d" in exI) apply(rule,rule h3) apply safe unfolding mem_ball
+ proof-
+ fix y::'a assume y:"dist x y < min (Min (op \<bullet> x ` d)) ?d" and y2: "\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> y\<bullet>i = 0"
+ have "setsum (op \<bullet> y) d \<le> setsum (\<lambda>i. x\<bullet>i + ?d) d"
+ proof(rule setsum_mono)
+ fix i assume "i \<in> d"
+ with d have i: "i \<in> Basis" by auto
+ have "abs (y\<bullet>i - x\<bullet>i) < ?d" apply(rule le_less_trans) using Basis_le_norm[OF i, of "y - x"]
using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2]
- by(auto simp add: norm_minus_commute)
- thus "y $$ i \<le> x $$ i + ?d" by auto qed
+ by (auto simp add: norm_minus_commute inner_simps)
+ thus "y \<bullet> i \<le> x \<bullet> i + ?d" by auto
+ qed
also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant real_eq_of_nat
using `0 < card d` by auto
- finally show "setsum (op $$ y) d \<le> 1" .
-
- fix i assume "i<DIM('a)" thus "0 \<le> y$$i"
+ finally show "setsum (op \<bullet> y) d \<le> 1" .
+
+ fix i :: 'a assume i: "i \<in> Basis" thus "0 \<le> y\<bullet>i"
proof(cases "i\<in>d") case True
- have "norm (x - y) < x$$i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]
- using Min_gr_iff[of "op $$ x ` d" "norm (x - y)"] `0 < card d` `i:d`
+ have "norm (x - y) < x\<bullet>i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]
+ using Min_gr_iff[of "op \<bullet> x ` d" "norm (x - y)"] `0 < card d` `i:d`
by (simp add: card_gt_0_iff)
- thus "0 \<le> y$$i" using component_le_norm[of "x - y" i] and as(1)[rule_format] by auto
+ thus "0 \<le> y\<bullet>i" using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format]
+ by (auto simp: inner_simps)
qed(insert y2, auto)
qed
} ultimately have
- "!!x :: 'a::euclidean_space. (x : rel_interior (convex hull insert 0 {basis i |i. i : d})) =
- (x : {x. (ALL i:d. 0 < x $$ i) &
- setsum (op $$ x) d < 1 & (ALL i<DIM('a). i ~: d --> x $$ i = 0)})" by blast
+ "\<And>x. (x : rel_interior (convex hull insert 0 d)) = (x \<in> {x. (ALL i:d. 0 < x \<bullet> i) &
+ setsum (op \<bullet> x) d < 1 & (\<forall>i\<in>Basis. i ~: d --> x \<bullet> i = 0)})" by blast
from this have ?thesis by (rule set_eqI)
} ultimately show ?thesis by blast
qed
-lemma rel_interior_substd_simplex_nonempty: assumes "d ~={}" "d\<subseteq>{..<DIM('a::euclidean_space)}"
+lemma rel_interior_substd_simplex_nonempty: assumes "d ~={}" "d\<subseteq>Basis"
obtains a::"'a::euclidean_space" where
- "a : rel_interior(convex hull (insert 0 {basis i | i . i : d}))" proof-
+ "a : rel_interior(convex hull (insert 0 d))" proof-
(* Proof is a modified copy of the proof of similar lemma interior_std_simplex_nonempty in Convex_Euclidean_Space.thy *)
- let ?D = d let ?a = "setsum (\<lambda>b::'a::euclidean_space. inverse (2 * real (card d)) *\<^sub>R b) {(basis i) | i. i \<in> ?D}"
- have *:"{basis i :: 'a | i. i \<in> ?D} = basis ` ?D" by auto
+ let ?D = d let ?a = "setsum (\<lambda>b::'a::euclidean_space. inverse (2 * real (card d)) *\<^sub>R b) ?D"
have "finite d" apply(rule finite_subset) using assms(2) by auto
hence d1: "0 < real(card d)" using `d ~={}` by auto
- { fix i assume "i:d" have "?a $$ i = inverse (2 * real (card d))"
- unfolding * setsum_reindex[OF basis_inj_on, OF assms(2)] o_def
+ { fix i assume "i:d"
+ have "?a \<bullet> i = inverse (2 * real (card d))"
apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real (card d)) else 0) ?D"])
- unfolding euclidean_component_setsum
+ unfolding inner_setsum_left
apply(rule setsum_cong2)
using `i:d` `finite d` setsum_delta'[of d i "(%k. inverse (2 * real (card d)))"] d1 assms(2)
- by (auto simp add: Euclidean_Space.basis_component[of i])}
+ by (auto simp: inner_simps inner_Basis set_rev_mp[OF _ assms(2)]) }
note ** = this
show ?thesis apply(rule that[of ?a]) unfolding rel_interior_substd_simplex[OF assms(2)] mem_Collect_eq
proof safe fix i assume "i:d"
have "0 < inverse (2 * real (card d))" using d1 by auto
- also have "...=?a $$ i" using **[of i] `i:d` by auto
- finally show "0 < ?a $$ i" by auto
- next have "setsum (op $$ ?a) ?D = setsum (\<lambda>i. inverse (2 * real (card d))) ?D"
+ also have "...=?a \<bullet> i" using **[of i] `i:d` by auto
+ finally show "0 < ?a \<bullet> i" by auto
+ next have "setsum (op \<bullet> ?a) ?D = setsum (\<lambda>i. inverse (2 * real (card d))) ?D"
by(rule setsum_cong2, rule **)
also have "\<dots> < 1" unfolding setsum_constant real_eq_of_nat divide_real_def[symmetric]
by (auto simp add:field_simps)
- finally show "setsum (op $$ ?a) ?D < 1" by auto
- next fix i assume "i<DIM('a)" and "i~:d"
- have "?a : (span {basis i | i. i : d})"
- apply (rule span_setsum[of "{basis i |i. i : d}" "(%b. b /\<^sub>R (2 * real (card d)))" "{basis i |i. i : d}"])
- using finite_substdbasis[of d] apply blast
+ finally show "setsum (op \<bullet> ?a) ?D < 1" by auto
+ next fix i assume "i\<in>Basis" and "i~:d"
+ have "?a : (span d)"
+ apply (rule span_setsum[of d "(%b. b /\<^sub>R (2 * real (card d)))" d])
+ using finite_subset[OF assms(2) finite_Basis]
+ apply blast
proof-
- { fix x assume "(x :: 'a::euclidean_space): {basis i |i. i : d}"
- hence "x : span {basis i |i. i : d}"
- using span_superset[of _ "{basis i |i. i : d}"] by auto
- hence "(x /\<^sub>R (2 * real (card d))) : (span {basis i |i. i : d})"
- using span_mul[of x "{basis i |i. i : d}" "(inverse (real (card d)) / 2)"] by auto
- } thus "\<forall>x\<in>{basis i |i. i \<in> d}. x /\<^sub>R (2 * real (card d)) \<in> span {basis i ::'a |i. i \<in> d}" by auto
+ { fix x assume "(x :: 'a::euclidean_space): d"
+ hence "x : span d"
+ using span_superset[of _ "d"] by auto
+ hence "(x /\<^sub>R (2 * real (card d))) : (span d)"
+ using span_mul[of x "d" "(inverse (real (card d)) / 2)"] by auto
+ } thus "\<forall>x\<in>d. x /\<^sub>R (2 * real (card d)) \<in> span d" by auto
qed
- thus "?a $$ i = 0 " using `i~:d` unfolding span_substd_basis[OF assms(2)] using `i<DIM('a)` by auto
+ thus "?a \<bullet> i = 0 " using `i~:d` unfolding span_substd_basis[OF assms(2)] using `i\<in>Basis` by auto
qed
qed
@@ -4608,14 +4614,14 @@
ultimately have **: "affine hull (convex hull insert 0 B) = affine hull S"
using affine_hull_span_0[of "convex hull insert 0 B"] affine_hull_span_0[of "S"]
assms hull_subset[of S] by auto
-obtain d and f::"'n=>'n" where fd: "card d = card B & linear f & f ` B = {basis i |i. i : (d :: nat set)} &
- f ` span B = {x. ALL i<DIM('n). i ~: d --> x $$ i = (0::real)} & inj_on f (span B)" and d:"d\<subseteq>{..<DIM('n)}"
+obtain d and f::"'n=>'n" where fd: "card d = card B & linear f & f ` B = d &
+ f ` span B = {x. \<forall>i\<in>Basis. i ~: d --> x \<bullet> i = (0::real)} & inj_on f (span B)" and d:"d\<subseteq>Basis"
using basis_to_substdbasis_subspace_isomorphism[of B,OF _ ] B_def by auto
hence "bounded_linear f" using linear_conv_bounded_linear by auto
have "d ~={}" using fd B_def `B ~={}` by auto
-have "(insert 0 {basis i |i. i : d}) = f ` (insert 0 B)" using fd linear_0 by auto
-hence "(convex hull (insert 0 {basis i |i. i : d})) = f ` (convex hull (insert 0 B))"
- using convex_hull_linear_image[of f "(insert 0 {basis i |i. i : d})"]
+have "(insert 0 d) = f ` (insert 0 B)" using fd linear_0 by auto
+hence "(convex hull (insert 0 d)) = f ` (convex hull (insert 0 B))"
+ using convex_hull_linear_image[of f "(insert 0 d)"]
convex_hull_linear_image[of f "(insert 0 B)"] `bounded_linear f` by auto
moreover have "rel_interior (f ` (convex hull insert 0 B)) =
f ` rel_interior (convex hull insert 0 B)"