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':