--- 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. *}
--- 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