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
```