src/HOL/Probability/Lebesgue_Measure.thy
 changeset 41546 2a12c23b7a34 parent 41097 a1abfa4e2b44 child 41654 32fe42892983
```     1.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Jan 14 15:56:42 2011 +0100
1.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Jan 14 15:59:49 2011 +0100
1.3 @@ -626,11 +626,38 @@
1.4    qed
1.5  qed
1.6
1.7 +lemma lebesgue_positive_integral_eq_borel:
1.8 +  "f \<in> borel_measurable borel \<Longrightarrow> lebesgue.positive_integral f = borel.positive_integral f "
1.9 +  by (auto intro!: lebesgue.positive_integral_subalgebra[symmetric]) default
1.10 +
1.11 +lemma lebesgue_integral_eq_borel:
1.12 +  assumes "f \<in> borel_measurable borel"
1.13 +  shows "lebesgue.integrable f = borel.integrable f" (is ?P)
1.14 +    and "lebesgue.integral f = borel.integral f" (is ?I)
1.15 +proof -
1.16 +  have *: "sigma_algebra borel" by default
1.17 +  have "sets borel \<subseteq> sets lebesgue" by auto
1.18 +  from lebesgue.integral_subalgebra[OF assms this _ *]
1.19 +  show ?P ?I by auto
1.20 +qed
1.21 +
1.22 +lemma borel_integral_has_integral:
1.23 +  fixes f::"'a::ordered_euclidean_space => real"
1.24 +  assumes f:"borel.integrable f"
1.25 +  shows "(f has_integral (borel.integral f)) UNIV"
1.26 +proof -
1.27 +  have borel: "f \<in> borel_measurable borel"
1.28 +    using f unfolding borel.integrable_def by auto
1.29 +  from f show ?thesis
1.30 +    using lebesgue_integral_has_integral[of f]
1.31 +    unfolding lebesgue_integral_eq_borel[OF borel] by simp
1.32 +qed
1.33 +
1.34  lemma continuous_on_imp_borel_measurable:
1.35    fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
1.36    assumes "continuous_on UNIV f"
1.37 -  shows "f \<in> borel_measurable lebesgue"
1.38 -  apply(rule lebesgue.borel_measurableI)
1.39 +  shows "f \<in> borel_measurable borel"
1.40 +  apply(rule borel.borel_measurableI)
1.41    using continuous_open_preimage[OF assms] unfolding vimage_def by auto
1.42
1.43  lemma (in measure_space) integral_monotone_convergence_pos':
```