summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | hoelzl |

Mon, 06 Oct 2014 16:27:31 +0200 | |

changeset 58588 | 93d87fd1583d |

parent 58587 | 5484f6079bcd |

child 58594 | 72e2f0e7e344 |

add measure space for (coinductive) streams

--- a/src/HOL/Probability/Probability.thy Mon Oct 06 16:27:07 2014 +0200 +++ b/src/HOL/Probability/Probability.thy Mon Oct 06 16:27:31 2014 +0200 @@ -2,12 +2,11 @@ imports Discrete_Topology Complete_Measure - Probability_Measure - Infinite_Product_Measure Projective_Limit Independent_Family Distributions Probability_Mass_Function + Stream_Space begin end

--- a/src/HOL/Probability/Sigma_Algebra.thy Mon Oct 06 16:27:07 2014 +0200 +++ b/src/HOL/Probability/Sigma_Algebra.thy Mon Oct 06 16:27:31 2014 +0200 @@ -2214,122 +2214,101 @@ using emeasure_extend_measure[OF M _ _ ms(2,3), of "(i,j)"] eq ms(1) `I i j` by (auto simp: subset_eq) -subsubsection {* Sigma algebra generated by function preimages *} +subsubsection {* Supremum of a set of \sigma-algebras *} + +definition "Sup_sigma M = sigma (\<Union>x\<in>M. space x) (\<Union>x\<in>M. sets x)" + +syntax + "_SUP_sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>\<^sub>\<sigma> _\<in>_./ _)" [0, 0, 10] 10) -definition - "vimage_algebra M S X = sigma S ((\<lambda>A. X -` A \<inter> S) ` sets M)" +translations + "\<Squnion>\<^sub>\<sigma> x\<in>A. B" == "CONST Sup_sigma ((\<lambda>x. B) ` A)" + +lemma space_Sup_sigma: "space (Sup_sigma M) = (\<Union>x\<in>M. space x)" + unfolding Sup_sigma_def by (rule space_measure_of) (auto dest: sets.sets_into_space) + +lemma sets_Sup_sigma: "sets (Sup_sigma M) = sigma_sets (\<Union>x\<in>M. space x) (\<Union>x\<in>M. sets x)" + unfolding Sup_sigma_def by (rule sets_measure_of) (auto dest: sets.sets_into_space) + +lemma in_Sup_sigma: "m \<in> M \<Longrightarrow> A \<in> sets m \<Longrightarrow> A \<in> sets (Sup_sigma M)" + unfolding sets_Sup_sigma by auto -lemma sigma_algebra_preimages: - fixes f :: "'x \<Rightarrow> 'a" - assumes "f \<in> S \<rightarrow> space M" - shows "sigma_algebra S ((\<lambda>A. f -` A \<inter> S) ` sets M)" - (is "sigma_algebra _ (?F ` sets M)") -proof (simp add: sigma_algebra_iff2, safe) - show "{} \<in> ?F ` sets M" by blast -next - fix A assume "A \<in> sets M" - moreover have "S - ?F A = ?F (space M - A)" +lemma sets_Sup_in_sets: + assumes "M \<noteq> {}" + assumes "\<And>m. m \<in> M \<Longrightarrow> space m = space N" + assumes "\<And>m. m \<in> M \<Longrightarrow> sets m \<subseteq> sets N" + shows "sets (Sup_sigma M) \<subseteq> sets N" +proof - + have *: "UNION M space = space N" using assms by auto - ultimately show "S - ?F A \<in> ?F ` sets M" - by blast -next - fix A :: "nat \<Rightarrow> 'x set" assume *: "range A \<subseteq> ?F ` M" - have "\<forall>i. \<exists>b. b \<in> M \<and> A i = ?F b" - proof safe - fix i - have "A i \<in> ?F ` M" using * by auto - then show "\<exists>b. b \<in> M \<and> A i = ?F b" by auto - qed - from choice[OF this] obtain b where b: "range b \<subseteq> M" "\<And>i. A i = ?F (b i)" - by auto - then have "(\<Union>i. A i) = ?F (\<Union>i. b i)" by auto - then show "(\<Union>i. A i) \<in> ?F ` M" using b(1) by blast + show ?thesis + unfolding sets_Sup_sigma * using assms by (auto intro!: sets.sigma_sets_subset) +qed + +lemma measurable_Sup_sigma1: + assumes m: "m \<in> M" and f: "f \<in> measurable m N" + and const_space: "\<And>m n. m \<in> M \<Longrightarrow> n \<in> M \<Longrightarrow> space m = space n" + shows "f \<in> measurable (Sup_sigma M) N" +proof - + have "space (Sup_sigma M) = space m" + using m by (auto simp add: space_Sup_sigma dest: const_space) + then show ?thesis + using m f unfolding measurable_def by (auto intro: in_Sup_sigma) qed -lemma sets_vimage_algebra[simp]: - "f \<in> S \<rightarrow> space M \<Longrightarrow> sets (vimage_algebra M S f) = (\<lambda>A. f -` A \<inter> S) ` sets M" - using sigma_algebra.sets_measure_of_eq[OF sigma_algebra_preimages, of f S M] - by (simp add: vimage_algebra_def) +lemma measurable_Sup_sigma2: + assumes M: "M \<noteq> {}" + assumes f: "\<And>m. m \<in> M \<Longrightarrow> f \<in> measurable N m" + shows "f \<in> measurable N (Sup_sigma M)" + unfolding Sup_sigma_def +proof (rule measurable_measure_of) + show "f \<in> space N \<rightarrow> UNION M space" + using measurable_space[OF f] M by auto +qed (auto intro: measurable_sets f dest: sets.sets_into_space) -lemma space_vimage_algebra[simp]: - "f \<in> S \<rightarrow> space M \<Longrightarrow> space (vimage_algebra M S f) = S" - using sigma_algebra.space_measure_of_eq[OF sigma_algebra_preimages, of f S M] - by (simp add: vimage_algebra_def) - -lemma in_vimage_algebra[simp]: - "f \<in> S \<rightarrow> space M \<Longrightarrow> A \<in> sets (vimage_algebra M S f) \<longleftrightarrow> (\<exists>B\<in>sets M. A = f -` B \<inter> S)" - by (simp add: image_iff) +subsection {* The smallest \sigma-algebra regarding a function *} -lemma measurable_vimage_algebra: - fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M" - shows "f \<in> measurable (vimage_algebra M S f) M" - unfolding measurable_def using assms by force +definition + "vimage_algebra X f M = sigma X {f -` A \<inter> X | A. A \<in> sets M}" + +lemma space_vimage_algebra[simp]: "space (vimage_algebra X f M) = X" + unfolding vimage_algebra_def by (rule space_measure_of) auto -lemma measurable_vimage: - fixes g :: "'a \<Rightarrow> 'c" and f :: "'d \<Rightarrow> 'a" - assumes "g \<in> measurable M M2" "f \<in> S \<rightarrow> space M" - shows "(\<lambda>x. g (f x)) \<in> measurable (vimage_algebra M S f) M2" -proof - - note measurable_vimage_algebra[OF assms(2)] - from measurable_comp[OF this assms(1)] - show ?thesis by (simp add: comp_def) -qed +lemma sets_vimage_algebra: "sets (vimage_algebra X f M) = sigma_sets X {f -` A \<inter> X | A. A \<in> sets M}" + unfolding vimage_algebra_def by (rule sets_measure_of) auto + +lemma sets_vimage_algebra2: + "f \<in> X \<rightarrow> space M \<Longrightarrow> sets (vimage_algebra X f M) = {f -` A \<inter> X | A. A \<in> sets M}" + using sigma_sets_vimage_commute[of f X "space M" "sets M"] + unfolding sets_vimage_algebra sets.sigma_sets_eq by simp -lemma sigma_sets_vimage: - assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S" - shows "sigma_sets S' ((\<lambda>X. f -` X \<inter> S') ` A) = (\<lambda>X. f -` X \<inter> S') ` sigma_sets S A" -proof (intro set_eqI iffI) - let ?F = "\<lambda>X. f -` X \<inter> S'" - fix X assume "X \<in> sigma_sets S' (?F ` A)" - then show "X \<in> ?F ` sigma_sets S A" - proof induct - case (Basic X) then obtain X' where "X = ?F X'" "X' \<in> A" - by auto - then show ?case by auto - next - case Empty then show ?case - by (auto intro!: image_eqI[of _ _ "{}"] sigma_sets.Empty) - next - case (Compl X) then obtain X' where X: "X = ?F X'" and "X' \<in> sigma_sets S A" - by auto - then have "S - X' \<in> sigma_sets S A" - by (auto intro!: sigma_sets.Compl) - then show ?case - using X assms by (auto intro!: image_eqI[where x="S - X'"]) - next - case (Union F) - then have "\<forall>i. \<exists>F'. F' \<in> sigma_sets S A \<and> F i = f -` F' \<inter> S'" - by (auto simp: image_iff Bex_def) - from choice[OF this] obtain F' where - "\<And>i. F' i \<in> sigma_sets S A" and "\<And>i. F i = f -` F' i \<inter> S'" - by auto - then show ?case - by (auto intro!: sigma_sets.Union image_eqI[where x="\<Union>i. F' i"]) - qed -next - let ?F = "\<lambda>X. f -` X \<inter> S'" - fix X assume "X \<in> ?F ` sigma_sets S A" - then obtain X' where "X' \<in> sigma_sets S A" "X = ?F X'" by auto - then show "X \<in> sigma_sets S' (?F ` A)" - proof (induct arbitrary: X) - case Empty then show ?case by (auto intro: sigma_sets.Empty) - next - case (Compl X') - have "S' - (S' - X) \<in> sigma_sets S' (?F ` A)" - apply (rule sigma_sets.Compl) - using assms by (auto intro!: Compl.hyps simp: Compl.prems) - also have "S' - (S' - X) = X" - using assms Compl by auto - finally show ?case . - next - case (Union F) - have "(\<Union>i. f -` F i \<inter> S') \<in> sigma_sets S' (?F ` A)" - by (intro sigma_sets.Union Union.hyps) simp - also have "(\<Union>i. f -` F i \<inter> S') = X" - using assms Union by auto - finally show ?case . - qed auto -qed +lemma in_vimage_algebra: "A \<in> sets M \<Longrightarrow> f -` A \<inter> X \<in> sets (vimage_algebra X f M)" + by (auto simp: vimage_algebra_def) + +lemma sets_image_in_sets: + assumes N: "space N = X" + assumes f: "f \<in> measurable N M" + shows "sets (vimage_algebra X f M) \<subseteq> sets N" + unfolding sets_vimage_algebra N[symmetric] + by (rule sets.sigma_sets_subset) (auto intro!: measurable_sets f) + +lemma measurable_vimage_algebra1: "f \<in> X \<rightarrow> space M \<Longrightarrow> f \<in> measurable (vimage_algebra X f M) M" + unfolding measurable_def by (auto intro: in_vimage_algebra) + +lemma measurable_vimage_algebra2: + assumes g: "g \<in> space N \<rightarrow> X" and f: "(\<lambda>x. f (g x)) \<in> measurable N M" + shows "g \<in> measurable N (vimage_algebra X f M)" + unfolding vimage_algebra_def +proof (rule measurable_measure_of) + fix A assume "A \<in> {f -` A \<inter> X | A. A \<in> sets M}" + then obtain Y where Y: "Y \<in> sets M" and A: "A = f -` Y \<inter> X" + by auto + then have "g -` A \<inter> space N = (\<lambda>x. f (g x)) -` Y \<inter> space N" + using g by auto + also have "\<dots> \<in> sets N" + using f Y by (rule measurable_sets) + finally show "g -` A \<inter> space N \<in> sets N" . +qed (insert g, auto) subsubsection {* Restricted Space Sigma Algebra *} @@ -2343,16 +2322,20 @@ by (simp add: space_restrict_space sets.sets_into_space) lemma sets_restrict_space: "sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M" -proof - - have "sigma_sets (\<Omega> \<inter> space M) ((\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M) = + unfolding restrict_space_def +proof (subst sets_measure_of) + show "op \<inter> \<Omega> ` sets M \<subseteq> Pow (\<Omega> \<inter> space M)" + by (auto dest: sets.sets_into_space) + have "sigma_sets (\<Omega> \<inter> space M) {((\<lambda>x. x) -` X) \<inter> (\<Omega> \<inter> space M) | X. X \<in> sets M} = (\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M" - using sigma_sets_vimage[of "\<lambda>x. x" "\<Omega> \<inter> space M" "space M" "sets M"] sets.space_closed[of M] - by (simp add: sets.sigma_sets_eq) - moreover have "(\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M = (op \<inter> \<Omega>) ` sets M" - using sets.sets_into_space by (intro image_cong) auto - ultimately show ?thesis - using sets.sets_into_space[of _ M] unfolding restrict_space_def - by (subst sets_measure_of) fastforce+ + by (subst sigma_sets_vimage_commute[symmetric, where \<Omega>' = "space M"]) + (auto simp add: sets.sigma_sets_eq) + moreover have "{((\<lambda>x. x) -` X) \<inter> (\<Omega> \<inter> space M) | X. X \<in> sets M} = (\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M" + by auto + moreover have "(\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M = (op \<inter> \<Omega>) ` sets M" + by (intro image_cong) (auto dest: sets.sets_into_space) + ultimately show "sigma_sets (\<Omega> \<inter> space M) (op \<inter> \<Omega> ` sets M) = op \<inter> \<Omega> ` sets M" + by simp qed lemma sets_restrict_space_iff:

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Probability/Stream_Space.thy Mon Oct 06 16:27:31 2014 +0200 @@ -0,0 +1,198 @@ +theory Stream_Space +imports + Infinite_Product_Measure + "~~/src/HOL/Datatype_Examples/Stream" +begin + +lemma stream_eq_Stream_iff: "s = x ## t \<longleftrightarrow> (shd s = x \<and> stl s = t)" + by (cases s) simp + +lemma Stream_snth: "(x ## s) !! n = (case n of 0 \<Rightarrow> x | Suc n \<Rightarrow> s !! n)" + by (cases n) simp_all + +lemma sets_PiM_cong: assumes "I = J" "\<And>i. i \<in> J \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)" + using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong) + +lemma nn_integral_le_0[simp]: "integral\<^sup>N M f \<le> 0 \<longleftrightarrow> integral\<^sup>N M f = 0" + using nn_integral_nonneg[of M f] by auto + +lemma restrict_UNIV: "restrict f UNIV = f" + by (simp add: restrict_def) + +definition to_stream :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a stream" where + "to_stream X = smap X nats" + +lemma to_stream_nat_case: "to_stream (case_nat x X) = x ## to_stream X" + unfolding to_stream_def + by (subst siterate.ctr) (simp add: smap_siterate[symmetric] stream.map_comp comp_def) + +definition stream_space :: "'a measure \<Rightarrow> 'a stream measure" where + "stream_space M = + distr (\<Pi>\<^sub>M i\<in>UNIV. M) (vimage_algebra (streams (space M)) snth (\<Pi>\<^sub>M i\<in>UNIV. M)) to_stream" + +lemma space_stream_space: "space (stream_space M) = streams (space M)" + by (simp add: stream_space_def) + +lemma streams_stream_space[intro]: "streams (space M) \<in> sets (stream_space M)" + using sets.top[of "stream_space M"] by (simp add: space_stream_space) + +lemma stream_space_Stream: + "x ## \<omega> \<in> space (stream_space M) \<longleftrightarrow> x \<in> space M \<and> \<omega> \<in> space (stream_space M)" + by (simp add: space_stream_space streams_Stream) + +lemma stream_space_eq_distr: "stream_space M = distr (\<Pi>\<^sub>M i\<in>UNIV. M) (stream_space M) to_stream" + unfolding stream_space_def by (rule distr_cong) auto + +lemma sets_stream_space_cong: "sets M = sets N \<Longrightarrow> sets (stream_space M) = sets (stream_space N)" + using sets_eq_imp_space_eq[of M N] by (simp add: stream_space_def vimage_algebra_def cong: sets_PiM_cong) + +lemma measurable_snth_PiM: "(\<lambda>\<omega> n. \<omega> !! n) \<in> measurable (stream_space M) (\<Pi>\<^sub>M i\<in>UNIV. M)" + by (auto intro!: measurable_vimage_algebra1 + simp: space_PiM streams_iff_sset sset_range image_subset_iff stream_space_def) + +lemma measurable_snth[measurable]: "(\<lambda>\<omega>. \<omega> !! n) \<in> measurable (stream_space M) M" + using measurable_snth_PiM measurable_component_singleton by (rule measurable_compose) simp + +lemma measurable_shd[measurable]: "shd \<in> measurable (stream_space M) M" + using measurable_snth[of 0] by simp + +lemma measurable_stream_space2: + assumes f_snth: "\<And>n. (\<lambda>x. f x !! n) \<in> measurable N M" + shows "f \<in> measurable N (stream_space M)" + unfolding stream_space_def measurable_distr_eq2 +proof (rule measurable_vimage_algebra2) + show "f \<in> space N \<rightarrow> streams (space M)" + using f_snth[THEN measurable_space] by (auto simp add: streams_iff_sset sset_range) + show "(\<lambda>x. op !! (f x)) \<in> measurable N (Pi\<^sub>M UNIV (\<lambda>i. M))" + proof (rule measurable_PiM_single') + show "(\<lambda>x. op !! (f x)) \<in> space N \<rightarrow> UNIV \<rightarrow>\<^sub>E space M" + using f_snth[THEN measurable_space] by auto + qed (rule f_snth) +qed + +lemma measurable_stream_coinduct[consumes 1, case_names shd stl, coinduct set: measurable]: + assumes "F f" + assumes h: "\<And>f. F f \<Longrightarrow> (\<lambda>x. shd (f x)) \<in> measurable N M" + assumes t: "\<And>f. F f \<Longrightarrow> F (\<lambda>x. stl (f x))" + shows "f \<in> measurable N (stream_space M)" +proof (rule measurable_stream_space2) + fix n show "(\<lambda>x. f x !! n) \<in> measurable N M" + using `F f` by (induction n arbitrary: f) (auto intro: h t) +qed + +lemma measurable_sdrop[measurable]: "sdrop n \<in> measurable (stream_space M) (stream_space M)" + by (rule measurable_stream_space2) (simp add: sdrop_snth) + +lemma measurable_stl[measurable]: "(\<lambda>\<omega>. stl \<omega>) \<in> measurable (stream_space M) (stream_space M)" + by (rule measurable_stream_space2) (simp del: snth.simps add: snth.simps[symmetric]) + +lemma measurable_to_stream[measurable]: "to_stream \<in> measurable (\<Pi>\<^sub>M i\<in>UNIV. M) (stream_space M)" + by (rule measurable_stream_space2) (simp add: to_stream_def) + +lemma measurable_Stream[measurable (raw)]: + assumes f[measurable]: "f \<in> measurable N M" + assumes g[measurable]: "g \<in> measurable N (stream_space M)" + shows "(\<lambda>x. f x ## g x) \<in> measurable N (stream_space M)" + by (rule measurable_stream_space2) (simp add: Stream_snth) + +lemma measurable_smap[measurable]: + assumes X[measurable]: "X \<in> measurable N M" + shows "smap X \<in> measurable (stream_space N) (stream_space M)" + by (rule measurable_stream_space2) simp + +lemma measurable_stake[measurable]: + "stake i \<in> measurable (stream_space (count_space UNIV)) (count_space (UNIV :: 'a::countable list set))" + by (induct i) auto + +lemma (in prob_space) prob_space_stream_space: "prob_space (stream_space M)" +proof - + interpret product_prob_space "\<lambda>_. M" UNIV by default + show ?thesis + by (subst stream_space_eq_distr) (auto intro!: P.prob_space_distr) +qed + +lemma (in prob_space) nn_integral_stream_space: + assumes [measurable]: "f \<in> borel_measurable (stream_space M)" + shows "(\<integral>\<^sup>+X. f X \<partial>stream_space M) = (\<integral>\<^sup>+x. (\<integral>\<^sup>+X. f (x ## X) \<partial>stream_space M) \<partial>M)" +proof - + interpret S: sequence_space M + by default + interpret P: pair_sigma_finite M "\<Pi>\<^sub>M i::nat\<in>UNIV. M" + by default + + have "(\<integral>\<^sup>+X. f X \<partial>stream_space M) = (\<integral>\<^sup>+X. f (to_stream X) \<partial>S.S)" + by (subst stream_space_eq_distr) (simp add: nn_integral_distr) + also have "\<dots> = (\<integral>\<^sup>+X. f (to_stream ((\<lambda>(s, \<omega>). case_nat s \<omega>) X)) \<partial>(M \<Otimes>\<^sub>M S.S))" + by (subst S.PiM_iter[symmetric]) (simp add: nn_integral_distr) + also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+X. f (to_stream ((\<lambda>(s, \<omega>). case_nat s \<omega>) (x, X))) \<partial>S.S \<partial>M)" + by (subst S.nn_integral_fst) simp_all + also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+X. f (x ## to_stream X) \<partial>S.S \<partial>M)" + by (auto intro!: nn_integral_cong simp: to_stream_nat_case) + also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+X. f (x ## X) \<partial>stream_space M \<partial>M)" + by (subst stream_space_eq_distr) + (simp add: nn_integral_distr cong: nn_integral_cong) + finally show ?thesis . +qed + +lemma (in prob_space) emeasure_stream_space: + assumes X[measurable]: "X \<in> sets (stream_space M)" + shows "emeasure (stream_space M) X = (\<integral>\<^sup>+t. emeasure (stream_space M) {x\<in>space (stream_space M). t ## x \<in> X } \<partial>M)" +proof - + have eq: "\<And>x xs. xs \<in> space (stream_space M) \<Longrightarrow> x \<in> space M \<Longrightarrow> + indicator X (x ## xs) = indicator {xs\<in>space (stream_space M). x ## xs \<in> X } xs" + by (auto split: split_indicator) + show ?thesis + using nn_integral_stream_space[of "indicator X"] + apply (auto intro!: nn_integral_cong) + apply (subst nn_integral_cong) + apply (rule eq) + apply simp_all + done +qed + +lemma (in prob_space) prob_stream_space: + assumes P[measurable]: "{x\<in>space (stream_space M). P x} \<in> sets (stream_space M)" + shows "\<P>(x in stream_space M. P x) = (\<integral>\<^sup>+t. \<P>(x in stream_space M. P (t ## x)) \<partial>M)" +proof - + interpret S: prob_space "stream_space M" + by (rule prob_space_stream_space) + show ?thesis + unfolding S.emeasure_eq_measure[symmetric] + by (subst emeasure_stream_space) (auto simp: stream_space_Stream intro!: nn_integral_cong) +qed + +lemma (in prob_space) AE_stream_space: + assumes [measurable]: "Measurable.pred (stream_space M) P" + shows "(AE X in stream_space M. P X) = (AE x in M. AE X in stream_space M. P (x ## X))" +proof - + interpret stream: prob_space "stream_space M" + by (rule prob_space_stream_space) + + have eq: "\<And>x X. indicator {x. \<not> P x} (x ## X) = indicator {X. \<not> P (x ## X)} X" + by (auto split: split_indicator) + show ?thesis + apply (subst AE_iff_nn_integral, simp) + apply (subst nn_integral_stream_space, simp) + apply (subst eq) + apply (subst nn_integral_0_iff_AE, simp) + apply (simp add: AE_iff_nn_integral[symmetric]) + done +qed + +lemma (in prob_space) AE_stream_all: + assumes [measurable]: "Measurable.pred M P" and P: "AE x in M. P x" + shows "AE x in stream_space M. stream_all P x" +proof - + { fix n have "AE x in stream_space M. P (x !! n)" + proof (induct n) + case 0 with P show ?case + by (subst AE_stream_space) (auto elim!: eventually_elim1) + next + case (Suc n) then show ?case + by (subst AE_stream_space) auto + qed } + then show ?thesis + unfolding stream_all_def by (simp add: AE_all_countable) +qed + +end