src/HOL/Probability/Infinite_Product_Measure.thy
changeset 49776 199d1d5bb17e
parent 47762 d31085f07f60
child 49780 92a58f80b20c
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 10 12:12:17 2012 +0200
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 10 12:12:18 2012 +0200
     1.3 @@ -8,31 +8,6 @@
     1.4    imports Probability_Measure Caratheodory
     1.5  begin
     1.6  
     1.7 -lemma (in product_sigma_finite)
     1.8 -  assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
     1.9 -  shows emeasure_fold_integral:
    1.10 -    "emeasure (Pi\<^isub>M (I \<union> J) M) A = (\<integral>\<^isup>+x. emeasure (Pi\<^isub>M J M) (merge I x J -` A \<inter> space (Pi\<^isub>M J M)) \<partial>Pi\<^isub>M I M)" (is ?I)
    1.11 -    and emeasure_fold_measurable:
    1.12 -    "(\<lambda>x. emeasure (Pi\<^isub>M J M) (merge I x J -` A \<inter> space (Pi\<^isub>M J M))) \<in> borel_measurable (Pi\<^isub>M I M)" (is ?B)
    1.13 -proof -
    1.14 -  interpret I: finite_product_sigma_finite M I by default fact
    1.15 -  interpret J: finite_product_sigma_finite M J by default fact
    1.16 -  interpret IJ: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" ..
    1.17 -  have merge: "(\<lambda>(x, y). merge I x J y) -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) \<in> sets (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
    1.18 -    by (intro measurable_sets[OF _ A] measurable_merge assms)
    1.19 -
    1.20 -  show ?I
    1.21 -    apply (subst distr_merge[symmetric, OF IJ])
    1.22 -    apply (subst emeasure_distr[OF measurable_merge[OF IJ(1)] A])
    1.23 -    apply (subst IJ.emeasure_pair_measure_alt[OF merge])
    1.24 -    apply (auto intro!: positive_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
    1.25 -    done
    1.26 -
    1.27 -  show ?B
    1.28 -    using IJ.measurable_emeasure_Pair1[OF merge]
    1.29 -    by (simp add: vimage_compose[symmetric] comp_def space_pair_measure cong: measurable_cong)
    1.30 -qed
    1.31 -
    1.32  lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
    1.33    unfolding restrict_def extensional_def by auto
    1.34