--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Aug 24 17:30:25 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Aug 24 09:08:07 2011 -0700
@@ -40,9 +40,6 @@
using assms apply (auto simp add: algebra_simps zero_le_divide_iff)
using add_divide_distrib[of u v "u+v"] by auto
-lemma card_ge1: assumes "d ~= {}" "finite d" shows "card d >= 1"
-by (metis Suc_eq_plus1 assms(1) assms(2) card_eq_0_iff fact_ge_one_nat fact_num_eq_if_nat one_le_mult_iff plus_nat.add_0)
-
lemma inj_on_image_mem_iff: "inj_on f B ==> (A <= B) ==> (f a : f`A) ==> (a : B) ==> (a : A)"
by (blast dest: inj_onD)
@@ -330,8 +327,7 @@
unfolding norm_eq_sqrt_inner by simp
-
-subsection {* Affine set and affine hull.*}
+subsection {* Affine set and affine hull *}
definition
affine :: "'a::real_vector set \<Rightarrow> bool" where
@@ -362,7 +358,7 @@
lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
by (metis affine_affine_hull hull_same)
-subsection {* Some explicit formulations (from Lars Schewe). *}
+subsubsection {* Some explicit formulations (from Lars Schewe) *}
lemma affine: fixes V::"'a::real_vector set"
shows "affine V \<longleftrightarrow> (\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (setsum (\<lambda>x. (u x) *\<^sub>R x)) s \<in> V)"
@@ -462,7 +458,7 @@
thus "\<exists>u. setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" apply(rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
unfolding if_smult scaleR_zero_left and setsum_restrict_set[OF assms, THEN sym] and * by auto qed
-subsection {* Stepping theorems and hence small special cases. *}
+subsubsection {* Stepping theorems and hence small special cases *}
lemma affine_hull_empty[simp]: "affine hull {} = {}"
apply(rule hull_unique) by auto
@@ -556,7 +552,7 @@
using mem_affine_3[of S x y z 1 v "-v"] assms by (simp add: algebra_simps)
-subsection {* Some relations between affine hull and subspaces. *}
+subsubsection {* Some relations between affine hull and subspaces *}
lemma affine_hull_insert_subset_span:
shows "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
@@ -599,7 +595,7 @@
shows "affine hull s = {a + v | v. v \<in> span {x - a | x. x \<in> s - {a}}}"
using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
-subsection{* Parallel Affine Sets *}
+subsubsection {* Parallel affine sets *}
definition affine_parallel :: "'a::real_vector set => 'a::real_vector set => bool"
where "affine_parallel S T = (? a. T = ((%x. a + x) ` S))"
@@ -673,7 +669,7 @@
lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s"
unfolding subspace_def affine_def by auto
-subsection{* Subspace Parallel to an Affine Set *}
+subsubsection {* Subspace parallel to an affine set *}
lemma subspace_affine:
shows "subspace S <-> (affine S & 0 : S)"
@@ -749,7 +745,7 @@
} from this show ?thesis using ex by auto
qed
-subsection {* Cones. *}
+subsection {* Cones *}
definition
cone :: "'a::real_vector set \<Rightarrow> bool" where
@@ -764,7 +760,7 @@
lemma cone_Inter[intro]: "(\<forall>s\<in>f. cone s) \<Longrightarrow> cone(\<Inter> f)"
unfolding cone_def by auto
-subsection {* Conic hull. *}
+subsubsection {* Conic hull *}
lemma cone_cone_hull: "cone (cone hull s)"
unfolding hull_def by auto
@@ -877,7 +873,7 @@
ultimately show ?thesis by blast
qed
-subsection {* Affine dependence and consequential theorems (from Lars Schewe). *}
+subsection {* Affine dependence and consequential theorems (from Lars Schewe) *}
definition
affine_dependent :: "'a::real_vector set \<Rightarrow> bool" where
@@ -921,7 +917,69 @@
thus ?lhs unfolding affine_dependent_explicit using assms by auto
qed
-subsection {* A general lemma. *}
+subsection {* Connectedness of convex sets *}
+
+lemma connected_real_lemma:
+ fixes f :: "real \<Rightarrow> 'a::metric_space"
+ assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2"
+ and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y - x) < d \<longrightarrow> dist(f y) (f x) < e"
+ and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1"
+ and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2"
+ and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)"
+ shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x")
+proof-
+ let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}"
+ have Se: " \<exists>x. x \<in> ?S" apply (rule exI[where x=a]) by (auto simp add: fa)
+ have Sub: "\<exists>y. isUb UNIV ?S y"
+ apply (rule exI[where x= b])
+ using ab fb e12 by (auto simp add: isUb_def setle_def)
+ from reals_complete[OF Se Sub] obtain l where
+ l: "isLub UNIV ?S l"by blast
+ have alb: "a \<le> l" "l \<le> b" using l ab fa fb e12
+ apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
+ by (metis linorder_linear)
+ have ale1: "\<forall>z \<ge> a. z < l \<longrightarrow> f z \<in> e1" using l
+ apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
+ by (metis linorder_linear not_le)
+ have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z - x) < d" by arith
+ have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith
+ have "\<And>d::real. 0 < d \<Longrightarrow> 0 < d/2 \<and> d/2 < d" by simp
+ then have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by blast
+ {assume le2: "f l \<in> e2"
+ from le2 fa fb e12 alb have la: "l \<noteq> a" by metis
+ hence lap: "l - a > 0" using alb by arith
+ from e2[rule_format, OF le2] obtain e where
+ e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis
+ from dst[OF alb e(1)] obtain d where
+ d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
+ let ?d' = "min (d/2) ((l - a)/2)"
+ have "?d' < d \<and> 0 < ?d' \<and> ?d' < l - a" using lap d(1)
+ by (simp add: min_max.less_infI2)
+ then have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" by auto
+ then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis
+ from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e2" by metis
+ from th0[rule_format, of "l - d'"] d' have "f (l - d') \<in> e2" by auto
+ moreover
+ have "f (l - d') \<in> e1" using ale1[rule_format, of "l -d'"] d' by auto
+ ultimately have False using e12 alb d' by auto}
+ moreover
+ {assume le1: "f l \<in> e1"
+ from le1 fa fb e12 alb have lb: "l \<noteq> b" by metis
+ hence blp: "b - l > 0" using alb by arith
+ from e1[rule_format, OF le1] obtain e where
+ e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis
+ from dst[OF alb e(1)] obtain d where
+ d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
+ have "\<And>d::real. 0 < d \<Longrightarrow> d/2 < d \<and> 0 < d/2" by simp
+ then have "\<exists>d'. d' < d \<and> d' >0" using d(1) by blast
+ then obtain d' where d': "d' > 0" "d' < d" by metis
+ from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e1" by auto
+ hence "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto
+ with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" by auto
+ with l d' have False
+ by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) }
+ ultimately show ?thesis using alb by metis
+qed
lemma convex_connected:
fixes s :: "'a::real_normed_vector set"
@@ -957,12 +1015,12 @@
thus ?thesis unfolding connected_def by auto
qed
-subsection {* One rather trivial consequence. *}
+text {* One rather trivial consequence. *}
lemma connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
by(simp add: convex_connected convex_UNIV)
-subsection {* Balls, being convex, are connected. *}
+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}"
@@ -1026,7 +1084,7 @@
shows "connected(cball x e)"
using convex_connected convex_cball by auto
-subsection {* Convex hull. *}
+subsection {* Convex hull *}
lemma convex_convex_hull: "convex(convex hull s)"
unfolding hull_def using convex_Inter[of "{t. convex t \<and> s \<subseteq> t}"]
@@ -1048,7 +1106,7 @@
shows "finite s \<Longrightarrow> bounded(convex hull s)"
using bounded_convex_hull finite_imp_bounded by auto
-subsection {* Convex hull is "preserved" by a linear function. *}
+subsubsection {* Convex hull is "preserved" by a linear function *}
lemma convex_hull_linear_image:
assumes "bounded_linear f"
@@ -1070,7 +1128,7 @@
shows "(f x) \<in> convex hull (f ` s)"
using convex_hull_linear_image[OF assms(1)] assms(2) by auto
-subsection {* Stepping theorems for convex hulls of finite sets. *}
+subsubsection {* Stepping theorems for convex hulls of finite sets *}
lemma convex_hull_empty[simp]: "convex hull {} = {}"
apply(rule hull_unique) by auto
@@ -1133,7 +1191,7 @@
qed
-subsection {* Explicit expression for convex hull. *}
+subsubsection {* Explicit expression for convex hull *}
lemma convex_hull_indexed:
fixes s :: "'a::real_vector set"
@@ -1204,7 +1262,7 @@
using assms and t(1) by auto
qed
-subsection {* Another formulation from Lars Schewe. *}
+subsubsection {* Another formulation from Lars Schewe *}
lemma setsum_constant_scaleR:
fixes y :: "'a::real_vector"
@@ -1268,7 +1326,7 @@
ultimately show ?thesis unfolding set_eq_iff by blast
qed
-subsection {* A stepping theorem for that expansion. *}
+subsubsection {* A stepping theorem for that expansion *}
lemma convex_hull_finite_step:
fixes s :: "'a::real_vector set" assumes "finite s"
@@ -1294,7 +1352,7 @@
ultimately show ?lhs apply(rule_tac x="\<lambda>x. if a = x then v else u x" in exI) unfolding setsum_clauses(2)[OF assms] by auto
qed
-subsection {* Hence some special cases. *}
+subsubsection {* Hence some special cases *}
lemma convex_hull_2:
"convex hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b | u v. 0 \<le> u \<and> 0 \<le> v \<and> u + v = 1}"
@@ -1326,7 +1384,7 @@
show ?thesis unfolding convex_hull_3 apply (auto simp add: *) apply(rule_tac x=v in exI) apply(rule_tac x=w in exI) apply (simp add: algebra_simps)
apply(rule_tac x=u in exI) apply(rule_tac x=v in exI) by (simp add: algebra_simps) qed
-subsection {* Relations among closure notions and corresponding hulls. *}
+subsection {* Relations among closure notions and corresponding hulls *}
lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"
unfolding affine_def convex_def by auto
@@ -2048,7 +2106,7 @@
from this show ?thesis using aff_dim_open[of "interior S"] aff_dim_subset_univ[of S] assms by auto
qed
-subsection{* Relative Interior of a Set *}
+subsection {* Relative interior of a set *}
definition "rel_interior S = {x. ? T. openin (subtopology euclidean (affine hull S)) T & x : T & T <= S}"
@@ -2217,7 +2275,7 @@
by (auto split: split_if_asm)
qed
-subsection "Relative open"
+subsubsection {* Relative open sets *}
definition "rel_open S <-> (rel_interior S) = S"
@@ -2324,7 +2382,7 @@
thus ?thesis using * by auto
qed
-subsection{* Relative interior preserves under linear transformations *}
+subsubsection{* Relative interior preserves under linear transformations *}
lemma rel_interior_translation_aux:
fixes a :: "'n::euclidean_space"
@@ -2832,7 +2890,7 @@
shows "continuous_on t (closest_point s)"
by(metis continuous_at_imp_continuous_on continuous_at_closest_point[OF assms])
-subsection {* Various point-to-set separating/supporting hyperplane theorems. *}
+subsubsection {* Various point-to-set separating/supporting hyperplane theorems. *}
lemma supporting_hyperplane_closed_point:
fixes z :: "'a::{real_inner,heine_borel}"
@@ -2891,7 +2949,7 @@
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
-subsection {* Now set-to-set for closed/compact sets. *}
+subsubsection {* Now set-to-set for closed/compact sets *}
lemma separating_hyperplane_closed_compact:
assumes "convex (s::('a::euclidean_space) set)" "closed s" "convex t" "compact t" "t \<noteq> {}" "s \<inter> t = {}"
@@ -2933,7 +2991,7 @@
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
-subsection {* General case without assuming closure and getting non-strict separation. *}
+subsubsection {* General case without assuming closure and getting non-strict separation *}
lemma separating_hyperplane_set_0:
assumes "convex s" "(0::'a::euclidean_space) \<notin> s"
@@ -2976,7 +3034,7 @@
done
qed
-subsection {* More convexity generalities. *}
+subsection {* More convexity generalities *}
lemma convex_closure:
fixes s :: "'a::real_normed_vector set"
@@ -3088,7 +3146,7 @@
ultimately show ?thesis by blast
qed
-subsection {* Convex set as intersection of halfspaces. *}
+subsection {* Convex set as intersection of halfspaces *}
lemma convex_halfspace_intersection:
fixes s :: "('a::euclidean_space) set"
@@ -3101,7 +3159,7 @@
apply(erule exE)+ apply(erule_tac x="-a" in allE, erule_tac x="-b" in allE) by auto
qed auto
-subsection {* Radon's theorem (from Lars Schewe). *}
+subsection {* Radon's theorem (from Lars Schewe) *}
lemma radon_ex_lemma:
assumes "finite c" "affine_dependent c"
@@ -3170,7 +3228,7 @@
from radon_partition[OF *] guess m .. then guess p ..
thus ?thesis apply(rule_tac that[of p m]) using s by auto qed
-subsection {* Helly's theorem. *}
+subsection {* Helly's theorem *}
lemma helly_induct: fixes f::"('a::euclidean_space) set set"
assumes "card f = n" "n \<ge> DIM('a) + 1"
@@ -3216,7 +3274,7 @@
shows "\<Inter> f \<noteq>{}"
apply(rule helly_induct) using assms by auto
-subsection {* Homeomorphism of all convex compact sets with nonempty interior. *}
+subsection {* Homeomorphism of all convex compact sets with nonempty interior *}
lemma compact_frontier_line_lemma:
fixes s :: "('a::euclidean_space) set"
@@ -3436,7 +3494,7 @@
shows "s homeomorphic t"
using assms by(meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
-subsection {* Epigraphs of convex functions. *}
+subsection {* Epigraphs of convex functions *}
definition "epigraph s (f::_ \<Rightarrow> real) = {xy. fst xy \<in> s \<and> f (fst xy) \<le> snd xy}"
@@ -3460,7 +3518,7 @@
"convex s \<Longrightarrow> convex_on s f \<longleftrightarrow> convex(epigraph s f)"
by(simp add: convex_epigraph)
-subsection {* Use this to derive general bound property of convex function. *}
+subsubsection {* Use this to derive general bound property of convex function *}
lemma convex_on:
assumes "convex s"
@@ -3479,7 +3537,7 @@
apply(rule mult_left_mono)using assms[unfolded convex] by auto
-subsection {* Convexity of general and special intervals. *}
+subsection {* Convexity of general and special intervals *}
lemma convexI: (* TODO: move to Library/Convex.thy *)
assumes "\<And>x y u v. \<lbrakk>x \<in> s; y \<in> s; 0 \<le> u; 0 \<le> v; u + v = 1\<rbrakk> \<Longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s"
@@ -3542,7 +3600,7 @@
"connected s \<longleftrightarrow> convex (s::(real^1) set)"
by(metis is_interval_convex convex_connected is_interval_connected_1)
*)
-subsection {* Another intermediate value theorem formulation. *}
+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"
@@ -3572,7 +3630,7 @@
by(rule ivt_decreasing_component_on_1)
(auto simp: continuous_at_imp_continuous_on)
-subsection {* A bound within a convex hull, and so an interval. *}
+subsection {* A bound within a convex hull, and so an interval *}
lemma convex_on_convex_hull_bound:
assumes "convex_on (convex hull s) f" "\<forall>x\<in>s. f x \<le> b"
@@ -3643,7 +3701,7 @@
unfolding mem_interval apply rule unfolding mem_Collect_eq apply(erule_tac x=i in allE)
by auto qed
-subsection {* And this is a finite set of vertices. *}
+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}"])
@@ -3654,7 +3712,7 @@
apply(rule image_eqI[where x="{i. i<DIM('a) \<and> x$$i = 1}"])
using as apply(subst euclidean_eq) by auto qed auto
-subsection {* Hence any cube (could do any nonempty interval). *}
+text {* Hence any cube (could do any nonempty interval). *}
lemma cube_convex_hull:
assumes "0 < d" obtains s::"('a::ordered_euclidean_space) set" where
@@ -3686,7 +3744,7 @@
obtain s where "finite s" "{0::'a..\<chi>\<chi> i.1} = 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. *}
+subsection {* Bounded convex function on open set is continuous *}
lemma convex_on_bounded_continuous:
fixes s :: "('a::real_normed_vector) set"
@@ -3737,7 +3795,7 @@
qed(insert `0<e`, auto)
qed(insert `0<e` `0<k` `0<B`, auto simp add:field_simps intro!:mult_pos_pos) qed
-subsection {* Upper bound on a ball implies upper and lower bounds. *}
+subsection {* Upper bound on a ball implies upper and lower bounds *}
lemma convex_bounds_lemma:
fixes x :: "'a::real_normed_vector"
@@ -3754,7 +3812,7 @@
hence "dist x y < 0" using False unfolding mem_cball not_le by (auto simp del: dist_not_less_zero)
thus "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>" using zero_le_dist[of x y] by auto qed
-subsection {* Hence a convex function on an open set is continuous. *}
+subsubsection {* Hence a convex function on an open set is continuous *}
lemma convex_on_continuous:
assumes "open (s::('a::ordered_euclidean_space) set)" "convex_on s f"
@@ -3797,7 +3855,7 @@
using `d>0` by auto
qed
-subsection {* Line segments, Starlike Sets, etc.*}
+subsection {* Line segments, Starlike Sets, etc. *}
(* Use the same overloading tricks as for intervals, so that
segment[a,b] is closed and segment(a,b) is open relative to affine hull. *)
@@ -3943,7 +4001,7 @@
"between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}"
unfolding between_mem_segment segment_convex_hull ..
-subsection {* Shrinking towards the interior of a convex set. *}
+subsection {* Shrinking towards the interior of a convex set *}
lemma mem_interior_convex_shrink:
fixes s :: "('a::euclidean_space) set"
@@ -3990,7 +4048,7 @@
thus ?thesis unfolding * apply - apply(rule mem_interior_convex_shrink)
using assms(1,4-5) `y\<in>s` by auto qed
-subsection {* Some obvious but surprisingly hard simplex lemmas. *}
+subsection {* Some obvious but surprisingly hard simplex lemmas *}
lemma simplex:
assumes "finite s" "0 \<notin> s"
@@ -4155,9 +4213,9 @@
unfolding substd_simplex[OF assms] by fastsimp
obtain a where a:"a:d" using `d ~= {}` by auto
let ?d = "(1 - setsum (op $$ x) d) / real (card d)"
- have "card d >= 1" using `d ~={}` card_ge1[of d] using `finite d` by auto
- have "Min ((op $$ x) ` d) > 0" apply(rule Min_grI) using as `card d >= 1` `finite d` by auto
- moreover have "?d > 0" apply(rule divide_pos_pos) using as using `card d >= 1` by(auto simp add: Suc_le_eq)
+ 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)
+ 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
have "x : rel_interior (convex hull (insert 0 ?p))"
@@ -4172,14 +4230,14 @@
by(auto simp add: norm_minus_commute)
thus "y $$ i \<le> x $$ i + ?d" by auto qed
also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat
- using `card d >= 1` by(auto simp add: Suc_le_eq)
+ 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"
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)"] `card d >= 1` `i:d`
- apply auto by (metis Suc_n_not_le_n True card_eq_0_iff finite_imageI)
+ using Min_gr_iff[of "op $$ 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
qed(insert y2, auto)
qed
@@ -4198,7 +4256,7 @@
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
have "finite d" apply(rule finite_subset) using assms(2) by auto
- hence d1: "real(card d) >= 1" using `d ~={}` card_ge1[of d] 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
apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real (card d)) else 0) ?D"])
@@ -4209,7 +4267,7 @@
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 simp add: Suc_le_eq)
+ 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"
@@ -4233,7 +4291,7 @@
qed
qed
-subsection{* Relative Interior of Convex Set *}
+subsection {* Relative interior of convex set *}
lemma rel_interior_convex_nonempty_aux:
fixes S :: "('n::euclidean_space) set"
@@ -4657,7 +4715,7 @@
} ultimately show ?thesis by auto
qed
-subsection{* Relative interior and closure under commom operations *}
+subsubsection {* Relative interior and closure under common operations *}
lemma rel_interior_inter_aux: "Inter {rel_interior S |S. S : I} <= Inter I"
proof-
@@ -5160,7 +5218,7 @@
} from this show ?thesis using h2 by blast
qed
-subsection{* Relative interior of convex cone *}
+subsubsection {* Relative interior of convex cone *}
lemma cone_rel_interior:
fixes S :: "('m::euclidean_space) set"