--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Aug 23 15:46:53 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Aug 23 16:17:22 2011 -0700
@@ -921,7 +921,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"
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Aug 23 15:46:53 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Aug 23 16:17:22 2011 -0700
@@ -20,72 +20,6 @@
notation inner (infix "\<bullet>" 70)
-subsection {* A connectedness or intermediate value lemma with several applications. *}
-
-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
-
-text{* One immediately useful corollary is the existence of square roots! --- Should help to get rid of all the development of square-root for reals as a special case *}
-
lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)"
proof-
have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith