diff --git a/thys/DiscretePricing/Infinite_Coin_Toss_Space.thy b/thys/DiscretePricing/Infinite_Coin_Toss_Space.thy --- a/thys/DiscretePricing/Infinite_Coin_Toss_Space.thy +++ b/thys/DiscretePricing/Infinite_Coin_Toss_Space.thy @@ -1,4591 +1,4594 @@ (* Title: Infinite_Coin_Toss_Space.thy Author: Mnacho Echenim, Univ. Grenoble Alpes *) section \Infinite coin toss space\ text \This section contains the formalization of the infinite coin toss space, i.e., the probability space constructed on infinite sequences of independent coin tosses.\ theory Infinite_Coin_Toss_Space imports Filtration Generated_Subalgebra Disc_Cond_Expect begin subsection \Preliminary results\ lemma decompose_init_prod: fixes n::nat shows "(\ i\ {0..n}. f i) = f 0 * (\ i\ {1..n}. f i)" proof (cases "Suc 0 \ n") case True thus ?thesis by (metis One_nat_def Suc_le_D True prod.atLeast0_atMost_Suc_shift prod.atLeast_Suc_atMost_Suc_shift) next case False thus ?thesis by (metis One_nat_def atLeastLessThanSuc_atLeastAtMost prod.atLeast0_lessThan_Suc_shift prod.atLeast_Suc_lessThan_Suc_shift) qed lemma Inter_nonempty_distrib: assumes "A \ {}" shows "\A \ B = (\ C\ A. (C\ B))" proof show "(\C\A. C \ B) \ \A \ B" proof fix x assume mem: "x \ (\C\A. C \ B)" from \A \ {}\ obtain C where "C\ A" by blast hence "x\ C\ B" using mem by blast hence in1: "x\ B" by auto have "\C. C\ A \ x \ C\B" using mem by blast hence "\C. C\ A \ x\ C" by auto hence in2: "x\ \A" by auto thus "x\ \A \ B" using in1 in2 by simp qed qed auto lemma enn2real_sum: shows "finite A \ (\a. a\ A\ f a < top) \enn2real (sum f A) = (\ a\ A. enn2real (f a))" proof (induct rule:finite_induct) case empty thus ?case by simp next case (insert a A) have "enn2real (sum f (insert a A)) = enn2real (f a + (sum f A))" by (simp add: insert.hyps(1) insert.hyps(2)) also have "... = enn2real (f a) + enn2real (sum f A)" by (simp add: enn2real_plus insert.hyps(1) insert.prems) also have "... = enn2real (f a) + (\ a\ A. enn2real (f a))" by (simp add: insert.hyps(3) insert.prems) also have "... = (\ a\ (insert a A). enn2real (f a))" by (metis calculation insert.hyps(1) insert.hyps(2) sum.insert) finally show ?case . qed lemma ennreal_sum: shows "finite A \ (\a. 0 \ f a) \ (\a\ A. ennreal (f a)) = ennreal (\a\ A. f a)" proof (induct rule:finite_induct) case empty thus ?case by simp next case (insert a A) have "(\a\ (insert a A). ennreal (f a)) = ennreal (f a) + (\a\ A. ennreal (f a))" by (simp add: insert.hyps(1) insert.hyps(2)) also have "... = ennreal (f a) + ennreal (\a\ A. f a)" by (simp add: insert.prems) also have "... = ennreal (f a + (\a\ A. f a))" by (simp add: insert.prems sum_nonneg) also have "... = ennreal (\a\ (insert a A). (f a))" using insert.hyps(1) insert.hyps(2) by auto finally show ?case . qed lemma stake_snth: assumes "stake n w = stake n x" shows "Suc i \ n \ snth w i = snth x i" by (metis Suc_le_eq assms stake_nth) lemma stake_snth_charact: assumes "stake n w = stake n x" shows "\i < n. snth w i = snth x i" proof (intro allI impI) fix i assume "i < n" thus "snth w i = snth x i" using Suc_leI assms stake_snth by blast qed lemma stake_snth': shows "(\i. Suc i \ n \ snth w i = snth x i) \stake n w = stake n x" proof (induct n arbitrary:w x) case 0 then show ?case by auto next case (Suc n) hence mh: "\i. Suc i \ Suc n \ w !! i = x !! i" by auto hence seq:"snth w n = snth x n" by auto have "stake n w = stake n x" using mh Suc by (meson Suc_leD Suc_le_mono) thus "stake (Suc n) w = stake (Suc n) x" by (metis seq stake_Suc) qed lemma stake_inter_snth: fixes x assumes "Suc 0 \ n" shows "{w\ space M. (stake n w = stake n x)} = (\ i \ {0.. n-1}. {w\ space M. (snth w i = snth x i)})" proof let ?S = "{w\ space M. (stake n w = stake n x)}" show "?S \ (\i\{0..n-1}. {w \ space M. w !! i = x !! i})" using stake_snth assms by fastforce show "(\i\{0..n-1}. {w \ space M. w !! i = x !! i}) \ ?S" proof fix w assume inter: "w \ (\i\{0..n-1}. {w \ space M. w !! i = x !! i})" have "\ i. 0 \ i \ i \ n-1 \ snth w i = snth x i" proof (intro allI impI) fix i assume "0 \ i \ i \ n-1" thus "snth w i = snth x i" using inter by auto qed hence "stake n w = stake n x" by (metis One_nat_def Suc_le_D diff_Suc_Suc diff_is_0_eq diff_zero le0 stake_snth') thus "w\ ?S" using inter by auto qed qed lemma streams_stake_set: shows "pw \ streams A \ set (stake n pw) \ A" proof (induct n arbitrary: pw) case (Suc n) note hyp = this have "set (stake (Suc 0) pw) \ A" proof - have "shd pw \ A" using hyp streams_shd[of pw A] by simp have "stake (Suc 0) pw = [shd pw]" by auto hence "set (stake (Suc 0) pw) = {shd pw}" by auto thus ?thesis using \shd pw \ A\ by auto qed thus ?case by (simp add: Suc.hyps Suc.prems streams_stl) qed simp lemma stake_finite_universe_induct: assumes "finite A" and "A \ {}" shows "(stake (Suc n) `(streams A)) = {s#w| s w. s\ A \ w\ (stake n `(streams A))}" (is "?L = ?R") proof show "?L \ ?R" proof fix l::"'a list" assume "l\ ?L" hence "\pw. pw \ streams A \ l = stake (Suc n) pw" by auto from this obtain pw where "pw \ streams A" and "l = stake (Suc n) pw" by blast hence "l = shd pw # stake n (stl pw)" unfolding stake_def by auto thus "l\ ?R" by (simp add: \pw \ streams A\ streams_shd streams_stl) qed show "?R \ ?L" proof fix l::"'a list" assume "l\ ?R" hence "\ s w. s\ A \ w\ (stake n `(streams A)) \ l = s# w" by auto from this obtain s and w where "s\ A" and "w\ (stake n `(streams A))" and "l = s# w" by blast note swprop = this have "\pw. pw \ streams A \ w = stake n pw" using swprop by auto from this obtain pw where "pw\ streams A" and "w = stake n pw" by blast note pwprop = this have "l \ lists A" proof - have "s\ A" using swprop by simp have "set w \ A" using pwprop streams_stake_set by simp have "set l = set w \ {s}" using swprop by auto thus ?thesis using \s\ A\ \set w \ A\ by auto qed have "\x. x \ A" using assms by auto from this obtain x where "x\ A" by blast let ?sx = "sconst x" let ?st = "shift l ?sx" have "l = stake (Suc n) ?st" by (simp add: pwprop(2) stake_shift swprop(3)) have "sset ?sx = {x}" by simp hence "sset ?sx \ A" using \x\ A\ by simp hence "?sx \ streams A" using sset_streams[of "sconst x"] by simp hence "?st \ streams A" using \l \ lists A\ shift_streams[of l A "sconst x"] by simp thus "l\ ?L" using \l = stake (Suc n) ?st\ by blast qed qed lemma stake_finite_universe_finite: assumes "finite A" and "A \ {}" shows "finite (stake n `(streams A))" proof (induction n) let ?L = "(stake 0 `(streams A))" have "streams A \ {}" proof assume "streams A = {}" have "\x. x \ A" using assms by auto from this obtain x where "x\ A" by blast let ?sx = "sconst x" have "sset ?sx = {x}" by simp hence "sset ?sx \ A" using \x\ A\ by simp hence "?sx \ streams A" using sset_streams[of "sconst x"] by simp thus False using \streams A = {}\ by simp qed have "stake 0 = (\s. [])" unfolding stake_def by simp hence "?L = {[]}" using \streams A \ {}\ by auto show "finite (stake 0 `(streams A))" by (simp add: \?L = {[]}\ image_constant_conv) next fix n assume "finite (stake n `(streams A))" note hyp = this have "(stake (Suc n) `(streams A)) = {s#w| s w. s\ A \ w\ (stake n `(streams A))}" (is "?L = ?R") using assms stake_finite_universe_induct[of A n] by simp have "finite ?R" by (simp add: assms(1) finite_image_set2 hyp) thus "finite ?L" using \?L = ?R\by simp qed lemma diff_streams_only_if: assumes "w \ x" shows "\n. snth w n \ snth x n" proof - have f1: "smap (\n. x !! (n - Suc 0)) (fromN (Suc 0)) \ w" by (metis assms stream_smap_fromN) obtain nn :: "'a stream \ nat stream \ (nat \ 'a) \ nat" where "\x0 x1 x2. (\v3. x2 (x1 !! v3) \ x0 !! v3) = (x2 (x1 !! nn x0 x1 x2) \ x0 !! nn x0 x1 x2)" by moura then have "x !! (fromN (Suc 0) !! nn w (fromN (Suc 0)) (\n. x !! (n - Suc 0)) - Suc 0) \ w !! nn w (fromN (Suc 0)) (\n. x !! (n - Suc 0))" using f1 by (meson smap_alt) then show ?thesis by (metis (no_types) snth_smap stream_smap_fromN) qed lemma diff_streams_if: assumes "\n. snth w n \ snth x n" shows "w\ x" using assms by auto lemma sigma_set_union_count: assumes "\ y\ A. B y \ sigma_sets X Y" and "countable A" shows "(\ y\ A. B y) \ sigma_sets X Y" by (metis (mono_tags, lifting) assms countable_image imageE sigma_sets_UNION) lemma sigma_set_inter_init: assumes "\i. i\(n::nat) \ A i \ sigma_sets sp B" and "B \ Pow sp" shows "(\ i\ {m. m\ n}. A i) \ sigma_sets sp B" by (metis (full_types) assms(1) assms(2) bot.extremum empty_iff mem_Collect_eq sigma_sets_INTER) lemma adapt_sigma_sets: assumes "\i. i \ n\ (X i) \ measurable M N" shows "sigma_algebra (space M) (sigma_sets (space M) (\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets N}))" proof (rule sigma_algebra_sigma_sets) show "(\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets N}) \ Pow (space M)" proof (rule UN_subset_iff[THEN iffD2], intro ballI) fix i assume "i \ {m. m\ n}" show "{X i -` A \ space M |A. A \ sets N} \ Pow (space M)" by auto qed qed subsection \Bernoulli streams\ text \Bernoulli streams represent the formal definition of the infinite coin toss space. The parameter \p\ represents the probability of obtaining a head after a coin toss.\ definition bernoulli_stream::"real \ (bool stream) measure" where "bernoulli_stream p = stream_space (measure_pmf (bernoulli_pmf p))" lemma bernoulli_stream_space: assumes "N = bernoulli_stream p" shows "space N = streams UNIV::bool" using assms unfolding bernoulli_stream_def stream_space_def by (simp add: assms bernoulli_stream_def space_stream_space) lemma bernoulli_stream_preimage: assumes "N = bernoulli_stream p" shows "f -` A \ (space N) = f-`A" using assms by (simp add: bernoulli_stream_space) lemma bernoulli_stream_component_probability: assumes "N = bernoulli_stream p" and "0 \ p" and "p \ 1" shows "\ n. emeasure N {w\ space N. (snth w n)} = p" proof have "prob_space N" using assms by (simp add: bernoulli_stream_def prob_space.prob_space_stream_space prob_space_measure_pmf) fix n::nat let ?S = "{w\ space N. (snth w n)}" have s: "?S \ sets N" proof - have "(\w. snth w n) \ measurable N (measure_pmf (bernoulli_pmf p))" using assms by (simp add: bernoulli_stream_def) moreover have "{True} \ sets (measure_pmf (bernoulli_pmf p))" by simp ultimately show ?thesis by simp qed let ?PM = "(\i::nat. (measure_pmf (bernoulli_pmf p)))" have isps: "product_prob_space ?PM" by unfold_locales let ?Z = "{X::nat\bool. X n = True}" let ?wPM = "Pi\<^sub>M UNIV ?PM" have "space ?wPM = UNIV" using space_PiM by fastforce hence "(to_stream -` ?S \ (space ?wPM)) = to_stream -` ?S" by simp also have "... = ?Z" using assms by (simp add:bernoulli_stream_space to_stream_def) also have "... = prod_emb UNIV ?PM {n} (Pi\<^sub>E {n} (\x::nat. {True}))" proof { fix X assume "X \ prod_emb UNIV ?PM {n} (Pi\<^sub>E {n} (\x::nat. {True}))" hence "restrict X {n} \ (Pi\<^sub>E {n} (\x::nat. {True}))" using prod_emb_iff[of X] by simp - hence "X n = True" by simp + hence "X n = True" + unfolding PiE_iff by auto hence "X \ ?Z" by simp } thus "prod_emb UNIV ?PM {n} (Pi\<^sub>E {n} (\x::nat. {True})) \ ?Z" by auto { fix X assume "X \ ?Z" hence "X n = True" by simp - hence "restrict X {n} \ (Pi\<^sub>E {n} (\x::nat. {True}))" by simp + hence "restrict X {n} \ (Pi\<^sub>E {n} (\x::nat. {True}))" + unfolding PiE_iff by auto moreover have "X \ extensional UNIV" by simp moreover have "\i \ UNIV. X i \ space (?PM i)" by auto ultimately have "X \ prod_emb UNIV ?PM {n} (Pi\<^sub>E {n} (\x::nat. {True}))" using prod_emb_iff[of X] by simp } thus "?Z \ prod_emb UNIV ?PM {n} (Pi\<^sub>E {n} (\x::nat. {True}))" by auto qed finally have inteq: "(to_stream -` ?S \ (space ?wPM)) = prod_emb UNIV ?PM {n} (Pi\<^sub>E {n} (\x::nat. {True}))" . have "emeasure N ?S = emeasure ?wPM (to_stream -` ?S \ (space ?wPM))" using assms emeasure_distr[of "to_stream" ?wPM "(vimage_algebra (streams (space (measure_pmf (bernoulli_pmf p)))) (!!) (Pi\<^sub>M UNIV (\i. measure_pmf (bernoulli_pmf p))))" ?S] measurable_to_stream[of "(measure_pmf (bernoulli_pmf p))"] s unfolding bernoulli_stream_def stream_space_def by auto also have "... = emeasure ?wPM (prod_emb UNIV ?PM {n} (Pi\<^sub>E {n} (\x::nat. {True})))" using inteq by simp also have "... = - (\i\{n}. emeasure (?PM i) ((\x::nat. {True}) i))" using isps by (auto simp add: product_prob_space.emeasure_PiM_emb) + (\i\{n}. emeasure (?PM i) ((\x::nat. {True}) i))" using isps + by (auto simp add: product_prob_space.emeasure_PiM_emb simp del: ext_funcset_to_sing_iff) also have "... = emeasure (?PM n) {True}" by simp also have "... = p" using assms by (simp add: emeasure_pmf_single) finally show "emeasure N ?S = p" . qed lemma bernoulli_stream_component_probability_compl: assumes "N = bernoulli_stream p" and "0 \ p" and "p \ 1" shows "\ n. emeasure N {w\ space N. \(snth w n)} = 1- p" proof fix n let ?A = "{w \ space N. \ w !! n}" let ?B = "{w \ space N. w !! n}" have "?A \ ?B = space N" by auto have "?A\?B = {}" by auto hence eqA: "?A = (?A\ ?B) - ?B" using Diff_cancel by blast moreover have "?A \ sets N" proof - have "(\w. snth w n) \ measurable N (measure_pmf (bernoulli_pmf p))" using assms by (simp add: bernoulli_stream_def) moreover have "{True} \ sets (measure_pmf (bernoulli_pmf p))" by simp ultimately show ?thesis by simp qed moreover have "?B \ sets N" proof - have "(\w. snth w n) \ measurable N (measure_pmf (bernoulli_pmf p))" using assms by (simp add: bernoulli_stream_def) moreover have "{True} \ sets (measure_pmf (bernoulli_pmf p))" by simp ultimately show ?thesis by simp qed ultimately have "emeasure N ((?A\ ?B) - ?B) = emeasure N (?A\ ?B) - emeasure N ?B" proof - have f1: "\S m. (S::bool stream set) \ sets m \ emeasure m S = \ \ emeasure m (space m) - emeasure m S = emeasure m (space m - S)" by (metis emeasure_compl infinity_ennreal_def) have "emeasure N {s \ space N. s !! n} \ \" using assms(1) assms(2) assms(3) ennreal_neq_top bernoulli_stream_component_probability by presburger then have "emeasure N (space N) - emeasure N {s \ space N. s !! n} = emeasure N (space N - {s \ space N. s !! n})" using f1 \{w \ space N. w !! n} \ sets N\ by blast then show ?thesis using \{w \ space N. \ w !! n} \ {w \ space N. w !! n} = space N\ by presburger qed hence "emeasure N ?A = emeasure N (?A\ ?B) - emeasure N ?B" using eqA by simp also have "... = 1 - emeasure N ?B" by (metis (no_types, lifting) \?A \ ?B = space N\ assms(1) bernoulli_stream_def prob_space.emeasure_space_1 prob_space.prob_space_stream_space prob_space_measure_pmf) also have "... = 1 - p" using bernoulli_stream_component_probability[of N p] assms by (metis (mono_tags) ennreal_1 ennreal_minus_if) finally show "emeasure N ?A = 1 - p" . qed lemma bernoulli_stream_sets: assumes "0 < q" and "q < 1" and "0 < p" and "p < 1" shows "sets (bernoulli_stream p) = sets (bernoulli_stream q)" unfolding bernoulli_stream_def by (rule sets_stream_space_cong, simp) locale infinite_coin_toss_space = fixes p::real and M::"bool stream measure" assumes p_gt_0: "0 \ p" and p_lt_1: "p \ 1" and bernoulli: "M = bernoulli_stream p" sublocale infinite_coin_toss_space \ prob_space by (simp add: bernoulli bernoulli_stream_def prob_space.prob_space_stream_space prob_space_measure_pmf) subsection \Natural filtration on the infinite coin toss space\ text \The natural filtration on the infinite coin toss space is the discrete filtration @{term F} such that @{term "F n"} represents the restricted measure space in which the outcome of the first @{term n} coin tosses is known.\ subsubsection \The projection function\ text \Intuitively, the restricted measure space in which the outcome of the first @{term n} coin tosses is known can be defined by any measurable function that maps all infinite sequences that agree on the first @{term n} coin tosses to the same element.\ definition (in infinite_coin_toss_space) pseudo_proj_True:: "nat \ bool stream \ bool stream" where "pseudo_proj_True n = (\w. shift (stake n w) (sconst True))" definition (in infinite_coin_toss_space) pseudo_proj_False:: "nat \ bool stream \ bool stream" where "pseudo_proj_False n = (\w. shift (append (stake n w) [False]) (sconst True))" lemma (in infinite_coin_toss_space) pseudo_proj_False_neq_True: shows "pseudo_proj_False n w \ pseudo_proj_True n w" proof (rule diff_streams_if, intro exI) have "snth (pseudo_proj_False n w) n = False" unfolding pseudo_proj_False_def by simp moreover have "snth (pseudo_proj_True n w) n = True" unfolding pseudo_proj_True_def by simp ultimately show "snth (pseudo_proj_False n w) n \ snth (pseudo_proj_True n w) n" by simp qed lemma (in infinite_coin_toss_space) pseudo_proj_False_measurable: shows "pseudo_proj_False n \ measurable (bernoulli_stream p) (bernoulli_stream p)" proof - let ?N = "bernoulli_stream p" have "id \ measurable ?N ?N" by simp moreover have "(\w. (sconst True)) \ measurable ?N ?N" using bernoulli_stream_space by simp ultimately show ?thesis using measurable_shift p_gt_0 p_lt_1 unfolding bernoulli_stream_def pseudo_proj_False_def by simp qed lemma (in infinite_coin_toss_space) pseudo_proj_True_stake: shows "stake n (pseudo_proj_True n w) = stake n w" by (simp add: pseudo_proj_True_def stake_shift) lemma (in infinite_coin_toss_space) pseudo_proj_False_stake: shows "stake n (pseudo_proj_False n w) = stake n w" by (simp add: pseudo_proj_False_def stake_shift) lemma (in infinite_coin_toss_space) pseudo_proj_True_stake_image: assumes "(stake n w) = stake n x" shows "pseudo_proj_True n w = pseudo_proj_True n x" by (simp add: assms pseudo_proj_True_def) lemma (in infinite_coin_toss_space) pseudo_proj_True_prefix: assumes "n \ m" and "pseudo_proj_True m x = pseudo_proj_True m y" shows "pseudo_proj_True n x = pseudo_proj_True n y" by (metis assms diff_is_0_eq id_stake_snth_sdrop length_stake pseudo_proj_True_def stake.simps(1) stake_shift) lemma (in infinite_coin_toss_space) pseudo_proj_True_measurable: shows "pseudo_proj_True n \ measurable (bernoulli_stream p) (bernoulli_stream p)" proof - let ?N = "bernoulli_stream p" have "id \ measurable ?N ?N" by simp moreover have "(\w. (sconst True)) \ measurable ?N ?N" using bernoulli_stream_space by simp ultimately show ?thesis using measurable_shift p_gt_0 p_lt_1 unfolding bernoulli_stream_def pseudo_proj_True_def by simp qed lemma (in infinite_coin_toss_space) pseudo_proj_True_finite_image: shows "finite (range (pseudo_proj_True n))" proof - let ?U = "UNIV::bool set" have "?U = {True, False}" by auto hence "finite ?U" by simp moreover have "?U \ {}" by auto ultimately have fi: "finite (stake n `streams ?U)" using stake_finite_universe_finite[of ?U] by simp let ?sh= "(\l. shift l (sconst True))" have "finite {?sh l|l. l\(stake n `streams ?U)}" using fi by simp moreover have "{?sh l|l. l\(stake n `streams ?U)} = range (pseudo_proj_True n)" unfolding pseudo_proj_True_def by auto ultimately show ?thesis by simp qed lemma (in infinite_coin_toss_space) pseudo_proj_False_finite_image: shows "finite (range (pseudo_proj_False n))" proof - let ?U = "UNIV::bool set" have "?U = {True, False}" by auto hence "finite ?U" by simp moreover have "?U \ {}" by auto ultimately have fi: "finite (stake n `streams ?U)" using stake_finite_universe_finite[of ?U] by simp let ?sh= "(\l. shift (l @ [False]) (sconst True))" have "finite {?sh l|l. l\(stake n `streams ?U)}" using fi by simp moreover have "{?sh l|l. l\(stake n `streams ?U)} = range (pseudo_proj_False n)" unfolding pseudo_proj_False_def by auto ultimately show ?thesis by simp qed lemma (in infinite_coin_toss_space) pseudo_proj_True_proj: shows "pseudo_proj_True n (pseudo_proj_True n w) = pseudo_proj_True n w" by (metis pseudo_proj_True_def pseudo_proj_True_stake) lemma (in infinite_coin_toss_space) pseudo_proj_True_Suc_False_proj: shows "pseudo_proj_True (Suc n) (pseudo_proj_False n w) = pseudo_proj_False n w" by (metis append_Nil2 cancel_comm_monoid_add_class.diff_cancel length_append_singleton length_stake order_refl pseudo_proj_False_def pseudo_proj_True_def stake.simps(1) stake_shift take_all) lemma (in infinite_coin_toss_space) pseudo_proj_True_Suc_proj: shows "pseudo_proj_True (Suc n) (pseudo_proj_True n w) = pseudo_proj_True n w" by (metis id_apply id_stake_snth_sdrop pseudo_proj_True_def pseudo_proj_True_stake shift_left_inj siterate.code stake_sdrop stream.sel(2)) lemma (in infinite_coin_toss_space) pseudo_proj_True_proj_Suc: shows "pseudo_proj_True n (pseudo_proj_True (Suc n) w) = pseudo_proj_True n w" by (meson Suc_n_not_le_n nat_le_linear pseudo_proj_True_prefix pseudo_proj_True_stake pseudo_proj_True_stake_image) lemma (in infinite_coin_toss_space) pseudo_proj_True_shift: shows "length l = n \ pseudo_proj_True n (shift l (sconst True)) = shift l (sconst True)" by (simp add: pseudo_proj_True_def stake_shift) lemma (in infinite_coin_toss_space) pseudo_proj_True_suc_img: shows "pseudo_proj_True (Suc n) w \ {pseudo_proj_True n w, pseudo_proj_False n w}" by (metis (full_types) cycle_decomp insertCI list.distinct(1) pseudo_proj_True_def pseudo_proj_False_def sconst_cycle shift_append stake_Suc) lemma (in infinite_coin_toss_space) measurable_snth_count_space: shows "(\w. snth w n) \ measurable (bernoulli_stream p) (count_space (UNIV::bool set))" by (simp add: bernoulli_stream_def) lemma (in infinite_coin_toss_space) pseudo_proj_True_same_img: assumes "pseudo_proj_True n w = pseudo_proj_True n x" shows "stake n w = stake n x" by (metis assms pseudo_proj_True_stake) lemma (in infinite_coin_toss_space) pseudo_proj_True_snth: assumes "pseudo_proj_True n x = pseudo_proj_True n w" shows "\i. Suc i \ n \ snth x i = snth w i" proof - fix i have "stake n w= stake n x" using assms by (metis pseudo_proj_True_stake) assume "Suc i \ n" thus "snth x i = snth w i" using \stake n w = stake n x\ stake_snth by auto qed lemma (in infinite_coin_toss_space) pseudo_proj_True_snth': assumes "(\i. Suc i \ n \ snth w i = snth x i)" shows "pseudo_proj_True n w = pseudo_proj_True n x" proof - have "stake n w = stake n x" using stake_snth'[of n w x] using assms by simp moreover have "stake n w = stake n x \ pseudo_proj_True n w = pseudo_proj_True n x" using pseudo_proj_True_stake_image[of n w x] by simp ultimately show ?thesis by auto qed lemma (in infinite_coin_toss_space) pseudo_proj_True_preimage: assumes "w = pseudo_proj_True n w" shows "(pseudo_proj_True n) -` {w} = (\i\ {m. Suc m \ n}. (\w. snth w i) -` {snth w i})" proof show "(pseudo_proj_True n) -` {w} \ (\i\{m. Suc m \ n}. (\w. snth w i) -` {snth w i})" proof fix x assume "x \ (pseudo_proj_True n) -`{w}" hence "pseudo_proj_True n x = pseudo_proj_True n w" using assms by auto hence "\i. i \{m. Suc m \ n} \ x \ (\x. snth x i) -`{snth w i}" by (metis (mono_tags) Suc_le_eq mem_Collect_eq pseudo_proj_True_stake stake_nth vimage_singleton_eq) thus "x \ (\i\{m. Suc m \ n}. (\w. snth w i) -` {snth w i})" by auto qed show "(\i\{m. Suc m \ n}. (\w. snth w i) -` {snth w i}) \ (pseudo_proj_True n) -` {w}" proof fix x assume "x\ (\i\{m. Suc m \ n}. (\w. snth w i) -` {snth w i})" hence "\i. i \{m. Suc m \ n} \ x \ (\x. snth x i) -`{snth w i}" by simp hence "\i. i \{m. Suc m \ n} \ snth x i = snth w i" by simp hence "\i. Suc i \ n \ snth x i = snth w i" by auto hence "pseudo_proj_True n x = pseudo_proj_True n w" using pseudo_proj_True_snth'[of n x w] by simp also have "... = w" using assms by simp finally have "pseudo_proj_True n x = w" . thus "x \ (pseudo_proj_True n) -`{w}" by auto qed qed lemma (in infinite_coin_toss_space) pseudo_proj_False_preimage: assumes "w = pseudo_proj_False n w" shows "(pseudo_proj_False n) -` {w} = (\i\ {m. Suc m \ n}. (\w. snth w i) -` {snth w i})" proof show "(pseudo_proj_False n) -` {w} \ (\i\{m. Suc m \ n}. (\w. snth w i) -` {snth w i})" proof fix x assume "x \ (pseudo_proj_False n) -`{w}" hence "pseudo_proj_False n x = pseudo_proj_False n w" using assms by auto hence "\i. i \{m. Suc m \ n} \ x \ (\x. snth x i) -`{snth w i}" by (metis (mono_tags) Suc_le_eq mem_Collect_eq pseudo_proj_False_stake stake_nth vimage_singleton_eq) thus "x \ (\i\{m. Suc m \ n}. (\w. snth w i) -` {snth w i})" by auto qed show "(\i\{m. Suc m \ n}. (\w. snth w i) -` {snth w i}) \ (pseudo_proj_False n) -` {w}" proof fix x assume "x\ (\i\{m. Suc m \ n}. (\w. snth w i) -` {snth w i})" hence "\i. i \{m. Suc m \ n} \ x \ (\x. snth x i) -`{snth w i}" by simp hence "\i. i \{m. Suc m \ n} \ snth x i = snth w i" by simp hence "\i. Suc i \ n \ snth x i = snth w i" by auto hence "pseudo_proj_False n x = pseudo_proj_False n w" by (metis (full_types) pseudo_proj_False_def stake_snth') also have "... = w" using assms by simp finally have "pseudo_proj_False n x = w" . thus "x \ (pseudo_proj_False n) -`{w}" by auto qed qed lemma (in infinite_coin_toss_space) pseudo_proj_True_preimage_stake: assumes "w = pseudo_proj_True n w" shows "(pseudo_proj_True n) -` {w} = {x. stake n x = stake n w}" proof show "{x. stake n x = stake n w} \ (pseudo_proj_True n) -` {w}" proof fix x assume "x \ {x. stake n x = stake n w}" hence "stake n x = stake n w" by auto hence "pseudo_proj_True n x = w" using assms pseudo_proj_True_def by auto thus "x \ (pseudo_proj_True n) -` {w}" by auto qed show "(pseudo_proj_True n) -` {w} \ {x. stake n x = stake n w}" proof fix x assume "x\ pseudo_proj_True n -`{w}" hence "pseudo_proj_True n x = pseudo_proj_True n w" using assms by auto hence "stake n x = stake n w" by (metis pseudo_proj_True_stake) thus "x\ {x. stake n x = stake n w}" by simp qed qed lemma (in infinite_coin_toss_space) pseudo_proj_False_preimage_stake: assumes "w = pseudo_proj_False n w" shows "(pseudo_proj_False n) -` {w} = {x. stake n x = stake n w}" proof show "{x. stake n x = stake n w} \ (pseudo_proj_False n) -` {w}" proof fix x assume "x \ {x. stake n x = stake n w}" hence "stake n x = stake n w" by auto hence "pseudo_proj_False n x = w" using assms pseudo_proj_False_def by auto thus "x \ (pseudo_proj_False n) -` {w}" by auto qed show "(pseudo_proj_False n) -` {w} \ {x. stake n x = stake n w}" proof fix x assume "x\ pseudo_proj_False n -`{w}" hence "pseudo_proj_False n x = pseudo_proj_False n w" using assms by auto hence "stake n x = stake n w" by (metis pseudo_proj_False_stake) thus "x\ {x. stake n x = stake n w}" by simp qed qed lemma (in infinite_coin_toss_space) pseudo_proj_True_preimage_stake_space: assumes "w = pseudo_proj_True n w" shows "(pseudo_proj_True n) -` {w} \ space M = {x\ space M. stake n x = stake n w}" proof - have "(pseudo_proj_True n) -` {w} = {x. stake n x = stake n w}" using assms by (simp add:pseudo_proj_True_preimage_stake) hence "(pseudo_proj_True n) -` {w}\ space M = {x. stake n x = stake n w}\ space M" by simp also have "... = {x\ space M. stake n x = stake n w}" by auto finally show ?thesis . qed lemma (in infinite_coin_toss_space) pseudo_proj_True_singleton: assumes "w = pseudo_proj_True n w" shows "(pseudo_proj_True n) -`{w} \ (space (bernoulli_stream p)) \ sets (bernoulli_stream p)" proof (cases "{m. (Suc m) \ n} = {}") case False have "\i. (\x. snth x i) \ measurable (bernoulli_stream p) (count_space UNIV)" by (simp add: measurable_snth_count_space) have fi: "\i. Suc i \ n \ (\w. snth w i) -` {snth w i} \ (space (bernoulli_stream p)) \ sets (bernoulli_stream p)" proof - fix i assume "Suc i \ n" have "(\x. snth x i) \ measurable (bernoulli_stream p) (count_space UNIV)" by (simp add: measurable_snth_count_space) moreover have "{snth w i} \ sets (count_space UNIV)" by auto ultimately show "(\x. snth x i) -` {snth w i}\ (space (bernoulli_stream p)) \ sets (bernoulli_stream p)" unfolding measurable_def by (simp add: measurable_snth_count_space) qed have "(\i\ {m. (Suc m) \ n}. (\w. snth w i) -` {snth w i}\ (space (bernoulli_stream p))) \ sets (bernoulli_stream p)" proof ((rule sigma_algebra.countable_INT''), auto) show "sigma_algebra (space (bernoulli_stream p)) (sets (bernoulli_stream p))" using measure_space measure_space_def by auto show "UNIV \ sets (bernoulli_stream p)" by (metis bernoulli_stream_space sets.top streams_UNIV) show "\i. Suc i \ n \ (\w. w !! i) -` {w !! i} \ space (bernoulli_stream p) \ sets (bernoulli_stream p)" using fi by simp qed moreover have "(\i\ {m. (Suc m) \ n}. (\w. snth w i) -` {snth w i}\ (space (bernoulli_stream p))) = (\i\ {m. (Suc m) \ n}. (\w. snth w i) -` {snth w i})\ (space (bernoulli_stream p))" using False Inter_nonempty_distrib by auto ultimately show ?thesis using assms pseudo_proj_True_preimage[of w n] by simp next case True hence "n = 0" using less_eq_Suc_le by auto hence "pseudo_proj_True n = (\w. sconst True)" by (simp add: pseudo_proj_True_def) hence "w = sconst True" using assms by simp hence "(pseudo_proj_True n) -`{w} \ (space (bernoulli_stream p)) = (space (bernoulli_stream p))" by (simp add: \pseudo_proj_True n = (\w. sconst True)\) thus "(pseudo_proj_True n) -`{w} \ (space (bernoulli_stream p))\ sets (bernoulli_stream p)" by simp qed lemma (in infinite_coin_toss_space) pseudo_proj_False_singleton: assumes "w = pseudo_proj_False n w" shows "(pseudo_proj_False n) -`{w} \ (space (bernoulli_stream p)) \ sets (bernoulli_stream p)" proof (cases "{m. (Suc m) \ n} = {}") case False have "\i. (\x. snth x i) \ measurable (bernoulli_stream p) (count_space UNIV)" by (simp add: measurable_snth_count_space) have fi: "\i. Suc i \ n \ (\w. snth w i) -` {snth w i} \ (space (bernoulli_stream p)) \ sets (bernoulli_stream p)" proof - fix i assume "Suc i \ n" have "(\x. snth x i) \ measurable (bernoulli_stream p) (count_space UNIV)" by (simp add: measurable_snth_count_space) moreover have "{snth w i} \ sets (count_space UNIV)" by auto ultimately show "(\x. snth x i) -` {snth w i}\ (space (bernoulli_stream p)) \ sets (bernoulli_stream p)" unfolding measurable_def by (simp add: measurable_snth_count_space) qed have "(\i\ {m. (Suc m) \ n}. (\w. snth w i) -` {snth w i}\ (space (bernoulli_stream p))) \ sets (bernoulli_stream p)" proof ((rule sigma_algebra.countable_INT''), auto) show "sigma_algebra (space (bernoulli_stream p)) (sets (bernoulli_stream p))" using measure_space measure_space_def by auto show "UNIV \ sets (bernoulli_stream p)" by (metis bernoulli_stream_space sets.top streams_UNIV) show "\i. Suc i \ n \ (\w. w !! i) -` {w !! i} \ space (bernoulli_stream p) \ sets (bernoulli_stream p)" using fi by simp qed moreover have "(\i\ {m. (Suc m) \ n}. (\w. snth w i) -` {snth w i}\ (space (bernoulli_stream p))) = (\i\ {m. (Suc m) \ n}. (\w. snth w i) -` {snth w i})\ (space (bernoulli_stream p))" using False Inter_nonempty_distrib by auto ultimately show ?thesis using assms pseudo_proj_False_preimage[of w n] by simp next case True hence "n = 0" using less_eq_Suc_le by auto hence "pseudo_proj_False n = (\w. False ## sconst True)" by (simp add: pseudo_proj_False_def) hence "w = False ## sconst True" using assms by simp hence "(pseudo_proj_False n) -`{w} \ (space (bernoulli_stream p)) = (space (bernoulli_stream p))" by (simp add: \pseudo_proj_False n = (\w. False##sconst True)\) thus "(pseudo_proj_False n) -`{w} \ (space (bernoulli_stream p))\ sets (bernoulli_stream p)" by simp qed lemma (in infinite_coin_toss_space) pseudo_proj_True_inverse_induct: assumes "w \ range (pseudo_proj_True n)" shows "(pseudo_proj_True n) -` {w} = (pseudo_proj_True (Suc n)) -` {w} \ (pseudo_proj_True (Suc n)) -`{pseudo_proj_False n w}" proof let ?y = "pseudo_proj_False n w" show "(pseudo_proj_True n) -` {w} \ (pseudo_proj_True (Suc n)) -` {w} \ (pseudo_proj_True (Suc n)) -`{?y}" proof fix z assume "z\ pseudo_proj_True n -`{w}" thus "z\ pseudo_proj_True (Suc n) -`{w} \ pseudo_proj_True (Suc n) -`{?y}" using pseudo_proj_False_def pseudo_proj_True_def pseudo_proj_True_stake pseudo_proj_True_suc_img by fastforce qed { fix z assume "z \ pseudo_proj_True (Suc n) -` {w}" hence "pseudo_proj_True (Suc n) z = w" by simp hence "pseudo_proj_True n z = pseudo_proj_True n w" by (metis pseudo_proj_True_proj_Suc) also have "... = w" using assms pseudo_proj_True_def pseudo_proj_True_stake by auto finally have "pseudo_proj_True n z = w" . } hence fst: "pseudo_proj_True (Suc n) -` {w} \ (pseudo_proj_True n) -` {w}" by blast { fix z assume "z \ pseudo_proj_True (Suc n) -` {?y}" hence "pseudo_proj_True n z = pseudo_proj_True n w" by (metis append1_eq_conv append_Nil2 cancel_comm_monoid_add_class.diff_cancel length_append_singleton length_stake order_refl pseudo_proj_False_def pseudo_proj_True_stake pseudo_proj_True_stake_image stake_Suc stake_invert_Nil stake_shift take_all vimage_singleton_eq) also have "... = w" using assms pseudo_proj_True_def pseudo_proj_True_stake by auto finally have "pseudo_proj_True n z = w" . } hence scd: "pseudo_proj_True (Suc n) -` {?y} \ (pseudo_proj_True n) -` {w}" by blast show "(pseudo_proj_True (Suc n)) -` {w} \ (pseudo_proj_True (Suc n)) -`{?y} \ (pseudo_proj_True n) -` {w}" using fst scd by auto qed subsubsection \Natural filtration locale\ text \This part is mainly devoted to the proof that the projection function defined above indeed permits to obtain a filtration on the infinite coin toss space, and that this filtration is initially trivial.\ definition (in infinite_coin_toss_space) nat_filtration::"nat \ bool stream measure" where "nat_filtration n = fct_gen_subalgebra M M (pseudo_proj_True n)" locale infinite_cts_filtration = infinite_coin_toss_space + fixes F assumes natural_filtration: "F = nat_filtration" lemma (in infinite_coin_toss_space) nat_filtration_space: shows "space (nat_filtration n) = UNIV" by (metis bernoulli bernoulli_stream_space fct_gen_subalgebra_space nat_filtration_def streams_UNIV) lemma (in infinite_coin_toss_space) nat_filtration_sets: shows "sets (nat_filtration n) = sigma_sets (space (bernoulli_stream p)) {pseudo_proj_True n -` B \ space M |B. B \ sets (bernoulli_stream p)}" proof - have "sigma_sets (space M) {pseudo_proj_True n -` S \ space M |S. S \ sets (bernoulli_stream p)} = sets (fct_gen_subalgebra M M (pseudo_proj_True n))" using bernoulli fct_gen_subalgebra_sets pseudo_proj_True_measurable by blast then show ?thesis using bernoulli nat_filtration_def by force qed lemma (in infinite_coin_toss_space) nat_filtration_singleton: assumes "pseudo_proj_True n w = w" shows "pseudo_proj_True n -`{w} \ sets (nat_filtration n)" proof - let ?pw = "pseudo_proj_True n -`{w}" have memset:"?pw \ sets M" using bernoulli assms bernoulli_stream_preimage[of _ _ "pseudo_proj_True n"] pseudo_proj_True_singleton[of w n] by simp have "pseudo_proj_True n -`?pw \ sets (nat_filtration n)" proof - have "pseudo_proj_True n -`?pw \ (space M) \ sets (nat_filtration n)" using memset by (metis fct_gen_subalgebra_sets_mem nat_filtration_def) moreover have "pseudo_proj_True n -`?pw \ (space M) = pseudo_proj_True n -`?pw" using bernoulli_stream_preimage[of _ _ "pseudo_proj_True n"] bernoulli by simp ultimately show "pseudo_proj_True n -`?pw \ sets (nat_filtration n)" by auto qed moreover have "pseudo_proj_True n -`?pw = ?pw" using pseudo_proj_True_proj by auto ultimately show ?thesis by simp qed lemma (in infinite_coin_toss_space) nat_filtration_pseudo_proj_True_measurable: shows "pseudo_proj_True n \ measurable (nat_filtration n) M" unfolding nat_filtration_def using bernoulli fct_gen_subalgebra_fct_measurable[of "pseudo_proj_True n" M M] pseudo_proj_True_measurable[of n] bernoulli_stream_space by auto lemma (in infinite_coin_toss_space) nat_filtration_comp_measurable: assumes "f \ measurable M N" and "f \ pseudo_proj_True n = f" shows "f \ measurable (nat_filtration n) N" by (metis assms measurable_comp nat_filtration_pseudo_proj_True_measurable) definition (in infinite_coin_toss_space) set_discriminating where "set_discriminating n f N \ (\w. f w \ f (pseudo_proj_True n w) \ (\A\sets N. (f w \ A) = (f (pseudo_proj_True n w) \ A)))" lemma (in infinite_coin_toss_space) set_discriminating_if: fixes f::"bool stream \ 'b::{t0_space}" assumes "f\ borel_measurable (nat_filtration n)" shows "set_discriminating n f borel" unfolding set_discriminating_def proof (intro allI impI) { fix w assume "f w \ (f \ (pseudo_proj_True n)) w" hence "\U. open U \ ( f w \ U = ((f \ (pseudo_proj_True n)) w \ U))" using separation_t0 by auto from this obtain A where "open A" and "f w\ A = ((f \ (pseudo_proj_True n)) w \ A)" by blast note Ah = this have "A\ sets borel" using Ah by simp hence "\A\sets borel. (f w \ A) = ((f \ (pseudo_proj_True n)) w \ A)" using Ah by blast } thus "\w. f w \ f (pseudo_proj_True n w) \ \A\sets borel. (f w \ A) = (f (pseudo_proj_True n w) \ A)" by simp qed lemma (in infinite_coin_toss_space) nat_filtration_not_borel_info: assumes "f\ measurable (nat_filtration n) N" and "set_discriminating n f N" shows "f\ pseudo_proj_True n = f" proof (rule ccontr) assume "f\ pseudo_proj_True n \ f" hence "\ w. (f\ (pseudo_proj_True n)) w \ f w" by auto from this obtain w where "(f\ (pseudo_proj_True n)) w \ f w" by blast note wh = this let ?x = "pseudo_proj_True n w" have "pseudo_proj_True n ?x = pseudo_proj_True n w" by (simp add: pseudo_proj_True_proj) have "f w \ f (pseudo_proj_True n w)" using wh by simp hence "\A \ sets N. ( f w \ A = (f ?x \ A))" using assms unfolding set_discriminating_def by simp from this obtain A where "A \ sets N" and "f w\ A = (f ?x \ A)" by blast note Ah = this have "f-` A\ (space (nat_filtration n)) \ sets (nat_filtration n)" using Ah assms borel_open measurable_sets by blast hence fn:"f-` A \ sets (nat_filtration n)" using nat_filtration_space by simp have "?x\ f-`A = (w \ f -`A)" using \pseudo_proj_True n ?x = pseudo_proj_True n w\ assms fct_gen_subalgebra_info[of "pseudo_proj_True n" M] bernoulli_stream_space by (metis Pi_I UNIV_I bernoulli fn nat_filtration_def streams_UNIV) also have "... = (f w \ A)" by simp also have "... = (f ?x \ A)" using Ah by simp also have "... = (?x \ f -`A)" by simp finally have "?x\ f-`A = (?x \ f -`A)" . thus False by simp qed lemma (in infinite_coin_toss_space) nat_filtration_info: fixes f::"bool stream \ 'b::{t0_space}" assumes "f\ borel_measurable (nat_filtration n)" shows "f\ pseudo_proj_True n = f" proof (rule nat_filtration_not_borel_info) show "f\ borel_measurable (nat_filtration n)" using assms by simp show "set_discriminating n f borel" using assms by (simp add: set_discriminating_if) qed lemma (in infinite_coin_toss_space) nat_filtration_not_borel_info': assumes "f\ measurable (nat_filtration n) N" and "set_discriminating n f N" shows "f\ pseudo_proj_False n = f" proof fix x have "(f \ pseudo_proj_False n) x = f (pseudo_proj_False n x)" by simp also have "... = f (pseudo_proj_True n (pseudo_proj_False n x))" using assms nat_filtration_not_borel_info by (metis comp_apply) also have "... = f (pseudo_proj_True n x)" proof - have "pseudo_proj_True n (pseudo_proj_False n x) = pseudo_proj_True n x" by (simp add: pseudo_proj_False_stake pseudo_proj_True_def) thus ?thesis by simp qed also have "... = f x" using assms nat_filtration_not_borel_info by (metis comp_apply) finally show "(f \ pseudo_proj_False n) x = f x" . qed lemma (in infinite_coin_toss_space) nat_filtration_info': fixes f::"bool stream \ 'b::{t0_space}" assumes "f\ borel_measurable (nat_filtration n)" shows "f\ pseudo_proj_False n = f" proof fix x have "(f \ pseudo_proj_False n) x = f (pseudo_proj_False n x)" by simp also have "... = f (pseudo_proj_True n (pseudo_proj_False n x))" using assms nat_filtration_info by (metis comp_apply) also have "... = f (pseudo_proj_True n x)" proof - have "pseudo_proj_True n (pseudo_proj_False n x) = pseudo_proj_True n x" by (simp add: pseudo_proj_False_stake pseudo_proj_True_def) thus ?thesis by simp qed also have "... = f x" using assms nat_filtration_info by (metis comp_apply) finally show "(f \ pseudo_proj_False n) x = f x" . qed lemma (in infinite_coin_toss_space) nat_filtration_borel_measurable_characterization: fixes f::"bool stream \ 'b::{t0_space}" assumes "f\ borel_measurable M" shows "f\ borel_measurable (nat_filtration n) \ f\ pseudo_proj_True n = f" using assms nat_filtration_comp_measurable nat_filtration_info by blast lemma (in infinite_coin_toss_space) nat_filtration_borel_measurable_init: fixes f::"bool stream \ 'b::{t0_space}" assumes "f\ borel_measurable (nat_filtration 0)" shows "f = (\w. f (sconst True))" proof fix w have "f w = f ((pseudo_proj_True 0) w)" using assms nat_filtration_info[of f 0] by (metis comp_apply) also have "... = f (sconst True)" by (simp add: pseudo_proj_True_def) finally show "f w = f (sconst True)" . qed lemma (in infinite_coin_toss_space) nat_filtration_Suc_sets: shows "sets (nat_filtration n) \ sets (nat_filtration (Suc n))" proof - { fix x assume "x\ {pseudo_proj_True n -` B \ space M |B. B \ sets M}" hence "\B. B \ sets M \ x = pseudo_proj_True n -` B \ space M" by auto from this obtain B where "B \ sets M" and "x = pseudo_proj_True n -` B \ space M" by blast note xhyps = this let ?Bim = "B\ (range (pseudo_proj_True n))" let ?preT = "(\n w. (pseudo_proj_True n) -` {w})" have "finite ?Bim" using pseudo_proj_True_finite_image by simp have "pseudo_proj_True n -`B \ (space M) = pseudo_proj_True n -`B" using bernoulli bernoulli_stream_preimage[of _ _ "pseudo_proj_True n"] by simp also have "... = pseudo_proj_True n -`?Bim" by auto also have "... = (\ w \ ?Bim.?preT n w)" by auto also have "... = (\ w \ ?Bim. (?preT (Suc n) w \ ?preT (Suc n) (pseudo_proj_False n w)))" by (simp add:pseudo_proj_True_inverse_induct) also have "... = (\ w \ ?Bim. ?preT (Suc n) w) \ (\ w \ ?Bim. ?preT (Suc n) (pseudo_proj_False n w))" by auto finally have tmpeq: "pseudo_proj_True n -`B \ (space M) = (\ w \ ?Bim. ?preT (Suc n) w) \ (\ w \ ?Bim. ?preT (Suc n) (pseudo_proj_False n w))" . have "(\ w \ ?Bim. ?preT (Suc n) w) \ sets (nat_filtration (Suc n))" using \finite ?Bim\ nat_filtration_singleton pseudo_proj_True_Suc_proj by auto moreover have "(\ w \ ?Bim. ?preT (Suc n) (pseudo_proj_False n w)) \ sets (nat_filtration (Suc n))" using \finite ?Bim\ by (simp add: nat_filtration_singleton pseudo_proj_True_Suc_False_proj sets.finite_UN) ultimately have "x \ sets (nat_filtration (Suc n))" using tmpeq xhyps by simp } note xmem = this have "sets (nat_filtration n) = sigma_sets (space M) {pseudo_proj_True n -` B \ space M |B. B \ sets M}" using bernoulli nat_filtration_sets by blast also have "... \ (nat_filtration (Suc n))" proof (rule sigma_algebra.sigma_sets_subset) show "{pseudo_proj_True n -` B \ space M |B. B \ sets M} \ sets (nat_filtration (Suc n))" using xmem by auto show "sigma_algebra (space M) (sets (nat_filtration (Suc n)))" by (metis bernoulli bernoulli_stream_space nat_filtration_space sets.sigma_algebra_axioms streams_UNIV) qed finally show ?thesis . qed lemma (in infinite_coin_toss_space) nat_filtration_subalgebra: shows "subalgebra M (nat_filtration n)" using bernoulli fct_gen_subalgebra_is_subalgebra nat_filtration_def pseudo_proj_True_measurable by metis lemma (in infinite_coin_toss_space) nat_discrete_filtration: shows "filtration M nat_filtration" unfolding filtration_def proof((intro conjI), (intro allI)+) { fix n let ?F = "nat_filtration n" show "subalgebra M ?F" using bernoulli fct_gen_subalgebra_is_subalgebra nat_filtration_def pseudo_proj_True_measurable by metis } note allrm = this show "\n m. n \ m \ subalgebra (nat_filtration m) (nat_filtration n)" proof (intro allI impI) let ?F = nat_filtration fix n::nat fix m show "n \ m \ subalgebra (nat_filtration m) (nat_filtration n)" proof (induct m) case (Suc m) have "subalgebra (?F (Suc m)) (?F m)" unfolding subalgebra_def proof (intro conjI) show speq: "space (?F m) = space (?F (Suc m))" by (simp add: nat_filtration_space) show "sets (?F m) \ sets (?F (Suc m))" using nat_filtration_Suc_sets by simp qed thus "n \ Suc m \ subalgebra (?F (Suc m)) (?F n)" using Suc using Suc.hyps le_Suc_eq subalgebra_def by fastforce next case 0 thus ?case by (simp add: subalgebra_def) qed qed qed lemma (in infinite_coin_toss_space) nat_info_filtration: shows "init_triv_filt M nat_filtration" unfolding init_triv_filt_def proof show "filtration M nat_filtration" by (simp add:nat_discrete_filtration) have img: "\ w\ space M. pseudo_proj_True 0 w = sconst True" unfolding pseudo_proj_True_def by simp show "sets (nat_filtration bot) = {{}, space M}" proof show "{{}, space M} \ sets (nat_filtration bot)" by (metis empty_subsetI insert_subset nat_filtration_subalgebra sets.empty_sets sets.top subalgebra_def) show "sets (nat_filtration bot) \ {{}, space M}" proof - have "\B \ sets (bernoulli_stream p). pseudo_proj_True 0 -` B \ space M \ {{}, space M}" proof fix B assume "B \ sets (bernoulli_stream p)" show "pseudo_proj_True 0 -` B \ space M \ {{}, space M}" proof (cases "sconst True \ B") case True hence "pseudo_proj_True 0 -` B \ space M = space M" using img by auto thus ?thesis by auto next case False hence "pseudo_proj_True 0 -` B \ space M = {}" using img by auto thus ?thesis by auto qed qed hence "{pseudo_proj_True 0 -` B \ space M |B. B \ sets (bernoulli_stream p)} \ {{}, space M}" by auto hence "sigma_sets (space (bernoulli_stream p)) {pseudo_proj_True 0 -` B \ space M |B. B \ sets (bernoulli_stream p)} \ {{}, space M}" using sigma_algebra.sigma_sets_subset[of "space (bernoulli_stream p)" "{{}, space M}"] by (simp add: bernoulli sigma_algebra_trivial) thus ?thesis by (simp add:nat_filtration_sets bot_nat_def) qed qed qed sublocale infinite_cts_filtration \ triv_init_disc_filtr_prob_space proof (unfold_locales, intro conjI) show "disc_filtr M F" unfolding disc_filtr_def using filtrationE2 nat_discrete_filtration nat_filtration_subalgebra natural_filtration by auto show "sets (F bot) = {{}, space M}" using nat_info_filtration natural_filtration unfolding init_triv_filt_def by simp qed lemma (in infinite_coin_toss_space) nat_filtration_vimage_finite: fixes f::"bool stream \ 'b::{t2_space}" assumes "f\ borel_measurable (nat_filtration n)" shows "finite (f`(space M))" using pseudo_proj_True_finite_image nat_filtration_info[of f n] by (metis assms bernoulli bernoulli_stream_space finite_imageI fun.set_map streams_UNIV) lemma (in infinite_coin_toss_space) nat_filtration_borel_measurable_simple: fixes f::"bool stream \ 'b::{t2_space}" assumes "f\ borel_measurable (nat_filtration n)" shows "simple_function M f" proof - have f1: "\m ma. (m::bool stream measure) \\<^sub>M (ma::'b measure) = {f \ space m \ space ma. \B. B \ sets ma \ f -` B \ space m \ sets m}" by (metis measurable_def) then have "f \ space (nat_filtration n) \ space borel \ (\B. B \ sets borel \ f -` B \ space (nat_filtration n) \ sets (nat_filtration n))" using assms by blast then have "f \ space M \ space borel \ (\B. B \ sets borel \ f -` B \ space M \ events)" by (metis (no_types) contra_subsetD nat_filtration_subalgebra subalgebra_def) then have "random_variable borel f" using f1 by blast then show ?thesis using assms nat_filtration_vimage_finite simple_function_borel_measurable by blast qed lemma (in infinite_coin_toss_space) nat_filtration_singleton_range_set: fixes f::"bool stream \ 'b::{t2_space}" assumes "f\ borel_measurable (nat_filtration n)" shows "\ A\ sets borel. range f \ A = {f x}" proof - let ?Ax = "range f - {f x}" have "range f = f`space M" using bernoulli bernoulli_stream_space by simp hence "finite ?Ax" using assms nat_filtration_vimage_finite by auto hence "\U. open U \ f x\ U \ U\ ?Ax = {}" by (simp add:open_except_set) then obtain U where "open U" and "f x\ U" and "U\ ?Ax = {}" by auto have "U \ sets borel" using \open U\ by simp have "range f \ U = {f x}" using \f x \ U\ \U\ ?Ax = {}\ by blast thus "\A\ sets borel. range f \ A = {f x}" using \U\ sets borel\ by auto qed lemma (in infinite_coin_toss_space) nat_filtration_borel_measurable_singleton: fixes f::"bool stream \ 'b::{t2_space}" assumes "f\ borel_measurable (nat_filtration n)" shows "f -`{f x} \ sets (nat_filtration n)" proof - let ?Ax = "f`space M - {f x}" have "finite ?Ax" using assms nat_filtration_vimage_finite by blast hence "\U. open U \ f x\ U \ U\ ?Ax = {}" by (simp add:open_except_set) then obtain U where "open U" and "f x\ U" and "U\ ?Ax = {}" by auto have "f x \ f ` space M" using bernoulli_stream_space bernoulli by simp hence "f`space M \ U = {f x}" using \f x\ U\ \U\ ?Ax = {}\ by blast hence "\A. open A\ f`space M \ A = {f x}" using \open U\ by auto from this obtain A where "open A" and inter: "f`space M \ A = {f x}" by auto have "A \ sets borel" using \open A\ by simp hence "f -`A \ space M \ sets (nat_filtration n)" using assms nat_filtration_space by (simp add: bernoulli bernoulli_stream_space in_borel_measurable_borel) hence "f -`A \ space M \ events" using nat_filtration_subalgebra by (meson subalgebra_def subset_eq) have "f -`{f x}\ space M = f -`A\ space M" proof have "f x\ A" using inter by auto thus "f -` {f x}\ space M \ f -` A\ space M" by auto show "f -` A\ space M \ f -` {f x}\ space M" proof fix y assume "y\ f-` A\ space M" hence "f y \ A\ f`space M" by simp hence "f y = f x" using inter by auto thus "y\ f -` {f x}\ space M" using \y\ f-` A\ space M\ by auto qed qed moreover have "f -`A \ space M \ (nat_filtration n)" using assms \A\ sets borel\ using \f -` A \ space M \ sets (nat_filtration n)\ by blast ultimately show ?thesis using bernoulli_stream_space bernoulli by simp qed lemma (in infinite_cts_filtration) borel_adapt_nat_filtration_info: fixes X::"nat \ bool stream \ 'b::{t0_space}" assumes "borel_adapt_stoch_proc F X" and "m \ n" shows "X m (pseudo_proj_True n w) = X m w" proof - have "X m \ borel_measurable (F n)" using assms natural_filtration using increasing_measurable_info by (metis adapt_stoch_proc_def) thus ?thesis using nat_filtration_info natural_filtration by (metis comp_apply) qed lemma (in infinite_coin_toss_space) nat_filtration_borel_measurable_integrable: assumes "f\ borel_measurable (nat_filtration n)" shows "integrable M f" proof - have "simple_function M f" using assms by (simp add: nat_filtration_borel_measurable_simple) moreover have "emeasure M {y \ space M. f y \ 0} \ \" by simp ultimately have "Bochner_Integration.simple_bochner_integrable M f" using Bochner_Integration.simple_bochner_integrable.simps by blast hence "has_bochner_integral M f (Bochner_Integration.simple_bochner_integral M f)" using has_bochner_integral_simple_bochner_integrable by auto thus ?thesis using integrable.simps by auto qed definition (in infinite_coin_toss_space) spick:: "bool stream \ nat \ bool \ bool stream" where "spick w n v = shift (stake n w) (v## sconst True)" lemma (in infinite_coin_toss_space) spickI: shows "stake n (spick w n v) = stake n w \ snth (spick w n v) n = v" by (simp add: spick_def stake_shift) lemma (in infinite_coin_toss_space) spick_eq_pseudo_proj_True: shows "spick w n True = pseudo_proj_True n w" unfolding spick_def pseudo_proj_True_def by (metis (full_types) id_apply siterate.code) lemma (in infinite_coin_toss_space) spick_eq_pseudo_proj_False: shows "spick w n False = pseudo_proj_False n w" unfolding spick_def pseudo_proj_False_def by simp lemma (in infinite_coin_toss_space) spick_pseudo_proj: shows "spick (pseudo_proj_True (Suc n) w) n v = spick w n v" by (metis pseudo_proj_True_proj_Suc pseudo_proj_True_stake spick_def) lemma (in infinite_coin_toss_space) spick_pseudo_proj_gen: shows "m < n \ spick (pseudo_proj_True n w) m v = spick w m v" by (metis Suc_leI pseudo_proj_True_proj pseudo_proj_True_prefix spick_pseudo_proj) lemma (in infinite_coin_toss_space) spick_nat_filtration_measurable: shows "(\w. spick w n v) \ measurable (nat_filtration n) M" proof (rule nat_filtration_comp_measurable) show "(\w. spick w n v) \ measurable M M" proof - let ?N = "bernoulli_stream p" have "id \ measurable ?N ?N" by simp moreover have "(\w. v## (sconst True)) \ measurable ?N ?N" using bernoulli_stream_space by simp ultimately show ?thesis using measurable_shift bernoulli p_gt_0 p_lt_1 unfolding bernoulli_stream_def spick_def by simp qed { fix w have "spick (pseudo_proj_True n w) n v = spick w n v" by (simp add: pseudo_proj_True_stake spick_def) } thus "(\w. spick w n v) \ pseudo_proj_True n = (\w. spick w n v)" by auto qed definition (in infinite_coin_toss_space) proj_rep_set: "proj_rep_set n = range (pseudo_proj_True n)" lemma (in infinite_coin_toss_space) proj_rep_set_finite: shows "finite (proj_rep_set n)" using pseudo_proj_True_finite_image by (simp add: proj_rep_set) lemma (in infinite_coin_toss_space) set_filt_contain: assumes "A\ sets (nat_filtration n)" and "w\ A" shows "pseudo_proj_True n -` {pseudo_proj_True n w} \ A" proof define indA where "indA = ((indicator A)::bool stream\real)" have "indA \ borel_measurable (nat_filtration n)" unfolding indA_def by (simp add: assms(1) borel_measurable_indicator) fix x assume "x \ pseudo_proj_True n -` {pseudo_proj_True n w}" have "indA x = indA (pseudo_proj_True n x)" using nat_filtration_info[symmetric, of "indicator A" n] \indA \ borel_measurable (nat_filtration n)\ unfolding indA_def by (metis comp_apply) also have "... = indA (pseudo_proj_True n w)" using \x \ pseudo_proj_True n -` {pseudo_proj_True n w}\ by simp also have "... = indA w" using nat_filtration_info[of "indicator A" n] \indA \ borel_measurable (nat_filtration n)\ unfolding indA_def by (metis comp_apply) also have "... = 1" using assms unfolding indA_def by simp finally have "indA x = 1" . thus "x\ A" unfolding indA_def by (simp add: indicator_eq_1_iff) qed lemma (in infinite_cts_filtration) measurable_range_rep: fixes f::"bool stream \ 'b::{t0_space}" assumes "f \ borel_measurable (nat_filtration n)" shows "range f = (\ r\(proj_rep_set n). {f(r)})" proof - have "f = f \ (pseudo_proj_True n)" using assms nat_filtration_info[of f n] by simp hence "range f = f `(proj_rep_set n)" by (metis fun.set_map proj_rep_set) also have "... = (\r\proj_rep_set n. {f r})" by blast finally show "range f = (\r\proj_rep_set n. {f r})" . qed lemma (in infinite_coin_toss_space) borel_measurable_stake: fixes f::"bool stream \ 'b::{t0_space}" assumes "f\ borel_measurable (nat_filtration n)" and "stake n w = stake n y" shows "f w = f y" proof - have "pseudo_proj_True n w = pseudo_proj_True n y" unfolding pseudo_proj_True_def using assms by simp thus ?thesis using assms nat_filtration_info by (metis comp_apply) qed subsubsection \Probability component\ text \The probability component permits to compute measures of subspaces in a straightforward way.\ definition prob_component where "prob_component (p::real) w n = (if (snth w n) then p else 1-p)" lemma prob_component_neq_zero: assumes "0 < p" and "p < 1" shows "prob_component p w n \ 0" using assms prob_component_def by auto lemma prob_component_measure: fixes x::"bool stream" assumes "0 \ p" and "p \ 1" shows "emeasure (measure_pmf (bernoulli_pmf p)) {snth x i} = prob_component p x i" unfolding prob_component_def using emeasure_pmf_single pmf_bernoulli_False pmf_bernoulli_True by (simp add: emeasure_pmf_single assms) lemma stake_preimage_measurable: fixes x::"bool stream" assumes "Suc 0 \ n" and "M = bernoulli_stream p" shows "{w\ space M. (stake n w = stake n x)} \ sets M" proof - let ?S = "{w\ space M. (stake n w = stake n x)}" have "?S = (\ i \ {0.. n-1}. {w\ space M. (snth w i = snth x i)})" using stake_inter_snth assms by simp moreover have "(\ i \ {0.. n-1}. {w\ space M. (snth w i = snth x i)}) \ sets M" proof - have "\ i \ n-1. {w\ space M. (snth w i = snth x i)} \ sets M" proof (intro allI impI) fix i assume "i \ n-1" thus "{w \ space M. w !! i = x !! i} \ sets M" proof - have "(\w. snth w i) \ measurable M (measure_pmf (bernoulli_pmf p))" using assms by (simp add: assms bernoulli_stream_def) thus ?thesis by simp qed qed thus ?thesis by auto qed ultimately show ?thesis by simp qed lemma snth_as_fct: fixes b assumes "M = bernoulli_stream p" shows "to_stream -` {w\ space M. snth w i = b} = {X::nat\bool. X i = b}" proof - let ?S = "{w\ space M. snth w i = b}" let ?PM = "(\i::nat. (measure_pmf (bernoulli_pmf p)))" have isps: "product_prob_space ?PM" by unfold_locales let ?Z = "{X::nat\bool. X i = b}" show "to_stream -`?S = ?Z" by (simp add: assms bernoulli_stream_space to_stream_def) qed lemma stake_as_fct: assumes "Suc 0 \ n" and "M= bernoulli_stream p" shows "to_stream -`{w\ space M. (stake n w = stake n x)} = {X::nat\bool. \i. 0 \ i \ i \ n-1 \ X i = snth x i}" proof - let ?S = "{w\ space M. (stake n w = stake n x)}" let ?Z = "{X::nat\bool. \i. 0 \ i \ i \ n-1 \ X i = snth x i}" have "to_stream -` ?S = to_stream -` (\ i \ {0.. n-1}. {w\ space M. (snth w i = snth x i)})" using \Suc 0 \ n\ stake_inter_snth by blast also have "... = (\ i \ {0.. n-1}. to_stream -`{w\ space M. (snth w i = snth x i)})" by auto also have "... = (\ i \ {0.. n-1}. {X::nat\bool. X i = snth x i})" using snth_as_fct assms by simp also have "... = ?Z" by auto finally show ?thesis . qed lemma bernoulli_stream_npref_prob: fixes x assumes "M = bernoulli_stream p" shows "emeasure M {w\ space M. (stake 0 w = stake 0 x)} = 1" proof - define S where "S = {w\ space M. (stake 0 w = stake 0 x)}" have "S = space M" unfolding S_def by simp thus ?thesis by (simp add: assms bernoulli_stream_def prob_space.emeasure_space_1 prob_space.prob_space_stream_space prob_space_measure_pmf) qed lemma bernoulli_stream_pref_prob: fixes x assumes "M =bernoulli_stream p" and "0 \ p" and "p \ 1" shows "n\ Suc 0\ emeasure M {w\ space M. (stake n w = stake n x)} = (\i\{0..n-1}. prob_component p x i)" proof - have "prob_space M" by (simp add: assms bernoulli_stream_def prob_space.prob_space_stream_space prob_space_measure_pmf) fix n::nat assume "n\ Suc 0" define S where "S = {w\ space M. (stake n w = stake n x)}" have s: "S \ sets M" unfolding S_def by (simp add: assms stake_preimage_measurable \Suc 0 \ n\) define PM where "PM = (\i::nat. (measure_pmf (bernoulli_pmf p)))" have isps: "product_prob_space PM" unfolding PM_def by unfold_locales define Z where "Z = {X::nat\bool. \i. 0 \ i \ i \ n-1 \ X i = snth x i}" let ?wPM = "Pi\<^sub>M UNIV PM" define imgSbs where "imgSbs = prod_emb UNIV PM {0..n-1} (Pi\<^sub>E {0..n-1} (\i::nat. {snth x i}))" have "space ?wPM = UNIV" using space_PiM unfolding PM_def by fastforce hence "(to_stream -` S \ (space ?wPM)) = to_stream -` S" by simp also have "... = Z" using stake_as_fct \Suc 0 \ n\ assms unfolding Z_def S_def by simp also have "... = imgSbs" proof { fix X assume "X \ imgSbs" hence "restrict X {0..n-1} \ (Pi\<^sub>E {0..n-1} (\i::nat. {snth x i}))" using prod_emb_iff[of X] unfolding imgSbs_def by simp hence "\i. 0 \ i \ i \ n-1 \ X i = snth x i" by auto hence "X \ Z" unfolding Z_def by simp } thus "imgSbs \ Z" by blast { fix X assume "X \ Z" hence "\i. 0 \ i \ i \ n-1 \ X i = snth x i" unfolding Z_def by simp hence "restrict X {0..n-1} \ (Pi\<^sub>E {0..n-1} (\i::nat. {snth x i}))" by simp moreover have "X \ extensional UNIV" by simp moreover have "\i \ UNIV. X i \ space (PM i)" unfolding PM_def by auto ultimately have "X \ imgSbs" using prod_emb_iff[of X] unfolding imgSbs_def by simp } thus "Z \ imgSbs" by auto qed finally have inteq: "(to_stream -` S \ (space ?wPM)) = imgSbs" . have "emeasure M S = emeasure ?wPM (to_stream -` S \ (space ?wPM))" using emeasure_distr[of "to_stream" ?wPM "M" S] measurable_to_stream[of "(measure_pmf (bernoulli_pmf p))"] s assms unfolding bernoulli_stream_def stream_space_def PM_def by (simp add: emeasure_distr) also have "... = emeasure ?wPM imgSbs" using inteq by simp also have "... = (\i\{0..n-1}. emeasure (PM i) ((\m::nat. {snth x m}) i))" using isps unfolding imgSbs_def PM_def by (auto simp add:product_prob_space.emeasure_PiM_emb) also have "... = (\i\{0..n-1}. prob_component p x i)" using prob_component_measure unfolding PM_def proof - have f1: "\N f. (\n. (n::nat) \ N \ \ 0 \ f n) \ (\n\N. ennreal (f n)) = ennreal (prod f N)" by (metis (no_types) prod_ennreal) obtain nn :: "(nat \ real) \ nat set \ nat" where f2: "\x0 x1. (\v2. v2 \ x1 \ \ 0 \ x0 v2) = (nn x0 x1 \ x1 \ \ 0 \ x0 (nn x0 x1))" by moura have f3: "\s n. if s !! n then prob_component p s n = p else p + prob_component p s n = 1" by (simp add: prob_component_def) { assume "prob_component p x (nn (prob_component p x) {0..n - 1}) \ p" then have "p + prob_component p x (nn (prob_component p x) {0..n - 1}) = 1" using f3 by metis then have "nn (prob_component p x) {0..n - 1} \ {0..n - 1} \ 0 \ prob_component p x (nn (prob_component p x) {0..n - 1})" using assms by linarith } then have "nn (prob_component p x) {0..n - 1} \ {0..n - 1} \ 0 \ prob_component p x (nn (prob_component p x) {0..n - 1})" using assms by linarith then have "(\n = 0..n - 1. ennreal (prob_component p x n)) = ennreal (prod (prob_component p x) {0..n - 1})" using f2 f1 by meson moreover have "(\n = 0..n - 1. ennreal (prob_component p x n)) = (\n = 0..n - 1. emeasure (measure_pmf (bernoulli_pmf p)) {x !! n})" using prob_component_measure[of p x] assms by simp ultimately show "(\n = 0..n - 1. emeasure (measure_pmf (bernoulli_pmf p)) {x !! n}) = ennreal (prod (prob_component p x) {0..n - 1})" using prob_component_measure[of p x] by simp qed finally show "emeasure M S = (\i\{0..n-1}. prob_component p x i)" . qed lemma bernoulli_stream_pref_prob': fixes x assumes "M = bernoulli_stream p" and "p \ 1" and "0 \ p" shows "emeasure M {w\ space M. (stake n w = stake n x)} = (\i\{0.. n") case True hence "emeasure M {w\ space M. (stake n w = stake n x)} = (\i\{0..n -1}. prob_component p x i)" using assms by (simp add: bernoulli_stream_pref_prob) moreover have "(\i\{0..n -1}. prob_component p x i) = (\i\{0..xa. xa \ {0.. prob_component p x xa = prob_component p x xa" by simp qed ultimately show ?thesis by simp next case False hence "n = 0" using False by simp have "{w\ space M. (stake n w = stake n x)} = space M" proof show "{w \ space M. stake n w = stake n x} \ space M" proof fix w assume "w\ {w \ space M. stake n w = stake n x}" thus "w \ space M" by auto qed show "space M \ {w \ space M. stake n w = stake n x}" proof fix w assume "w\ space M" have "stake 0 w = stake 0 x" by simp hence "stake n w = stake n x" using \n = 0\ by simp thus "w\ {w \ space M. stake n w = stake n x}" using \w\ space M\ by auto qed qed hence "emeasure M {w \ space M. stake n w = stake n x} = emeasure M (space M)" by simp also have "... = 1" using assms by (simp add: bernoulli_stream_def prob_space.emeasure_space_1 prob_space.prob_space_stream_space prob_space_measure_pmf) also have "... = (\i\{0..n = 0\ by simp finally show ?thesis . qed lemma bernoulli_stream_stake_prob: fixes x assumes "M = bernoulli_stream p" and "p \ 1" and "0 \ p" shows "measure M {w\ space M. (stake n w = stake n x)} = (\i\{0.. space M. (stake n w = stake n x)} = emeasure M {w\ space M. (stake n w = stake n x)}" by (metis (no_types, lifting) assms(1) bernoulli_stream_def emeasure_eq_ennreal_measure emeasure_space ennreal_one_neq_top neq_top_trans prob_space.emeasure_space_1 prob_space.prob_space_stream_space prob_space_measure_pmf) also have "... = (\i\{0.. 1" and "0 \ p" and "w\ range (pseudo_proj_True n)" shows "measure M (pseudo_proj_True n -`{w} \ space M) = (\i\{0.. space M = {x\ space M. (stake n w = stake n x)}" using assms(4) infinite_coin_toss_space.pseudo_proj_True_def infinite_coin_toss_space_axioms pseudo_proj_True_preimage_stake pseudo_proj_True_stake by force thus ?thesis using bernoulli_stream_stake_prob assms proof - have "pseudo_proj_True n w = w" using \w \ range (pseudo_proj_True n)\ pseudo_proj_True_proj by blast then show ?thesis using bernoulli bernoulli_stream_stake_prob p_gt_0 p_lt_1 pseudo_proj_True_preimage_stake_space by presburger qed qed lemma bernoulli_stream_element_prob_rec: fixes x assumes "M = bernoulli_stream p" and "0 \ p" and "p \ 1" shows "\ n. emeasure M {w\ space M. (stake (Suc n) w = stake (Suc n) x)} = (emeasure M {w\ space M. (stake n w = stake n x)} * prob_component p x n)" proof - fix n define S where "S = {w\ space M. (stake (Suc n) w = stake (Suc n) x)}" define precS where "precS = {w\ space M. (stake n w = stake n x)}" show "emeasure M S = emeasure M precS * prob_component p x n" proof (cases " n\ 0") case True hence "n=0" by simp hence "emeasure M S = (\i\{0..n}. prob_component p x i)" unfolding S_def using bernoulli_stream_pref_prob assms diff_Suc_1 le_refl by presburger also have "... = prob_component p x 0" using True by simp also have "... = emeasure M precS * prob_component p x n" using bernoulli_stream_npref_prob assms by (simp add: \n=0\ precS_def) finally show "emeasure M S = emeasure M precS * prob_component p x n" . next case False hence "n \ Suc 0" by simp hence "emeasure M S = (\i\{0..n}. prob_component p x i)" unfolding S_def using bernoulli_stream_pref_prob diff_Suc_1 le_refl assms by fastforce also have "... = (\i\{0..n-1}. prob_component p x i) * prob_component p x n" using \n \ Suc 0\ by (metis One_nat_def Suc_le_lessD Suc_pred prod.atLeast0_atMost_Suc) also have "... = emeasure M precS * prob_component p x n" using bernoulli_stream_pref_prob unfolding precS_def using \Suc 0 \ n\ ennreal_mult'' assms prob_component_def by auto finally show "emeasure M S = emeasure M precS * prob_component p x n" . qed qed lemma bernoulli_stream_element_prob_rec': fixes x assumes "M = bernoulli_stream p" and "0 \ p" and "p \ 1" shows "\ n. measure M {w\ space M. (stake (Suc n) w = stake (Suc n) x)} = (measure M {w\ space M. (stake n w = stake n x)} * prob_component p x n)" proof - fix n have "ennreal (measure M {w\ space M. (stake (Suc n) w = stake (Suc n) x)}) = emeasure M {w\ space M. (stake (Suc n) w = stake (Suc n) x)}" by (metis (no_types, lifting) assms(1) bernoulli_stream_def emeasure_eq_ennreal_measure emeasure_space ennreal_top_neq_one neq_top_trans prob_space.emeasure_space_1 prob_space.prob_space_stream_space prob_space_measure_pmf) also have "... = (emeasure M {w\ space M. (stake n w = stake n x)} * prob_component p x n)" using bernoulli_stream_element_prob_rec assms by simp also have "... = (measure M {w\ space M. (stake n w = stake n x)} * prob_component p x n)" proof - have "prob_space M" using assms(1) bernoulli_stream_def prob_space.prob_space_stream_space prob_space_measure_pmf by auto then show ?thesis by (simp add: ennreal_mult'' finite_measure.emeasure_eq_measure mult.commute prob_space_def) qed finally have "ennreal (measure M {w\ space M. (stake (Suc n) w = stake (Suc n) x)}) = (measure M {w\ space M. (stake n w = stake n x)} * prob_component p x n)" . thus "measure M {w\ space M. (stake (Suc n) w = stake (Suc n) x)} = (measure M {w\ space M. (stake n w = stake n x)} * prob_component p x n)" using assms prob_component_def by auto qed lemma (in infinite_coin_toss_space) bernoulli_stream_pseudo_prob_rec': fixes x assumes "pseudo_proj_True n x = x" shows "measure M (pseudo_proj_True (Suc n) -`{x}) = (measure M (pseudo_proj_True n-`{x}) * prob_component p x n)" proof - have "pseudo_proj_True (Suc n) -`{x} = {w. (stake (Suc n) w = stake (Suc n) x)}" using pseudo_proj_True_preimage_stake assms by (metis pseudo_proj_True_Suc_proj) moreover have "pseudo_proj_True n -`{x} = {w. (stake n w = stake n x)}" using pseudo_proj_True_preimage_stake assms by simp ultimately show ?thesis using assms bernoulli_stream_element_prob_rec' by (simp add: bernoulli bernoulli_stream_space p_gt_0 p_lt_1) qed lemma (in infinite_coin_toss_space) bernoulli_stream_pref_prob_pos: fixes x assumes "0 < p" and "p < 1" shows "emeasure M {w\ space M. (stake n w = stake n x)} > 0" proof (induct n) case 0 hence "emeasure M {w\ space M. (stake 0 w = stake 0 x)} = 1" using bernoulli_stream_npref_prob[of M p x] bernoulli by simp thus ?case by simp next case (Suc n) have "emeasure M {w \ space M. stake (Suc n) w = stake (Suc n) x} = (emeasure M {w\ space M. (stake n w = stake n x)} * prob_component p x n)" using bernoulli_stream_element_prob_rec bernoulli p_gt_0 p_lt_1 by simp thus ?case using Suc using assms p_gt_0 p_lt_1 prob_component_def by (simp add: ennreal_zero_less_mult_iff) qed lemma (in infinite_coin_toss_space) bernoulli_stream_pref_prob_neq_zero: fixes x assumes "0 < p" and "p < 1" shows "emeasure M {w\ space M. (stake n w = stake n x)} \ 0" proof (induct n) case 0 hence "emeasure M {w\ space M. (stake 0 w = stake 0 x)} = 1" using bernoulli_stream_npref_prob[of M p x] bernoulli by simp thus ?case by simp next case (Suc n) have "emeasure M {w \ space M. stake (Suc n) w = stake (Suc n) x} = (emeasure M {w\ space M. (stake n w = stake n x)} * prob_component p x n)" using bernoulli_stream_element_prob_rec bernoulli assms by simp thus ?case using Suc using assms p_gt_0 p_lt_1 prob_component_def by auto qed lemma (in infinite_coin_toss_space) pseudo_proj_element_prob_pref: assumes "w\ range (pseudo_proj_True n)" shows "emeasure M {y\ space M. \x \ (pseudo_proj_True n -`{w}). y = c ## x} = prob_component p (c##w) 0 * emeasure M ((pseudo_proj_True n) -`{w} \ space M)" proof - have "pseudo_proj_True n w = w" using assms pseudo_proj_True_def pseudo_proj_True_stake by auto have "pseudo_proj_True (Suc n) (c##w) = c##w" using assms pseudo_proj_True_def pseudo_proj_True_stake by auto have "{y\ space M. \x \ (pseudo_proj_True n -`{w}). y = c ## x} = pseudo_proj_True (Suc n) -`{c##w} \ space M" proof show "{y\ space M. \x\pseudo_proj_True n -` {w}. y = c ## x} \ pseudo_proj_True (Suc n) -` {c ## w} \ space M" proof fix y assume "y\ {y\ space M. \x\pseudo_proj_True n -` {w}. y = c ## x}" hence "y\ space M" and "\x \ pseudo_proj_True n -` {w}. y = c ## x" by auto from this obtain x where "x\ pseudo_proj_True n -` {w}" and "y = c## x" by auto have "pseudo_proj_True (Suc n) y = c##w" using \x\ pseudo_proj_True n -` {w}\ \y = c## x\ unfolding pseudo_proj_True_def by simp thus "y \ pseudo_proj_True (Suc n) -` {c ## w} \ space M" using \y\ space M\ by auto qed show "pseudo_proj_True (Suc n) -` {c ## w} \ space M \ {y\ space M. \x\pseudo_proj_True n -` {w}. y = c ## x}" proof fix y assume "y \ pseudo_proj_True (Suc n) -` {c ## w} \ space M" hence "pseudo_proj_True (Suc n) y = c##w" and "y\ space M" by auto have "pseudo_proj_True n (stl y) = pseudo_proj_True n w" proof (rule pseudo_proj_True_snth') have "pseudo_proj_True (Suc n) (c##w) = c##w" using \pseudo_proj_True (Suc n) (c##w) = c##w\ . also have "... = pseudo_proj_True (Suc n) y" using \pseudo_proj_True (Suc n) y = c##w\ by simp finally have "pseudo_proj_True (Suc n) (c##w) = pseudo_proj_True (Suc n) y" . hence "\i. Suc i \ Suc n \ (c##w)!! i = y!! i" by (simp add: pseudo_proj_True_snth) thus "\i. Suc i \ n \ stl y !! i = w !! i" by fastforce qed also have "... = w" using assms pseudo_proj_True_def pseudo_proj_True_stake by auto finally have "pseudo_proj_True n (stl y) = w" . hence "stl y \ (pseudo_proj_True n) -` {w}" by simp moreover have "y = c##(stl y)" proof - have "stake (Suc n) y = stake (Suc n) (pseudo_proj_True (Suc n) y)" unfolding pseudo_proj_True_def using pseudo_proj_True_def pseudo_proj_True_stake by auto hence "shd y = shd (pseudo_proj_True (Suc n) y)" by simp also have "... = shd (c##w)" using \pseudo_proj_True (Suc n) y = c##w\ by simp also have "... = c" by simp finally have "shd y = c" . thus ?thesis by (simp add: stream_eq_Stream_iff) qed ultimately show "y\ {y\ space M. \x\pseudo_proj_True n -` {w}. y = c ## x}" using \y\ space M\ by auto qed qed hence "emeasure M {y\ space M. \x \ (pseudo_proj_True n -`{w}). y = c ## x} = emeasure M (pseudo_proj_True (Suc n) -`{c##w}\ space M)" by simp also have "... = emeasure M {y\ space M. stake (Suc n) y = stake (Suc n) (c##w)}" using \pseudo_proj_True (Suc n) (c##w) = c##w\ by (simp add:pseudo_proj_True_preimage_stake_space) also have "... = (\i\{0..n}. prob_component p (c##w) i)" using bernoulli_stream_pref_prob[of M p "Suc n" "c##w"] bernoulli p_lt_1 p_gt_0 diff_Suc_1 le_refl by simp also have "... = prob_component p (c##w) 0 * (\i\{1..n}. prob_component p (c##w) i)" by (simp add: decompose_init_prod) also have "... = prob_component p (c##w) 0 * (\i\{1..< Suc n}. prob_component p (c##w) i)" proof - have "(\i\{1..n}. prob_component p (c##w) i) = (\i\{1..< Suc n}. prob_component p (c##w) i)" proof (rule prod.cong) show "{1..n} = {1..x. x \ {1.. prob_component p (c ## w) x = prob_component p (c ## w) x" by simp qed thus ?thesis by simp qed also have "... = prob_component p (c##w) 0 * (\i\{0..< n}. prob_component p w i)" proof - have "(\i\{1..< Suc n}. prob_component p (c##w) i) = (\i\{0..< n}. prob_component p w i)" proof (rule prod.reindex_cong) show "inj_on (\n. Suc n) {0..x. x \ {0..< n} \ prob_component p (c ## w) (Suc x) = prob_component p w x" by (simp add: prob_component_def) qed thus ?thesis by simp qed also have "... = prob_component p (c##w) 0 * emeasure M {y \ space M. stake n y = stake n w}" using bernoulli_stream_pref_prob'[symmetric, of M p w n] ennreal_mult' p_gt_0 p_lt_1 bernoulli prob_component_def by auto also have "... = prob_component p (c##w) 0 * emeasure M (pseudo_proj_True n -` {w} \ space M)" using pseudo_proj_True_preimage_stake_space \pseudo_proj_True n w = w\ by (simp add: pseudo_proj_True_preimage_stake_space) finally show ?thesis . qed subsubsection \Filtration equivalence for the natural filtration\ lemma (in infinite_coin_toss_space) nat_filtration_null_set: assumes "A\ sets (nat_filtration n)" and "0 < p" and "p < 1" and "emeasure M A = 0" shows "A = {}" proof (rule ccontr) assume "A\ {}" hence "\w. w\ A" by auto from this obtain w where "w \ A" by auto hence inc: "pseudo_proj_True n -` {pseudo_proj_True n w} \ A" using assms by (simp add: set_filt_contain) have "0 < emeasure M {x\ space M. (stake n x = stake n (pseudo_proj_True n w))}" using assms by (simp add: bernoulli_stream_pref_prob_pos) also have "... = emeasure M (pseudo_proj_True n -` {pseudo_proj_True n w})" using pseudo_proj_True_preimage_stake pseudo_proj_True_proj bernoulli bernoulli_stream_space by simp also have "... \ emeasure M A" proof (rule emeasure_mono, (simp add: inc)) show "A \ events" using assms nat_discrete_filtration unfolding filtration_def subalgebra_def by auto qed finally have "0 < emeasure M A" . thus False using assms by simp qed lemma (in infinite_coin_toss_space) nat_filtration_AE_zero: fixes f::"bool stream \ real" assumes "AE w in M. f w = 0" and "f\ borel_measurable (nat_filtration n)" and "0 < p" and "p < 1" shows "\w. f w = 0" proof - from \AE w in M. f w = 0\ obtain N' where Nprops: "{w\ space M. \f w = 0} \ N'" "N'\ sets M" "emeasure M N' = 0" by (force elim:AE_E) have "{w\ space M. f w < 0} \ sets (nat_filtration n)" by (metis (no_types) assms(2) bernoulli bernoulli_stream_space borel_measurable_iff_less nat_filtration_space streams_UNIV) moreover have "{w\ space M. f w > 0} \ sets (nat_filtration n)" by (metis (no_types) assms(2) bernoulli bernoulli_stream_space borel_measurable_iff_greater nat_filtration_space streams_UNIV) moreover have "{w\ space M. \f w = 0} = {w\ space M. f w < 0} \ {w\ space M. f w > 0}" by auto ultimately have "{w\ space M. \f w = 0} \ sets (nat_filtration n)" by auto hence "emeasure M {w\ space M. \f w = 0} = 0" using Nprops by (metis (no_types, lifting) emeasure_eq_0) hence "{w\ space M. \f w = 0} = {}" using \{w\ space M. \f w = 0} \ sets (nat_filtration n)\ nat_filtration_null_set[of "{w \ space M. f w \ 0}" n] assms by simp hence "{w. f w\ 0} = {}" by (simp add:bernoulli_stream_space bernoulli) thus ?thesis by auto qed lemma (in infinite_coin_toss_space) nat_filtration_AE_eq: fixes f::"bool stream \ real" assumes "AE w in M. f w = g w" and "0 < p" and "p < 1" and "f\ borel_measurable (nat_filtration n)" and "g\ borel_measurable (nat_filtration n)" shows "f w = g w" proof - define diff where "diff = (\w. f w - g w)" have "AE w in M. diff w = 0" proof (rule AE_mp) show "AE w in M. f w = g w" using assms by simp show "AE w in M. f w = g w \ diff w = 0" by (rule AE_I2, intro impI, (simp add: diff_def)) qed have "\w. diff w = 0" proof (rule nat_filtration_AE_zero) show "AE w in M. diff w = 0" using \AE w in M. diff w = 0\ . show "diff \ borel_measurable (nat_filtration n)" using assms unfolding diff_def by simp show "0 < p" and "p < 1" using assms by auto qed thus "f w = g w" unfolding diff_def by auto qed lemma (in infinite_coin_toss_space) bernoulli_stream_equiv: assumes "N = bernoulli_stream q" and "0 < p" and "p < 1" and "0 < q" and "q < 1" shows "filt_equiv nat_filtration M N" unfolding filt_equiv_def proof (intro conjI) have "sets (stream_space (measure_pmf (bernoulli_pmf p))) = sets (stream_space (measure_pmf (bernoulli_pmf q)))" by (rule sets_stream_space_cong, simp) thus "events = sets N" using assms bernoulli unfolding bernoulli_stream_def by simp show "filtration M nat_filtration" by (simp add:nat_discrete_filtration) show "\t A. A \ sets (nat_filtration t) \ (emeasure M A = 0) = (emeasure N A = 0)" proof (intro allI impI) fix n fix A assume "A\ sets (nat_filtration n)" show "(emeasure M A = 0) = (emeasure N A = 0)" proof { assume "emeasure M A = 0" hence "A = {}" using \A\ sets (nat_filtration n)\ using assms by (simp add:nat_filtration_null_set) thus "emeasure N A = 0" by simp } { assume "emeasure N A = 0" hence "A = {}" using \A\ sets (nat_filtration n)\ infinite_coin_toss_space.nat_filtration_null_set[of q N A n] assms using \events = sets N\ bernoulli bernoulli_stream_space infinite_coin_toss_space.nat_filtration_sets infinite_coin_toss_space_def nat_filtration_sets by force thus "emeasure M A = 0" by simp } qed qed qed lemma (in infinite_coin_toss_space) bernoulli_nat_filtration: assumes "N = bernoulli_stream q" and "0 < q" and "q < 1" and "0 < p" and "p < 1" shows "infinite_cts_filtration q N nat_filtration" proof (unfold_locales) have "0 < q" using assms by simp thus "0 \ q" by simp have "q < 1" using assms by simp thus "q \ 1" by simp show "N = bernoulli_stream q" using assms by simp show "nat_filtration = infinite_coin_toss_space.nat_filtration N" proof - have "filt_equiv nat_filtration M N" using \q < 1\ \0 < q\ by (simp add: assms bernoulli_stream_equiv) hence "sets M = sets N" unfolding filt_equiv_def by simp hence "space M = space N" using sets_eq_imp_space_eq by auto have "\m. nat_filtration m = infinite_coin_toss_space.nat_filtration N m" proof fix m have "infinite_coin_toss_space.nat_filtration N m = fct_gen_subalgebra N N (pseudo_proj_True m)" using \0 \ q\ \N = bernoulli_stream q\ \q \ 1\ infinite_coin_toss_space.intro infinite_coin_toss_space.nat_filtration_def by blast thus "nat_filtration m = infinite_coin_toss_space.nat_filtration N m" unfolding nat_filtration_def using fct_gen_subalgebra_cong[of M N M N "pseudo_proj_True m"] \sets M = sets N\ \space M = space N\ by simp qed thus ?thesis by auto qed qed subsubsection \More results on the projection function\ lemma (in infinite_coin_toss_space) pseudo_proj_True_Suc_prefix: shows "pseudo_proj_True (Suc n) w = (w!!0)## pseudo_proj_True n (stl w)" proof - have "pseudo_proj_True (Suc n) w = shift (stake (Suc n) w) (sconst True)" unfolding pseudo_proj_True_def by simp also have "... = shift (w!!0 # (stake n (stl w))) (sconst True)" by simp also have "... = w!!0 ## shift (stake n (stl w)) (sconst True)" by simp also have "... = w!!0 ## pseudo_proj_True n (stl w)" unfolding pseudo_proj_True_def by simp finally show ?thesis . qed lemma (in infinite_coin_toss_space) pseudo_proj_True_img: assumes "pseudo_proj_True n w = w" shows "w\ range (pseudo_proj_True n)" by (metis assms rangeI) lemma (in infinite_coin_toss_space) sconst_if: assumes "\n. snth w n = True" shows "w = sconst True" proof - obtain nn :: "(bool \ bool) \ bool stream \ bool stream \ nat" where "\p s n sa sb na pa sc pb sd se. (\ p (s !! n::bool) \ smap p s \ sa \ sa !! n) \ (\ sb !! na \ smap pa sc \ sb \ pa (sc !! na::bool)) \ (\ pb (sd !! nn pb sd se) \ \ se !! nn pb sd se \ smap pb sd = se)" using smap_alt by moura then show ?thesis by (metis (no_types) assms eq_id_iff id_funpow snth_siterate) qed lemma (in infinite_coin_toss_space) pseudo_proj_True_suc_img_pref: shows "range (pseudo_proj_True (Suc n)) = {y. \w \ range (pseudo_proj_True n). y = True ## w} \ {y. \w \ range (pseudo_proj_True n). y = False ## w}" proof show "range (pseudo_proj_True (Suc n)) \ {y. \w \ range (pseudo_proj_True n). y = True ## w} \ {y. \w \ range (pseudo_proj_True n). y = False ## w}" proof fix x assume "x \ range (pseudo_proj_True (Suc n))" hence "x = pseudo_proj_True (Suc n) x" using pseudo_proj_True_proj by auto define xp where "xp = stl x" have "xp = stl (shift (stake (Suc n) x) (sconst True))" using \x = pseudo_proj_True (Suc n) x\ unfolding xp_def pseudo_proj_True_def by simp also have "... = shift ((stake n (stl x))) (sconst True)" by simp finally have "xp = shift ((stake n (stl x))) (sconst True)" . hence "xp \ range (pseudo_proj_True n)" using pseudo_proj_True_def by auto show "x\ {y. \w \ range (pseudo_proj_True n) . y = True ## w} \ {y. \w \ range (pseudo_proj_True n). y = False ## w}" proof (cases "snth x 0") case True have "x = True ## xp" unfolding xp_def using True by (simp add: stream_eq_Stream_iff) hence "x \ {y. \w \ range (pseudo_proj_True n). y = True ## w}" using \xp \ range (pseudo_proj_True n)\ by auto thus ?thesis by auto next case False have "x = False ## xp" unfolding xp_def using False by (simp add: stream_eq_Stream_iff) hence "x \ {y. \w \ range (pseudo_proj_True n). y = False ## w}" using \xp \ range (pseudo_proj_True n)\ by auto thus ?thesis by auto qed qed have "{y. \w \ range (pseudo_proj_True n) . y = True ## w} \ range (pseudo_proj_True (Suc n))" proof fix y assume "y \ {y. \w \ range (pseudo_proj_True n) . y = True ## w}" hence "\w. w \ range (pseudo_proj_True n) \ y = True ## w" by auto from this obtain w where "w\ range (pseudo_proj_True n)" and "y = True ## w" by auto have "w = pseudo_proj_True n w" using pseudo_proj_True_proj \w\ range (pseudo_proj_True n)\ by auto hence "y = True ## (shift (stake n w) (sconst True))" using \y = True ## w\ unfolding pseudo_proj_True_def by simp also have "... = shift (stake (Suc n) (True ## w)) (sconst True)" by simp also have "... = pseudo_proj_True (Suc n) (True ## w)" unfolding pseudo_proj_True_def by simp finally have "y = pseudo_proj_True (Suc n) (True##w)" . thus "y \ range (pseudo_proj_True (Suc n))" by simp qed moreover have "{y. \w \ range (pseudo_proj_True n) . y = False ## w} \ range (pseudo_proj_True (Suc n))" proof fix y assume "y \ {y. \w \ range (pseudo_proj_True n) . y = False ## w}" hence "\w. w \ range (pseudo_proj_True n) \ y = False ## w" by auto from this obtain w where "w\ range (pseudo_proj_True n)" and "y = False ## w" by auto have "w = pseudo_proj_True n w" using pseudo_proj_True_proj \w\ range (pseudo_proj_True n)\ by auto hence "y = False ## (shift (stake n w) (sconst True))" using \y = False ## w\ unfolding pseudo_proj_True_def by simp also have "... = shift (stake (Suc n) (False ## w)) (sconst True)" by simp also have "... = pseudo_proj_True (Suc n) (False ## w)" unfolding pseudo_proj_True_def by simp finally have "y = pseudo_proj_True (Suc n) (False##w)" . thus "y \ range (pseudo_proj_True (Suc n))" by simp qed ultimately show "{y. \w \ range (pseudo_proj_True n) . y = True ## w} \ {y. \w \ range (pseudo_proj_True n) . y = False ## w} \ range (pseudo_proj_True (Suc n))" by simp qed lemma (in infinite_coin_toss_space) reindex_pseudo_proj: shows "(\w\range (pseudo_proj_True n). f (c ## w)) = (\y\{y. \w \ range (pseudo_proj_True n). y = c ## w}.f y)" proof (rule sum.reindex_cong[symmetric],auto) define ccons where "ccons = (\w. c## w)" show "inj_on ccons (range (pseudo_proj_True n))" proof fix x y assume "x\ range (pseudo_proj_True n)" and "y\ range (pseudo_proj_True n)" and "ccons x = ccons y" hence "c##x = c##y" unfolding ccons_def by simp thus "x = y" by simp qed qed lemma (in infinite_coin_toss_space) pseudo_proj_True_imp_False: assumes "pseudo_proj_True n w = pseudo_proj_True n x" shows "pseudo_proj_False n w = pseudo_proj_False n x" by (metis assms pseudo_proj_False_def pseudo_proj_True_stake) lemma (in infinite_coin_toss_space) pseudo_proj_Suc_prefix: assumes "pseudo_proj_True n w = pseudo_proj_True n x" shows "pseudo_proj_True (Suc n) w \ {pseudo_proj_True n x, pseudo_proj_False n x}" proof - have "pseudo_proj_False n w = pseudo_proj_False n x" using assms pseudo_proj_True_imp_False[of n w x] by simp hence "{pseudo_proj_True n w, pseudo_proj_False n w} = {pseudo_proj_True n x, pseudo_proj_False n x}" using assms by simp thus ?thesis using pseudo_proj_True_suc_img[of n w] by simp qed lemma (in infinite_coin_toss_space) pseudo_proj_Suc_preimage: shows "range (pseudo_proj_True (Suc n)) \ (pseudo_proj_True n) -` {pseudo_proj_True n x} = {pseudo_proj_True n x, pseudo_proj_False n x}" proof show "range (pseudo_proj_True (Suc n)) \ pseudo_proj_True n -` {pseudo_proj_True n x} \ {pseudo_proj_True n x, pseudo_proj_False n x}" proof fix w assume "w\ range (pseudo_proj_True (Suc n)) \ pseudo_proj_True n -` {pseudo_proj_True n x}" hence "w\ range (pseudo_proj_True (Suc n))" and "w\ pseudo_proj_True n -` {pseudo_proj_True n x}" by auto hence "pseudo_proj_True n w = pseudo_proj_True n x" by simp have "w = pseudo_proj_True (Suc n) w" using \w\ range (pseudo_proj_True (Suc n))\ using pseudo_proj_True_proj by auto also have "... \ {pseudo_proj_True n x, pseudo_proj_False n x}" using \pseudo_proj_True n w = pseudo_proj_True n x\ pseudo_proj_Suc_prefix by simp finally show "w \ {pseudo_proj_True n x, pseudo_proj_False n x}" . qed show "{pseudo_proj_True n x, pseudo_proj_False n x} \ range (pseudo_proj_True (Suc n)) \ pseudo_proj_True n -` {pseudo_proj_True n x}" proof - have "pseudo_proj_True n x \ range (pseudo_proj_True (Suc n)) \ pseudo_proj_True n -` {pseudo_proj_True n x}" by (simp add: pseudo_proj_True_Suc_proj pseudo_proj_True_img pseudo_proj_True_proj) moreover have "pseudo_proj_False n x \ range (pseudo_proj_True (Suc n)) \ pseudo_proj_True n -` {pseudo_proj_True n x}" by (metis (no_types, lifting) Int_iff UnI2 infinite_coin_toss_space.pseudo_proj_False_def infinite_coin_toss_space_axioms pseudo_proj_True_Suc_False_proj pseudo_proj_True_inverse_induct pseudo_proj_True_stake rangeI singletonI vimage_eq) ultimately show ?thesis by auto qed qed lemma (in infinite_cts_filtration) f_borel_Suc_preimage: assumes "f\ measurable (F n) N" and "set_discriminating n f N" shows "range (pseudo_proj_True (Suc n)) \ f -` {f x} = (pseudo_proj_True n) ` (f -` {f x}) \ (pseudo_proj_False n) ` (f -` {f x})" proof - have "range (pseudo_proj_True (Suc n)) \ f -` {f x} = (\ w\ {y. f y = f x}.{pseudo_proj_True n w, pseudo_proj_False n w})" proof show "range (pseudo_proj_True (Suc n)) \ f -` {f x} \ (\w\{y. f y = f x}. {pseudo_proj_True n w, pseudo_proj_False n w})" proof fix w assume "w\ range (pseudo_proj_True (Suc n)) \ f -` {f x}" hence "w\ range (pseudo_proj_True (Suc n))" and "w\ f -` {f x}" by auto hence "f w = f x" by simp hence "w\ {y. f y = f x}" by simp have "w = pseudo_proj_True (Suc n) w" using \w\ range (pseudo_proj_True (Suc n))\ using pseudo_proj_True_proj by auto also have "... \ {pseudo_proj_True n w, pseudo_proj_False n w}" using pseudo_proj_Suc_prefix by auto also have "... \ (\w\{y. f y = f x}. {pseudo_proj_True n w, pseudo_proj_False n w})" using \w\ {y. f y = f x}\ by auto finally show "w \ (\w\{y. f y = f x}. {pseudo_proj_True n w, pseudo_proj_False n w})" . qed show "(\w\{y. f y = f x}. {pseudo_proj_True n w, pseudo_proj_False n w}) \ range (pseudo_proj_True (Suc n)) \ f -` {f x}" proof fix w assume "w \ (\w\{y. f y = f x}. {pseudo_proj_True n w, pseudo_proj_False n w})" hence "\y. f y = f x \ w\ {pseudo_proj_True n y, pseudo_proj_False n y}" by auto from this obtain y where "f y = f x" and "w\ {pseudo_proj_True n y, pseudo_proj_False n y}" by auto hence "w = pseudo_proj_True n y \ w = pseudo_proj_False n y" by auto show "w \ range (pseudo_proj_True (Suc n)) \ f -` {f x}" proof (cases "w = pseudo_proj_True n y") case True hence "f w = f y" using assms nat_filtration_not_borel_info natural_filtration by (metis comp_apply) thus ?thesis using \f y = f x\ by (simp add: True pseudo_proj_True_Suc_proj pseudo_proj_True_img) next case False hence "f w = f y" using assms nat_filtration_not_borel_info natural_filtration by (metis Int_iff \w \ {pseudo_proj_True n y, pseudo_proj_False n y}\ comp_apply pseudo_proj_Suc_preimage singletonD vimage_eq) thus ?thesis using \f y = f x\ using \w \ {pseudo_proj_True n y, pseudo_proj_False n y}\ pseudo_proj_Suc_preimage by auto qed qed qed also have "... = (\ w\ {y. f y = f x}.{pseudo_proj_True n w}) \ (\ w\ {y. f y = f x}.{pseudo_proj_False n w})" by auto also have "... = (pseudo_proj_True n) ` {y. f y = f x} \ (pseudo_proj_False n) `{y. f y = f x}" by auto also have "... = (pseudo_proj_True n) ` (f -` {f x}) \ (pseudo_proj_False n) ` (f -` {f x})" by auto finally show ?thesis . qed lemma (in infinite_cts_filtration) pseudo_proj_preimage: assumes "g\ measurable (F n) N" and "set_discriminating n g N" shows "pseudo_proj_True n -` (g -` {g z}) = pseudo_proj_True n -` (pseudo_proj_True n `(g -` {g z}))" proof show "pseudo_proj_True n -` g -` {g z} \ pseudo_proj_True n -` pseudo_proj_True n ` g -` {g z}" proof fix w assume "w\ pseudo_proj_True n -` g -` {g z}" have "pseudo_proj_True n w = pseudo_proj_True n (pseudo_proj_True n w)" by (simp add: pseudo_proj_True_proj) also have "... \ pseudo_proj_True n `(g -` {g z})" using \w\ pseudo_proj_True n -` g -` {g z}\ by simp finally have "pseudo_proj_True n w \ pseudo_proj_True n `(g -` {g z})" . thus "w\ pseudo_proj_True n -` (pseudo_proj_True n `(g -` {g z}))" by simp qed show "pseudo_proj_True n -` pseudo_proj_True n ` g -` {g z} \ pseudo_proj_True n -` g -` {g z}" proof fix w assume "w \ pseudo_proj_True n -` pseudo_proj_True n ` g -` {g z}" hence "\y. pseudo_proj_True n w = pseudo_proj_True n y \ g y = g z" by auto from this obtain y where "pseudo_proj_True n w = pseudo_proj_True n y" and "g y = g z" by auto have "g (pseudo_proj_True n w) = g (pseudo_proj_True n y)" using \pseudo_proj_True n w = pseudo_proj_True n y\ by simp also have "... = g y" using assms nat_filtration_not_borel_info natural_filtration by (metis comp_apply) also have "... = g z" using \g y = g z\ . finally have "g (pseudo_proj_True n w) = g z" . thus "w\ pseudo_proj_True n -` g -` {g z}" by simp qed qed lemma (in infinite_cts_filtration) borel_pseudo_proj_preimage: fixes g::"bool stream \ 'b::{t0_space}" assumes "g\ borel_measurable (F n)" shows "pseudo_proj_True n -` (g -` {g z}) = pseudo_proj_True n -` (pseudo_proj_True n `(g -` {g z}))" using pseudo_proj_preimage[of g n borel z] set_discriminating_if[of g n] natural_filtration assms by simp lemma (in infinite_cts_filtration) pseudo_proj_False_preimage: assumes "g\ measurable (F n) N" and "set_discriminating n g N" shows "pseudo_proj_False n -` (g -` {g z}) = pseudo_proj_False n -` (pseudo_proj_False n `(g -` {g z}))" proof show "pseudo_proj_False n -` g -` {g z} \ pseudo_proj_False n -` pseudo_proj_False n ` g -` {g z}" proof fix w assume "w\ pseudo_proj_False n -` g -` {g z}" have "pseudo_proj_False n w = pseudo_proj_False n (pseudo_proj_False n w)" using pseudo_proj_False_def pseudo_proj_False_stake by auto also have "... \ pseudo_proj_False n `(g -` {g z})" using \w\ pseudo_proj_False n -` g -` {g z}\ by simp finally have "pseudo_proj_False n w \ pseudo_proj_False n `(g -` {g z})" . thus "w\ pseudo_proj_False n -` (pseudo_proj_False n `(g -` {g z}))" by simp qed show "pseudo_proj_False n -` pseudo_proj_False n ` g -` {g z} \ pseudo_proj_False n -` g -` {g z}" proof fix w assume "w \ pseudo_proj_False n -` pseudo_proj_False n ` g -` {g z}" hence "\y. pseudo_proj_False n w = pseudo_proj_False n y \ g y = g z" by auto from this obtain y where "pseudo_proj_False n w = pseudo_proj_False n y" and "g y = g z" by auto have "g (pseudo_proj_False n w) = g (pseudo_proj_False n y)" using \pseudo_proj_False n w = pseudo_proj_False n y\ by simp also have "... = g y" using assms nat_filtration_not_borel_info' natural_filtration by (metis comp_apply) also have "... = g z" using \g y = g z\ . finally have "g (pseudo_proj_False n w) = g z" . thus "w\ pseudo_proj_False n -` g -` {g z}" by simp qed qed lemma (in infinite_cts_filtration) borel_pseudo_proj_False_preimage: fixes g::"bool stream \ 'b::{t0_space}" assumes "g\ borel_measurable (F n)" shows "pseudo_proj_False n -` (g -` {g z}) = pseudo_proj_False n -` (pseudo_proj_False n `(g -` {g z}))" using pseudo_proj_False_preimage[of g n borel z] set_discriminating_if[of g n] natural_filtration assms by simp lemma (in infinite_cts_filtration) pseudo_proj_preimage': assumes "g\ measurable (F n) N" and "set_discriminating n g N" shows "pseudo_proj_True n -` (g -` {g z}) = g -` {g z}" proof show "pseudo_proj_True n -` g -` {g z} \ g -` {g z}" proof fix w assume "w\ pseudo_proj_True n -` g -` {g z}" have "g w = g (pseudo_proj_True n w)" using assms nat_filtration_not_borel_info natural_filtration by (metis comp_apply) also have "... = g z" using \w\ pseudo_proj_True n -` g -` {g z}\ by simp finally have "g w = g z". thus "w\ g -`{g z}" by simp qed show "g -` {g z} \ pseudo_proj_True n -` g -` {g z}" proof fix w assume "w \ g -` {g z}" have "g (pseudo_proj_True n w) = g w" using assms nat_filtration_not_borel_info natural_filtration by (metis comp_apply) also have "... = g z" using \w\ g -`{g z}\ by simp finally have "g (pseudo_proj_True n w) = g z" . thus "w\ pseudo_proj_True n -` g -` {g z}" by simp qed qed lemma (in infinite_cts_filtration) borel_pseudo_proj_preimage': fixes g::"bool stream \ 'b::{t0_space}" assumes "g\ borel_measurable (F n)" shows "pseudo_proj_True n -` (g -` {g z}) = g -` {g z}" using assms natural_filtration by (simp add: set_discriminating_if pseudo_proj_preimage') lemma (in infinite_cts_filtration) pseudo_proj_False_preimage': assumes "g\ measurable (F n) N" and "set_discriminating n g N" shows "pseudo_proj_False n -` (g -` {g z}) = g -` {g z}" proof show "pseudo_proj_False n -` g -` {g z} \ g -` {g z}" proof fix w assume "w\ pseudo_proj_False n -` g -` {g z}" have "g w = g (pseudo_proj_False n w)" using assms nat_filtration_not_borel_info' natural_filtration by (metis comp_apply) also have "... = g z" using \w\ pseudo_proj_False n -` g -` {g z}\ by simp finally have "g w = g z". thus "w\ g -`{g z}" by simp qed show "g -` {g z} \ pseudo_proj_False n -` g -` {g z}" proof fix w assume "w \ g -` {g z}" have "g (pseudo_proj_False n w) = g w" using assms nat_filtration_not_borel_info' natural_filtration by (metis comp_apply) also have "... = g z" using \w\ g -`{g z}\ by simp finally have "g (pseudo_proj_False n w) = g z" . thus "w\ pseudo_proj_False n -` g -` {g z}" by simp qed qed lemma (in infinite_cts_filtration) borel_pseudo_proj_False_preimage': fixes g::"bool stream \ 'b::{t0_space}" assumes "g\ borel_measurable (F n)" shows "pseudo_proj_False n -` (g -` {g z}) = g -` {g z}" using assms natural_filtration by (simp add: set_discriminating_if pseudo_proj_False_preimage') subsubsection \Integrals and conditional expectations on the natural filtration\ lemma (in infinite_cts_filtration) cst_integral: fixes f::"bool stream\real" assumes "f \ borel_measurable (F 0)" and "f (sconst True) = c" shows "has_bochner_integral M f c" proof - have "space M = space (F 0)" using filtration by (simp add: filtration_def subalgebra_def) have "f\ borel_measurable M" using assms(1) nat_filtration_borel_measurable_integrable natural_filtration by blast have "\d. \x\ space (F 0). f x = d" proof (rule triv_measurable_cst) show "space (F 0) = space M" using \space M = space (F 0)\ .. show "sets (F 0) = {{}, space M}" using info_disc_filtr by (simp add: init_triv_filt_def bot_nat_def) show "f \ borel_measurable (F 0)" using assms by simp show "space M \ {}" by (simp add:not_empty) qed from this obtain d where "\x\ space (F 0). f x = d" by auto hence "\ x\ space M. f x = d" using \space M = space (F 0)\ by simp hence "f (sconst True) = d" using bernoulli_stream_space bernoulli by simp hence "c = d" using assms by simp hence "\x\ space M. f x = c" using \\ x\ space M. f x = d\ \c = d\ by simp have "f\ borel_measurable M" using assms(1) nat_filtration_borel_measurable_integrable natural_filtration by blast have "integral\<^sup>N M f = integral\<^sup>N M (\w. c)" proof (rule nn_integral_cong) fix x assume "x\ space M" thus "ennreal (f x) = ennreal c" using \\ x\ space M. f x = d\ \c = d\ by auto qed also have "... = integral\<^sup>N M (\w. c * (indicator (space M)) w)" by (simp add: nn_integral_cong) also have "... = ennreal c * emeasure M (space M)" using nn_integral_cmult_indicator[of "space M" M c] by (simp add: nn_integral_cong) also have "... = ennreal c" by (simp add: emeasure_space_1) finally have "integral\<^sup>N M f = ennreal c" . hence "integral\<^sup>N M (\x. - f x) = ennreal (-c)" by (simp add: \\x\space M. f x = d\ \c = d\ emeasure_space_1 nn_integral_cong) show "has_bochner_integral M f c" proof (cases "0 \ c") case True hence "AE x in M. 0 \ f x" using \\x\ space M. f x = c\ by simp thus ?thesis using \random_variable borel f\ True \integral\<^sup>N M f = ennreal c\ by (simp add: has_bochner_integral_nn_integral) next case False let ?mf = "\w. - f w" have "AE x in M. 0 \ ?mf x" using \\x\ space M. f x = c\ False by simp hence "has_bochner_integral M ?mf (-c)" using \random_variable borel f\ False \integral\<^sup>N M (\x. - f x) = ennreal (-c)\ by (simp add: has_bochner_integral_nn_integral) thus ?thesis using has_bochner_integral_minus by fastforce qed qed lemma (in infinite_cts_filtration) cst_nn_integral: fixes f::"bool stream\real" assumes "f \ borel_measurable (F 0)" and "\w. 0 \ f w" and "f (sconst True) = c" shows "integral\<^sup>N M f = ennreal c" using assms cst_integral by (simp add: assms(1) has_bochner_integral_iff nn_integral_eq_integral) lemma (in infinite_cts_filtration) suc_measurable: fixes f::"bool stream \ 'b::{t0_space}" assumes "f\ borel_measurable (F (Suc n))" shows "(\w. f (c ## w)) \ borel_measurable (F n)" proof - have "(\w. f (c ## w)) \ borel_measurable (nat_filtration n)" proof (rule nat_filtration_comp_measurable) have "f\ borel_measurable M" using assms using measurable_from_subalg nat_filtration_subalgebra natural_filtration by blast hence "f\ borel_measurable (stream_space (measure_pmf (bernoulli_pmf p)))" using bernoulli unfolding bernoulli_stream_def by simp have "(\w. c ## w) \ (stream_space (measure_pmf (bernoulli_pmf p)) \\<^sub>M stream_space (measure_pmf (bernoulli_pmf p)))" proof (rule measurable_Stream) show "(\x. c) \ stream_space (measure_pmf (bernoulli_pmf p)) \\<^sub>M measure_pmf (bernoulli_pmf p)" by simp show "(\x. x) \ stream_space (measure_pmf (bernoulli_pmf p)) \\<^sub>M stream_space (measure_pmf (bernoulli_pmf p))" by simp qed hence "(\w. f (c ## w)) \ (stream_space (measure_pmf (bernoulli_pmf p)) \\<^sub>M borel)" using \f\ borel_measurable (stream_space (measure_pmf (bernoulli_pmf p)))\ measurable_comp[of "(\w. c ## w)" "stream_space (measure_pmf (bernoulli_pmf p))" "stream_space (measure_pmf (bernoulli_pmf p))" f borel] by simp thus "random_variable borel (\w. f (c ## w))" using bernoulli unfolding bernoulli_stream_def by simp have "\w. f (c ## (pseudo_proj_True n w)) = f (c##w)" proof fix w have "c## (pseudo_proj_True n w) = pseudo_proj_True (Suc n) (c##w)" unfolding pseudo_proj_True_def by simp hence "f (c ## (pseudo_proj_True n w)) = f (pseudo_proj_True (Suc n) (c##w))" by simp also have "... = f (c##w)" using assms nat_filtration_info[of f "Suc n"] natural_filtration by (metis comp_apply) finally show "f (c ## (pseudo_proj_True n w)) = f (c##w)" . qed thus "(\w. f (c ## w)) \ pseudo_proj_True n = (\w. f (c ## w))" by auto qed thus "(\w. f (c ## w)) \ borel_measurable (F n)" using natural_filtration by simp qed lemma (in infinite_cts_filtration) F_n_nn_integral_pos: fixes f::"bool stream\real" shows "\f. (\x. 0 \ f x) \ f \ borel_measurable (F n) \ integral\<^sup>N M f = (\ w\ range (pseudo_proj_True n). (emeasure M ((pseudo_proj_True n) -`{w} \ space M)) * ennreal (f w))" proof (induct n) case 0 have "range (pseudo_proj_True 0) = {sconst True}" proof have "\w. pseudo_proj_True 0 w = sconst True" proof - fix w show "pseudo_proj_True 0 w = sconst True" unfolding pseudo_proj_True_def by simp qed thus "range (pseudo_proj_True 0) \ {sconst True}" by auto show "{sconst True} \ range (pseudo_proj_True 0)" using \range (pseudo_proj_True 0) \ {sconst True}\ subset_singletonD by fastforce qed hence "(emeasure M ((pseudo_proj_True 0) -`{sconst True} \ space M)) = ennreal 1" by (metis Int_absorb1 UNIV_I emeasure_eq_measure image_eqI prob_space subsetI vimage_eq) have "(\ w\ range (pseudo_proj_True 0). f w) = (\ w\ {sconst True}. f w)" using \range (pseudo_proj_True 0) = {sconst True}\ sum.cong[of "range (pseudo_proj_True n)" "{sconst True}" f f] by simp also have "... = f (sconst True)" by simp finally have "(\ w\ range (pseudo_proj_True 0). f w) = f (sconst True)" . hence "(\ w\ range (pseudo_proj_True 0). (emeasure M ((pseudo_proj_True 0) -`{w} \ space M)) * f w) = f (sconst True)" using \(emeasure M ((pseudo_proj_True 0) -`{sconst True} \ space M)) = ennreal 1\ by (simp add: \range (pseudo_proj_True 0) = {sconst True}\) thus "integral\<^sup>N M f = (\ w\ range (pseudo_proj_True 0). (emeasure M ((pseudo_proj_True 0) -`{w} \ space M)) * f w)" using 0 by (simp add:cst_nn_integral) next case (Suc n) define BP where "BP = measure_pmf (bernoulli_pmf p)" have "integral\<^sup>N M f = integral\<^sup>N (stream_space BP) f" using bernoulli unfolding bernoulli_stream_def BP_def by simp also have "... = \\<^sup>+ x. \\<^sup>+ X. f (x ## X) \stream_space BP \BP" proof (rule prob_space.nn_integral_stream_space) show "prob_space BP" unfolding BP_def by (simp add: bernoulli bernoulli_stream_def prob_space.prob_space_stream_space prob_space_measure_pmf) have "f\ borel_measurable (stream_space BP)" using bernoulli Suc unfolding bernoulli_stream_def BP_def using measurable_from_subalg nat_filtration_subalgebra natural_filtration by blast thus "(\X. ennreal (f X)) \ borel_measurable (stream_space BP)" by simp qed also have "... = (\x. (\\<^sup>+ X. f (x ## X) \stream_space BP)) True * ennreal p + (\x. (\\<^sup>+ X. f (x ## X) \stream_space BP)) False * ennreal (1 -p)" using p_gt_0 p_lt_1 unfolding BP_def by simp also have "... = (\\<^sup>+ X. f (True ## X) \stream_space BP) * p + (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * (f (False ## w))) * (1-p)" proof - define ff where "ff = (\w. f (False ## w))" have "\x. 0 \ ff x" using Suc unfolding ff_def by simp moreover have "ff\ borel_measurable (F n)" using Suc unfolding ff_def by (simp add:suc_measurable) ultimately have "(\\<^sup>+ x. ennreal (ff x) \M) = (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * ennreal (ff w))" using Suc by simp thus ?thesis unfolding ff_def by (simp add: BP_def bernoulli bernoulli_stream_def) qed also have "... = (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * (f (True ## w))) * p + (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * (f (False ## w))) * (1-p)" proof - define ft where "ft = (\w. f (True ## w))" have "\x. 0 \ ft x" using Suc unfolding ft_def by simp moreover have "ft\ borel_measurable (F n)" using Suc unfolding ft_def by (simp add:suc_measurable) ultimately have "(\\<^sup>+ x. ennreal (ft x) \M) = (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * ennreal (ft w))" using Suc by simp thus ?thesis unfolding ft_def by (simp add: BP_def bernoulli bernoulli_stream_def) qed also have "... = (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * p * (f (True ## w))) + (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * (f (False ## w)))* (1-p)" proof - have "(\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * (f (True ## w))) * p = (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * (f (True ## w)) * p)" by (rule sum_distrib_right) also have "... = (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * p * (f (True ## w)))" proof (rule sum.cong, simp) fix w assume "w\ range (pseudo_proj_True n)" show "emeasure M (pseudo_proj_True n -` {w} \ space M) * ennreal (f (True ## w)) * ennreal p = emeasure M (pseudo_proj_True n -` {w} \ space M) * ennreal p * ennreal (f (True ## w))" proof - have "ennreal (f (True ## w)) * ennreal p = ennreal p * ennreal (f (True ## w))" by (simp add:mult.commute) hence "\x. x * ennreal (f (True ## w)) * ennreal p = x * ennreal p * ennreal (f (True ## w))" by (simp add: semiring_normalization_rules(16)) thus ?thesis by simp qed qed finally have "(\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * (f (True ## w))) * p = (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * p * (f (True ## w)))" . thus ?thesis by simp qed also have "... = (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * p * (f (True ## w))) + (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * (1-p) * (f (False ## w)))" proof - have "(\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * (f (False ## w))) * (1-p) = (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * (f (False ## w)) * (1-p))" by (rule sum_distrib_right) also have "... = (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * (1-p) * (f (False ## w)))" proof (rule sum.cong, simp) fix w assume "w\ range (pseudo_proj_True n)" show "emeasure M (pseudo_proj_True n -` {w} \ space M) * ennreal (f (False ## w)) * ennreal (1-p) = emeasure M (pseudo_proj_True n -` {w} \ space M) * ennreal (1-p) * ennreal (f (False ## w))" proof - have "ennreal (f (False ## w)) * ennreal (1-p) = ennreal (1-p) * ennreal (f (False ## w))" by (simp add:mult.commute) hence "\x. x * ennreal (f (False ## w)) * ennreal (1-p) = x * ennreal (1-p) * ennreal (f (False ## w))" by (simp add: semiring_normalization_rules(16)) thus ?thesis by simp qed qed finally have "(\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * (f (False ## w))) * (1-p) = (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * (1-p) * (f (False ## w)))" . thus ?thesis by simp qed also have "... = (\y\{y. \w \ range (pseudo_proj_True n). y = True ## w}. emeasure M (pseudo_proj_True n -` {stl y} \ space M) * p * (f (y))) + (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * (1-p) * (f (False ## w)))" proof - have "(\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * p * (f (True ## w))) = (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {stl (True##w)} \ space M) * p * (f (True ## w)))" by simp also have "... = (\y\{y. \w \ range (pseudo_proj_True n). y = True ## w}. emeasure M (pseudo_proj_True n -` {stl y} \ space M) * p * (f (y)))" by (rule reindex_pseudo_proj) finally have "(\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * p * (f (True ## w))) = (\y\{y. \w \ range (pseudo_proj_True n). y = True ## w}. emeasure M (pseudo_proj_True n -` {stl y} \ space M) * p * (f (y)))" . thus ?thesis by simp qed also have "... = (\y\{y. \w \ range (pseudo_proj_True n). y = True ## w}. emeasure M (pseudo_proj_True n -` {stl y} \ space M) * p * (f (y))) + (\y\{y. \w \ range (pseudo_proj_True n). y = False ## w}. emeasure M (pseudo_proj_True n -` {stl y} \ space M) * (1-p) * (f (y)))" proof - have "(\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * (1-p) * (f (False ## w))) = (\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {stl (False##w)} \ space M) * (1-p) * (f (False ## w)))" by simp also have "... = (\y\{y. \w \ range (pseudo_proj_True n). y = False ## w}. emeasure M (pseudo_proj_True n -` {stl y} \ space M) * (1-p) * (f (y)))" by (rule reindex_pseudo_proj) finally have "(\w\range (pseudo_proj_True n). emeasure M (pseudo_proj_True n -` {w} \ space M) * (1-p) * (f (False ## w))) = (\y\{y. \w \ range (pseudo_proj_True n). y = False ## w}. emeasure M (pseudo_proj_True n -` {stl y} \ space M) * (1-p) * (f (y)))" . thus ?thesis by simp qed also have "... = (\y\{y. \w \ range (pseudo_proj_True n). y = True ## w}. (prob_component p y 0) * emeasure M (pseudo_proj_True n -` {stl y} \ space M) * (f (y))) + (\y\{y. \w \ range (pseudo_proj_True n). y = False ## w}. emeasure M (pseudo_proj_True n -` {stl y} \ space M) * (1-p) * (f (y)))" proof - have "\y \{y. \w \ range (pseudo_proj_True n). y = True ## w}. emeasure M (pseudo_proj_True n -` {stl y} \ space M) * p = prob_component p y 0 * emeasure M (pseudo_proj_True n -` {stl y} \ space M)" proof fix y assume "y \{y. \w \ range (pseudo_proj_True n). y = True ## w}" hence "\w \ range (pseudo_proj_True n). y = True ## w" by simp from this obtain w where "w\ range (pseudo_proj_True n)" and "y = True ## w" by auto have "emeasure M (pseudo_proj_True n -` {stl y} \ space M) * p = p *emeasure M (pseudo_proj_True n -` {stl y} \ space M)" by (simp add:mult.commute) also have "... = prob_component p y 0 * emeasure M (pseudo_proj_True n -` {stl y} \ space M)" using \y = True ## w\ unfolding prob_component_def by simp finally show "emeasure M (pseudo_proj_True n -` {stl y} \ space M) * p = prob_component p y 0 * emeasure M (pseudo_proj_True n -` {stl y} \ space M)" . qed thus ?thesis by auto qed also have "... = (\y\{y. \w \ range (pseudo_proj_True n). y = True ## w}. (prob_component p y 0) * emeasure M (pseudo_proj_True n -` {stl y} \ space M) * (f (y))) + (\y\{y. \w \ range (pseudo_proj_True n). y = False ## w}. (prob_component p y 0) * emeasure M (pseudo_proj_True n -` {stl y} \ space M) * (f (y)))" proof - have "\y \{y. \w \ range (pseudo_proj_True n). y = False ## w}. emeasure M (pseudo_proj_True n -` {stl y} \ space M) * (1-p) = prob_component p y 0 * emeasure M (pseudo_proj_True n -` {stl y} \ space M)" proof fix y assume "y \{y. \w \ range (pseudo_proj_True n). y = False ## w}" hence "\w \ range (pseudo_proj_True n). y = False ## w" by simp from this obtain w where "w\ range (pseudo_proj_True n)" and "y = False ## w" by auto have "emeasure M (pseudo_proj_True n -` {stl y} \ space M) * (1-p) = (1-p) *emeasure M (pseudo_proj_True n -` {stl y} \ space M)" by (simp add:mult.commute) also have "... = prob_component p y 0 * emeasure M (pseudo_proj_True n -` {stl y} \ space M)" using \y = False ## w\ unfolding prob_component_def by simp finally show "emeasure M (pseudo_proj_True n -` {stl y} \ space M) * (1-p) = prob_component p y 0 * emeasure M (pseudo_proj_True n -` {stl y} \ space M)" . qed thus ?thesis by auto qed also have "... = (\y\{y. \w \ range (pseudo_proj_True n). y = True ## w}. emeasure M {z \ space M. \x\pseudo_proj_True n -` {stl y}. z = True ## x} * (f y)) + (\y\{y. \w \ range (pseudo_proj_True n). y = False ## w}. (prob_component p y 0) * emeasure M (pseudo_proj_True n -` {stl y} \ space M) * (f (y)))" proof - have "(\y | \w\range (pseudo_proj_True n). y = True ## w. ennreal (prob_component p y 0) * emeasure M (pseudo_proj_True n -` {stl y} \ space M) * (f y)) = (\y\{y. \w \ range (pseudo_proj_True n). y = True ## w}. emeasure M {z \ space M. \x\pseudo_proj_True n -` {stl y}. z = True ## x} * (f y))" proof (rule sum.cong, simp) fix xx assume "xx \ {y. \w\range (pseudo_proj_True n). y = True ## w}" hence "\w\range (pseudo_proj_True n). xx = True ## w" by simp from this obtain ww where "ww\range (pseudo_proj_True n)" and "xx = True## ww" by auto have "ennreal (prob_component p (True##ww) 0) * emeasure M (pseudo_proj_True n -` {ww} \ space M) = emeasure M {z \ space M. \x\pseudo_proj_True n -` {ww}. z = True ## x}" using \ww\range (pseudo_proj_True n)\ by (rule pseudo_proj_element_prob_pref[symmetric]) thus "ennreal (prob_component p xx 0) * emeasure M (pseudo_proj_True n -` {stl xx} \ space M) * (f xx) = emeasure M {z \ space M. \x\pseudo_proj_True n -` {stl xx}. z = True ## x} * (f xx)" using \xx = True##ww\ by simp qed thus ?thesis by simp qed also have "... = (\y\{y. \w \ range (pseudo_proj_True n). y = True ## w}. emeasure M {z \ space M. \x\pseudo_proj_True n -` {stl y}. z = True ## x} * (f y)) + (\y\{y. \w \ range (pseudo_proj_True n). y = False ## w}. emeasure M {z \ space M. \x\pseudo_proj_True n -` {stl y}. z = False ## x} * (f y))" proof - have "(\y | \w\range (pseudo_proj_True n). y = False ## w. ennreal (prob_component p y 0) * emeasure M (pseudo_proj_True n -` {stl y} \ space M) * (f y)) = (\y\{y. \w \ range (pseudo_proj_True n). y = False ## w}. emeasure M {z \ space M. \x\pseudo_proj_True n -` {stl y}. z = False ## x} * (f y))" proof (rule sum.cong, simp) fix xx assume "xx \ {y. \w\range (pseudo_proj_True n). y = False ## w}" hence "\w\range (pseudo_proj_True n). xx = False ## w" by simp from this obtain ww where "ww\range (pseudo_proj_True n)" and "xx = False## ww" by auto have "ennreal (prob_component p (False##ww) 0) * emeasure M (pseudo_proj_True n -` {ww} \ space M) = emeasure M {z \ space M. \x\pseudo_proj_True n -` {ww}. z = False ## x}" using \ww\range (pseudo_proj_True n)\ by (rule pseudo_proj_element_prob_pref[symmetric]) thus "ennreal (prob_component p xx 0) * emeasure M (pseudo_proj_True n -` {stl xx} \ space M) * (f xx) = emeasure M {z \ space M. \x\pseudo_proj_True n -` {stl xx}. z = False ## x} * (f xx)" using \xx = False##ww\ by simp qed thus ?thesis by simp qed also have "... = (\w\ range (pseudo_proj_True n). emeasure M {z \ space M. \x\pseudo_proj_True n -` {w}. z = True ## x} * (f (True##w))) + (\w \ range (pseudo_proj_True n). emeasure M {z \ space M. \x\pseudo_proj_True n -` {w}. z = False ## x} * (f (False##w)))" proof - have "\c. (\y\{y. \w \ range (pseudo_proj_True n). y = c ## w}. emeasure M {z \ space M. \x\pseudo_proj_True n -` {stl y}. z = c ## x} * (f y)) = (\w\ range (pseudo_proj_True n). emeasure M {z \ space M. \x\pseudo_proj_True n -` {w}. z = c ## x} * (f (c##w)))" proof - fix c have "(\y\{y. \w \ range (pseudo_proj_True n). y = c ## w}. emeasure M {z \ space M. \x\pseudo_proj_True n -` {stl y}. z = c ## x} * (f y)) = (\w\ range (pseudo_proj_True n). emeasure M {z \ space M. \x\pseudo_proj_True n -` {stl (c##w)}. z = c ## x} * (f (c##w)))" by (rule reindex_pseudo_proj[symmetric]) also have "... = (\w\ range (pseudo_proj_True n). emeasure M {z \ space M. \x\pseudo_proj_True n -` {w}. z = c ## x} * (f (c##w)))" by simp finally show "(\y\{y. \w \ range (pseudo_proj_True n). y = c ## w}. emeasure M {z \ space M. \x\pseudo_proj_True n -` {stl y}. z = c ## x} * (f y)) = (\w\ range (pseudo_proj_True n). emeasure M {z \ space M. \x\pseudo_proj_True n -` {w}. z = c ## x} * (f (c##w)))" . qed thus ?thesis by auto qed also have "... = (\w\ {w. w\ range (pseudo_proj_True (Suc n)) \ w!!0 = True}. emeasure M (pseudo_proj_True (Suc n) -` {w} \ (space M)) * (f w)) + (\w\ {w. w\ range (pseudo_proj_True (Suc n)) \ w!!0 = False}. emeasure M (pseudo_proj_True (Suc n) -` {w} \ (space M)) * (f w))" proof - have "\c. (\w\ range (pseudo_proj_True n). emeasure M {z \ space M. \x\pseudo_proj_True n -` {w}. z = c ## x} * (f (c##w))) = (\w\ {w. w\ range (pseudo_proj_True (Suc n)) \ w!!0 = c}. emeasure M (pseudo_proj_True (Suc n) -` {w} \ (space M)) * (f w))" proof - fix c show "(\w\ range (pseudo_proj_True n). emeasure M {z \ space M. \x\pseudo_proj_True n -` {w}. z = c ## x} * (f (c##w))) = (\w\ {w. w\ range (pseudo_proj_True (Suc n)) \ w!!0 = c}. emeasure M (pseudo_proj_True (Suc n) -` {w} \ (space M)) * (f w))" proof (rule sum.reindex_cong) show "inj_on stl {w \ range (pseudo_proj_True (Suc n)). w !! 0 = c}" proof fix x y assume "x \ {w \ range (pseudo_proj_True (Suc n)). w !! 0 = c}" and "y \ {w \ range (pseudo_proj_True (Suc n)). w !! 0 = c}" and "stl x = stl y" have "x!!0 = c" using \x \ {w \ range (pseudo_proj_True (Suc n)). w !! 0 = c}\ by simp moreover have "y!!0 = c" using \y \ {w \ range (pseudo_proj_True (Suc n)). w !! 0 = c}\ by simp ultimately show "x = y" using \stl x= stl y\ by (smt snth.simps(1) stream_eq_Stream_iff) (*by (metis (full_types, hide_lams) pmf_bernoulli_True snth.simps(1) stream_eq_Stream_iff) *) qed show "range (pseudo_proj_True n) = stl ` {w \ range (pseudo_proj_True (Suc n)). w !! 0 = c}" proof show "range (pseudo_proj_True n) \ stl ` {w \ range (pseudo_proj_True (Suc n)). w !! 0 = c}" proof fix x assume "x\ range (pseudo_proj_True n)" hence "pseudo_proj_True n x = x" using pseudo_proj_True_proj by auto have "pseudo_proj_True (Suc n) (c##x) = c##x" proof - have "pseudo_proj_True (Suc n) (c##x) = c ## pseudo_proj_True n x" using pseudo_proj_True_Suc_prefix[of n "c##x"] by simp also have "... = c## x" using \pseudo_proj_True n x = x\ by simp finally show ?thesis . qed hence "c##x\ range (pseudo_proj_True (Suc n))" by (simp add: pseudo_proj_True_img) thus "x\ stl`{w \ range (pseudo_proj_True (Suc n)). w !! 0 = c}" proof - have "\s. (s \ range (pseudo_proj_True (Suc n)) \ s !! 0 = c) \ stl s = x" by (metis (no_types) \c ## x \ range (pseudo_proj_True (Suc n))\ snth.simps(1) stream.sel(1) stream.sel(2)) then show ?thesis by force qed qed show "stl ` {w \ range (pseudo_proj_True (Suc n)). w !! 0 = c} \ range (pseudo_proj_True n)" proof fix x assume "x\ stl ` {w \ range (pseudo_proj_True (Suc n)). w !! 0 = c}" hence "\ w\ {w \ range (pseudo_proj_True (Suc n)). w !! 0 = c}. x = stl w" by auto from this obtain w where "w \ {w \ range (pseudo_proj_True (Suc n)). w !! 0 = c}" and "x = stl w" by auto have "w\ range (pseudo_proj_True (Suc n))" and "w!!0 = c" using \w \ {w \ range (pseudo_proj_True (Suc n)). w !! 0 = c}\ by auto have "c##x = w" using \x = stl w\ \w!!0 = c\ by force also have "... = pseudo_proj_True (Suc n) w" using \w\ range (pseudo_proj_True (Suc n))\ using pseudo_proj_True_proj by auto also have "... = c ## pseudo_proj_True n x" using \x = stl w\ \w!!0 = c\ by (simp add:pseudo_proj_True_Suc_prefix) finally have "c##x = c## pseudo_proj_True n x" . hence "x = pseudo_proj_True n x" by simp thus "x\ range (pseudo_proj_True n)" by auto qed qed show "\x. x \ {w \ range (pseudo_proj_True (Suc n)). w !! 0 = c} \ emeasure M {z \ space M. \x\pseudo_proj_True n -` {stl x}. z = c ## x} * ennreal (f (c ## stl x)) = emeasure M (pseudo_proj_True (Suc n) -` {x} \ space M) * ennreal (f x)" proof - fix w assume "w \ {w \ range (pseudo_proj_True (Suc n)). w !! 0 = c}" hence "w \ range (pseudo_proj_True (Suc n))" and "w !! 0 = c" by auto have "{z \ space M. \x\pseudo_proj_True n -` {stl w}. z = c ## x} = (pseudo_proj_True (Suc n) -` {w} \ space M)" proof show "{z \ space M. \x\pseudo_proj_True n -` {stl w}. z = c ## x} \ pseudo_proj_True (Suc n) -` {w} \ space M" proof fix z assume "z \ {z \ space M. \x\pseudo_proj_True n -` {stl w}. z = c ## x}" hence "\x\pseudo_proj_True n -` {stl w}. z = c ## x" and "z\ space M" by auto from \\x\pseudo_proj_True n -` {stl w}. z = c ## x\ obtain x where "x\pseudo_proj_True n -` {stl w}" and "z = c##x" by auto have "pseudo_proj_True (Suc n) z = c ## pseudo_proj_True n x" using \z = c##x\ by (simp add:pseudo_proj_True_Suc_prefix) also have "... = c## stl w" using \x\pseudo_proj_True n -` {stl w}\ by simp also have "... = w" using \w !! 0 = c\ by force finally have "pseudo_proj_True (Suc n) z = w" . thus "z\ pseudo_proj_True (Suc n) -` {w} \ space M" using \z\ space M\ by auto qed show "pseudo_proj_True (Suc n) -` {w} \ space M \ {z \ space M. \x\pseudo_proj_True n -` {stl w}. z = c ## x}" proof fix z assume "z\ pseudo_proj_True (Suc n) -` {w} \ space M" hence "z\ space M" and "pseudo_proj_True (Suc n) z = w" by auto hence "stl w = stl (pseudo_proj_True (Suc n) z)" by simp also have "... = pseudo_proj_True n (stl z)" by (simp add: pseudo_proj_True_Suc_prefix) finally have "stl w = pseudo_proj_True n (stl z)" . hence "stl z \ pseudo_proj_True n -` {stl w}" by simp have "z!!0 ## pseudo_proj_True n (stl z) = w" using pseudo_proj_True_Suc_prefix \pseudo_proj_True (Suc n) z = w\ by simp also have "... = c## (stl w)" using \w!!0 = c\ by force finally have "z!!0 ## pseudo_proj_True n (stl z) = c## (stl w)" . hence "z!!0 = c" by simp hence "z =c## (stl z)" by force thus "z\ {z \ space M. \x\pseudo_proj_True n -` {stl w}. z = c ## x}" using \z\ space M\ \stl z \ pseudo_proj_True n -` {stl w}\ by auto qed qed hence "emeasure M {z \ space M. \x\pseudo_proj_True n -` {stl w}. z = c ## x} * ennreal (f (c ## stl w)) = emeasure M (pseudo_proj_True (Suc n) -` {w} \ space M) * ennreal (f (c ## stl w))" by simp also have "... = emeasure M (pseudo_proj_True (Suc n) -` {w} \ space M) * ennreal (f w)" using \w!!0 = c\ by force finally show "emeasure M {z \ space M. \x\pseudo_proj_True n -` {stl w}. z = c ## x} * ennreal (f (c ## stl w)) = emeasure M (pseudo_proj_True (Suc n) -` {w} \ space M) * ennreal (f w)" . qed qed qed thus ?thesis by simp qed also have "... = (\w\ {w \ range (pseudo_proj_True (Suc n)). w !! 0 = True} \ {w \ range (pseudo_proj_True (Suc n)). w !! 0 = False}. emeasure M (pseudo_proj_True (Suc n) -` {w} \ space M) * ennreal (f w))" proof (rule sum.union_disjoint[symmetric]) show "finite {w \ range (pseudo_proj_True (Suc n)). w !! 0 = True}" by (simp add: pseudo_proj_True_finite_image) show "finite {w \ range (pseudo_proj_True (Suc n)). w !! 0 = False}" by (simp add: pseudo_proj_True_finite_image) show "{w \ range (pseudo_proj_True (Suc n)). w !! 0 = True} \ {w \ range (pseudo_proj_True (Suc n)). w !! 0 = False} = {}" by auto qed also have "... = (\w\ range (pseudo_proj_True (Suc n)).emeasure M (pseudo_proj_True (Suc n) -` {w} \ space M) * ennreal (f w))" proof (rule sum.cong) show "{w \ range (pseudo_proj_True (Suc n)). w !! 0 = True} \ {w \ range (pseudo_proj_True (Suc n)). w !! 0 = False} = range (pseudo_proj_True (Suc n))" proof show "{w \ range (pseudo_proj_True (Suc n)). w !! 0 = True} \ {w \ range (pseudo_proj_True (Suc n)). w !! 0 = False} \ range (pseudo_proj_True (Suc n))" by auto show "range (pseudo_proj_True (Suc n)) \ {w \ range (pseudo_proj_True (Suc n)). w !! 0 = True} \ {w \ range (pseudo_proj_True (Suc n)). w !! 0 = False}" by (simp add: subsetI) qed qed simp finally show "integral\<^sup>N M f = (\w\ range (pseudo_proj_True (Suc n)). emeasure M (pseudo_proj_True (Suc n) -` {w} \ space M) * ennreal (f w))" . qed lemma (in infinite_cts_filtration) F_n_integral_pos: fixes f::"bool stream\real" assumes "f\ borel_measurable (F n)" and "\w. 0 \ f w" shows "has_bochner_integral M f (\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M)) * (f w))" proof - have "integral\<^sup>N M f = (\ w\ range (pseudo_proj_True n). (emeasure M ((pseudo_proj_True n) -`{w} \ space M)) * (f w))" using assms by (simp add: F_n_nn_integral_pos) have "integral\<^sup>L M f = enn2real (integral\<^sup>N M f)" proof (rule integral_eq_nn_integral) show "AE x in M. 0\ f x" using assms by simp show "random_variable borel f" using assms using measurable_from_subalg nat_filtration_subalgebra natural_filtration by blast qed also have "... = enn2real (\ w\ range (pseudo_proj_True n). (emeasure M ((pseudo_proj_True n) -`{w} \ space M)) * (f w))" using assms by (simp add: F_n_nn_integral_pos) also have "... = (\ w\ range (pseudo_proj_True n). enn2real ((emeasure M ((pseudo_proj_True n) -`{w} \ space M)) * (f w)))" proof (rule enn2real_sum) show "finite (range (pseudo_proj_True n))" by (simp add: pseudo_proj_True_finite_image) show "\w. w \ range (pseudo_proj_True n) \ emeasure M (pseudo_proj_True n -` {w} \ space M) * ennreal (f w) < \" proof - fix w assume "w\ range (pseudo_proj_True n)" show "emeasure M (pseudo_proj_True n -` {w} \ space M) * ennreal (f w) < \" by (simp add: emeasure_eq_measure ennreal_mult_less_top) qed qed also have "... = (\ w\ range (pseudo_proj_True n). ((measure M ((pseudo_proj_True n) -`{w} \ space M)) * (f w)))" by (simp add: Sigma_Algebra.measure_def assms(2) enn2real_mult) finally have "integral\<^sup>L M f =(\ w\ range (pseudo_proj_True n). ((measure M ((pseudo_proj_True n) -`{w} \ space M)) * (f w)))" . moreover have "integrable M f" proof (rule integrableI_nn_integral_finite) show "random_variable borel f" using assms using measurable_from_subalg nat_filtration_subalgebra natural_filtration by blast show "AE x in M. 0 \ f x" using assms by simp have "(\\<^sup>+ x. ennreal (f x) \M) = (\ w\ range (pseudo_proj_True n). (emeasure M ((pseudo_proj_True n) -`{w} \ space M)) * (f w))" using assms by (simp add: F_n_nn_integral_pos) also have "... = (\ w\ range (pseudo_proj_True n). ennreal (measure M ((pseudo_proj_True n) -`{w} \ space M) * (f w)))" proof (rule sum.cong, simp) fix x assume "x\ range (pseudo_proj_True n)" thus "emeasure M (pseudo_proj_True n -` {x} \ space M) * ennreal (f x) = ennreal (prob (pseudo_proj_True n -` {x} \ space M) * f x)" using assms(2) emeasure_eq_measure ennreal_mult'' by auto qed also have "... = ennreal (\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M) * (f w)))" proof (rule ennreal_sum) show "finite (range (pseudo_proj_True n))" by (simp add: pseudo_proj_True_finite_image) show "\w. 0 \ prob (pseudo_proj_True n -` {w} \ space M) * f w" using assms(2) measure_nonneg zero_le_mult_iff by blast qed finally show "(\\<^sup>+ x. ennreal (f x) \M) = ennreal (\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M) * (f w)))" . qed ultimately show ?thesis using has_bochner_integral_iff by blast qed lemma (in infinite_cts_filtration) F_n_integral: fixes f::"bool stream\real" assumes "f\ borel_measurable (F n)" shows "has_bochner_integral M f (\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M)) * (f w))" proof - define fpos where "fpos = (\w. max 0 (f w))" define fneg where "fneg = (\w. max 0 (-f w))" have "\w. 0 \ fpos w" unfolding fpos_def by simp have "\w. 0 \ fneg w" unfolding fneg_def by simp have "fpos \ borel_measurable (F n)" using assms unfolding fpos_def by simp have "fneg \ borel_measurable (F n)" using assms unfolding fneg_def by simp have "has_bochner_integral M fpos (\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M)) * (fpos w))" using \fpos\ borel_measurable (F n)\ \\w. 0 \ fpos w\ by (simp add: F_n_integral_pos) moreover have "has_bochner_integral M fneg (\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M)) * (fneg w))" using \fneg\ borel_measurable (F n)\ \\w. 0 \ fneg w\ by (simp add: F_n_integral_pos) ultimately have posd: "has_bochner_integral M (\w. fpos w - fneg w) ((\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M)) * (fpos w)) - (\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M)) * (fneg w)))" by (simp add:has_bochner_integral_diff) have "((\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M)) * (fpos w)) - (\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M)) * (fneg w))) = (\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M) * fpos w - (measure M ((pseudo_proj_True n) -`{w} \ space M)) * fneg w))" by (rule sum_subtractf[symmetric]) also have "... = (\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M) * (fpos w - fneg w)))" proof (rule sum.cong, simp) fix x assume "x\ range (pseudo_proj_True n)" show "prob (pseudo_proj_True n -` {x} \ space M) * fpos x - prob (pseudo_proj_True n -` {x} \ space M) * fneg x = prob (pseudo_proj_True n -` {x} \ space M) * (fpos x - fneg x)" by (rule right_diff_distrib[symmetric]) qed also have "... = (\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M) * f w))" proof (rule sum.cong, simp) fix x assume "x\ range (pseudo_proj_True n)" show "prob (pseudo_proj_True n -` {x} \ space M) * (fpos x - fneg x) = prob (pseudo_proj_True n -` {x} \ space M) * f x" unfolding fpos_def fneg_def by auto qed finally have "((\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M)) * (fpos w)) - (\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M)) * (fneg w))) = (\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M) * f w))" . hence "has_bochner_integral M (\w. fpos w - fneg w) (\ w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M) * f w))" using posd by simp moreover have "\w. fpos w - fneg w = f w" unfolding fpos_def fneg_def by auto ultimately show ?thesis using has_bochner_integral_diff by simp qed lemma (in infinite_cts_filtration) F_n_integral_prob_comp: fixes f::"bool stream\real" assumes "f\ borel_measurable (F n)" shows "has_bochner_integral M f (\ w\ range (pseudo_proj_True n). (prod (prob_component p w) {0.. w\ range (pseudo_proj_True n). (measure M ((pseudo_proj_True n) -`{w} \ space M)) * f w = (prod (prob_component p w) {0.. range (pseudo_proj_True n)" thus "prob (pseudo_proj_True n -` {w} \ space M) * f w = prod (prob_component p w) {0..real" assumes "f\ borel_measurable (F n)" shows "expectation f = (\ w\ range (pseudo_proj_True n). (prod (prob_component p w) {0.. B = {}" and "A \ B = C" shows "sum g C = sum g A + sum g B" using sum.union_disjoint[OF assms(1-3)] and assms(4) by auto lemma (in infinite_cts_filtration) borel_Suc_expectation: fixes f::"bool stream\ real" assumes "f\ borel_measurable (F (Suc n))" and "g\ measurable (F n) N" and "set_discriminating n g N" and "g -` {g z} \ sets (F n)" and "\y z. (g y = g z \ snth y n = snth z n) \ f y = f z" shows "expectation (\x. f x * indicator (g -` {g z}) x) = prob (g -` {g z}) * (p * f (pseudo_proj_True n z) + (1 -p) * f (pseudo_proj_False n z))" proof - define expind where "expind = (\x. f x * indicator (g -` {g z}) x)" have "expind\ borel_measurable (F (Suc n))" unfolding expind_def proof (rule borel_measurable_times, (simp add:assms(1,2))) show "indicator (g -` {g z}) \ borel_measurable (F (Suc n))" proof (rule borel_measurable_indicator) have "g -` {g z} \ sets (nat_filtration n)" using assms nat_filtration_borel_measurable_singleton natural_filtration by simp hence "g -` {g z} \ sets (F n)" using natural_filtration by simp thus "g -` {g z} \ sets (F (Suc n))" using nat_filtration_Suc_sets natural_filtration by blast qed qed hence "expectation expind = (\ w\ range (pseudo_proj_True (Suc n)). (measure M ((pseudo_proj_True (Suc n)) -`{w} \ space M)) * (expind w))" by (simp add:F_n_integral has_bochner_integral_integral_eq) also have "... = (\ w\ range (pseudo_proj_True (Suc n)) \ g -` {g z}. (measure M ((pseudo_proj_True (Suc n)) -`{w} \ space M)) * (expind w)) + (\ w\ range (pseudo_proj_True (Suc n)) - g -` {g z}. (measure M ((pseudo_proj_True (Suc n)) -`{w} \ space M)) * (expind w))" by (simp add: Int_Diff_Un Int_Diff_disjoint assms sum_union_disjoint' pseudo_proj_True_finite_image) also have "... = (\ w\ range (pseudo_proj_True (Suc n)) \ g -` {g z}. (measure M ((pseudo_proj_True (Suc n)) -`{w} \ space M)) * (expind w))" proof - have "\w\ range (pseudo_proj_True (Suc n)) - g -` {g z}. expind w = 0" proof fix w assume "w\ range (pseudo_proj_True (Suc n)) - g -` {g z}" thus "expind w = 0" unfolding expind_def by simp qed thus ?thesis by simp qed also have "... = (\ w\ range (pseudo_proj_True (Suc n)) \ g -` {g z}. (measure M ((pseudo_proj_True (Suc n)) -`{w} \ space M)) * f w)" proof - have "\w\ range (pseudo_proj_True (Suc n)) \ g -` {g z}. expind w = f w" proof fix w assume "w\ range (pseudo_proj_True (Suc n)) \ g -` {g z}" hence "w\ g -`{g z}" by simp thus "expind w = f w" unfolding expind_def by simp qed thus ?thesis by simp qed also have "... = (\ w\ (pseudo_proj_True n) ` (g -` {g z}) \ (pseudo_proj_False n) ` (g -` {g z}). (measure M ((pseudo_proj_True (Suc n)) -`{w} \ space M)) * f w)" using f_borel_Suc_preimage[of g] assms(1,2, 3) by auto also have "... = (\ w\ (pseudo_proj_True n) ` (g -` {g z}). (measure M ((pseudo_proj_True (Suc n)) -`{w} \ space M)) * f w) + (\w\ (pseudo_proj_False n) ` (g -` {g z}). (measure M ((pseudo_proj_True (Suc n)) -`{w} \ space M)) * f w)" proof (rule sum_union_disjoint') show "finite (pseudo_proj_True n ` g -` {g z})" proof - have "finite (range (pseudo_proj_True n))" by (simp add: pseudo_proj_True_finite_image) moreover have "pseudo_proj_True n ` g -` {g z} \ range (pseudo_proj_True n)" by (simp add: image_mono) ultimately show ?thesis by (simp add:finite_subset) qed show "finite (pseudo_proj_False n ` g -` {g z})" proof - have "finite (range (pseudo_proj_False n))" by (metis image_subsetI infinite_super proj_rep_set proj_rep_set_finite pseudo_proj_True_Suc_False_proj rangeI) moreover have "pseudo_proj_False n ` g -` {g z} \ range (pseudo_proj_False n)" by (simp add: image_mono) ultimately show ?thesis by (simp add:finite_subset) qed show "pseudo_proj_True n ` g -` {g z} \ pseudo_proj_False n ` g -` {g z} = {}" proof (rule ccontr) assume "pseudo_proj_True n ` g -` {g z} \ pseudo_proj_False n ` g -` {g z} \ {}" hence "\y. y\ pseudo_proj_True n ` g -` {g z} \ pseudo_proj_False n ` g -` {g z}" by auto from this obtain y where "y\ pseudo_proj_True n ` g -` {g z}" and "y\ pseudo_proj_False n ` g -` {g z}" by auto have "\yt. yt\ g -`{g z} \ y = pseudo_proj_True n yt" using \y\ pseudo_proj_True n ` g -` {g z}\ by auto from this obtain yt where "y = pseudo_proj_True n yt" by auto have "\yf. yf\ g -`{g z} \ y = pseudo_proj_False n yf" using \y\ pseudo_proj_False n ` g -` {g z}\ by auto from this obtain yf where "y = pseudo_proj_False n yf" by auto have "snth y n = True" using \y = pseudo_proj_True n yt\ unfolding pseudo_proj_True_def by simp moreover have "snth y n = False" using \y = pseudo_proj_False n yf\ unfolding pseudo_proj_False_def by simp ultimately show False by simp qed qed simp also have "... = (\w\pseudo_proj_True n ` g -` {g z}. prob (pseudo_proj_True (Suc n) -` {w} \ space M) * f (pseudo_proj_True n z)) + (\w\pseudo_proj_False n ` g -` {g z}. prob (pseudo_proj_True (Suc n) -` {w} \ space M) * f w)" proof - define zt where "zt = pseudo_proj_True n z" have eqw: "\w. w\pseudo_proj_True n ` g -` {g z} \ (g w = g zt \ snth w n = snth zt n)" proof fix w assume "w\ pseudo_proj_True n ` g -` {g z}" hence "\y. w = pseudo_proj_True n y \ g y = g z" by auto from this obtain yt where "w = pseudo_proj_True n yt" and "g yt = g z" by auto have "g w= g yt" using \w = pseudo_proj_True n yt\ nat_filtration_not_borel_info[of g] natural_filtration assms by (metis comp_apply) also have "... = g zt" using assms using nat_filtration_not_borel_info[of g] natural_filtration \g yt = g z\ unfolding zt_def by (metis comp_apply) finally show "g w = g zt" . show "w !! n = zt !! n" using \w = pseudo_proj_True n yt\ unfolding zt_def pseudo_proj_True_def by simp qed hence "\w. w\pseudo_proj_True n ` g -` {g z} \ f w = f zt" proof fix w assume "w \ pseudo_proj_True n ` g -` {g z}" hence "g w = g zt \ snth w n = snth zt n" using eqw [of w] by simp thus "f w = f zt" using assms(5) by blast qed thus ?thesis by simp qed also have "... = (\w\pseudo_proj_True n ` g -` {g z}. prob (pseudo_proj_True (Suc n) -` {w} \ space M) * f (pseudo_proj_True n z)) + (\w\pseudo_proj_False n ` g -` {g z}. prob (pseudo_proj_True (Suc n) -` {w} \ space M) * f (pseudo_proj_False n z))" proof - define zf where "zf = pseudo_proj_False n z" have eqw: "\w. w\pseudo_proj_False n ` g -` {g z} \ (g w = g zf \ snth w n = snth zf n)" proof fix w assume "w\ pseudo_proj_False n ` g -` {g z}" hence "\y. w = pseudo_proj_False n y \ g y = g z" by auto from this obtain yf where "w = pseudo_proj_False n yf" and "g yf = g z" by auto have "g w= g yf" using \w = pseudo_proj_False n yf\ nat_filtration_not_borel_info'[of g] natural_filtration assms by (metis comp_apply) also have "... = g zf" using assms using nat_filtration_not_borel_info'[of g] natural_filtration \g yf = g z\ unfolding zf_def by (metis comp_apply) finally show "g w = g zf" . show "w !! n = zf !! n" using \w = pseudo_proj_False n yf\ unfolding zf_def pseudo_proj_False_def by simp qed hence "\w. w\pseudo_proj_False n ` g -` {g z} \ f w = f zf" proof fix w assume "w\ pseudo_proj_False n ` g -` {g z}" hence "g w = g zf \ snth w n = snth zf n" using eqw [of w] by simp thus "f w = f zf" using assms by blast qed thus ?thesis by simp qed also have "... = (\w\pseudo_proj_True n ` g -` {g z}. prob (pseudo_proj_True (Suc n) -` {w} \ space M)) * f (pseudo_proj_True n z) + (\w\pseudo_proj_False n ` g -` {g z}. prob (pseudo_proj_True (Suc n) -` {w} \ space M)) * f (pseudo_proj_False n z)" by (simp add: sum_distrib_right) also have "... = (\w\pseudo_proj_True n ` g -` {g z}. prob ({x. stake n x = stake n w}) * p) * f (pseudo_proj_True n z) + (\w\pseudo_proj_False n ` g -` {g z}. prob (pseudo_proj_True (Suc n) -` {w} \ space M)) * f (pseudo_proj_False n z)" proof - have "\w. w\pseudo_proj_True n ` g -` {g z} \ (prob (pseudo_proj_True (Suc n) -` {w}) = (prob ({x. stake n x = stake n w})) * p)" proof - fix w assume "w\pseudo_proj_True n ` g -` {g z}" hence "\y. w = pseudo_proj_True n y \ g y = g z" by auto from this obtain yt where "w = pseudo_proj_True n yt" and "g yt = g z" by auto hence "snth w n" unfolding pseudo_proj_True_def by simp have "pseudo_proj_True (Suc n) w = w" using \w = pseudo_proj_True n yt\ by (simp add: pseudo_proj_True_Suc_proj) hence "pseudo_proj_True (Suc n) -` {w} = {x. stake (Suc n) x = stake (Suc n) w}" using pseudo_proj_True_preimage_stake by simp hence "prob (pseudo_proj_True (Suc n) -` {w}) = prob {x. stake n x = stake n w} * prob_component p w n" using bernoulli_stream_element_prob_rec' bernoulli bernoulli_stream_space p_lt_1 p_gt_0 by simp also have "... = prob {x. stake n x = stake n w} * p" using \snth w n\ unfolding prob_component_def by simp finally show "prob (pseudo_proj_True (Suc n) -` {w}) = prob {x. stake n x = stake n w} * p" . qed thus ?thesis using bernoulli bernoulli_stream_space by simp qed also have "... = (\w\pseudo_proj_True n ` g -` {g z}. prob ({x. stake n x = stake n w}) * p) * f (pseudo_proj_True n z) + (\w\pseudo_proj_False n ` g -` {g z}. prob {x. stake n x = stake n w} * (1 -p)) * f (pseudo_proj_False n z)" proof - have "\w. w\pseudo_proj_False n ` g -` {g z} \ (prob (pseudo_proj_True (Suc n) -` {w} \ space M) = (prob {x. stake n x = stake n w}) * (1-p))" proof - fix w assume "w\pseudo_proj_False n ` g -` {g z}" hence "\y. w = pseudo_proj_False n y \ g y = g z" by auto from this obtain yt where "w = pseudo_proj_False n yt" and "g yt = g z" by auto hence "\snth w n" unfolding pseudo_proj_False_def by simp have "pseudo_proj_True (Suc n) w = w" using \w = pseudo_proj_False n yt\ by (simp add: pseudo_proj_True_Suc_False_proj) hence "pseudo_proj_True (Suc n) -`{w} = {x. stake (Suc n) x = stake (Suc n) w}" using pseudo_proj_True_preimage_stake by simp hence "prob (pseudo_proj_True (Suc n) -`{w}) = prob {x. stake n x = stake n w} * prob_component p w n" using bernoulli_stream_element_prob_rec' bernoulli bernoulli_stream_space p_lt_1 p_gt_0 by simp also have "... = prob {x. stake n x = stake n w} * (1-p)" using \\snth w n\ unfolding prob_component_def by simp finally show "prob (pseudo_proj_True (Suc n) -`{w} \ space M) = prob {x. stake n x = stake n w} * (1-p)" using bernoulli bernoulli_stream_space by simp qed thus ?thesis by simp qed also have "... = (\w\pseudo_proj_True n ` g -` {g z}. prob ({x. stake n x = stake n w})) * p * f (pseudo_proj_True n z) + (\w\pseudo_proj_False n ` g -` {g z}. prob {x. stake n x = stake n w}) * (1 -p) * f (pseudo_proj_False n z)" by (simp add:sum_distrib_right) also have "... = prob (g -` {g z}) * p * f (pseudo_proj_True n z) + (\w\pseudo_proj_False n ` g -` {g z}. prob {x. stake n x = stake n w}) * (1 -p) * f (pseudo_proj_False n z)" proof - have projset: "\w. w\pseudo_proj_True n ` g -` {g z} \ {x. stake n x = stake n w} \ sets M" proof - fix w assume "w\ pseudo_proj_True n ` g -` {g z}" hence "\y. w = pseudo_proj_True n y" by auto from this obtain y where "w = pseudo_proj_True n y" by auto hence "w = pseudo_proj_True n w" by (simp add: pseudo_proj_True_proj) hence "pseudo_proj_True n -`{w} = {x. stake n x = stake n w}" using pseudo_proj_True_preimage_stake by simp moreover have "pseudo_proj_True n -`{w} \ sets M" using \w = pseudo_proj_True n w\ bernoulli bernoulli_stream_space pseudo_proj_True_singleton by auto ultimately show "{x. stake n x = stake n w} \ sets M" by simp qed have "(\w\pseudo_proj_True n ` g -` {g z}. prob ({x. stake n x = stake n w})) = prob (\w\pseudo_proj_True n ` g -` {g z}. {x. stake n x = stake n w})" proof (rule finite_measure_finite_Union[symmetric]) show "finite (pseudo_proj_True n ` g -` {g z})" by (meson finite_subset image_mono pseudo_proj_True_finite_image subset_UNIV) show "(\i. {x. stake n x = stake n i}) ` pseudo_proj_True n ` g -` {g z} \ events" using projset by auto show "disjoint_family_on (\i. {x. stake n x = stake n i}) (pseudo_proj_True n ` g -` {g z})" unfolding disjoint_family_on_def proof (intro ballI impI) fix u v assume "u \ pseudo_proj_True n ` g -` {g z}" and "v\ pseudo_proj_True n ` g -` {g z}" and "u \ v" note uvprops = this show "{x. stake n x = stake n u} \ {x. stake n x = stake n v} = {}" proof (rule ccontr) assume "{x. stake n x = stake n u} \ {x. stake n x = stake n v} \ {}" hence "\ uu. uu\ {x. stake n x = stake n u} \ {x. stake n x = stake n v}" by auto from this obtain uu where "uu\ {x. stake n x = stake n u} \ {x. stake n x = stake n v}" by auto hence "stake n uu = stake n u" and "stake n uu = stake n v" by auto moreover have "stake n u \ stake n v" by (metis uvprops imageE pseudo_proj_True_proj pseudo_proj_True_stake_image) ultimately show False by simp qed qed qed also have "... = prob (\w\pseudo_proj_True n ` g -` {g z}. pseudo_proj_True n -`{w})" proof - have "\w. w\pseudo_proj_True n ` g -` {g z} \ {x. stake n x = stake n w} = pseudo_proj_True n -`{w}" using pseudo_proj_True_preimage_stake pseudo_proj_True_proj by force hence "(\w\pseudo_proj_True n ` g -` {g z}. {x. stake n x = stake n w}) = (\w\pseudo_proj_True n ` g -` {g z}. pseudo_proj_True n -`{w})" by auto thus ?thesis by simp qed also have "... = prob (pseudo_proj_True n -`(pseudo_proj_True n ` g -` {g z}))" by (metis vimage_eq_UN) also have "... = prob (g -` {g z})" using pseudo_proj_preimage[symmetric, of g n N z] pseudo_proj_preimage'[of g n] assms by simp finally have "(\w\pseudo_proj_True n ` g -` {g z}. prob ({x. stake n x = stake n w})) = prob (g -` {g z})" . thus ?thesis by simp qed also have "... = prob (g -` {g z}) * p * f (pseudo_proj_True n z) + prob (g -`{g z}) * (1 -p) * f (pseudo_proj_False n z)" proof - have projset: "\w. w\pseudo_proj_False n ` g -` {g z} \ {x. stake n x = stake n w} \ sets M" proof - fix w assume "w\ pseudo_proj_False n ` g -` {g z}" hence "\y. w = pseudo_proj_False n y" by auto from this obtain y where "w = pseudo_proj_False n y" by auto hence "w = pseudo_proj_False n w" using pseudo_proj_False_def pseudo_proj_False_stake by auto hence "pseudo_proj_False n -`{w} = {x. stake n x = stake n w}" using pseudo_proj_False_preimage_stake by simp moreover have "pseudo_proj_False n -`{w} \ sets M" using \w = pseudo_proj_False n w\ bernoulli bernoulli_stream_space pseudo_proj_False_singleton by auto ultimately show "{x. stake n x = stake n w} \ sets M" by simp qed have "(\w\pseudo_proj_False n ` g -` {g z}. prob ({x. stake n x = stake n w})) = prob (\w\pseudo_proj_False n ` g -` {g z}. {x. stake n x = stake n w})" proof (rule finite_measure_finite_Union[symmetric]) show "finite (pseudo_proj_False n ` g -` {g z})" by (meson finite_subset image_mono pseudo_proj_False_finite_image subset_UNIV) show "(\i. {x. stake n x = stake n i}) ` pseudo_proj_False n ` g -` {g z} \ events" using projset by auto show "disjoint_family_on (\i. {x. stake n x = stake n i}) (pseudo_proj_False n ` g -` {g z})" unfolding disjoint_family_on_def proof (intro ballI impI) fix u v assume "u \ pseudo_proj_False n ` g -` {g z}" and "v\ pseudo_proj_False n ` g -` {g z}" and "u \ v" note uvprops = this show "{x. stake n x = stake n u} \ {x. stake n x = stake n v} = {}" proof (rule ccontr) assume "{x. stake n x = stake n u} \ {x. stake n x = stake n v} \ {}" hence "\ uu. uu\ {x. stake n x = stake n u} \ {x. stake n x = stake n v}" by auto from this obtain uu where "uu\ {x. stake n x = stake n u} \ {x. stake n x = stake n v}" by auto hence "stake n uu = stake n u" and "stake n uu = stake n v" by auto moreover have "stake n u \ stake n v" using pseudo_proj_False_def pseudo_proj_False_stake uvprops by auto ultimately show False by simp qed qed qed also have "... = prob (\w\pseudo_proj_False n ` g -` {g z}. pseudo_proj_False n -`{w})" proof - have "\w. w\pseudo_proj_False n ` g -` {g z} \ {x. stake n x = stake n w} = pseudo_proj_False n -`{w}" using pseudo_proj_False_preimage_stake pseudo_proj_False_def pseudo_proj_False_stake by force hence "(\w\pseudo_proj_False n ` g -` {g z}. {x. stake n x = stake n w}) = (\w\pseudo_proj_False n ` g -` {g z}. pseudo_proj_False n -`{w})" by auto thus ?thesis by simp qed also have "... = prob (pseudo_proj_False n -`(pseudo_proj_False n ` g -` {g z}))" by (metis vimage_eq_UN) also have "... = prob (g -` {g z})" using pseudo_proj_False_preimage[symmetric, of g n N z] pseudo_proj_False_preimage'[of g n] assms by simp finally have "(\w\pseudo_proj_False n ` g -` {g z}. prob ({x. stake n x = stake n w})) = prob (g -` {g z})" . thus ?thesis by simp qed also have "... = prob (g -` {g z}) * (p * f (pseudo_proj_True n z) + (1 -p) * f (pseudo_proj_False n z))" using distrib_left[symmetric, of "prob (g -` {g z})" "p * f (pseudo_proj_True n z)" "(1 - p) * f (pseudo_proj_False n z)"] by simp finally show "expectation (\x. f x * indicator (g -` {g z}) x) = prob (g -` {g z}) * (p * f (pseudo_proj_True n z) + (1 -p) * f (pseudo_proj_False n z))" unfolding expind_def . qed lemma (in infinite_cts_filtration) borel_Suc_expectation_pseudo_proj: fixes f::"bool stream\ real" assumes "f\ borel_measurable (F (Suc n))" shows "expectation (\x. f x * indicator (pseudo_proj_True n -` {pseudo_proj_True n z}) x) = prob (pseudo_proj_True n -` {pseudo_proj_True n z}) * (p * (f (pseudo_proj_True n z)) + (1-p) * (f (pseudo_proj_False n z)))" proof (rule borel_Suc_expectation) show "f \ borel_measurable (F (Suc n))" using assms by simp show "pseudo_proj_True n \ F n \\<^sub>M M" by (simp add: nat_filtration_pseudo_proj_True_measurable natural_filtration) show "pseudo_proj_True n -` {pseudo_proj_True n z} \ sets (F n)" by (simp add: nat_filtration_singleton natural_filtration pseudo_proj_True_proj) show "\y z. (pseudo_proj_True n y = pseudo_proj_True n z \ snth y n = snth z n) \ f y = f z" proof (intro allI impI conjI) fix y z assume "pseudo_proj_True n y = pseudo_proj_True n z \ y !! n = z !! n" hence "pseudo_proj_True n y = pseudo_proj_True n z" and "snth y n = snth z n" by auto hence "pseudo_proj_True (Suc n) y = pseudo_proj_True (Suc n) z" unfolding pseudo_proj_True_def by (metis (full_types) \pseudo_proj_True n y = pseudo_proj_True n z\ pseudo_proj_True_same_img stake_Suc) thus "f y = f z" using nat_filtration_info assms natural_filtration by (metis comp_apply) qed show "set_discriminating n (pseudo_proj_True n) M" unfolding set_discriminating_def using pseudo_proj_True_proj by simp qed lemma (in infinite_cts_filtration) f_borel_Suc_expl_cond_expect: assumes "f\ borel_measurable (F (Suc n))" and "g\ measurable (F n) N" and "set_discriminating n g N" and "g -` {g w} \ sets (F n)" and "\y z. (g y = g z \ snth y n = snth z n) \ f y = f z" and "0 < p" and "p < 1" shows "expl_cond_expect M g f w = p * f (pseudo_proj_True n w) + (1 - p) * f (pseudo_proj_False n w)" proof - have nz:"prob (g -`{g w}) \ 0" proof - have "pseudo_proj_True n -`{pseudo_proj_True n w} \ g -` {g w}" proof - have "\f n m s. f \ F n \\<^sub>M m \ \ set_discriminating n f m \ pseudo_proj_True n -` f -` {f s::'a} = f -` {f s}" by (meson pseudo_proj_preimage') then show ?thesis using assms by blast qed moreover have "prob (pseudo_proj_True n -`{pseudo_proj_True n w}) > 0" using bernoulli_stream_pref_prob_pos pseudo_proj_True_preimage_stake bernoulli bernoulli_stream_space emeasure_eq_measure pseudo_proj_True_proj assms by auto moreover have "pseudo_proj_True n -`{pseudo_proj_True n w} \ sets M" using bernoulli bernoulli_stream_space pseudo_proj_True_proj pseudo_proj_True_singleton by auto moreover have "g -`{g w} \ events" using assms natural_filtration nat_filtration_subalgebra unfolding subalgebra_def by blast ultimately show ?thesis using measure_increasing increasingD proof - have "g -` {g w} \ events \ pseudo_proj_True n -` {pseudo_proj_True n w} \ events \ prob (pseudo_proj_True n -` {pseudo_proj_True n w}) \ prob (g -` {g w})" using \pseudo_proj_True n -` {pseudo_proj_True n w} \ g -` {g w}\ increasingD measure_increasing by blast then show ?thesis using \0 < prob (pseudo_proj_True n -` {pseudo_proj_True n w})\ \g -` {g w} \ events\ \pseudo_proj_True n -` {pseudo_proj_True n w} \ events\ by linarith qed qed hence "expl_cond_expect M g f w = expectation (\x. f x * indicator (g -` {g w} \ space M) x) / prob (g -` {g w} \ space M)" unfolding expl_cond_expect_def img_dce_def by simp also have "... = expectation (\x. f x * indicator (g -` {g w}) x) / prob (g -` {g w})" using bernoulli by (simp add:bernoulli_stream_space) also have "... = prob (g -` {g w}) * (p * f (pseudo_proj_True n w) + (1 -p) * f (pseudo_proj_False n w)) / prob (g -` {g w})" proof - have "expectation (\x. f x * indicator (g -` {g w}) x) = prob (g -` {g w}) * (p * f (pseudo_proj_True n w) + (1 -p) * f (pseudo_proj_False n w))" proof (rule borel_Suc_expectation) show "f \ borel_measurable (F (Suc n))" using assms by simp show "g \ F n \\<^sub>M N" using assms by simp show "set_discriminating n g N" using assms by simp show "g -` {g w} \ sets (F n)" using assms by simp show "\y z. g y = g z \ y !! n = z !! n \ f y = f z" using assms(5) by blast qed thus ?thesis by simp qed also have "... = p * f (pseudo_proj_True n w) + (1 -p) * f (pseudo_proj_False n w)" using nz by simp finally show ?thesis . qed lemma (in infinite_cts_filtration) f_borel_Suc_real_cond_exp: assumes "f\ borel_measurable (F (Suc n))" and "g\ measurable (F n) N" and "set_discriminating n g N" and "\w. g -` {g w} \ sets (F n)" and "\r\range g \ space N. \A\sets N. range g \ A = {r}" and "\y z. (g y = g z \ snth y n = snth z n) \ f y = f z" and "0 < p" and "p < 1" shows "AE w in M. real_cond_exp M (fct_gen_subalgebra M N g) f w = p * f (pseudo_proj_True n w) + (1 - p) * f (pseudo_proj_False n w)" proof - have "AE w in M. real_cond_exp M (fct_gen_subalgebra M N g) f w = expl_cond_expect M g f w" proof (rule charact_cond_exp') show "disc_fct g" proof - have "g = g \ (pseudo_proj_True n)" using nat_filtration_not_borel_info[of g n] assms natural_filtration by simp have "disc_fct (pseudo_proj_True n)" unfolding disc_fct_def using pseudo_proj_True_finite_image by (simp add: countable_finite) hence "disc_fct (g \ (pseudo_proj_True n))" unfolding disc_fct_def by (metis countable_image image_comp) thus ?thesis using \g = g \ (pseudo_proj_True n)\ by simp qed show "integrable M f" using assms nat_filtration_borel_measurable_integrable natural_filtration by simp show "random_variable N g" using assms filtration_measurable natural_filtration nat_filtration_subalgebra using nat_discrete_filtration by blast show "\r\range g \ space N. \A\sets N. range g \ A = {r}" using assms by simp qed moreover have "\w. expl_cond_expect M g f w = p * f (pseudo_proj_True n w) + (1 - p) * f (pseudo_proj_False n w)" using assms f_borel_Suc_expl_cond_expect by blast ultimately show ?thesis by simp qed lemma (in infinite_cts_filtration) f_borel_Suc_real_cond_exp_proj: assumes "f\ borel_measurable (F (Suc n))" and "0 < p" and "p < 1" shows "AE w in M. real_cond_exp M (fct_gen_subalgebra M M (pseudo_proj_True n)) f w = p * f (pseudo_proj_True n w) + (1 - p) * f (pseudo_proj_False n w)" proof (rule f_borel_Suc_real_cond_exp) show "f \ borel_measurable (F (Suc n))" using assms by simp show "pseudo_proj_True n \ F n \\<^sub>M M" by (simp add: nat_filtration_pseudo_proj_True_measurable natural_filtration) show "\w. pseudo_proj_True n -` {pseudo_proj_True n w} \ sets (F n)" proof fix w show "pseudo_proj_True n -` {pseudo_proj_True n w} \ sets (F n) " by (simp add: nat_filtration_singleton natural_filtration pseudo_proj_True_proj) qed show "\r\range (pseudo_proj_True n) \ space M. \A\events. range (pseudo_proj_True n) \ A = {r}" proof (intro ballI) fix r assume "r \ range (pseudo_proj_True n) \ space M" hence "r\ range (pseudo_proj_True n)" and "r\ space M" by auto hence "pseudo_proj_True n r = r" using pseudo_proj_True_proj by auto hence "(pseudo_proj_True n) -`{r} \ space M \ sets M" using pseudo_proj_True_singleton bernoulli by simp moreover have "range (pseudo_proj_True n) \ ((pseudo_proj_True n) -`{r} \ space M) = {r}" proof have "r\ range (pseudo_proj_True n) \ (pseudo_proj_True n -` {r} \ space M)" using \pseudo_proj_True n r = r\ \r \ range (pseudo_proj_True n)\ \r \ space M\ by blast thus "{r} \ range (pseudo_proj_True n) \ (pseudo_proj_True n -` {r} \ space M)" by auto show "range (pseudo_proj_True n) \ (pseudo_proj_True n -` {r} \ space M) \ {r}" proof fix x assume "x \ range (pseudo_proj_True n) \ (pseudo_proj_True n -` {r} \ space M)" hence "x\ range (pseudo_proj_True n)" and "x\ (pseudo_proj_True n -` {r})" by auto have "x = pseudo_proj_True n x" using \x\ range (pseudo_proj_True n)\ pseudo_proj_True_proj by auto also have "... = r" using \x\ (pseudo_proj_True n -` {r})\ by simp finally have "x = r" . thus "x\ {r}" by simp qed qed ultimately show "\A\events. range (pseudo_proj_True n) \ A = {r}" by auto qed show "\y z. pseudo_proj_True n y = pseudo_proj_True n z \ y !! n = z !! n \ f y = f z" proof (intro allI impI conjI) fix y z assume "pseudo_proj_True n y = pseudo_proj_True n z \ y !! n = z !! n" hence "pseudo_proj_True n y = pseudo_proj_True n z" and "snth y n = snth z n" by auto hence "pseudo_proj_True (Suc n) y = pseudo_proj_True (Suc n) z" unfolding pseudo_proj_True_def by (metis (full_types) \pseudo_proj_True n y = pseudo_proj_True n z\ pseudo_proj_True_same_img stake_Suc) thus "f y = f z" using nat_filtration_info assms natural_filtration by (metis comp_apply) qed show "set_discriminating n (pseudo_proj_True n) M" unfolding set_discriminating_def using pseudo_proj_True_proj by simp show "0 < p" and "p < 1" using assms by auto qed subsection \Images of stochastic processes by prefixes of streams\ text \We define a function that, given a stream of coin tosses and a stochastic process, returns a stream of the values of the stochastic process up to a given time. This function will be used to characterize the smallest filtration that, at any time n, makes each random variable of a given stochastic process measurable up to time n.\ subsubsection \Definitions\ primrec smap_stoch_proc where "smap_stoch_proc 0 f k w = []" | "smap_stoch_proc (Suc n) f k w = (f k w) # (smap_stoch_proc n f (Suc k) w)" lemma smap_stoch_proc_length: shows "length (smap_stoch_proc n f k w) = n" by (induction n arbitrary:k) auto lemma smap_stoch_proc_nth: shows "Suc p \ Suc n \ nth (smap_stoch_proc (Suc n) f k w) p = f (k+p) w" proof (induction n arbitrary:p k) case 0 hence "p = 0" by simp hence "(smap_stoch_proc (Suc 0) f k w) ! p = ((f k w) # (smap_stoch_proc 0 f (Suc k) w))!0" by simp also have "... = f (k+p) w" using \p=0\ by simp finally show ?case . next case (Suc n) show ?case proof (cases "\m. p = Suc m") case True from this obtain m where "p = Suc m" by auto hence "smap_stoch_proc (Suc (Suc n)) f k w ! p = (smap_stoch_proc (Suc n) f (Suc k) w) ! m" by simp also have "... = f ((Suc k) + m) w" using Suc(1)[of m] Suc.prems \p = Suc m\ by blast also have "... = f (k + (Suc m)) w" by simp finally show "smap_stoch_proc (Suc (Suc n)) f k w ! p = f (k + p) w" using \p = Suc m\ by simp next case False hence "p = 0" using less_Suc_eq_0_disj by blast thus "smap_stoch_proc (Suc (Suc n)) f k w ! p = f (k+p) w" by simp qed qed definition proj_stoch_proc where "proj_stoch_proc f n = (\w. shift (smap_stoch_proc n f 0 w) (sconst (f n w)))" lemma proj_stoch_proc_component: shows "k < n \ (snth (proj_stoch_proc f n w) k) = f k w" and "n \ k \ (snth (proj_stoch_proc f n w) k) = f n w" proof - show "k < n \ proj_stoch_proc f n w !! k = f k w" proof - assume "k < n" hence "\m. n = Suc m" using less_imp_Suc_add by blast from this obtain m where "n = Suc m" by auto have "proj_stoch_proc f n w !! k = (smap_stoch_proc n f 0 w) ! k" unfolding proj_stoch_proc_def using \k by (simp add: smap_stoch_proc_length) also have "... = f k w" using \n = Suc m\ \k < n\ smap_stoch_proc_nth by (metis Suc_leI add.left_neutral) finally show ?thesis . qed show "n \ k \ (snth (proj_stoch_proc f n w) k) = f n w" proof - assume "n \ k" hence "proj_stoch_proc f n w !! k = (sconst (f n w)) !! (k - n)" by (simp add: proj_stoch_proc_def smap_stoch_proc_length) also have "... = f n w" by simp finally show ?thesis . qed qed lemma proj_stoch_proc_component': assumes "k \ n" shows "f k x = snth (proj_stoch_proc f n x) k" proof (cases "k < n") case True thus ?thesis using proj_stoch_proc_component[of k n f x] assms by simp next case False hence "k = n" using assms by simp thus ?thesis using proj_stoch_proc_component[of k n f x] assms by simp qed lemma proj_stoch_proc_eq_snth: assumes "proj_stoch_proc f n x = proj_stoch_proc f n y" and "k \ n" shows "f k x = f k y" proof - have "f k x = snth (proj_stoch_proc f n x) k" using assms proj_stoch_proc_component'[of k n f] by simp also have "... = snth (proj_stoch_proc f n y) k" using assms by simp also have "... = f k y" using assms proj_stoch_proc_component'[of k n f] by simp finally show ?thesis . qed lemma proj_stoch_measurable_if_adapted: assumes "filtration M F" and "adapt_stoch_proc F f N" shows "proj_stoch_proc f n \ measurable M (stream_space N)" proof (rule measurable_stream_space2) fix m show "(\x. proj_stoch_proc f n x !! m) \ M \\<^sub>M N" proof (cases "m < n") case True hence "\x. proj_stoch_proc f n x !! m = f m x" by (simp add: proj_stoch_proc_component) hence "(\x. proj_stoch_proc f n x !! m) = f m" by simp thus ?thesis using assms unfolding adapt_stoch_proc_def filtration_def by (metis measurable_from_subalg) next case False hence "\x. proj_stoch_proc f n x !! m = f n x" by (simp add: proj_stoch_proc_component) hence "(\x. proj_stoch_proc f n x !! m) = f n" by simp thus ?thesis using assms unfolding adapt_stoch_proc_def filtration_def by (metis measurable_from_subalg) qed qed lemma proj_stoch_adapted_if_adapted: assumes "filtration M F" and "adapt_stoch_proc F f N" shows "proj_stoch_proc f n \ measurable (F n) (stream_space N)" proof (rule measurable_stream_space2) fix m show "(\x. proj_stoch_proc f n x !! m) \ measurable (F n) N" proof (cases "m < n") case True hence "\x. proj_stoch_proc f n x !! m = f m x" by (simp add: proj_stoch_proc_component) hence "(\x. proj_stoch_proc f n x !! m) = f m" by simp thus ?thesis using assms unfolding adapt_stoch_proc_def filtration_def by (metis True measurable_from_subalg not_less order.asym) next case False hence "\x. proj_stoch_proc f n x !! m = f n x" by (simp add: proj_stoch_proc_component) hence "(\x. proj_stoch_proc f n x !! m) = f n" by simp thus ?thesis using assms unfolding adapt_stoch_proc_def by metis qed qed lemma proj_stoch_adapted_if_adapted': assumes "filtration M F" and "adapt_stoch_proc F f N" shows "adapt_stoch_proc F (proj_stoch_proc f) (stream_space N)" unfolding adapt_stoch_proc_def proof fix n show "proj_stoch_proc f n \ F n \\<^sub>M stream_space N" using assms by (simp add: proj_stoch_adapted_if_adapted) qed lemma (in infinite_cts_filtration) proj_stoch_proj_invariant: fixes X::"nat \ bool stream \ 'b::{t0_space}" assumes "borel_adapt_stoch_proc F X" shows "proj_stoch_proc X n w = proj_stoch_proc X n (pseudo_proj_True n w)" proof - have "\m. snth (proj_stoch_proc X n w) m = snth (proj_stoch_proc X n (pseudo_proj_True n w)) m" proof - fix m show "snth (proj_stoch_proc X n w) m = snth (proj_stoch_proc X n (pseudo_proj_True n w)) m" proof (cases "m < n") case True hence "snth (proj_stoch_proc X n w) m = X m w" by (simp add: proj_stoch_proc_component) also have "... = X m (pseudo_proj_True n w)" proof (rule borel_adapt_nat_filtration_info[symmetric], (simp add:assms)) show "m \ n" using True by linarith qed also have "... = snth (proj_stoch_proc X n (pseudo_proj_True n w)) m" using True by (simp add: proj_stoch_proc_component) finally show ?thesis . next case False hence "snth (proj_stoch_proc X n w) m = X n w" by (simp add: proj_stoch_proc_component) also have "... = X n (pseudo_proj_True n w)" by (rule borel_adapt_nat_filtration_info[symmetric]) (auto simp add:assms) also have "... = snth (proj_stoch_proc X n (pseudo_proj_True n w)) m" using False by (simp add: proj_stoch_proc_component) finally show ?thesis . qed qed thus "proj_stoch_proc X n w = proj_stoch_proc X n (pseudo_proj_True n w)" using diff_streams_only_if by auto qed lemma (in infinite_cts_filtration) proj_stoch_set_finite_range: fixes X::"nat \ bool stream \ 'b::{t0_space}" assumes "borel_adapt_stoch_proc F X" shows "finite (range (proj_stoch_proc X n))" proof - have "finite (range (pseudo_proj_True n))" using pseudo_proj_True_finite_image by simp moreover have "proj_stoch_proc X n = (proj_stoch_proc X n) \ (pseudo_proj_True n)" proof fix x show "proj_stoch_proc X n x = (proj_stoch_proc X n \ pseudo_proj_True n) x" using assms proj_stoch_proj_invariant by (metis comp_apply) qed ultimately show ?thesis by (metis finite_imageI fun.set_map) qed lemma (in infinite_cts_filtration) proj_stoch_set_discriminating: fixes X::"nat \ bool stream \ 'b::{t0_space}" assumes "borel_adapt_stoch_proc F X" shows "set_discriminating n (proj_stoch_proc X n) N" proof - have "\w. proj_stoch_proc X n w = proj_stoch_proc X n (pseudo_proj_True n w)" using assms proj_stoch_proj_invariant by auto thus ?thesis unfolding set_discriminating_def by simp qed lemma (in infinite_cts_filtration) proj_stoch_preimage: assumes "borel_adapt_stoch_proc F X" shows "(proj_stoch_proc X n) -` {proj_stoch_proc X n w} = (\i\ {m. m \ n}. (X i) -` {X i w})" proof define psX where "psX = proj_stoch_proc X n" show "proj_stoch_proc X n -` {proj_stoch_proc X n w} \ (\i\{m. m \ n}. X i -` {X i w})" proof fix x assume "x \ proj_stoch_proc X n -` {proj_stoch_proc X n w}" hence "psX x = psX w" unfolding psX_def using assms by simp hence "\i. i \{m. m \ n} \ x \ (X i) -`{X i w}" proof - fix i assume "i\ {m. m\n}" hence "i \ n" by auto have "X i x = snth (psX x) i" unfolding psX_def by (metis Suc_le_eq Suc_le_mono \i \ n\ le_Suc_eq nat.simps(1) proj_stoch_proc_component(1) proj_stoch_proc_component(2)) also have "... = snth (psX w) i" using \psX x = psX w\ by simp also have "... = X i w" unfolding psX_def by (metis Suc_le_eq Suc_le_mono \i \ n\ le_Suc_eq nat.simps(1) proj_stoch_proc_component(1) proj_stoch_proc_component(2)) finally have "X i x = X i w" . thus "x \ (X i) -`{X i w}" by simp qed thus "x \ (\i\{m. m \ n}. (X i) -` {X i w})" by auto qed show "(\i\{m. m \ n}. (X i) -` {X i w}) \ (proj_stoch_proc X n) -` {proj_stoch_proc X n w}" proof fix x assume "x\ (\i\{m. m \ n}. (X i) -` {X i w})" hence "\i. i \{m. m \ n} \ x \ (X i) -`{X i w}" by simp hence "\i. i \{m. m \ n} \ X i x = X i w" by simp hence "\i. i \ n \ X i x = X i w" by auto hence "psX x = psX w" unfolding psX_def by (metis (mono_tags, hide_lams) diff_streams_only_if linear not_le order_refl proj_stoch_proc_component(1) proj_stoch_proc_component(2)) thus "x \ (proj_stoch_proc X n) -` {proj_stoch_proc X n w}" unfolding psX_def by auto qed qed lemma (in infinite_cts_filtration) proj_stoch_singleton_set: fixes X::"nat \ bool stream \ ('b::t2_space)" assumes "borel_adapt_stoch_proc F X" shows "(proj_stoch_proc X n) -` {proj_stoch_proc X n w} \ sets (F n)" proof - have "\i. i \ n \ (X i) \ measurable (F n) borel" by (meson adapt_stoch_proc_def assms increasing_measurable_info) have "(\i\ {m. m \ n}. (X i) -` {X i w}) \ sets (F n)" proof ((rule sigma_algebra.countable_INT''), auto) show "sigma_algebra (space (F n)) (sets (F n))" using measure_space measure_space_def by auto show "UNIV \ sets (F n)" using \sigma_algebra (space (F n)) (sets (F n))\ nat_filtration_space natural_filtration sigma_algebra.sigma_sets_eq sigma_sets_top by fastforce have "\i. i \ n \ (X i) -` {X i w} \ sets (nat_filtration n)" proof (rule nat_filtration_borel_measurable_singleton) fix i assume "i \ n" show "X i \ borel_measurable (nat_filtration n)" using assms natural_filtration unfolding adapt_stoch_proc_def using \i \ n\ increasing_measurable_info by blast qed thus "\i. i \ n \ (X i) -` {X i w} \ sets (F n)" using natural_filtration by simp qed thus ?thesis using assms by (simp add: proj_stoch_preimage) qed lemma (in infinite_cts_filtration) finite_range_stream_space: fixes f::"'a \ 'b::t1_space" assumes "finite (range f)" shows "(\w. snth w i) -` (open_exclude_set (f x) (range f)) \ sets (stream_space borel)" proof - define opex where "opex = open_exclude_set (f x) (range f)" have "open opex" and "opex \ (range f) = {f x}" using assms unfolding opex_def by (auto simp add:open_exclude_finite) hence "opex\ sets borel" by simp hence vim: "(\w. snth w i) -` opex \ sets (vimage_algebra (streams (space borel)) (\w. snth w i) borel)" by (metis in_vimage_algebra inf_top.right_neutral space_borel streams_UNIV) have "(\w. snth w i) -` opex \ sets (\i. vimage_algebra (streams (space borel)) (\w. snth w i) borel)" proof (rule in_sets_SUP, simp) show "\i. i \ UNIV \ space (vimage_algebra (streams (space borel)) (\w. w !! i) borel) = UNIV" by simp show "(\w. w !! i) -` opex \ sets (vimage_algebra (streams (space borel)) (\w. w !! i) borel)" using vim by simp qed thus ?thesis using sets_stream_space_eq unfolding opex_def by blast qed lemma (in infinite_cts_filtration) proj_stoch_range_singleton: fixes X::"nat \ bool stream \ ('b::t2_space)" assumes "borel_adapt_stoch_proc F X" and "r\ range (proj_stoch_proc X n)" shows "\A\sets (stream_space borel). range (proj_stoch_proc X n) \ A = {r}" proof - have "\x. r = proj_stoch_proc X n x" using assms by auto from this obtain x where "r = proj_stoch_proc X n x" by auto have "\i. i \ n \ (X i) \ measurable (F n) borel" by (meson adapt_stoch_proc_def assms increasing_measurable_info) hence fin: "\i. i \ n \ finite (range (X i))" by (metis bernoulli bernoulli_stream_space nat_filtration_vimage_finite natural_filtration streams_UNIV) show ?thesis proof define cand where "cand = (\i \ {m. m\ n}. (\w. snth w i) -` (open_exclude_set (X i x) (range (X i))))" show "cand \ sets (stream_space borel)" unfolding cand_def proof ((rule sigma_algebra.countable_INT''), auto) show "UNIV \ sets (stream_space borel)" by (metis space_borel streams_UNIV streams_stream_space) show "sigma_algebra (space (stream_space borel)) (sets (stream_space borel))" by (simp add: sets.sigma_algebra_axioms) show "\i. i \ n \ (\w. w !! i) -` open_exclude_set (X i x) (range (X i)) \ sets (stream_space borel)" proof - fix i assume "i \ n" thus "(\w. w !! i) -` open_exclude_set (X i x) (range (X i)) \ sets (stream_space borel)" using fin by (simp add:finite_range_stream_space) qed qed have "range (proj_stoch_proc X n) \ cand = {proj_stoch_proc X n x}" proof have "proj_stoch_proc X n x \ range (proj_stoch_proc X n) \ cand" proof show "proj_stoch_proc X n x \ range (proj_stoch_proc X n)" by simp show "proj_stoch_proc X n x \ cand" unfolding cand_def proof fix i assume "i\ {m. m\ n}" hence "i \ n" by simp hence "snth (proj_stoch_proc X n x) i = X i x" by (metis le_antisym not_less proj_stoch_proc_component) also have "... \ open_exclude_set (X i x) (range (X i))" using assms open_exclude_finite(2) by (metis IntE \i \ n\ fin insert_iff rangeI) finally have "snth (proj_stoch_proc X n x) i \ open_exclude_set (X i x) (range (X i))" . thus "proj_stoch_proc X n x \ (\w. w !! i) -` open_exclude_set (X i x) (range (X i))" by simp qed qed thus "{proj_stoch_proc X n x} \ range (proj_stoch_proc X n) \ cand" by simp show "range (proj_stoch_proc X n) \ cand \ {proj_stoch_proc X n x}" proof fix z assume "z\ range (proj_stoch_proc X n) \ cand" hence "\y. z = proj_stoch_proc X n y" by auto from this obtain y where "z = proj_stoch_proc X n y" by auto hence "proj_stoch_proc X n y \ cand" using \z\ range (proj_stoch_proc X n) \ cand\ by simp have "\i. i\n \ X i y = X i x" proof (intro allI impI) fix i assume "i \ n" hence "X i y = snth (proj_stoch_proc X n y) i" by (metis le_antisym not_less proj_stoch_proc_component) also have "... \ open_exclude_set (X i x) (range (X i))" using \proj_stoch_proc X n y \ cand\ \i \ n\ unfolding cand_def by simp finally have "X i y \ open_exclude_set (X i x) (range (X i))" . thus "X i y = X i x" using assms using assms open_exclude_finite(2) by (metis Int_iff \i \ n\ empty_iff fin insert_iff rangeI) qed hence "\i. snth (proj_stoch_proc X n y) i = snth (proj_stoch_proc X n x) i" using proj_stoch_proc_component by (metis nat_le_linear not_less) hence "proj_stoch_proc X n y = proj_stoch_proc X n x" using diff_streams_only_if by auto thus "z\ {proj_stoch_proc X n x}" using \z = proj_stoch_proc X n y\ by auto qed qed thus "range (proj_stoch_proc X n) \ cand = {r}" using \r = proj_stoch_proc X n x\ by simp qed qed definition (in infinite_cts_filtration) stream_space_single where "stream_space_single X r = (if (\U. U\ sets (stream_space borel) \ U\ (range X) = {r}) then SOME U. U\ sets (stream_space borel) \ U \ (range X) = {r} else {})" lemma (in infinite_cts_filtration) stream_space_singleI: assumes "\U. U\ sets (stream_space borel) \ U\ (range X) = {r}" shows "stream_space_single X r \ sets (stream_space borel) \ stream_space_single X r \ (range X) = {r}" proof - let ?V = "SOME U. U\ sets (stream_space borel) \ U\ (range X) = {r}" have vprop: "?V\ sets (stream_space borel) \ ?V \ (range X) = {r}" using someI_ex[of "\U. U\ sets (stream_space borel) \ U\ (range X) = {r}"] assms by blast show ?thesis by (simp add:stream_space_single_def vprop assms) qed lemma (in infinite_cts_filtration) fixes X::"nat \ bool stream \ ('b::t2_space)" assumes "borel_adapt_stoch_proc F X" and "r\ range (proj_stoch_proc X n)" shows stream_space_single_set: "stream_space_single (proj_stoch_proc X n) r \ sets (stream_space borel)" and stream_space_single_preimage: "stream_space_single (proj_stoch_proc X n) r \ range (proj_stoch_proc X n) = {r}" proof - have "\A\sets (stream_space borel). range (proj_stoch_proc X n) \ A = {r}" by (simp add: assms proj_stoch_range_singleton) hence "\U. U \ sets (stream_space borel) \ U \ range (proj_stoch_proc X n) = {r}" by auto hence a: "stream_space_single (proj_stoch_proc X n) r \ sets (stream_space borel) \ stream_space_single (proj_stoch_proc X n) r \ (range (proj_stoch_proc X n)) = {r}" using stream_space_singleI[of "proj_stoch_proc X n"] by simp thus "stream_space_single (proj_stoch_proc X n) r \ sets (stream_space borel)" by simp show "stream_space_single (proj_stoch_proc X n) r \ range (proj_stoch_proc X n) = {r}" using a by simp qed subsubsection \Induced filtration, relationship with filtration generated by underlying stochastic process\ definition comp_proj_i where "comp_proj_i X n i y = {z\ range (proj_stoch_proc X n). snth z i = y}" lemma (in infinite_cts_filtration) comp_proj_i_finite: fixes X::"nat \ bool stream \ 'b::{t0_space}" assumes "borel_adapt_stoch_proc F X" shows "finite (comp_proj_i X n i y)" proof - have "finite (range (proj_stoch_proc X n))" using proj_stoch_set_finite_range[of X] assms by simp thus ?thesis unfolding comp_proj_i_def by simp qed lemma stoch_proc_comp_proj_i_preimage: assumes "i \ n" shows "(X i) -` {X i x} = (\z\ comp_proj_i X n i (X i x). (proj_stoch_proc X n) -` {z})" proof show "X i -` {X i x} \ (\z\comp_proj_i X n i (X i x). proj_stoch_proc X n -` {z})" proof fix w assume "w \ X i -` {X i x}" hence "X i w = X i x" by simp hence "snth (proj_stoch_proc X n w) i = X i x" using assms by (metis le_neq_implies_less proj_stoch_proc_component(1) proj_stoch_proc_component(2)) hence "(proj_stoch_proc X n w) \ comp_proj_i X n i (X i x)" unfolding comp_proj_i_def by simp moreover have "w\ proj_stoch_proc X i -` {proj_stoch_proc X i w}" by simp ultimately show "w\ (\z\comp_proj_i X n i (X i x). proj_stoch_proc X n -` {z})" by simp qed show "(\z\comp_proj_i X n i (X i x). proj_stoch_proc X n -` {z}) \ X i -` {X i x}" proof - have "\z\ comp_proj_i X n i (X i x). proj_stoch_proc X n -` {z} \ X i -` {X i x}" proof fix z assume "z\ comp_proj_i X n i (X i x)" hence "z\ range (proj_stoch_proc X n)" and "snth z i = X i x" unfolding comp_proj_i_def by auto show "proj_stoch_proc X n -` {z} \ X i -` {X i x}" proof fix w assume "w\proj_stoch_proc X n -` {z}" have "X i w = snth (proj_stoch_proc X n w) i" using assms by (metis le_neq_implies_less proj_stoch_proc_component(1) proj_stoch_proc_component(2)) also have "... = snth z i" using \w\proj_stoch_proc X n -` {z}\ by auto also have "... = X i x" using \snth z i = X i x\ by simp finally have "X i w = X i x" . thus "w\ X i -` {X i x}" by simp qed qed thus ?thesis by auto qed qed (* comp_proj to remove? *) definition comp_proj where "comp_proj X n y = {z\ range (proj_stoch_proc X n). snth z n = y}" lemma (in infinite_cts_filtration) comp_proj_finite: fixes X::"nat \ bool stream \ 'b::{t0_space}" assumes "borel_adapt_stoch_proc F X" shows "finite (comp_proj X n y)" proof - have "finite (range (proj_stoch_proc X n))" using proj_stoch_set_finite_range[of X] assms by simp thus ?thesis unfolding comp_proj_def by simp qed lemma stoch_proc_comp_proj_preimage: shows "(X n) -` {X n x} = (\z\ comp_proj X n (X n x). (proj_stoch_proc X n) -` {z})" proof show "X n -` {X n x} \ (\z\comp_proj X n (X n x). proj_stoch_proc X n -` {z})" proof fix w assume "w \ X n -` {X n x}" hence "X n w = X n x" by simp hence "snth (proj_stoch_proc X n w) n = X n x" by (simp add: proj_stoch_proc_component(2)) hence "(proj_stoch_proc X n w) \ comp_proj X n (X n x)" unfolding comp_proj_def by simp moreover have "w\ proj_stoch_proc X n -` {proj_stoch_proc X n w}" by simp ultimately show "w\ (\z\comp_proj X n (X n x). proj_stoch_proc X n -` {z})" by simp qed show "(\z\comp_proj X n (X n x). proj_stoch_proc X n -` {z}) \ X n -` {X n x}" proof - have "\z\ comp_proj X n (X n x). proj_stoch_proc X n -` {z} \ X n -` {X n x}" proof fix z assume "z\ comp_proj X n (X n x)" hence "z\ range (proj_stoch_proc X n)" and "snth z n = X n x" unfolding comp_proj_def by auto show "proj_stoch_proc X n -` {z} \ X n -` {X n x}" proof fix w assume "w\proj_stoch_proc X n -` {z}" have "X n w = snth (proj_stoch_proc X n w) n" by (simp add: proj_stoch_proc_component(2)) also have "... = snth z n" using \w\proj_stoch_proc X n -` {z}\ by auto also have "... = X n x" using \snth z n = X n x\ by simp finally have "X n w = X n x" . thus "w\ X n -` {X n x}" by simp qed qed thus ?thesis by auto qed qed lemma comp_proj_stoch_proc_preimage: shows "(proj_stoch_proc X n) -` {proj_stoch_proc X n x} = (\ i\ {m. m\n}. (X i) -`{X i x})" proof show "proj_stoch_proc X n -` {proj_stoch_proc X n x} \ (\i\{m. m \ n}. X i -` {X i x})" proof fix z assume "z\ proj_stoch_proc X n -` {proj_stoch_proc X n x}" hence "proj_stoch_proc X n z = proj_stoch_proc X n x" by simp hence "\i\n. X i z = X i x" using proj_stoch_proc_component by (metis less_le) hence "\i\n. z\ X i -`{X i x}" by simp thus "z\ (\i\{m. m \ n}. X i -` {X i x})" by simp qed show "(\i\{m. m \ n}. X i -` {X i x}) \ proj_stoch_proc X n -` {proj_stoch_proc X n x}" proof fix z assume "z\ (\i\{m. m \ n}. X i -` {X i x})" hence "\i\ n. X i z = X i x" by auto hence "\i. snth (proj_stoch_proc X n z) i = snth (proj_stoch_proc X n x) i" using proj_stoch_proc_component by (metis nat_le_linear not_less) hence "proj_stoch_proc X n z = proj_stoch_proc X n x" using diff_streams_only_if by auto thus "z\ proj_stoch_proc X n -` {proj_stoch_proc X n x}" by simp qed qed definition stoch_proc_filt where "stoch_proc_filt M X N (n::nat) = gen_subalgebra M (sigma_sets (space M) (\ i\ {m. m\ n}. {(X i -`A) \ (space M) | A. A\ sets N }))" lemma stoch_proc_filt_space: shows "space (stoch_proc_filt M X N n) = space M" unfolding stoch_proc_filt_def by (simp add:gen_subalgebra_space) lemma stoch_proc_filt_sets: assumes "\i. i \ n\ (X i) \ measurable M N" shows "sets (stoch_proc_filt M X N n) = (sigma_sets (space M) (\ i\ {m. m\ n}. {(X i -`A) \ (space M) | A. A\ sets N }))" unfolding stoch_proc_filt_def proof (rule gen_subalgebra_sigma_sets) show "sigma_algebra (space M) (sigma_sets (space M) (\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets N}))" using assms by (simp add: adapt_sigma_sets) show "sigma_sets (space M) (\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets N}) \ sets M" proof (rule sigma_algebra.sigma_sets_subset, rule Sigma_Algebra.sets.sigma_algebra_axioms, rule UN_subset_iff[THEN iffD2], intro ballI) fix i assume "i\ {m. m\n}" thus "{X i -` A \ space M |A. A \ sets N} \ sets M" using assms measurable_sets by blast qed qed lemma stoch_proc_filt_adapt: assumes "\n. X n \ measurable M N" shows "adapt_stoch_proc (stoch_proc_filt M X N) X N" unfolding adapt_stoch_proc_def proof fix m show "X m \ measurable (stoch_proc_filt M X N m) N" unfolding measurable_def proof ((intro CollectI), (intro conjI)) have "space (stoch_proc_filt M X N m) = space M" by (simp add: stoch_proc_filt_space) thus "X m \ space (stoch_proc_filt M X N m) \ space N" using assms unfolding measurable_def by simp show "\y\sets N. X m -` y \ space (stoch_proc_filt M X N m) \ sets (stoch_proc_filt M X N m)" proof fix B assume "B\ sets N" have "X m -` B \ space (stoch_proc_filt M X N m) = X m -`B \ space M" using \space (stoch_proc_filt M X N m) = space M\ by simp also have "... \ (\ i\ {p. p\ m}. {(X i -`A) \ (space M) | A. A\ sets N })" using \B\ sets N\ by auto also have "... \ sigma_sets (space M) (\ i\ {p. p\ m}. {(X i -`A) \ (space M) | A. A\ sets N })" by auto also have "... = sets (stoch_proc_filt M X N m)" using assms stoch_proc_filt_sets by blast finally show "X m -` B \ space (stoch_proc_filt M X N m) \ sets (stoch_proc_filt M X N m)" . qed qed qed lemma stoch_proc_filt_disc_filtr: assumes "\i. (X i) \ measurable M N" shows "disc_filtr M (stoch_proc_filt M X N)" unfolding disc_filtr_def proof (intro conjI allI impI) { fix n show "subalgebra M (stoch_proc_filt M X N n)" unfolding subalgebra_def proof show "space (stoch_proc_filt M X N n) = space M" by (simp add:stoch_proc_filt_space) show "sets (stoch_proc_filt M X N n) \ sets M" proof - have "sigma_sets (space M) (\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets N}) \ sets M" proof (rule sigma_algebra.sigma_sets_subset, rule Sigma_Algebra.sets.sigma_algebra_axioms, rule UN_subset_iff[THEN iffD2], intro ballI) fix i assume "i\ {m. m\n}" thus "{X i -` A \ space M |A. A \ sets N} \ sets M" using assms measurable_sets by blast qed thus ?thesis using assms by (simp add:stoch_proc_filt_sets) qed qed } { fix n fix p assume "(n::nat) \ p" show "subalgebra (stoch_proc_filt M X N p) (stoch_proc_filt M X N n)" unfolding subalgebra_def proof have "space (stoch_proc_filt M X N n) = space M" by (simp add: stoch_proc_filt_space) also have "... = space (stoch_proc_filt M X N p)" by (simp add: stoch_proc_filt_space) finally show "space (stoch_proc_filt M X N n) = space (stoch_proc_filt M X N p)" . show "sets (stoch_proc_filt M X N n) \ sets (stoch_proc_filt M X N p)" proof - have "sigma_sets (space M) (\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets N}) \ sigma_sets (space M) (\i\{m. m \ p}. {X i -` A \ space M |A. A \ sets N})" proof (rule sigma_sets_mono') show "(\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets N}) \ (\i\{m. m \ p}. {X i -` A \ space M |A. A \ sets N})" proof (rule UN_subset_iff[THEN iffD2], intro ballI) fix i assume "i\ {m. m\n}" show "{X i -` A \ space M |A. A \ sets N} \ (\i\{m. m \ p}. {X i -` A \ space M |A. A \ sets N})" using \i \ {m. m \ n}\ \n \ p\ order_trans by auto qed qed thus ?thesis using assms by (simp add:stoch_proc_filt_sets) qed qed } qed lemma gen_subalgebra_eq_space_sets: assumes "space M = space N" and "P = Q" and "P\ Pow (space M)" shows "sets (gen_subalgebra M P) = sets (gen_subalgebra N Q)" unfolding gen_subalgebra_def using assms by simp lemma stoch_proc_filt_eq_sets: assumes "space M = space N" shows "sets (stoch_proc_filt M X P n) = sets (stoch_proc_filt N X P n)" unfolding stoch_proc_filt_def proof (rule gen_subalgebra_eq_space_sets, (simp add: assms)+) show "sigma_sets (space N) (\x\{m. m \ n}. {X x -` A \ space N |A. A \ sets P}) \ Pow (space N)" proof (rule sigma_algebra.sigma_sets_subset) show "sigma_algebra (space N) (Pow (space N))" by (simp add: sigma_algebra_Pow) show "(\x\{m. m \ n}. {X x -` A \ space N |A. A \ sets P}) \ Pow (space N)" by auto qed qed lemma (in infinite_cts_filtration) stoch_proc_filt_triv_init: fixes X::"nat \ bool stream \ real" assumes "borel_adapt_stoch_proc nat_filtration X" shows "init_triv_filt M (stoch_proc_filt M X borel)" unfolding init_triv_filt_def proof show "filtration M (stoch_proc_filt M X borel)" using stoch_proc_filt_disc_filtr unfolding filtration_def by (metis adapt_stoch_proc_def assms disc_filtr_def measurable_from_subalg nat_filtration_subalgebra) show "sets (stoch_proc_filt M X borel bot) = {{}, space M}" proof - have seteq: "sets (stoch_proc_filt M X borel 0) = (sigma_sets (space M) (\ i\ {m. m\ 0}. {(X i -`A) \ (space M) | A. A\ sets borel}))" proof (rule stoch_proc_filt_sets) show "\i. i \ 0 \ random_variable borel (X i)" proof - fix i::nat assume "i \ 0" show "random_variable borel (X i)" using assms unfolding adapt_stoch_proc_def using filtration_measurable nat_discrete_filtration using natural_filtration by blast qed qed have "triv_init_disc_filtr_prob_space M nat_filtration" proof (unfold_locales, intro conjI) show "disc_filtr M nat_filtration" unfolding disc_filtr_def using filtrationE2 nat_discrete_filtration nat_filtration_subalgebra by auto show "sets (nat_filtration \) = {{}, space M}" using nat_info_filtration unfolding init_triv_filt_def by simp qed hence "\c. \w \ space M. ((X 0 w)::real) = c" using assms triv_init_disc_filtr_prob_space.adapted_init[of M nat_filtration X] by simp from this obtain c where img: "\w \ space M. (X 0 w) = c" by auto have "(\ i\ {m. m\ 0}. {(X i -`A) \ (space M) | A. A\ sets borel}) = {(X 0 -`A) \ (space M) | A. A\ sets borel}" by auto also have "... = {{}, space M}" proof show "{X 0 -` A \ space M |A. A \ sets borel} \ {{}, space M}" proof - have "\A \ sets borel. (X 0 -`A) \ (space M) \ {{}, space M}" proof fix A::"real set" assume "A\ sets borel" show "(X 0 -`A) \ (space M) \ {{}, space M}" proof (cases "c\ A") case True hence "X 0 -` A \ space M = space M" using img by auto thus ?thesis by simp next case False hence "X 0 -` A \ space M = {}" using img by auto thus ?thesis by simp qed qed thus ?thesis by auto qed show "{{}, space M} \ {X 0 -` A \ space M |A. A \ sets borel}" proof - have "{} \ {X 0 -` A \ space M |A. A \ sets borel}" by blast moreover have "space M \ {X 0 -` A \ space M |A. A \ sets borel}" proof - have "UNIV \ X 0 -` space borel" using space_borel by blast then show ?thesis using bernoulli_stream_space by blast qed ultimately show ?thesis by auto qed qed finally have "(\ i\ {m. m\ 0}. {(X i -`A) \ (space M) | A. A\ sets borel}) = {{}, space M}" . moreover have "sigma_sets (space M) {{}, space M} = {{}, space M}" proof - have "sigma_sets (space M) {space M} = {{}, space M}" by simp have "sigma_sets (space M) (sigma_sets (space M) {space M}) = sigma_sets (space M) {space M}" by (rule sigma_sets_sigma_sets_eq, simp) also have "... = {{}, space M}" by simp finally show ?thesis by simp qed ultimately show ?thesis using seteq by (simp add: bot_nat_def) qed qed lemma (in infinite_cts_filtration) stream_space_borel_union: fixes X::"nat \ bool stream \ ('b::t2_space)" assumes "borel_adapt_stoch_proc F X" and "i\ n" and "A\ sets borel" shows "\y\ A\ range (X i). X i -`{y} = (proj_stoch_proc X n) -` (\z\ comp_proj_i X n i y. (stream_space_single (proj_stoch_proc X n) z))" proof fix y assume "y\ A\ range (X i)" hence "\x. y = X i x" by auto from this obtain x where "y = X i x" by auto hence "X i -`{y} = X i -`{X i x}" by simp also have "... = (\z\ comp_proj_i X n i (X i x). (proj_stoch_proc X n) -` {z})" using \i\ n\ by (simp add: stoch_proc_comp_proj_i_preimage) also have "... = (\z\ comp_proj_i X n i (X i x). (proj_stoch_proc X n) -` (stream_space_single (proj_stoch_proc X n) z))" proof - have "\z\ comp_proj_i X n i (X i x). (proj_stoch_proc X n) -` {z} = (proj_stoch_proc X n) -` (stream_space_single (proj_stoch_proc X n) z)" proof fix z assume "z \ comp_proj_i X n i (X i x)" have "stream_space_single (proj_stoch_proc X n) z \ range (proj_stoch_proc X n) = {z}" using stream_space_single_preimage assms proof - have "z \ range (proj_stoch_proc X n)" using \z \ comp_proj_i X n i (X i x)\ comp_proj_i_def by force then show ?thesis by (meson assms stream_space_single_preimage) qed thus "(proj_stoch_proc X n) -` {z} = (proj_stoch_proc X n) -` (stream_space_single (proj_stoch_proc X n) z)" by auto qed thus ?thesis by auto qed also have "... = proj_stoch_proc X n -` (\z\ comp_proj_i X n i y. (stream_space_single (proj_stoch_proc X n) z))" by (simp add: \y = X i x\ vimage_Union) finally show "X i -`{y} = (proj_stoch_proc X n) -` (\z\ comp_proj_i X n i y. (stream_space_single (proj_stoch_proc X n) z))" using \y = X i x\ by simp qed lemma (in infinite_cts_filtration) proj_stoch_pre_borel: fixes X::"nat \ bool stream \ ('b::t2_space)" assumes "borel_adapt_stoch_proc F X" shows "proj_stoch_proc X n -` {proj_stoch_proc X n x} \ sets (stoch_proc_filt M X borel n)" proof - have "proj_stoch_proc X n -` {proj_stoch_proc X n x} = (\ i\ {m. m\n}. (X i) -`{X i x})" by (simp add:comp_proj_stoch_proc_preimage) also have "... \ sigma_sets (space M) (\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets borel})" proof - have inset: "\i\n. (X i) -`{X i x} \ {X i -` A \ space M |A. A \ sets borel}" proof (intro allI impI) fix i assume "i \ n" have "\U. open U \ U\ (range (X i)) = {X i x}" proof - have "\U. open U \ X i x\ U \ U\ ((range (X i))-{X i x}) = {}" proof (rule open_except_set) have "finite (range (X i))" using assms by (metis adapt_stoch_proc_def bernoulli bernoulli_stream_space nat_filtration_vimage_finite natural_filtration streams_UNIV) thus "finite (range (X i) -{X i x})" by auto show "X i x\ (range (X i)) -{X i x}" by simp qed thus ?thesis using assms by auto qed from this obtain U where "open U" and "U\ (range (X i)) = {X i x}" by auto have "X i -` {X i x} = X i -`U" using \U\ (range (X i)) = {X i x}\ by auto also have "... = X i -` U \ space M" using bernoulli bernoulli_stream_space by simp finally have "X i -` {X i x} = X i -` U \ space M" . moreover have "U \ sets borel" using \open U\ by simp ultimately show "(X i) -`{X i x} \ {X i -` A \ space M |A. A \ sets borel}" by auto qed show ?thesis proof (rule sigma_set_inter_init) show "(\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets borel}) \ Pow (space M)" by auto show "\i. i \ n \ X i -` {X i x} \ sigma_sets (space M) (\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets borel})" using inset by (metis (no_types, lifting) UN_I mem_Collect_eq sigma_sets.Basic) qed qed also have "... = sets (stoch_proc_filt M X borel n)" proof (rule stoch_proc_filt_sets[symmetric]) fix i assume "i \ n" show "random_variable borel (X i)" using assms borel_adapt_stoch_proc_borel_measurable by blast qed finally show "proj_stoch_proc X n -` {proj_stoch_proc X n x} \ sets (stoch_proc_filt M X borel n)" . qed lemma (in infinite_cts_filtration) stoch_proc_filt_gen: fixes X::"nat \ bool stream \ ('b::t2_space)" assumes "borel_adapt_stoch_proc F X" shows "stoch_proc_filt M X borel n = fct_gen_subalgebra M (stream_space borel) (proj_stoch_proc X n)" proof - have "(\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets borel}) \ {proj_stoch_proc X n -` B \ space M |B. B \ sets (stream_space borel)}" proof (rule UN_subset_iff[THEN iffD2], intro ballI) fix i assume "i\ {m. m\n}" hence "i \ n" by simp show "{X i -` A \ space M |A. A \ sets borel} \ {proj_stoch_proc X n -` B \ space M |B. B \ sets (stream_space borel)}" proof - have "\A. A\ sets borel \ X i -` A \ space M \ {proj_stoch_proc X n -` B \ space M |B. B \ sets (stream_space borel)}" proof - fix A::"'b set" assume "A\ sets borel" have "X i -`A \ space M = X i -` A" using bernoulli bernoulli_stream_space by simp also have "... = X i -`(A\ range (X i))" by auto also have "... = (\ y\ A\ range (X i). X i -`{y})" by auto also have "... = (\ y\ A\ range (X i). (proj_stoch_proc X n) -` (\z\ comp_proj_i X n i y. (stream_space_single (proj_stoch_proc X n) z)))" using stream_space_borel_union assms \i\n\ \A\sets borel\ by (metis (mono_tags, lifting) image_cong) also have "... = (proj_stoch_proc X n) -` (\ y\ A\ range (X i). (\z\ comp_proj_i X n i y. (stream_space_single (proj_stoch_proc X n) z)))" by (simp add: vimage_Union) finally have "X i -`A \ space M = (proj_stoch_proc X n) -` (\ y\ A\ range (X i). (\z\ comp_proj_i X n i y. (stream_space_single (proj_stoch_proc X n) z)))" . moreover have "(\ y\ A\ range (X i). (\z\ comp_proj_i X n i y. (stream_space_single (proj_stoch_proc X n) z))) \ sets (stream_space borel)" proof - have "finite (A\ range (X i))" proof - have "finite (range (X i))" using assms by (metis adapt_stoch_proc_def bernoulli bernoulli_stream_space nat_filtration_vimage_finite natural_filtration streams_UNIV) thus ?thesis by auto qed moreover have "\y\ A\ range (X i). (\z\ comp_proj_i X n i y. (stream_space_single (proj_stoch_proc X n) z)) \ sets (stream_space borel)" proof fix y assume "y\ A\ range (X i)" have "finite (comp_proj_i X n i y)" by (simp add: assms comp_proj_i_finite) moreover have "\z\ comp_proj_i X n i y. (stream_space_single (proj_stoch_proc X n) z) \ sets (stream_space borel)" proof fix z assume "z\ comp_proj_i X n i y" thus "(stream_space_single (proj_stoch_proc X n) z) \ sets (stream_space borel)" using assms stream_space_single_set unfolding comp_proj_i_def by auto qed ultimately show "(\z\ comp_proj_i X n i y. (stream_space_single (proj_stoch_proc X n) z)) \ sets (stream_space borel)" by blast qed ultimately show ?thesis by blast qed ultimately show "X i -` A \ space M \ {proj_stoch_proc X n -` B \ space M |B. B \ sets (stream_space borel)}" by (metis (mono_tags, lifting) \X i -` A \ space M = X i -` A\ mem_Collect_eq) qed thus ?thesis by auto qed qed hence l: "sigma_sets (space M) (\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets borel}) \ sigma_sets (space M) {proj_stoch_proc X n -` B \ space M |B. B \ sets (stream_space borel)}" by (rule sigma_sets_mono') have "{proj_stoch_proc X n -` B \ space M |B. B \ sets (stream_space borel)} \ sigma_sets (space M) (\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets borel})" proof - have "\B\ sets (stream_space borel). proj_stoch_proc X n -` B \ space M \ sigma_sets (space M) (\ i\ {m. m\ n}. {(X i -`A) \ (space M) | A. A\ sets borel })" proof fix B::"'b stream set" assume "B\ sets (stream_space borel)" have "proj_stoch_proc X n -` B \ space M = proj_stoch_proc X n -`B" using bernoulli bernoulli_stream_space by simp also have "... = proj_stoch_proc X n -` (B \ range (proj_stoch_proc X n))" by auto also have "... = proj_stoch_proc X n -` (\ y\ (B \ range (proj_stoch_proc X n)). {y})" by simp also have "... = (\ y\ (B \ range (proj_stoch_proc X n)). proj_stoch_proc X n -`{y})" by auto finally have eqB: "proj_stoch_proc X n -` B \ space M = (\ y\ (B \ range (proj_stoch_proc X n)). proj_stoch_proc X n -`{y})" . have "\y\ (B \ range (proj_stoch_proc X n)). proj_stoch_proc X n -`{y} \ sigma_sets (space M) (\ i\ {m. m\ n}. {(X i -`A) \ (space M) | A. A\ sets borel })" proof fix y assume "y \ B \ range (proj_stoch_proc X n)" hence "\x. y = proj_stoch_proc X n x" by auto from this obtain x where "y = proj_stoch_proc X n x" by auto have "proj_stoch_proc X n -`{proj_stoch_proc X n x} \ sets (stoch_proc_filt M X borel n)" by (rule proj_stoch_pre_borel, simp add:assms) also have "... = sigma_sets (space M) (\ i\ {m. m\ n}. {(X i -`A) \ (space M) | A. A\ sets borel })" proof (rule stoch_proc_filt_sets) fix i assume "i\ n" show "random_variable borel (X i)" using assms borel_adapt_stoch_proc_borel_measurable by blast qed finally show "proj_stoch_proc X n -`{y} \ sigma_sets (space M) (\ i\ {m. m\ n}. {(X i -`A) \ (space M) | A. A\ sets borel })" using \y = proj_stoch_proc X n x\ by simp qed hence "(\ y\ (B \ range (proj_stoch_proc X n)). proj_stoch_proc X n -`{y}) \ sigma_sets (space M) (\ i\ {m. m\ n}. {(X i -`A) \ (space M) | A. A\ sets borel })" proof (rule sigma_set_union_count) have "finite (range (proj_stoch_proc X n))" by (simp add: assms proj_stoch_set_finite_range) thus "countable (B \ range (proj_stoch_proc X n))" by (simp add: countable_finite) qed thus "proj_stoch_proc X n -` B \ space M \ sigma_sets (space M) (\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets borel})" using eqB by simp qed thus ?thesis by auto qed hence "sigma_sets (space M) {proj_stoch_proc X n -` B \ space M |B. B \ sets (stream_space borel)} \ sigma_sets (space M) (\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets borel})" by (rule sigma_sets_mono) hence "sigma_sets (space M) {proj_stoch_proc X n -` B \ space M |B. B \ sets (stream_space borel)} = sigma_sets (space M) (\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets borel})" using l by simp thus ?thesis unfolding stoch_proc_filt_def fct_gen_subalgebra_def by simp qed lemma (in infinite_coin_toss_space) stoch_proc_subalg_nat_filt: assumes "borel_adapt_stoch_proc nat_filtration X" shows "subalgebra (nat_filtration n) (stoch_proc_filt M X borel n)" unfolding subalgebra_def proof show "space (stoch_proc_filt M X borel n) = space (nat_filtration n)" by (simp add: fct_gen_subalgebra_space nat_filtration_def stoch_proc_filt_space) show "sets (stoch_proc_filt M X borel n) \ sets (nat_filtration n)" proof - have "\i \ n. (\ A\ sets borel. X i -`A \ space M \ sets (nat_filtration n))" proof (intro allI impI) fix i assume "i \ n" have "X i \ borel_measurable (nat_filtration n)" by (metis \i \ n\ adapt_stoch_proc_def assms filtrationE2 measurable_from_subalg nat_discrete_filtration) show "\A\sets borel. X i -` A \ space M \ sets (nat_filtration n)" proof fix A::"'a set" assume "A\ sets borel" thus "X i -` A \ space M \ sets (nat_filtration n)" using \X i \ borel_measurable (nat_filtration n)\ by (metis bernoulli bernoulli_stream_space measurable_sets nat_filtration_space streams_UNIV) qed qed hence "(\ i\ {m. m\ n}. {(X i -`A) \ (space M) | A. A\ sets borel }) \ sets (nat_filtration n)" by auto hence "sigma_sets (space M) (\ i\ {m. m\ n}. {(X i -`A) \ (space M) | A. A\ sets borel }) \ sets (nat_filtration n)" by (metis (no_types, lifting) bernoulli bernoulli_stream_space nat_filtration_space sets.sigma_sets_subset streams_UNIV) thus ?thesis using assms stoch_proc_filt_sets unfolding adapt_stoch_proc_def proof - assume "\t. X t \ borel_measurable (nat_filtration t)" then have f1: "\n m. X n \ borel_measurable m \ \ subalgebra m (nat_filtration n)" by (meson measurable_from_subalg) have "\n. subalgebra M (nat_filtration n)" by (metis infinite_coin_toss_space.nat_filtration_subalgebra infinite_coin_toss_space_axioms) then show ?thesis using f1 \\n X N M. (\i. i \ n \ X i \ M \\<^sub>M N) \ sets (stoch_proc_filt M X N n) = sigma_sets (space M) (\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets N})\ \sigma_sets (space M) (\i\{m. m \ n}. {X i -` A \ space M |A. A \ sets borel}) \ sets (nat_filtration n)\ by blast qed qed qed lemma (in infinite_coin_toss_space) assumes "N = bernoulli_stream q" and "0 \ q" and "q \ 1" and "0 < p" and "p < 1" and "filt_equiv nat_filtration M N" shows filt_equiv_sgt: "0 < q" and filt_equiv_slt: "q < 1" proof - have "space M = space N" using assms filt_equiv_space by simp have eqs: "{w\ space M. (snth w 0)} = pseudo_proj_True (Suc 0) -`{True ##sconst True}" proof show "{w \ space M. w !! 0} \ pseudo_proj_True (Suc 0) -` {True ##sconst True}" proof fix w assume "w \ {w \ space M. w !! 0}" hence "snth w 0" by simp hence "pseudo_proj_True (Suc 0) w = True##sconst True" by (simp add: pseudo_proj_True_def) thus "w \ pseudo_proj_True (Suc 0) -` {True##sconst True}" by simp qed show "pseudo_proj_True (Suc 0) -` {True##sconst True} \ {w \ space M. w !! 0}" proof fix w assume "w \ pseudo_proj_True (Suc 0) -` {True##sconst True}" hence "pseudo_proj_True (Suc 0) w = True##sconst True" by simp hence "snth w 0" by (metis pseudo_proj_True_Suc_prefix stream_eq_Stream_iff) thus "w\ {w \ space M. w !! 0}" using bernoulli bernoulli_stream_space by simp qed qed hence natset: "{w\ space M. (snth w 0)} \ sets (nat_filtration (Suc 0))" proof - have "pseudo_proj_True (Suc 0) -` {True##sconst True} \ sets (nat_filtration (Suc 0))" proof (rule nat_filtration_singleton) show "pseudo_proj_True (Suc 0) (True##sconst True) = True## sconst True" unfolding pseudo_proj_True_def by simp qed thus ?thesis using eqs by simp qed have eqf: "{w\ space M. \(snth w 0)} = pseudo_proj_True (Suc 0) -`{False ##sconst True}" proof show "{w \ space M. \(snth w 0)} \ pseudo_proj_True (Suc 0) -` {False ##sconst True}" proof fix w assume "w \ {w \ space M. \(snth w 0)}" hence "\(snth w 0)" by simp hence "pseudo_proj_True (Suc 0) w = False ##sconst True" by (simp add: pseudo_proj_True_def) thus "w \ pseudo_proj_True (Suc 0) -` {False ## sconst True}" by simp qed show "pseudo_proj_True (Suc 0) -` {False ## sconst True} \ {w \ space M. \(snth w 0)}" proof fix w assume "w \ pseudo_proj_True (Suc 0) -` {False##sconst True}" hence "pseudo_proj_True (Suc 0) w = False##sconst True" by simp hence "\(snth w 0)" by (metis pseudo_proj_True_Suc_prefix stream_eq_Stream_iff) thus "w\ {w \ space M. \(snth w 0)}" using bernoulli bernoulli_stream_space by simp qed qed hence natsetf: "{w\ space M. \(snth w 0)} \ sets (nat_filtration (Suc 0))" proof - have "pseudo_proj_True (Suc 0) -` {False##sconst True} \ sets (nat_filtration (Suc 0))" proof (rule nat_filtration_singleton) show "pseudo_proj_True (Suc 0) (False##sconst True) = False##sconst True" unfolding pseudo_proj_True_def by simp qed thus ?thesis using eqf by simp qed (*have "prob_space N" using assms by (simp add: bernoulli_stream_def prob_space.prob_space_stream_space prob_space_measure_pmf)*) show "0 < q" proof (rule ccontr) assume "\ 0 < q" hence "q = 0" using assms by simp hence "emeasure N {w\ space N. (snth w 0)} = q" using bernoulli_stream_component_probability[of N q] assms by blast hence "emeasure N {w\ space N. (snth w 0)} = 0" using \q = 0\ by simp hence "emeasure M {w\ space M. (snth w 0)} = 0" using assms natset unfolding filt_equiv_def by (simp add: \space M = space N\) moreover have "emeasure M {w\ space M. (snth w 0)} = p" using bernoulli_stream_component_probability[of M p] bernoulli p_lt_1 p_gt_0 by blast ultimately show False using assms by simp qed show "q < 1" proof (rule ccontr) assume "\ q < 1" hence "q = 1" using assms by simp hence "emeasure N {w\ space N. \(snth w 0)} = 1 -q" using bernoulli_stream_component_probability_compl[of N q] assms by blast hence "emeasure N {w\ space N. \(snth w 0)} = 0" using \q = 1\ by simp hence "emeasure M {w\ space M. \(snth w 0)} = 0" using assms natsetf unfolding filt_equiv_def by (simp add: \space M = space N\) moreover have "emeasure M {w\ space M. \(snth w 0)} = 1-p" using bernoulli_stream_component_probability_compl[of M p] bernoulli p_lt_1 p_gt_0 by blast ultimately show False using assms by simp qed qed lemma stoch_proc_filt_filt_equiv: assumes "filt_equiv F M N" shows "stoch_proc_filt M f P n = stoch_proc_filt N f P n" using assms filt_equiv_space filt_equiv_sets unfolding stoch_proc_filt_def proof - have "space N = space M" by (metis assms filt_equiv_space) then show "gen_subalgebra M (sigma_sets (space M) (\n\{na. na \ n}. {f n -` C \ space M |C. C \ sets P})) = gen_subalgebra N (sigma_sets (space N) (\n\{na. na \ n}. {f n -` C \ space N |C. C \ sets P}))" by (simp add: gen_subalgebra_def) qed lemma filt_equiv_filt: assumes "filt_equiv F M N" and "filtration M G" shows "filtration N G" unfolding filtration_def proof (intro allI conjI impI) { fix t show "subalgebra N (G t)" using assms unfolding filtration_def filt_equiv_def by (metis sets_eq_imp_space_eq subalgebra_def) } { fix s::'c fix t assume "s \ t" thus "subalgebra (G t) (G s)" using assms unfolding filtration_def by simp } qed lemma filt_equiv_borel_AE_eq_iff: fixes f::"'a\ real" assumes "filt_equiv F M N" and "f\ borel_measurable (F t)" and "g\ borel_measurable (F t)" and "prob_space N" and "prob_space M" shows "(AE w in M. f w = g w) \ (AE w in N. f w = g w)" proof - { assume fst: "AE w in M. f w = g w" have set0: "{w\ space M. f w \ g w} \ sets (F t) \ emeasure M {w\ space M. f w \ g w} = 0" proof (rule filtrated_prob_space.AE_borel_eq, (auto simp add: assms)) show "filtrated_prob_space M F" using assms unfolding filt_equiv_def by (simp add: filtrated_prob_space_axioms.intro filtrated_prob_space_def) show "AE w in M. f w = g w" using fst . qed hence "emeasure N {w\ space M. f w \ g w} = 0" using assms unfolding filt_equiv_def by auto moreover have "{w\ space M. f w \ g w} \ sets N" using set0 assms unfolding filt_equiv_def filtration_def subalgebra_def by auto ultimately have "AE w in N. f w = g w" proof - have "space M = space N" by (metis assms(1) filt_equiv_space) then have "\p. almost_everywhere N p \ {a \ space N. \ p a} \ {a \ space N. f a \ g a}" using AE_iff_measurable \emeasure N {w \ space M. f w \ g w} = 0\ \{w \ space M. f w \ g w} \ sets N\ by auto then show ?thesis by metis qed } note a = this { assume scd: "AE w in N. f w = g w" have "space M = space N" by (metis assms(1) filt_equiv_space) have set0: "{w\ space N. f w \ g w} \ sets (F t) \ emeasure N {w\ space N. f w \ g w} = 0" proof (rule filtrated_prob_space.AE_borel_eq, (auto simp add: assms)) show "filtrated_prob_space N F" using assms unfolding filt_equiv_def by (metis \prob_space N\ assms(1) filt_equiv_filtration filtrated_prob_space_axioms.intro filtrated_prob_space_def) show "AE w in N. f w = g w" using scd . qed hence "emeasure M {w\ space M. f w \ g w} = 0" using assms unfolding filt_equiv_def by (metis (full_types) assms(1) filt_equiv_space) moreover have "{w\ space M. f w \ g w} \ sets M" using set0 assms unfolding filt_equiv_def filtration_def subalgebra_def by (metis (mono_tags) \space M = space N\ contra_subsetD) ultimately have "AE w in M. f w= g w" proof - have "\p. almost_everywhere M p \ {a \ space M. \ p a} \ {a \ space M. f a \ g a}" using AE_iff_measurable \emeasure M {w \ space M. f w \ g w} = 0\ \{w \ space M. f w \ g w} \ sets M\ by auto then show ?thesis by metis qed } thus ?thesis using a by auto qed lemma (in infinite_coin_toss_space) filt_equiv_triv_init: assumes "filt_equiv F M N" and "init_triv_filt M G" shows "init_triv_filt N G" unfolding init_triv_filt_def proof show "filtration N G" using assms filt_equiv_filt[of F M N G] unfolding init_triv_filt_def by simp show "sets (G \) = {{}, space N}" using assms filt_equiv_space[of F M N] unfolding init_triv_filt_def by simp qed lemma (in infinite_coin_toss_space) fct_gen_subalgebra_meas_info: assumes "\w. f (g w) = f w" and "f \ space M \ space N" and "g \ space M \ space M" shows "g \ measurable (fct_gen_subalgebra M N f) (fct_gen_subalgebra M N f)" unfolding measurable_def proof (intro CollectI conjI) show "g \ space (fct_gen_subalgebra M N f) \ space (fct_gen_subalgebra M N f)" using assms by (simp add: fct_gen_subalgebra_space) show "\y\sets (fct_gen_subalgebra M N f). g -` y \ space (fct_gen_subalgebra M N f) \ sets (fct_gen_subalgebra M N f)" proof fix B assume "B\ sets (fct_gen_subalgebra M N f)" hence "B \ {f -` B \ space M |B. B \ sets N}" using assms by (simp add:fct_gen_subalgebra_sigma_sets) from this obtain C where "C\ sets N" and "B = f -`C \ space M" by auto note Cprops = this have "g -` B \ space (fct_gen_subalgebra M N f) = g -` B \ space M" using assms by (simp add: fct_gen_subalgebra_space) also have "... = g -` (f -` C \ space M) \ space M" using Cprops by simp also have "... = g -` (f -` C)" using bernoulli bernoulli_stream_space by simp also have "... = (f\ g) -` C" by auto also have "... = f -` C" proof show "(f \ g) -` C \ f -` C" proof fix w assume "w \ (f \ g) -` C" hence "f (g w) \ C" by simp hence "f w \ C" using assms by simp thus "w\ f -`C" by simp qed show "f -` C \ (f \ g) -` C" proof fix w assume "w\ f -`C" hence "f w \ C" by simp hence "f (g w) \ C" using assms by simp thus "w\ (f \ g) -` C" by simp qed qed also have "... \ sets (fct_gen_subalgebra M N f)" using Cprops(2) \B \ sets (fct_gen_subalgebra M N f)\ bernoulli bernoulli_stream_space inf_top.right_neutral by auto finally show "g -` B \ space (fct_gen_subalgebra M N f) \ sets (fct_gen_subalgebra M N f)" . qed qed end \ No newline at end of file