Theory Executable_Randomized_Algorithms.Coin_Space
section ‹Coin Flip Space›
text ‹In this section, we introduce the coin flip space, an infinite lazy stream of booleans and
introduce a probability measure and topology for the space.›
theory Coin_Space
imports
"HOL-Probability.Probability"
"HOL-Library.Code_Lazy"
begin
lemma stream_eq_iff:
assumes "⋀i. x !! i = y !! i"
shows "x = y"
proof -
have "x = smap id x" by (simp add: stream.map_id)
also have "... = y" using assms unfolding smap_alt by auto
finally show ?thesis by simp
qed
text ‹Notation for the discrete $\sigma$-algebra:›
abbreviation discrete_sigma_algebra
where "discrete_sigma_algebra ≡ count_space UNIV"
open_bundle discrete_sigma_algebra_syntax
begin
notation discrete_sigma_algebra (‹𝒟›)
end
lemma map_prod_measurable[measurable]:
assumes "f ∈ M →⇩M M'"
assumes "g ∈ N →⇩M N'"
shows "map_prod f g ∈ M ⨂⇩M N →⇩M M' ⨂⇩M N'"
using assms by (subst measurable_pair_iff) simp
lemma measurable_sigma_sets_with_exception:
fixes f :: "'a ⇒ 'b :: countable"
assumes "⋀x. x ≠ d ⟹ f -` {x} ∩ space M ∈ sets M"
shows "f ∈ M →⇩M count_space UNIV"
proof -
define A :: "'b set set" where "A = (λx. {x}) ` UNIV"
have 0: "sets (count_space UNIV) = sigma_sets (UNIV :: 'b set) A"
unfolding A_def by (subst sigma_sets_singletons) auto
have 1: "f -` {x} ∩ space M ∈ sets M" for x
proof (cases "x = d")
case True
have "f -` {d} ∩ space M = space M - (⋃y ∈ UNIV - {d}. f -` {y} ∩ space M)"
by (auto simp add:set_eq_iff)
also have "... ∈ sets M"
using assms
by (intro sets.compl_sets sets.countable_UN) auto
finally show ?thesis
using True by simp
next
case False
then show ?thesis using assms by simp
qed
hence 1: "⋀y. y ∈ A ⟹ f -` y ∩ space M ∈ sets M"
unfolding A_def by auto
thus ?thesis
by (intro measurable_sigma_sets[OF 0]) simp_all
qed
lemma restr_empty_eq: "restrict_space M {} = restrict_space N {}"
by (intro measure_eqI) (auto simp add:sets_restrict_space)
lemma (in prob_space) distr_stream_space_snth [simp]:
assumes "sets M = sets N"
shows "distr (stream_space M) N (λxs. snth xs n) = M"
proof -
have "distr (stream_space M) N (λxs. snth xs n) = distr (stream_space M) M (λxs. snth xs n)"
by (rule distr_cong) (use assms in auto)
also have "… = distr (Pi⇩M UNIV (λi. M)) M (λf. f n)"
by (subst stream_space_eq_distr, subst distr_distr) (auto simp: to_stream_def o_def)
also have "… = M"
by (intro distr_PiM_component prob_space_axioms) auto
finally show ?thesis .
qed
lemma (in prob_space) distr_stream_space_shd [simp]:
assumes "sets M = sets N"
shows "distr (stream_space M) N shd = M"
using distr_stream_space_snth[OF assms, of 0] by (simp del: distr_stream_space_snth)
lemma shift_measurable:
assumes "set x ⊆ space M"
shows "(λbs. x @- bs) ∈ stream_space M →⇩M stream_space M"
proof -
have "(λbs. (x @- bs) !! n) ∈ (stream_space M) →⇩M M" for n
proof (cases "n < length x")
case True
have "(λbs. (x @- bs) !! n) = (λbs. x ! n)"
using True by simp
also have "... ∈ stream_space M →⇩M M"
using assms True by (intro measurable_const) auto
finally show ?thesis by simp
next
case False
have "(λbs. (x @- bs) !! n) = (λbs. bs !! (n - length x))"
using False by simp
also have "... ∈ (stream_space M) →⇩M M"
by (intro measurable_snth)
finally show ?thesis by simp
qed
thus ?thesis
by (intro measurable_stream_space2) auto
qed
lemma (in sigma_finite_measure) restrict_space_pair_lift:
assumes "A' ∈ sets A"
shows "restrict_space A A' ⨂⇩M M = restrict_space (A ⨂⇩M M) (A' × space M)" (is "?L = ?R")
proof -
let ?X = "((∩) (A' × space M) ` {a × b |a b. a ∈ sets A ∧ b ∈ sets M})"
have 0: "A' ⊆ space A"
using assms sets.sets_into_space by blast
have "?X ⊆ {a × b |a b. a ∈ sets (restrict_space A A') ∧ b ∈ sets M}"
proof (rule image_subsetI)
fix x assume "x ∈ {a × b |a b. a ∈ sets A ∧ b ∈ sets M}"
then obtain u v where uv_def: "x = u × v" "u ∈ sets A" "v ∈ sets M"
by auto
have 1:"u ∩ A' ∈ sets (restrict_space A A')"
using uv_def(2) unfolding sets_restrict_space by auto
have "v ⊆ space M"
using uv_def(3) sets.sets_into_space by auto
hence "A' × space M ∩ x = (u ∩ A') × v"
unfolding uv_def(1) by auto
also have "... ∈ {a × b |a b. a ∈ sets (restrict_space A A') ∧ b ∈ sets M}"
using 1 uv_def(3) by auto
finally show "A' × space M ∩ x ∈ {a × b |a b. a ∈ sets (restrict_space A A') ∧ b ∈ sets M}"
by simp
qed
moreover have "{a × b |a b. a ∈ sets (restrict_space A A') ∧ b ∈ sets M} ⊆ ?X"
proof (rule subsetI)
fix x assume "x ∈ {a × b |a b. a ∈ sets (restrict_space A A') ∧ b ∈ sets M}"
then obtain u v where uv_def: "x = u × v" "u ∈ sets (restrict_space A A')" "v ∈ sets M"
by auto
have "x = (A' × space M) ∩ x"
unfolding uv_def(1) using uv_def(2,3) sets.sets_into_space
by (intro Int_absorb1[symmetric]) (auto simp add:sets_restrict_space)
moreover have "u ∈ sets A" using uv_def(2) assms unfolding sets_restrict_space by blast
hence "x ∈ {a × b |a b. a ∈ sets A ∧ b ∈ sets M}"
unfolding uv_def(1) using uv_def(3) by auto
ultimately show "x ∈ ?X"
by simp
qed
ultimately have 2: "?X = {a × b |a b. a ∈ sets (restrict_space A A') ∧ b ∈ sets M}" by simp
have "sets ?R = sigma_sets (A'×space M) ((∩) (A'×space M) ` {a×b |a b. a ∈ sets A∧b ∈ sets M})"
unfolding sets_restrict_space sets_pair_measure using assms sets.sets_into_space
by (intro sigma_sets_Int sigma_sets.Basic) auto
also have "... = sets (restrict_space A A' ⨂⇩M M)"
unfolding sets_pair_measure space_restrict_space Int_absorb2[OF 0] sets_restrict_space 2
by auto
finally have 3:"sets (restrict_space (A ⨂⇩M M) (A' × space M)) = sets (restrict_space A A' ⨂⇩M M)"
by simp
have 4: "emeasure (restrict_space A A'⨂⇩MM) S = emeasure (restrict_space (A⨂⇩MM) (A'×space M)) S"
(is "?L1 = ?R1") if 5:"S ∈ sets (restrict_space A A' ⨂⇩M M)" for S
proof -
have "Pair x -` S = {}" if "x ∉ A'" "x ∈ space A" for x
using that 5 by (auto simp add:3[symmetric] sets_restrict_space)
hence 5: "emeasure M (Pair x -` S) = 0" if "x ∉ A'" "x ∈ space A" for x
using that by auto
have "?L1 = (∫⇧+ x. emeasure M (Pair x -` S) ∂restrict_space A A')"
by (intro emeasure_pair_measure_alt[OF that])
also have "... = (∫⇧+x∈A'. emeasure M (Pair x -` S) ∂A)"
using assms by (intro nn_integral_restrict_space) auto
also have "... = (∫⇧+x. emeasure M (Pair x -` S) ∂A)"
using 5 by (intro nn_integral_cong) force
also have "... = emeasure (A ⨂⇩M M) S"
using that assms by (intro emeasure_pair_measure_alt[symmetric])
(auto simp add:3[symmetric] sets_restrict_space)
also have "... = ?R1"
using assms that by (intro emeasure_restrict_space[symmetric])
(auto simp add:3[symmetric] sets_restrict_space)
finally show ?thesis by simp
qed
show ?thesis using 3 4
by (intro measure_eqI) auto
qed
lemma to_stream_comb_seq_eq:
"to_stream (comb_seq n x y) = stake n (to_stream x) @- to_stream y"
unfolding comb_seq_def to_stream_def
by (intro stream_eq_iff) simp
lemma to_stream_snth: "to_stream ((!!) x) = x"
by (intro ext stream_eq_iff) (simp add:to_stream_def)
lemma snth_to_stream: "snth (to_stream x) = x"
by (intro ext) (simp add:to_stream_def)
lemma (in prob_space) branch_stream_space:
"(λ(x, y). stake n x @- y) ∈ stream_space M ⨂⇩M stream_space M →⇩M stream_space M"
"distr (stream_space M ⨂⇩M stream_space M) (stream_space M) (λ(x,y). stake n x@-y)
= stream_space M" (is "?L = ?R")
proof -
let ?T = "stream_space M"
let ?S = "PiM UNIV (λ_. M)"
interpret S: sequence_space "M"
by standard
show 0:"(λ(x, y). stake n x @- y) ∈ ?T ⨂⇩M ?T →⇩M ?T"
by simp
have "?L = distr (distr ?S ?T to_stream ⨂⇩M distr ?S ?T to_stream) ?T (λ(x,y). stake n x@-y)"
by (subst (1 2) stream_space_eq_distr) simp
also have "... = distr (distr (?S ⨂⇩M ?S) (?T ⨂⇩M ?T) (λ(x, y). (to_stream x, to_stream y)))
?T (λ(x, y). stake n x @- y)"
using prob_space_imp_sigma_finite[OF prob_space_stream_space]
by (intro arg_cong2[where f="(λx y. distr x ?T y)"] pair_measure_distr)
(simp_all flip:stream_space_eq_distr)
also have "... = distr (?S⨂⇩M?S) ?T ((λ(x, y). stake n x@-y)∘(λ(x, y). (to_stream x,to_stream y)))"
by (intro distr_distr 0) (simp add: measurable_pair_iff)
also have "... = distr (?S⨂⇩M?S) ?T ((λ(x, y). stake n (to_stream x) @- to_stream y))"
by (simp add:comp_def case_prod_beta')
also have "... = distr (?S⨂⇩M?S) ?T (to_stream ∘ (λ(x, y). comb_seq n x y))"
using to_stream_comb_seq_eq[symmetric]
by (intro arg_cong2[where f="(λx y. distr x ?T y)"] ext) auto
also have "... = distr (distr (?S⨂⇩M?S) ?S (λ(x, y). comb_seq n x y)) ?T to_stream"
by (intro distr_distr[symmetric] measurable_comb_seq) simp
also have "... = distr ?S ?T to_stream"
by (subst S.PiM_comb_seq) simp
also have "... = ?R"
unfolding stream_space_eq_distr[symmetric] by simp
finally show "?L = ?R"
by simp
qed
text ‹The type for the coin flip space is isomorphic to @{typ "bool stream"}. Nevertheless, we
introduce it as a separate type to be able to introduce a topology and mark it as a lazy type for
code-generation:›
codatatype coin_stream = Coin (chd:bool) (ctl:coin_stream)
code_lazy_type coin_stream
primcorec from_coins :: "coin_stream ⇒ bool stream" where
"from_coins coins = chd coins ## (from_coins (ctl coins))"
primcorec to_coins :: "bool stream ⇒ coin_stream" where
"to_coins str = Coin (shd str) (to_coins (stl str))"
lemma to_from_coins: "to_coins (from_coins x) = x"
by (rule coin_stream.coinduct[where R="(λx y. x = to_coins (from_coins y))"]) simp_all
lemma from_to_coins: "from_coins (to_coins x) = x"
by (rule stream.coinduct[where R="(λx y. x = from_coins (to_coins y))"]) simp_all
lemma bij_to_coins: "bij to_coins"
by (intro bij_betwI[where g="from_coins"] to_from_coins from_to_coins) auto
lemma bij_from_coins: "bij from_coins"
by (intro bij_betwI[where g="to_coins"] to_from_coins from_to_coins) auto
definition cshift where "cshift x y = to_coins (x @- from_coins y)"
definition cnth where "cnth x n = from_coins x !! n"
definition ctake where "ctake n x = stake n (from_coins x)"
definition cdrop where "cdrop n x = to_coins (sdrop n (from_coins x))"
definition rel_coins where "rel_coins x y = (to_coins x = y)"
definition cprefix where "cprefix x y ⟷ ctake (length x) y = x"
definition cconst where "cconst x = to_coins (sconst x)"
context
includes lifting_syntax
begin
lemma bi_unique_rel_coins [transfer_rule]: "bi_unique rel_coins"
unfolding rel_coins_def using inj_onD[OF bij_is_inj[OF bij_to_coins]]
by (intro bi_uniqueI left_uniqueI right_uniqueI) auto
lemma bi_total_rel_coins [transfer_rule]: "bi_total rel_coins"
unfolding rel_coins_def using from_to_coins to_from_coins
by (intro bi_totalI left_totalI right_totalI) auto
lemma cnth_transfer [transfer_rule]: "(rel_coins ===> (=) ===> (=)) snth cnth"
unfolding rel_coins_def cnth_def rel_fun_def by (auto simp:from_to_coins)
lemma cshift_transfer [transfer_rule]: "((=) ===> rel_coins ===> rel_coins) shift cshift"
unfolding rel_coins_def cshift_def rel_fun_def by (auto simp:from_to_coins)
lemma ctake_transfer [transfer_rule]: "((=) ===> rel_coins ===> (=)) stake ctake"
unfolding rel_coins_def ctake_def rel_fun_def by (auto simp:from_to_coins)
lemma cdrop_transfer [transfer_rule]: "((=) ===> rel_coins ===> rel_coins) sdrop cdrop"
unfolding rel_coins_def cdrop_def rel_fun_def by (auto simp:from_to_coins)
lemma chd_transfer [transfer_rule]: "(rel_coins ===> (=)) shd chd"
unfolding rel_coins_def rel_fun_def by (auto simp:from_to_coins)
lemma ctl_transfer [transfer_rule]: "(rel_coins ===> rel_coins) stl ctl"
unfolding rel_coins_def rel_fun_def by (auto simp:from_to_coins)
lemma cconst_transfer [transfer_rule]: "((=) ===> rel_coins) sconst cconst"
unfolding rel_coins_def cconst_def rel_fun_def by (auto simp:from_to_coins)
end
lemma coins_eq_iff:
assumes "⋀i. cnth x i = cnth y i"
shows "x = y"
proof -
have "(∀i. cnth x i = cnth y i) ⟶ x = y"
by transfer (use stream_eq_iff in auto)
thus ?thesis using assms by simp
qed
lemma length_ctake [simp]: "length (ctake n x) = n"
by transfer (rule length_stake)
lemma ctake_nth[simp]: "m < n ⟹ ctake n s ! m = cnth s m"
by transfer (rule stake_nth)
lemma ctake_cdrop: "cshift (ctake n s) (cdrop n s) = s"
by transfer (rule stake_sdrop)
lemma cshift_append[simp]: "cshift (p@q) s = cshift p (cshift q s)"
by transfer (rule shift_append)
lemma cshift_empty[simp]: "cshift [] xs = xs"
by transfer simp
lemma ctake_null[simp]: "ctake 0 xs = []"
by transfer simp
lemma ctake_Suc[simp]: "ctake (Suc n) s = chd s # ctake n (ctl s)"
by transfer simp
lemma cdrop_null[simp]: "cdrop 0 s = s"
by transfer simp
lemma cdrop_Suc[simp]: "cdrop (Suc n) s = cdrop n (ctl s)"
by transfer simp
lemma chd_shift[simp]: "chd (cshift xs s) = (if xs = [] then chd s else hd xs)"
by transfer simp
lemma ctl_shift[simp]: "ctl (cshift xs s) = (if xs = [] then ctl s else cshift (tl xs) s)"
by transfer simp
lemma shd_sconst[simp]: "chd (cconst x) = x"
by transfer simp
lemma take_ctake: "take n (ctake m s) = ctake (min n m) s"
by transfer (rule take_stake)
lemma ctake_add[simp]: "ctake m s @ ctake n (cdrop m s) = ctake (m + n) s"
by transfer (rule stake_add)
lemma cdrop_add[simp]: "cdrop m (cdrop n s) = cdrop (n + m) s"
by transfer (rule sdrop_add)
lemma cprefix_iff: "cprefix x y ⟷ (∀i < length x. cnth y i = x ! i)" (is "?L ⟷ ?R")
proof -
have "?L ⟷ ctake (length x) y = x"
unfolding cprefix_def by simp
also have "... ⟷ (∀i < length x . (ctake (length x) y) ! i = x ! i)"
by (simp add: list_eq_iff_nth_eq)
also have "... ⟷ ?R"
by (intro all_cong) simp
finally show ?thesis by simp
qed
text ‹A non-empty shift is not idempotent:›
lemma empty_if_shift_idem:
assumes "⋀cs. cshift h cs = cs"
shows "h = []"
proof (cases h)
case Nil
then show ?thesis by simp
next
case (Cons hh ht)
have "[hh] = ctake 1 (cshift (hh#ht) (cconst (¬ hh)))"
by simp
also have "... = ctake 1 (cconst (¬ hh))"
using assms unfolding Cons by simp
also have "... = [¬ hh]" by simp
finally show ?thesis by simp
qed
text ‹Stream version of @{thm [source] prefix_length_prefix}:›
lemma cprefix_length_prefix:
assumes "length x ≤ length y"
assumes "cprefix x bs" "cprefix y bs"
shows "prefix x y"
proof -
have "take (length x) y = take (length x) (ctake (length y) bs)"
using assms(3) unfolding cprefix_def by simp
also have "... = ctake (length x) bs"
unfolding take_ctake using assms by simp
also have "... = x"
using assms(2) unfolding cprefix_def by simp
finally have "take (length x) y = x"
by simp
thus ?thesis
by (metis take_is_prefix)
qed
lemma same_prefix_not_parallel:
assumes "cprefix x bs" "cprefix y bs"
shows "¬(x ∥ y)"
using assms cprefix_length_prefix
by (cases "length x ≤ length y") auto
lemma ctake_shift:
"ctake m (cshift xs ys) = (if m ≤ length xs then take m xs else xs @ ctake (m - length xs) ys)"
proof (induction m arbitrary: xs)
case (Suc m xs)
thus ?case
by (cases xs) auto
qed auto
lemma ctake_shift_small [simp]: "m ≤ length xs ⟹ ctake m (cshift xs ys) = take m xs"
and ctake_shift_big [simp]:
"m ≥ length xs ⟹ ctake m (cshift xs ys) = xs @ ctake (m - length xs) ys"
by (subst ctake_shift; simp)+
lemma cdrop_shift:
"cdrop m (cshift xs ys) = (if m ≤ length xs then cshift (drop m xs) ys else cdrop (m - length xs) ys)"
proof (induction m arbitrary: xs)
case (Suc m xs)
thus ?case
by (cases xs) auto
qed auto
lemma cdrop_shift_small [simp]:
"m ≤ length xs ⟹ cdrop m (cshift xs ys) = cshift (drop m xs) ys"
and cdrop_shift_big [simp]:
"m ≥ length xs ⟹ cdrop m (cshift xs ys) = cdrop (m - length xs) ys"
by (subst cdrop_shift; simp)+
text ‹Infrastructure for building coin streams:›
primcorec cmap_iterate ::" ('a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ coin_stream"
where
"cmap_iterate m f s = Coin (m s) (cmap_iterate m f (f s))"
lemma cmap_iterate: "cmap_iterate m f s = to_coins (smap m (siterate f s))"
proof (rule coin_stream.coinduct
[where R="(λxs ys. (∃x. xs = cmap_iterate m f x ∧ ys= to_coins (smap m (siterate f x))))"])
show "∃x. cmap_iterate m f s = cmap_iterate m f x ∧
to_coins (smap m (siterate f s)) = to_coins (smap m (siterate f x))"
by (intro exI[where x="s"] refl conjI)
next
fix xs ys
assume "∃x. xs = cmap_iterate m f x ∧ ys = to_coins (smap m (siterate f x))"
then obtain x where 0:"xs = cmap_iterate m f x" "ys = to_coins (smap m (siterate f x))"
by auto
have "chd xs = chd ys"
unfolding 0 by (subst cmap_iterate.ctr, subst siterate.ctr) simp
moreover have "ctl xs = cmap_iterate m f (f x)"
unfolding 0 by (subst cmap_iterate.ctr) simp
moreover have "ctl ys = to_coins(smap m(siterate f (f x)))"
unfolding 0 by (subst siterate.ctr) simp
ultimately show
"chd xs = chd ys ∧ (∃x. ctl xs=cmap_iterate m f x ∧ ctl ys = to_coins (smap m (siterate f x)))"
by auto
qed
definition build_coin_gen :: "('a ⇒ bool list) ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ coin_stream"
where
"build_coin_gen m f s = cmap_iterate (hd ∘ fst)
(λ(r,s'). (if tl r = [] then (m s', f s') else (tl r, s'))) (m s, f s)"
lemma build_coin_gen_aux:
fixes f :: "'a ⇒ 'b stream"
assumes "⋀x. (∃n y. n ≠ [] ∧ f x = n@-f y ∧ g x = n@-g y)"
shows "f x = g x"
proof (rule stream.coinduct[where R="(λxs ys. (∃x n. xs = n @- (f x) ∧ ys = n @- (g x)))"])
show "∃y n. f x = n @-(f y) ∧ g x = n @- (g y)"
by (intro exI[where x="x"] exI[where x="[]"]) auto
next
fix xs ys :: "'b stream"
assume "∃x n. xs = n @- (f x) ∧ ys = n @- (g x)"
hence "∃x n. n ≠ [] ∧ xs = n @- (f x) ∧ ys = n @- (g x)"
using assms by (metis shift.simps(1))
then obtain x n where 0:"xs = n @- (f x)" "ys = n @- (g x)" "n ≠ []"
by auto
have "shd xs = shd ys"
using 0 by simp
moreover have "stl xs = tl n@-(f x)" "stl ys = tl n@-(g x)"
using 0 by auto
ultimately show "shd xs = shd ys ∧ (∃x n. stl xs = n@- (f x) ∧ stl ys = n@- (g x))"
by auto
qed
lemma build_coin_gen:
assumes "⋀x. m x ≠ []"
shows "build_coin_gen m f s = to_coins (flat (smap m (siterate f s)))"
proof -
let ?g = "(λ(r, s'). if tl r = [] then (m s', f s') else (tl r, s'))"
have liter: "smap (hd ∘ fst) (siterate ?g (bs, x)) =
bs @- (smap (hd ∘ fst) (siterate ?g (m x, f x)))" if "bs ≠ []" for x bs
using that
proof (induction bs rule:list_nonempty_induct)
case (single y)
then show ?case by (subst siterate.ctr) simp
next
case (cons y ys)
then show ?case by (subst siterate.ctr) (simp add:comp_def)
qed
have "smap(hd∘fst) (siterate ?g (m x,f x)) = m x@- smap(hd∘fst) (siterate ?g (m (f x), f (f x)))"
for x by (subst liter[OF assms]) auto
moreover have "flat (smap m (siterate f x)) = m x @- flat (smap m (siterate f (f x)))" for x
by (subst siterate.ctr) (simp add:flat_Stream[OF assms])
ultimately have "∃n y. n ≠ [] ∧
smap (hd ∘ fst) (siterate ?g (m x, f x)) = n @- smap (hd ∘ fst) (siterate ?g (m y, f y)) ∧
flat (smap m (siterate f x)) = n @- flat (smap m (siterate f y))" for x
by (intro exI[where x="m x"] exI[where x="f x"] conjI assms)
hence "smap (hd ∘ fst) (siterate ?g (m s', f s')) = flat (smap m (siterate f s'))" for s'
by (rule build_coin_gen_aux[where f="(λx. smap (hd ∘ fst) (siterate ?g (m x, f x)))"])
thus ?thesis
unfolding build_coin_gen_def cmap_iterate by simp
qed
text ‹Measure space for coin streams:›
definition coin_space :: "coin_stream measure"
where "coin_space = embed_measure (stream_space (measure_pmf (pmf_of_set UNIV))) to_coins"
open_bundle coin_space_syntax
begin
notation coin_space (‹ℬ›)
end
lemma space_coin_space: "space ℬ = UNIV"
using bij_is_surj[OF bij_to_coins]
unfolding coin_space_def space_embed_measure space_stream_space by simp
lemma B_t_eq_distr: "ℬ = distr (stream_space (pmf_of_set UNIV)) ℬ to_coins"
unfolding coin_space_def by (intro embed_measure_eq_distr bij_is_inj[OF bij_to_coins])
lemma from_coins_measurable: "from_coins ∈ ℬ →⇩M (stream_space (pmf_of_set UNIV))"
unfolding coin_space_def by (intro measurable_embed_measure1) (simp add:from_to_coins)
lemma to_coins_measurable: "to_coins ∈ (stream_space (pmf_of_set UNIV)) →⇩M ℬ"
unfolding coin_space_def
by (intro measurable_embed_measure2 bij_is_inj[OF bij_to_coins])
lemma chd_measurable: "chd ∈ ℬ →⇩M 𝒟"
proof -
have 0:"chd (to_coins x) = shd x" for x
using chd_transfer unfolding rel_fun_def by auto
thus ?thesis
unfolding coin_space_def by (intro measurable_embed_measure1) simp
qed
lemma cnth_measurable: "(λxs. cnth xs i) ∈ ℬ →⇩M 𝒟"
unfolding coin_space_def cnth_def by (intro measurable_embed_measure1) (simp add:from_to_coins)
lemma B_eq_distr:
"stream_space (pmf_of_set UNIV) = distr ℬ (stream_space (pmf_of_set UNIV)) from_coins"
(is "?L = ?R")
proof -
let ?S = "stream_space (pmf_of_set UNIV)"
have "?R = distr (distr ?S ℬ to_coins) ?S from_coins"
using B_t_eq_distr by simp
also have "... = distr ?S ?S (from_coins ∘ to_coins)"
by (intro distr_distr to_coins_measurable from_coins_measurable)
also have "... = distr ?S ?S id"
unfolding id_def comp_def from_to_coins by simp
also have "... = ?L"
unfolding id_def by simp
finally show ?thesis
by simp
qed
lemma B_t_finite: "emeasure ℬ (space ℬ) = 1"
proof -
let ?S = "stream_space (pmf_of_set (UNIV::bool set))"
have "1 = emeasure ?S (space ?S)"
by (intro prob_space.emeasure_space_1[symmetric] prob_space.prob_space_stream_space
prob_space_measure_pmf)
also have "... = emeasure ℬ (from_coins -` (space (stream_space (pmf_of_set UNIV))) ∩ space ℬ)"
by (subst B_eq_distr) (intro emeasure_distr from_coins_measurable sets.top)
also have "... = emeasure ℬ (space ℬ)"
unfolding space_coin_space space_stream_space vimage_def by simp
finally show ?thesis by simp
qed