--- a/src/HOL/Analysis/Bochner_Integration.thy Wed May 15 12:47:15 2019 +0100
+++ b/src/HOL/Analysis/Bochner_Integration.thy Wed May 15 14:43:32 2019 +0100
@@ -1932,6 +1932,24 @@
integral\<^sup>L M f \<le> integral\<^sup>L M g"
by (intro integral_mono_AE) auto
+lemma integral_norm_bound_integral:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{banach,second_countable_topology}"
+ assumes "integrable M f" "integrable M g" "\<And>x. x \<in> space M \<Longrightarrow> norm(f x) \<le> g x"
+ shows "norm (\<integral>x. f x \<partial>M) \<le> (\<integral>x. g x \<partial>M)"
+proof -
+ have "norm (\<integral>x. f x \<partial>M) \<le> (\<integral>x. norm (f x) \<partial>M)"
+ by (rule integral_norm_bound)
+ also have "... \<le> (\<integral>x. g x \<partial>M)"
+ using assms integrable_norm integral_mono by blast
+ finally show ?thesis .
+qed
+
+lemma integral_abs_bound_integral:
+ fixes f :: "'a::euclidean_space \<Rightarrow> real"
+ assumes "integrable M f" "integrable M g" "\<And>x. x \<in> space M \<Longrightarrow> \<bar>f x\<bar> \<le> g x"
+ shows "\<bar>\<integral>x. f x \<partial>M\<bar> \<le> (\<integral>x. g x \<partial>M)"
+ by (metis integral_norm_bound_integral assms real_norm_def)
+
text \<open>The next two statements are useful to bound Lebesgue integrals, as they avoid one
integrability assumption. The price to pay is that the upper function has to be nonnegative,
but this is often true and easy to check in computations.\<close>
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed May 15 12:47:15 2019 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed May 15 14:43:32 2019 +0100
@@ -3119,12 +3119,29 @@
using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
qed (use le in \<open>force intro!: always_eventually split: split_indicator\<close>)
+corollary absolutely_integrable_on_const [simp]:
+ fixes c :: "'a::euclidean_space"
+ assumes "S \<in> lmeasurable"
+ shows "(\<lambda>x. c) absolutely_integrable_on S"
+ by (metis (full_types) assms absolutely_integrable_integrable_bound integrable_on_const order_refl)
+
lemma absolutely_integrable_continuous:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
shows "continuous_on (cbox a b) f \<Longrightarrow> f absolutely_integrable_on cbox a b"
using absolutely_integrable_integrable_bound
by (simp add: absolutely_integrable_on_def continuous_on_norm integrable_continuous)
+lemma continous_imp_integrable:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "continuous_on (cbox a b) f"
+ shows "integrable (lebesgue_on (cbox a b)) f"
+proof -
+ have "f absolutely_integrable_on cbox a b"
+ by (simp add: absolutely_integrable_continuous assms)
+ then show ?thesis
+ by (simp add: integrable_restrict_space set_integrable_def)
+qed
+
subsection \<open>Componentwise\<close>
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Wed May 15 12:47:15 2019 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Wed May 15 14:43:32 2019 +0100
@@ -304,15 +304,10 @@
qed (auto simp: Ioc_inj mono_F)
lemma measure_interval_measure_Ioc:
- assumes "a \<le> b"
- assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y"
- assumes right_cont_F : "\<And>a. continuous (at_right a) F"
+ assumes "a \<le> b" and "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y" and "\<And>a. continuous (at_right a) F"
shows "measure (interval_measure F) {a <.. b} = F b - F a"
unfolding measure_def
- apply (subst emeasure_interval_measure_Ioc)
- apply fact+
- apply (simp add: assms)
- done
+ by (simp add: assms emeasure_interval_measure_Ioc)
lemma emeasure_interval_measure_Ioc_eq:
"(\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y) \<Longrightarrow> (\<And>a. continuous (at_right a) F) \<Longrightarrow>
@@ -409,6 +404,11 @@
shows "f \<in> measurable (lebesgue_on S) M \<longleftrightarrow> g \<in> measurable (lebesgue_on S) M"
by (metis (mono_tags, lifting) IntD1 assms measurable_cong_simp space_restrict_space)
+lemma integrable_lebesgue_on_UNIV_eq:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}"
+ shows "integrable (lebesgue_on UNIV) f = integrable lebesgue f"
+ by (auto simp: integrable_restrict_space)
+
text\<^marker>\<open>tag unimportant\<close> \<open>Measurability of continuous functions\<close>
lemma continuous_imp_measurable_on_sets_lebesgue:
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Wed May 15 12:47:15 2019 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Wed May 15 14:43:32 2019 +0100
@@ -956,6 +956,15 @@
lemma ennreal_numeral[simp]: "ennreal (numeral n) = numeral n"
using ennreal_of_nat_eq_real_of_nat[of "numeral n"] by simp
+lemma ennreal_less_numeral_iff [simp]: "ennreal n < numeral w \<longleftrightarrow> n < numeral w"
+ by (metis ennreal_less_iff ennreal_numeral less_le not_less zero_less_numeral)
+
+lemma numeral_less_ennreal_iff [simp]: "numeral w < ennreal n \<longleftrightarrow> numeral w < n"
+ using ennreal_less_iff zero_le_numeral by fastforce
+
+lemma numeral_le_ennreal_iff [simp]: "numeral n \<le> ennreal m \<longleftrightarrow> numeral n \<le> m"
+ by (metis not_le ennreal_less_numeral_iff)
+
lemma min_ennreal: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> min (ennreal x) (ennreal y) = ennreal (min x y)"
by (auto split: split_min)