# HG changeset patch
# User immler
# Date 1395133978 -3600
# Node ID f0d2609c4cdcc85ae43de7e43a9a63ce0f6654b6
# Parent  c4daa97ac57a2b697ecc082fbd279274af7751d0
additional lemmas

diff -r c4daa97ac57a -r f0d2609c4cdc src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 18 10:12:58 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 18 10:12:58 2014 +0100
@@ -5231,6 +5231,14 @@
   apply auto
   done
 
+lemma integral_component_lbound_real:
+  assumes "f integrable_on {a ::real .. b}"
+    and "\<forall>x\<in>{a .. b}. B \<le> f(x)\<bullet>k"
+    and "k \<in> Basis"
+  shows "B * content {a .. b} \<le> (integral {a .. b} f)\<bullet>k"
+  using assms
+  by (metis box_real(2) integral_component_lbound)
+
 lemma integral_component_ubound:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "f integrable_on cbox a b"
@@ -5243,6 +5251,14 @@
   apply auto
   done
 
+lemma integral_component_ubound_real:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "f integrable_on {a .. b}"
+    and "\<forall>x\<in>{a .. b}. f x\<bullet>k \<le> B"
+    and "k \<in> Basis"
+  shows "(integral {a .. b} f)\<bullet>k \<le> B * content {a .. b}"
+  using assms
+  by (metis box_real(2) integral_component_ubound)
 
 subsection {* Uniform limit of integrable functions is integrable. *}
 
diff -r c4daa97ac57a -r f0d2609c4cdc src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Tue Mar 18 10:12:58 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Tue Mar 18 10:12:58 2014 +0100
@@ -205,6 +205,12 @@
   using bounded_cbox[of a b]
   by (metis interval_cbox)
 
+lemma convex_closed_interval:
+  fixes a :: "'a::ordered_euclidean_space"
+  shows "convex {a .. b}"
+  using convex_box[of a b]
+  by (metis interval_cbox)
+
 lemma image_affinity_interval: fixes m::real
   fixes a b c :: "'a::ordered_euclidean_space"
   shows "(\<lambda>x. m *\<^sub>R x + c) ` {a..b} =
@@ -223,6 +229,11 @@
   "is_interval {a .. (b::'a::ordered_euclidean_space)}"
   by (metis cbox_interval is_interval_cbox)
 
+lemma compact_interval:
+  fixes a b::"'a::ordered_euclidean_space"
+  shows "compact {a .. b}"
+  by (metis compact_cbox interval_cbox)
+
 no_notation
   eucl_less (infix "<e" 50)
 
@@ -250,6 +261,16 @@
   using integrable_on_subcbox[of f s a b] assms
   by (simp add: cbox_interval)
 
+lemma
+  fixes a b::"'a::ordered_euclidean_space"
+  shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)"
+    and bdd_below_cbox[intro, simp]: "bdd_below (cbox a b)"
+    and bdd_above_box[intro, simp]: "bdd_above (box a b)"
+    and bdd_below_box[intro, simp]: "bdd_below (box a b)"
+  unfolding atomize_conj
+  by (metis bdd_above_Icc bdd_above_mono bdd_below_Icc bdd_below_mono bounded_box
+    bounded_subset_cbox interval_cbox)
+
 instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
 begin