prove measurable_into_infprod_algebra and measure_infprod
authorhoelzl
Tue Apr 05 19:55:04 2011 +0200 (2011-04-05)
changeset 4225708d717c82828
parent 42256 461624ffd382
child 42259 5ff3a11e18ca
prove measurable_into_infprod_algebra and measure_infprod
src/HOL/Probability/Infinite_Product_Measure.thy
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Apr 05 17:10:51 2011 +0200
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Apr 05 19:55:04 2011 +0200
     1.3 @@ -319,7 +319,7 @@
     1.4  translations
     1.5    "PIP x:I. M" == "CONST Pi\<^isub>P I (%x. M)"
     1.6  
     1.7 -sublocale product_prob_space \<subseteq> G: algebra generator
     1.8 +sublocale product_prob_space \<subseteq> G!: algebra generator
     1.9  proof
    1.10    let ?G = generator
    1.11    show "sets ?G \<subseteq> Pow (space ?G)"
    1.12 @@ -738,19 +738,19 @@
    1.13      done
    1.14  qed
    1.15  
    1.16 -sublocale product_prob_space \<subseteq> measure_space "Pi\<^isub>P I M"
    1.17 +sublocale product_prob_space \<subseteq> P: measure_space "Pi\<^isub>P I M"
    1.18    using infprod_spec by auto
    1.19  
    1.20  lemma (in product_prob_space) measure_infprod_emb:
    1.21    assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)"
    1.22 -  shows "measure (Pi\<^isub>P I M) (emb I J X) = measure (Pi\<^isub>M J M) X"
    1.23 +  shows "\<mu> (emb I J X) = measure (Pi\<^isub>M J M) X"
    1.24  proof -
    1.25    have "emb I J X \<in> sets generator"
    1.26      using assms by (rule generatorI')
    1.27    with \<mu>G_eq[OF assms] infprod_spec show ?thesis by auto
    1.28  qed
    1.29  
    1.30 -sublocale product_prob_space \<subseteq> prob_space "Pi\<^isub>P I M"
    1.31 +sublocale product_prob_space \<subseteq> P: prob_space "Pi\<^isub>P I M"
    1.32  proof
    1.33    obtain i where "i \<in> I" using I_not_empty by auto
    1.34    interpret i: finite_product_sigma_finite M "{i}" by default auto
    1.35 @@ -758,11 +758,11 @@
    1.36    have "?X \<in> sets (Pi\<^isub>M {i} M)"
    1.37      by auto
    1.38    from measure_infprod_emb[OF _ _ _ this] `i \<in> I`
    1.39 -  have "measure (Pi\<^isub>P I M) (emb I {i} ?X) = measure (M i) (space (M i))"
    1.40 +  have "\<mu> (emb I {i} ?X) = measure (M i) (space (M i))"
    1.41      by (simp add: i.measure_times)
    1.42    also have "emb I {i} ?X = space (Pi\<^isub>P I M)"
    1.43      using `i \<in> I` by (auto simp: emb_def infprod_algebra_def generator_def)
    1.44 -  finally show "measure (Pi\<^isub>P I M) (space (Pi\<^isub>P I M)) = 1"
    1.45 +  finally show "\<mu> (space (Pi\<^isub>P I M)) = 1"
    1.46      using M.measure_space_1 by simp
    1.47  qed
    1.48  
    1.49 @@ -784,4 +784,199 @@
    1.50      unfolding infprod_algebra_def by auto
    1.51  qed
    1.52  
    1.53 +lemma (in product_prob_space) emb_in_infprod_algebra[intro]:
    1.54 +  fixes J assumes J: "finite J" "J \<subseteq> I" and X: "X \<in> sets (Pi\<^isub>M J M)"
    1.55 +  shows "emb I J X \<in> sets (\<Pi>\<^isub>P i\<in>I. M i)"
    1.56 +proof cases
    1.57 +  assume "J = {}"
    1.58 +  with X have "emb I J X = space (\<Pi>\<^isub>P i\<in>I. M i) \<or> emb I J X = {}"
    1.59 +    by (auto simp: emb_def infprod_algebra_def generator_def
    1.60 +                   product_algebra_def product_algebra_generator_def image_constant sigma_def)
    1.61 +  then show ?thesis by auto
    1.62 +next
    1.63 +  assume "J \<noteq> {}"
    1.64 +  show ?thesis unfolding infprod_algebra_def
    1.65 +    by simp (intro in_sigma generatorI'  `J \<noteq> {}` J X)
    1.66 +qed
    1.67 +
    1.68 +lemma (in product_prob_space) finite_measure_infprod_emb:
    1.69 +  assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)"
    1.70 +  shows "\<mu>' (emb I J X) = finite_measure.\<mu>' (Pi\<^isub>M J M) X"
    1.71 +proof -
    1.72 +  interpret J: finite_product_prob_space M J by default fact+
    1.73 +  from assms have "emb I J X \<in> sets (Pi\<^isub>P I M)" by auto
    1.74 +  with assms show "\<mu>' (emb I J X) = J.\<mu>' X"
    1.75 +    unfolding \<mu>'_def J.\<mu>'_def
    1.76 +    unfolding measure_infprod_emb[OF assms]
    1.77 +    by auto
    1.78 +qed
    1.79 +
    1.80 +lemma (in finite_product_prob_space) finite_measure_times:
    1.81 +  assumes "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)"
    1.82 +  shows "\<mu>' (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu>' i (A i))"
    1.83 +  using assms
    1.84 +  unfolding \<mu>'_def M.\<mu>'_def
    1.85 +  by (subst measure_times[OF assms])
    1.86 +     (auto simp: finite_measure_eq M.finite_measure_eq setprod_extreal)
    1.87 +
    1.88 +lemma (in product_prob_space) finite_measure_infprod_emb_Pi:
    1.89 +  assumes J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> X j \<in> sets (M j)"
    1.90 +  shows "\<mu>' (emb I J (Pi\<^isub>E J X)) = (\<Prod>j\<in>J. M.\<mu>' j (X j))"
    1.91 +proof cases
    1.92 +  assume "J = {}"
    1.93 +  then have "emb I J (Pi\<^isub>E J X) = space infprod_algebra"
    1.94 +    by (auto simp: infprod_algebra_def generator_def sigma_def emb_def)
    1.95 +  then show ?thesis using `J = {}` prob_space by simp
    1.96 +next
    1.97 +  assume "J \<noteq> {}"
    1.98 +  interpret J: finite_product_prob_space M J by default fact+
    1.99 +  have "(\<Prod>i\<in>J. M.\<mu>' i (X i)) = J.\<mu>' (Pi\<^isub>E J X)"
   1.100 +    using J `J \<noteq> {}` by (subst J.finite_measure_times) auto
   1.101 +  also have "\<dots> = \<mu>' (emb I J (Pi\<^isub>E J X))"
   1.102 +    using J `J \<noteq> {}` by (intro finite_measure_infprod_emb[symmetric]) auto
   1.103 +  finally show ?thesis by simp
   1.104 +qed
   1.105 +
   1.106 +lemma sigma_sets_mono: assumes "A \<subseteq> sigma_sets X B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
   1.107 +proof
   1.108 +  fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
   1.109 +    by induct (insert `A \<subseteq> sigma_sets X B`, auto intro: sigma_sets.intros)
   1.110 +qed
   1.111 +
   1.112 +lemma sigma_sets_mono': assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
   1.113 +proof
   1.114 +  fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
   1.115 +    by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros)
   1.116 +qed
   1.117 +
   1.118 +lemma sigma_sets_subseteq: "A \<subseteq> sigma_sets X A"
   1.119 +  by (auto intro: sigma_sets.Basic)
   1.120 +
   1.121 +lemma (in product_prob_space) infprod_algebra_alt:
   1.122 +  "Pi\<^isub>P I M = sigma \<lparr> space = space (Pi\<^isub>P I M),
   1.123 +    sets = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i))),
   1.124 +    measure = measure (Pi\<^isub>P I M) \<rparr>"
   1.125 +  (is "_ = sigma \<lparr> space = ?O, sets = ?M, measure = ?m \<rparr>")
   1.126 +proof (rule measure_space.equality)
   1.127 +  let ?G = "\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^isub>M J M)"
   1.128 +  have "sigma_sets ?O ?M = sigma_sets ?O ?G"
   1.129 +  proof (intro equalityI sigma_sets_mono UN_least)
   1.130 +    fix J assume J: "J \<in> {J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}"
   1.131 +    have "emb I J ` Pi\<^isub>E J ` (\<Pi> i\<in>J. sets (M i)) \<subseteq> emb I J ` sets (Pi\<^isub>M J M)" by auto
   1.132 +    also have "\<dots> \<subseteq> ?G" using J by (rule UN_upper)
   1.133 +    also have "\<dots> \<subseteq> sigma_sets ?O ?G" by (rule sigma_sets_subseteq)
   1.134 +    finally show "emb I J ` Pi\<^isub>E J ` (\<Pi> i\<in>J. sets (M i)) \<subseteq> sigma_sets ?O ?G" .
   1.135 +    have "emb I J ` sets (Pi\<^isub>M J M) = emb I J ` sigma_sets (space (Pi\<^isub>M J M)) (Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
   1.136 +      by (simp add: sets_sigma product_algebra_generator_def product_algebra_def)
   1.137 +    also have "\<dots> = sigma_sets (space (Pi\<^isub>M I M)) (emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
   1.138 +      using J M.sets_into_space
   1.139 +      by (auto simp: emb_def_raw intro!: sigma_sets_vimage[symmetric]) blast
   1.140 +    also have "\<dots> \<subseteq> sigma_sets (space (Pi\<^isub>M I M)) ?M"
   1.141 +      using J by (intro sigma_sets_mono') auto
   1.142 +    finally show "emb I J ` sets (Pi\<^isub>M J M) \<subseteq> sigma_sets ?O ?M"
   1.143 +      by (simp add: infprod_algebra_def generator_def)
   1.144 +  qed
   1.145 +  then show "sets (Pi\<^isub>P I M) = sets (sigma \<lparr> space = ?O, sets = ?M, measure = ?m \<rparr>)"
   1.146 +    by (simp_all add: infprod_algebra_def generator_def sets_sigma)
   1.147 +qed simp_all
   1.148 +
   1.149 +lemma (in product_prob_space) infprod_algebra_alt2:
   1.150 +  "Pi\<^isub>P I M = sigma \<lparr> space = space (Pi\<^isub>P I M),
   1.151 +    sets = (\<Union>i\<in>I. (\<lambda>A. (\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M)) ` sets (M i)),
   1.152 +    measure = measure (Pi\<^isub>P I M) \<rparr>"
   1.153 +  (is "_ = ?S")
   1.154 +proof (rule measure_space.equality)
   1.155 +  let "sigma \<lparr> space = ?O, sets = ?A, \<dots> = _ \<rparr>" = ?S
   1.156 +  let ?G = "(\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
   1.157 +  have "sets (Pi\<^isub>P I M) = sigma_sets ?O ?G"
   1.158 +    by (subst infprod_algebra_alt) (simp add: sets_sigma)
   1.159 +  also have "\<dots> = sigma_sets ?O ?A"
   1.160 +  proof (intro equalityI sigma_sets_mono subsetI)
   1.161 +    interpret A: sigma_algebra ?S
   1.162 +      by (rule sigma_algebra_sigma) auto
   1.163 +    fix A assume "A \<in> ?G"
   1.164 +    then obtain J B where "finite J" "J \<noteq> {}" "J \<subseteq> I" "A = emb I J (Pi\<^isub>E J B)"
   1.165 +        and B: "\<And>i. i \<in> J \<Longrightarrow> B i \<in> sets (M i)"
   1.166 +      by auto
   1.167 +    then have A: "A = (\<Inter>j\<in>J. (\<lambda>x. x j) -` (B j) \<inter> space (Pi\<^isub>P I M))"
   1.168 +      by (auto simp: emb_def infprod_algebra_def generator_def Pi_iff)
   1.169 +    { fix j assume "j\<in>J"
   1.170 +      with `J \<subseteq> I` have "j \<in> I" by auto
   1.171 +      with `j \<in> J` B have "(\<lambda>x. x j) -` (B j) \<inter> space (Pi\<^isub>P I M) \<in> sets ?S"
   1.172 +        by (auto simp: sets_sigma intro: sigma_sets.Basic) }
   1.173 +    with `finite J` `J \<noteq> {}` have "A \<in> sets ?S"
   1.174 +      unfolding A by (intro A.finite_INT) auto
   1.175 +    then show "A \<in> sigma_sets ?O ?A" by (simp add: sets_sigma)
   1.176 +  next
   1.177 +    fix A assume "A \<in> ?A"
   1.178 +    then obtain i B where i: "i \<in> I" "B \<in> sets (M i)"
   1.179 +        and "A = (\<lambda>x. x i) -` B \<inter> space (Pi\<^isub>P I M)"
   1.180 +      by auto
   1.181 +    then have "A = emb I {i} (Pi\<^isub>E {i} (\<lambda>_. B))"
   1.182 +      by (auto simp: emb_def infprod_algebra_def generator_def Pi_iff)
   1.183 +    with i show "A \<in> sigma_sets ?O ?G"
   1.184 +      by (intro sigma_sets.Basic UN_I[where a="{i}"]) auto
   1.185 +  qed
   1.186 +  finally show "sets (Pi\<^isub>P I M) = sets ?S"
   1.187 +    by (simp add: sets_sigma)
   1.188 +qed simp_all
   1.189 +
   1.190 +lemma (in product_prob_space) measurable_into_infprod_algebra:
   1.191 +  assumes "sigma_algebra N"
   1.192 +  assumes f: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. f x i) \<in> measurable N (M i)"
   1.193 +  assumes ext: "\<And>x. x \<in> space N \<Longrightarrow> f x \<in> extensional I"
   1.194 +  shows "f \<in> measurable N (Pi\<^isub>P I M)"
   1.195 +proof -
   1.196 +  interpret N: sigma_algebra N by fact
   1.197 +  have f_in: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. f x i) \<in> space N \<rightarrow> space (M i)"
   1.198 +    using f by (auto simp: measurable_def)
   1.199 +  { fix i A assume i: "i \<in> I" "A \<in> sets (M i)"
   1.200 +    then have "f -` (\<lambda>x. x i) -` A \<inter> f -` space infprod_algebra \<inter> space N = (\<lambda>x. f x i) -` A \<inter> space N"
   1.201 +      using f_in ext by (auto simp: infprod_algebra_def generator_def)
   1.202 +    also have "\<dots> \<in> sets N"
   1.203 +      by (rule measurable_sets f i)+
   1.204 +    finally have "f -` (\<lambda>x. x i) -` A \<inter> f -` space infprod_algebra \<inter> space N \<in> sets N" . }
   1.205 +  with f_in ext show ?thesis
   1.206 +    by (subst infprod_algebra_alt2)
   1.207 +       (auto intro!: N.measurable_sigma simp: Pi_iff infprod_algebra_def generator_def)
   1.208 +qed
   1.209 +
   1.210 +subsection {* Sequence space *}
   1.211 +
   1.212 +locale sequence_space = product_prob_space M "UNIV :: nat set" for M
   1.213 +
   1.214 +lemma (in sequence_space) infprod_in_sets[intro]:
   1.215 +  fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)"
   1.216 +  shows "Pi UNIV E \<in> sets (Pi\<^isub>P UNIV M)"
   1.217 +proof -
   1.218 +  have "Pi UNIV E = (\<Inter>i. emb UNIV {..i} (\<Pi>\<^isub>E j\<in>{..i}. E j))"
   1.219 +    using E E[THEN M.sets_into_space]
   1.220 +    by (auto simp: emb_def Pi_iff extensional_def) blast
   1.221 +  with E show ?thesis
   1.222 +    by (auto intro: emb_in_infprod_algebra)
   1.223 +qed
   1.224 +
   1.225 +lemma (in sequence_space) measure_infprod:
   1.226 +  fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)"
   1.227 +  shows "(\<lambda>n. \<Prod>i\<le>n. M.\<mu>' i (E i)) ----> \<mu>' (Pi UNIV E)"
   1.228 +proof -
   1.229 +  let "?E n" = "emb UNIV {..n} (Pi\<^isub>E {.. n} E)"
   1.230 +  { fix n :: nat
   1.231 +    interpret n: finite_product_prob_space M "{..n}" by default auto
   1.232 +    have "(\<Prod>i\<le>n. M.\<mu>' i (E i)) = n.\<mu>' (Pi\<^isub>E {.. n} E)"
   1.233 +      using E by (subst n.finite_measure_times) auto
   1.234 +    also have "\<dots> = \<mu>' (?E n)"
   1.235 +      using E by (intro finite_measure_infprod_emb[symmetric]) auto
   1.236 +    finally have "(\<Prod>i\<le>n. M.\<mu>' i (E i)) = \<mu>' (?E n)" . }
   1.237 +  moreover have "Pi UNIV E = (\<Inter>n. ?E n)"
   1.238 +    using E E[THEN M.sets_into_space]
   1.239 +    by (auto simp: emb_def extensional_def Pi_iff) blast
   1.240 +  moreover have "range ?E \<subseteq> sets (Pi\<^isub>P UNIV M)"
   1.241 +    using E by auto
   1.242 +  moreover have "decseq ?E"
   1.243 +    by (auto simp: emb_def Pi_iff decseq_def)
   1.244 +  ultimately show ?thesis
   1.245 +    by (simp add: finite_continuity_from_above)
   1.246 +qed
   1.247 +
   1.248  end
   1.249 \ No newline at end of file