5 header {*Infinite Product Measure*} |
5 header {*Infinite Product Measure*} |
6 |
6 |
7 theory Infinite_Product_Measure |
7 theory Infinite_Product_Measure |
8 imports Probability_Measure Caratheodory |
8 imports Probability_Measure Caratheodory |
9 begin |
9 begin |
10 |
|
11 lemma (in product_sigma_finite) |
|
12 assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)" |
|
13 shows emeasure_fold_integral: |
|
14 "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) |
|
15 and emeasure_fold_measurable: |
|
16 "(\<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) |
|
17 proof - |
|
18 interpret I: finite_product_sigma_finite M I by default fact |
|
19 interpret J: finite_product_sigma_finite M J by default fact |
|
20 interpret IJ: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" .. |
|
21 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)" |
|
22 by (intro measurable_sets[OF _ A] measurable_merge assms) |
|
23 |
|
24 show ?I |
|
25 apply (subst distr_merge[symmetric, OF IJ]) |
|
26 apply (subst emeasure_distr[OF measurable_merge[OF IJ(1)] A]) |
|
27 apply (subst IJ.emeasure_pair_measure_alt[OF merge]) |
|
28 apply (auto intro!: positive_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure) |
|
29 done |
|
30 |
|
31 show ?B |
|
32 using IJ.measurable_emeasure_Pair1[OF merge] |
|
33 by (simp add: vimage_compose[symmetric] comp_def space_pair_measure cong: measurable_cong) |
|
34 qed |
|
35 |
10 |
36 lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B" |
11 lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B" |
37 unfolding restrict_def extensional_def by auto |
12 unfolding restrict_def extensional_def by auto |
38 |
13 |
39 lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)" |
14 lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)" |