# HG changeset patch
# User huffman
# Date 1272206517 25200
# Node ID fd98d5da1268580924b805e96a1d1eb4ead39fe9
# Parent  7808fbc9c3b4b2f2a44f7cbf5d7f9ad211a63495
add lemmas convex_real_interval and convex_box

diff -r 7808fbc9c3b4 -r fd98d5da1268 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Apr 24 21:29:22 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Apr 25 07:41:57 2010 -0700
@@ -401,9 +401,38 @@
 lemma convex_halfspace_gt: "convex {x. inner a x > b}"
    using convex_halfspace_lt[of "-a" "-b"] by auto
 
+lemma convex_real_interval:
+  fixes a b :: "real"
+  shows "convex {a..}" and "convex {..b}"
+  and "convex {a<..}" and "convex {..<b}"
+  and "convex {a..b}" and "convex {a<..b}"
+  and "convex {a..<b}" and "convex {a<..<b}"
+proof -
+  have "{a..} = {x. a \<le> inner 1 x}" by auto
+  thus 1: "convex {a..}" by (simp only: convex_halfspace_ge)
+  have "{..b} = {x. inner 1 x \<le> b}" by auto
+  thus 2: "convex {..b}" by (simp only: convex_halfspace_le)
+  have "{a<..} = {x. a < inner 1 x}" by auto
+  thus 3: "convex {a<..}" by (simp only: convex_halfspace_gt)
+  have "{..<b} = {x. inner 1 x < b}" by auto
+  thus 4: "convex {..<b}" by (simp only: convex_halfspace_lt)
+  have "{a..b} = {a..} \<inter> {..b}" by auto
+  thus "convex {a..b}" by (simp only: convex_Int 1 2)
+  have "{a<..b} = {a<..} \<inter> {..b}" by auto
+  thus "convex {a<..b}" by (simp only: convex_Int 3 2)
+  have "{a..<b} = {a..} \<inter> {..<b}" by auto
+  thus "convex {a..<b}" by (simp only: convex_Int 1 4)
+  have "{a<..<b} = {a<..} \<inter> {..<b}" by auto
+  thus "convex {a<..<b}" by (simp only: convex_Int 3 4)
+qed
+
+lemma convex_box:
+  assumes "\<And>i. convex {x. P i x}"
+  shows "convex {x. \<forall>i. P i (x$i)}"
+using assms unfolding convex_def by auto
+
 lemma convex_positive_orthant: "convex {x::real^'n. (\<forall>i. 0 \<le> x$i)}"
-  unfolding convex_def apply auto apply(erule_tac x=i in allE)+
-  apply(rule add_nonneg_nonneg) by(auto simp add: mult_nonneg_nonneg)
+by (rule convex_box, simp add: atLeast_def [symmetric] convex_real_interval)
 
 subsection {* Explicit expressions for convexity in terms of arbitrary sums. *}