src/HOL/Probability/Bochner_Integration.thy

     by (cases "\<integral>\<^sup>+ x. ereal (f x) \<partial>M") (auto intro!: integrableI_nn_integral_finite assms)
   from nn_integral_eq_integral[OF this nonneg] show ?thesis
     by simp
 qed
   
+lemma has_bochner_integral_nn_integral:
+  assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
+  assumes "(\<integral>\<^sup>+x. f x \<partial>M) = ereal x"
+  shows "has_bochner_integral M f x"
+  unfolding has_bochner_integral_iff
+  using assms by (auto simp: assms integral_eq_nn_integral intro: integrableI_nn_integral_finite)
+
 lemma integrableI_simple_bochner_integrable:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   shows "simple_bochner_integrable M f \<Longrightarrow> integrable M f"
   by (intro integrableI_sequence[where s="\<lambda>_. f"] borel_measurable_simple_function)
      (auto simp: zero_ereal_def[symmetric] simple_bochner_integrable.simps)