summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Infinite_Product_Measure.thy

changeset 42166 | efd229daeb2c |

parent 42148 | d596e7bb251f |

child 42257 | 08d717c82828 |

1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Mar 30 17:54:01 2011 +0200 1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Mar 30 17:54:10 2011 +0200 1.3 @@ -750,4 +750,38 @@ 1.4 with \<mu>G_eq[OF assms] infprod_spec show ?thesis by auto 1.5 qed 1.6 1.7 +sublocale product_prob_space \<subseteq> prob_space "Pi\<^isub>P I M" 1.8 +proof 1.9 + obtain i where "i \<in> I" using I_not_empty by auto 1.10 + interpret i: finite_product_sigma_finite M "{i}" by default auto 1.11 + let ?X = "\<Pi>\<^isub>E i\<in>{i}. space (M i)" 1.12 + have "?X \<in> sets (Pi\<^isub>M {i} M)" 1.13 + by auto 1.14 + from measure_infprod_emb[OF _ _ _ this] `i \<in> I` 1.15 + have "measure (Pi\<^isub>P I M) (emb I {i} ?X) = measure (M i) (space (M i))" 1.16 + by (simp add: i.measure_times) 1.17 + also have "emb I {i} ?X = space (Pi\<^isub>P I M)" 1.18 + using `i \<in> I` by (auto simp: emb_def infprod_algebra_def generator_def) 1.19 + finally show "measure (Pi\<^isub>P I M) (space (Pi\<^isub>P I M)) = 1" 1.20 + using M.measure_space_1 by simp 1.21 +qed 1.22 + 1.23 +lemma (in product_prob_space) measurable_component: 1.24 + assumes "i \<in> I" 1.25 + shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>P I M) (M i)" 1.26 +proof (unfold measurable_def, safe) 1.27 + fix x assume "x \<in> space (Pi\<^isub>P I M)" 1.28 + then show "x i \<in> space (M i)" 1.29 + using `i \<in> I` by (auto simp: infprod_algebra_def generator_def) 1.30 +next 1.31 + fix A assume "A \<in> sets (M i)" 1.32 + with `i \<in> I` have 1.33 + "(\<Pi>\<^isub>E x \<in> {i}. A) \<in> sets (Pi\<^isub>M {i} M)" 1.34 + "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M) = emb I {i} (\<Pi>\<^isub>E x \<in> {i}. A)" 1.35 + by (auto simp: infprod_algebra_def generator_def emb_def) 1.36 + from generatorI[OF _ _ _ this] `i \<in> I` 1.37 + show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M) \<in> sets (Pi\<^isub>P I M)" 1.38 + unfolding infprod_algebra_def by auto 1.39 +qed 1.40 + 1.41 end 1.42 \ No newline at end of file