--- 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