author immler Tue, 18 Mar 2014 10:12:58 +0100 changeset 56190 f0d2609c4cdc parent 56189 c4daa97ac57a child 56191 159b0c88b4a4
--- 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