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