# HG changeset patch
# User hoelzl
# Date 1412605651 -7200
# Node ID 93d87fd1583db58e0ecc73654a3d6367499fb51e
# Parent  5484f6079bcd52185ca0e67468894aceacb03af7
add measure space for (coinductive) streams

diff -r 5484f6079bcd -r 93d87fd1583d src/HOL/Probability/Probability.thy
--- 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
diff -r 5484f6079bcd -r 93d87fd1583d src/HOL/Probability/Sigma_Algebra.thy
--- 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:
diff -r 5484f6079bcd -r 93d87fd1583d src/HOL/Probability/Stream_Space.thy
--- /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