--- a/src/HOL/Analysis/Bochner_Integration.thy Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Thu Aug 15 16:11:56 2019 +0100
@@ -1581,12 +1581,17 @@
end
-lemma integrable_mult_left_iff:
+lemma integrable_mult_left_iff [simp]:
fixes f :: "'a \<Rightarrow> real"
shows "integrable M (\<lambda>x. c * f x) \<longleftrightarrow> c = 0 \<or> integrable M f"
using integrable_mult_left[of c M f] integrable_mult_left[of "1 / c" M "\<lambda>x. c * f x"]
by (cases "c = 0") auto
+lemma integrable_mult_right_iff [simp]:
+ fixes f :: "'a \<Rightarrow> real"
+ shows "integrable M (\<lambda>x. f x * c) \<longleftrightarrow> c = 0 \<or> integrable M f"
+ using integrable_mult_left_iff [of M c f] by (simp add: mult.commute)
+
lemma integrableI_nn_integral_finite:
assumes [measurable]: "f \<in> borel_measurable M"
and nonneg: "AE x in M. 0 \<le> f x"
@@ -2939,7 +2944,7 @@
have "(\<integral>\<^sup>+ y. ennreal (norm (s i (x, y))) \<partial>M) \<le> (\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M)"
using x s by (intro nn_integral_mono) auto
also have "(\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M) < \<infinity>"
- using int_2f by (simp add: integrable_iff_bounded)
+ using int_2f unfolding integrable_iff_bounded by simp
finally show "(\<integral>\<^sup>+ xa. ennreal (norm (s i (x, xa))) \<partial>M) < \<infinity>" .
qed
then have "integral\<^sup>L M (\<lambda>y. s i (x, y)) = simple_bochner_integral M (\<lambda>y. s i (x, y))"