Theory StandardBorel
section ‹Standard Borel Spaces›
theory StandardBorel
imports "HOL-Probability.Probability"
begin
text ‹A standard Borel space is the Borel space associated with a Polish space.
Here, we define standard Borel spaces in another, but equivallent, way.
See \<^cite>‹"Heunen_2017"› Proposition 5. ›
abbreviation "real_borel ≡ borel :: real measure"
abbreviation "nat_borel ≡ borel :: nat measure"
abbreviation "ennreal_borel ≡ borel :: ennreal measure"
abbreviation "bool_borel ≡ borel :: bool measure"
subsection ‹ Definition ›
locale standard_borel =
fixes M :: "'a measure"
assumes exist_fg: "∃f ∈ M →⇩M real_borel. ∃g ∈ real_borel →⇩M M.
∀x ∈ space M. (g ∘ f) x = x"
begin
abbreviation "fg ≡ (SOME k. (fst k) ∈ M →⇩M real_borel ∧
(snd k) ∈ real_borel →⇩M M ∧
(∀x ∈ space M. ((snd k) ∘ (fst k)) x = x))"
definition "f ≡ (fst fg)"
definition "g ≡ (snd fg)"
lemma
shows f_meas[simp,measurable] : "f ∈ M →⇩M real_borel"
and g_meas[simp,measurable] : "g ∈ real_borel →⇩M M"
and gf_comp_id[simp]: "⋀x. x ∈ space M ⟹ (g ∘ f) x = x"
"⋀x. x ∈ space M ⟹ g (f x) = x"
proof -
obtain f' g' where h:
"f' ∈ M →⇩M real_borel" "g' ∈ real_borel →⇩M M" "∀x ∈ space M. (g' ∘ f') x = x"
using exist_fg by blast
have "f ∈ borel_measurable M ∧ g ∈ real_borel →⇩M M ∧ (∀x∈space M. (g ∘ f) x = x)"
unfolding f_def g_def
by(rule someI2[where a="(f',g')"]) (use h in auto)
thus "f ∈ borel_measurable M" "g ∈ real_borel →⇩M M"
"⋀x. x ∈ space M ⟹ (g ∘ f) x = x" "⋀x. x ∈ space M ⟹ g (f x) = x"
by auto
qed
lemma standard_borel_sets[simp]:
assumes "sets M = sets Y"
shows "standard_borel Y"
unfolding standard_borel_def
using measurable_cong_sets[OF assms refl,of real_borel] measurable_cong_sets[OF refl assms,of real_borel] sets_eq_imp_space_eq[OF assms] exist_fg
by simp
lemma f_inj:
"inj_on f (space M)"
by standard (use gf_comp_id(2) in fastforce)
lemma singleton_sets:
assumes "x ∈ space M"
shows "{x} ∈ sets M"
proof -
let ?y = "f x"
let ?U = "f -` {?y}"
have "?U ∩ space M ∈ sets M"
using borel_measurable_vimage f_meas by blast
moreover have "?U ∩ space M = {x}"
using assms f_inj by(auto simp:inj_on_def)
ultimately show ?thesis
by simp
qed
lemma countable_space_discrete:
assumes "countable (space M)"
shows "sets M = sets (count_space (space M))"
proof
show "sets (count_space (space M)) ⊆ sets M"
proof auto
fix U
assume 1:"U ⊆ space M"
then have 2:"countable U"
using assms countable_subset by auto
have 3:"U = (⋃x∈U. {x})" by auto
moreover have "... ∈ sets M"
by(rule sets.countable_UN''[of U "λx. {x}"]) (use 1 2 singleton_sets in auto)
ultimately show "U ∈ sets M"
by simp
qed
qed (simp add: sets.sets_into_space subsetI)
end
lemma standard_borelI:
assumes "f ∈ Y →⇩M real_borel"
"g ∈ real_borel →⇩M Y"
and "⋀y. y ∈ space Y ⟹ (g ∘ f) y = y"
shows "standard_borel Y"
unfolding standard_borel_def
by (intro bexI[OF _ assms(1)] bexI[OF _ assms(2)]) (auto dest: assms(3))
locale standard_borel_space_UNIV = standard_borel +
assumes space_UNIV:"space M = UNIV"
begin
lemma gf_comp_id'[simp]:
"g ∘ f = id" "g (f x) = x"
using space_UNIV gf_comp_id
by(simp_all add: id_def comp_def)
lemma f_inj':
"inj f"
using f_inj by(simp add: space_UNIV)
lemma g_surj':
"surj g"
using gf_comp_id'(2) surjI by blast
end
lemma standard_borel_space_UNIVI:
assumes "f ∈ Y →⇩M real_borel"
"g ∈ real_borel →⇩M Y"
"(g ∘ f) = id"
and "space Y = UNIV"
shows "standard_borel_space_UNIV Y"
using assms
by(auto intro!: standard_borelI simp: standard_borel_space_UNIV_def standard_borel_space_UNIV_axioms_def)
lemma standard_borel_space_UNIVI':
assumes "standard_borel Y"
and "space Y = UNIV"
shows "standard_borel_space_UNIV Y"
using assms by(simp add: standard_borel_space_UNIV_def standard_borel_space_UNIV_axioms_def)
subsection ‹ $\mathbb{R}$, $\mathbb{N}$, Boolean, $[0,\infty]$ ›
text ‹ $\mathbb{R}$ is a standard Borel space. ›
interpretation real : standard_borel_space_UNIV "real_borel"
by(auto intro!: standard_borel_space_UNIVI)
text‹ A non-empty Borel subspace of $\mathbb{R}$ is also a standard Borel space. ›
lemma real_standard_borel_subset:
assumes "U ∈ sets real_borel"
and "U ≠ {}"
shows "standard_borel (restrict_space real_borel U)"
proof -
have std1: "id ∈ (restrict_space real_borel U) →⇩M real_borel"
by (simp add: measurable_restrict_space1)
obtain x where hx : "x ∈ U"
using assms(2) by auto
define g :: "real ⇒ real"
where "g ≡ (λr. if r ∈ U then r else x)"
have "g ∈ real_borel →⇩M real_borel"
unfolding g_def by(rule borel_measurable_continuous_on_if) (simp_all add: assms(1))
hence std2: "g ∈ real_borel →⇩M (restrict_space real_borel U)"
by(auto intro!: measurable_restrict_space2 simp: g_def hx)
have std3: "∀y∈ space (restrict_space real_borel U). (g ∘ id) y = y"
by(simp add: g_def space_restrict_space)
show ?thesis
using std1 std2 std3 standard_borel_def by blast
qed
text ‹ A non-empty measurable subset of a standard Borel space is also a standard Borel space.›
lemma(in standard_borel) standard_borel_subset:
assumes "U ∈ sets M"
"U ≠ {}"
shows "standard_borel (restrict_space M U)"
proof -
let ?ginvU = "g -` U"
have hgu1:"?ginvU ∈ sets real_borel"
using assms(1) g_meas measurable_sets_borel by blast
have hgu2:"f ` U ⊆ ?ginvU"
using gf_comp_id sets.sets_into_space[OF assms(1)] by fastforce
hence hgu3:"?ginvU ≠ {}"
using assms(2) by blast
interpret r_borel_set: standard_borel "restrict_space real_borel ?ginvU"
by(rule real_standard_borel_subset[OF hgu1 hgu3])
have std1: "r_borel_set.f ∘ f ∈ (restrict_space M U) →⇩M real_borel"
using sets.sets_into_space[OF assms(1)]
by(auto intro!: measurable_comp[where N="restrict_space real_borel ?ginvU"] measurable_restrict_space3)
have std2: "g ∘ r_borel_set.g ∈ real_borel →⇩M (restrict_space M U)"
by(auto intro!: measurable_comp[where N="restrict_space real_borel ?ginvU"] measurable_restrict_space3[OF g_meas])
have std3: "∀x∈ space (restrict_space M U). ((g ∘ r_borel_set.g) ∘ (r_borel_set.f ∘ f)) x = x"
by (simp add: space_restrict_space)
show ?thesis
using std1 std2 std3 standard_borel_def by blast
qed
text ‹ $\mathbb{N}$ is a standard Borel space. ›
interpretation nat : standard_borel_space_UNIV nat_borel
proof -
define n_to_r :: "nat ⇒ real"
where "n_to_r ≡ (λn. of_real n)"
define r_to_n :: "real ⇒ nat"
where "r_to_n ≡ (λr. nat ⌊r⌋)"
have n_to_r_measurable: "n_to_r ∈ nat_borel →⇩M real_borel"
using borel_measurable_count_space measurable_cong_sets sets_borel_eq_count_space
by blast
have r_to_n_measurable: "r_to_n ∈ real_borel →⇩M nat_borel"
by(simp add: r_to_n_def)
have n_to_r_to_n_id: "r_to_n ∘ n_to_r = id"
by(simp add: n_to_r_def r_to_n_def comp_def id_def)
show "standard_borel_space_UNIV nat_borel"
using standard_borel_space_UNIVI[OF n_to_r_measurable r_to_n_measurable n_to_r_to_n_id]
by simp
qed
text ‹ For a countable space $X$, $X$ is a standard Borel space iff $X$ is a discrete space. ›
lemma countable_standard_iff:
assumes "space X ≠ {}"
and "countable (space X)"
shows "standard_borel X ⟷ sets X = sets (count_space (space X))"
proof
show "standard_borel X ⟹ sets X = sets (count_space (space X))"
using standard_borel.countable_space_discrete assms by simp
next
assume h[measurable_cong]: "sets X = sets (count_space (space X))"
show "standard_borel X"
proof(rule standard_borelI[where f="nat.f ∘ to_nat_on (space X)" and g="from_nat_into (space X) ∘ nat.g"])
show "nat.f ∘ to_nat_on (space X) ∈ borel_measurable X"
by simp
next
have [simp]: "from_nat_into (space X) ∈ UNIV → (space X)"
using from_nat_into[OF assms(1)] by simp
hence [measurable]: "from_nat_into (space X) ∈ nat_borel →⇩M X"
using measurable_count_space_eq1[of _ _ X] measurable_cong_sets[OF sets_borel_eq_count_space]
by blast
show "from_nat_into (space X) ∘ nat.g ∈ real_borel →⇩M X"
by simp
next
fix x
assume "x ∈ space X"
then show "(from_nat_into (space X) ∘ nat.g ∘ (nat.f ∘ to_nat_on (space X))) x = x"
using from_nat_into_to_nat_on[OF assms(2)] by simp
qed
qed
text ‹ $\mathbb{B}$ is a standard Borel space. ›
lemma to_bool_measurable:
assumes "f -` {True} ∩ space M ∈ sets M"
shows "f ∈ M →⇩M bool_borel"
proof(rule measurableI)
fix A
assume h:"A ∈ sets bool_borel"
have h2: "f -` {False} ∩ space M ∈ sets M"
proof -
have "- {False} = {True}"
by auto
thus ?thesis
by(simp add: vimage_sets_compl_iff[where A="{False}"] assms)
qed
have "A ⊆ {True,False}"
by auto
then consider "A = {}" | "A = {True}" | "A = {False}" | "A = {True,False}"
by auto
thus "f -` A ∩ space M ∈ sets M"
proof cases
case 1
then show ?thesis
by simp
next
case 2
then show ?thesis
by(simp add: assms)
next
case 3
then show ?thesis
by(simp add: h2)
next
case 4
then have "f -` A = f -` {True} ∪ f -` {False}"
by auto
thus ?thesis
using assms h2
by (metis Int_Un_distrib2 sets.Un)
qed
qed simp
interpretation bool : standard_borel_space_UNIV bool_borel
using countable_standard_iff[of bool_borel]
by(auto intro!: standard_borel_space_UNIVI' simp: sets_borel_eq_count_space)
text ‹ $[0,\infty]$ (the set of extended non-negative real numbers) is a standard Borel space. ›
interpretation ennreal : standard_borel_space_UNIV ennreal_borel
proof -
define preal_to_real :: "ennreal ⇒ real"
where "preal_to_real ≡ (λr. if r = ∞ then -1
else enn2real r)"
define real_to_preal :: "real ⇒ ennreal"
where "real_to_preal ≡ (λr. if r = -1 then ∞
else ennreal r)"
have preal_to_real_measurable: "preal_to_real ∈ ennreal_borel →⇩M real_borel"
unfolding preal_to_real_def by simp
have real_to_preal_measurable: "real_to_preal ∈ real_borel →⇩M ennreal_borel"
unfolding real_to_preal_def by simp
have preal_real_preal_id: "real_to_preal ∘ preal_to_real = id"
proof
fix r :: ennreal
show "(real_to_preal ∘ preal_to_real) r = id r"
using ennreal_enn2real_if[of r] ennreal_neg
by(auto simp add: real_to_preal_def preal_to_real_def)
qed
show "standard_borel_space_UNIV ennreal_borel"
using standard_borel_space_UNIVI[OF preal_to_real_measurable real_to_preal_measurable preal_real_preal_id]
by simp
qed
subsection ‹ $\mathbb{R}\times\mathbb{R}$ ›
definition real_to_01open :: "real ⇒ real" where
"real_to_01open r ≡ arctan r / pi + 1 / 2"
definition real_to_01open_inverse :: "real ⇒ real" where
"real_to_01open_inverse r ≡ tan (pi * r - (pi / 2))"
lemma real_to_01open_inverse_correct:
"real_to_01open_inverse ∘ real_to_01open = id"
by(auto simp add: real_to_01open_def real_to_01open_inverse_def distrib_left tan_arctan)
lemma real_to_01open_inverse_correct':
assumes "0 < r" "r < 1"
shows "real_to_01open (real_to_01open_inverse r) = r"
unfolding real_to_01open_def real_to_01open_inverse_def
proof -
have "arctan (tan (pi * r - pi / 2)) = pi * r - pi / 2"
using arctan_unique[of "pi * r - pi / 2"] assms
by simp
hence "arctan (tan (pi * r - pi / 2)) / pi + 1 / 2 = ((pi * r) - pi / 2)/ pi + 1/2"
by simp
also have "... = r - 1/2 + 1/2"
by (metis (no_types, opaque_lifting) divide_inverse mult.left_neutral nonzero_mult_div_cancel_left pi_neq_zero right_diff_distrib)
finally show "arctan (tan (pi * r - pi / 2)) / pi + 1 / 2 = r"
by simp
qed
lemma real_to_01open_01 :
"0 < real_to_01open r ∧ real_to_01open r < 1"
proof
have "- pi / 2 < arctan r" by(simp add: arctan_lbound)
hence "0 < arctan r + pi / 2" by simp
hence "0 < (1 / pi) * (arctan r + pi / 2)" by simp
thus "0 < real_to_01open r"
by (simp add: add_divide_distrib real_to_01open_def)
next
have "arctan r < pi / 2" using arctan_ubound by simp
hence "arctan r + pi / 2 < pi" by simp
hence "(1 / pi) * (arctan r + pi / 2) < 1" by simp
thus "real_to_01open r < 1"
by(simp add: real_to_01open_def add_divide_distrib)
qed
lemma real_to_01open_continuous:
"continuous_on UNIV real_to_01open"
proof -
have "continuous_on UNIV ((λx. x / pi + 1 / 2) ∘ arctan)"
proof (rule continuous_on_compose)
show "continuous_on UNIV arctan"
by (simp add: continuous_on_arctan)
next
show "continuous_on (range arctan) (λx. x / pi + 1 / 2)"
by(auto intro!: continuous_on_add continuous_on_divide)
qed
thus ?thesis
by(simp add: real_to_01open_def)
qed
lemma real_to_01open_inverse_continuous:
"continuous_on {0<..<1} real_to_01open_inverse"
unfolding real_to_01open_inverse_def
proof(rule Transcendental.continuous_on_tan)
have [simp]: "(λx. pi * x - pi / 2) = (λx. x - pi/2) ∘ (λx. pi * x)"
by auto
have "continuous_on {0<..<1} ..."
proof(rule continuous_on_compose)
show "continuous_on {0<..<1} ((*) pi)"
by simp
next
show "continuous_on ((*) pi ` {0<..<1}) (λx. x - pi / 2)"
using continuous_on_diff[of "(*) pi ` {0<..<1}" "λx. x"]
by simp
qed
thus "continuous_on {0<..<1} (λx. pi * x - pi / 2)" by simp
next
have "∀r∈{0<..<1::real}. -(pi/2) < pi * r - pi / 2 ∧ pi * r - pi / 2 < pi/2"
by simp
thus "∀r∈{0<..<1::real}. cos (pi * r - pi / 2) ≠ 0"
using cos_gt_zero_pi by fastforce
qed
lemma real_to_01open_inverse_measurable:
"real_to_01open_inverse ∈ restrict_space real_borel {0<..<1} →⇩M real_borel"
using borel_measurable_continuous_on_restrict real_to_01open_inverse_continuous
by simp
fun r01_binary_expansion'' :: "real ⇒ nat ⇒ nat × real × real" where
"r01_binary_expansion'' r 0 = (if 1/2 ≤ r then (1,1 ,1/2)
else (0,1/2, 0))" |
"r01_binary_expansion'' r (Suc n) = (let (_,ur,lr) = r01_binary_expansion'' r n;
k = (ur + lr)/2 in
(if k ≤ r then (1,ur,k)
else (0,k,lr)))"
text ‹ $a_n$ where $r = 0.a_0 a_1 a_2 ....$ for $0 < r < 1$.›
definition r01_binary_expansion' :: "real ⇒ nat ⇒ nat" where
"r01_binary_expansion' r n ≡ fst (r01_binary_expansion'' r n)"
text ‹$a_n = 0$ or $1$.›
lemma real01_binary_expansion'_0or1:
"r01_binary_expansion' r n ∈ {0,1}"
by (cases n) (simp_all add: r01_binary_expansion'_def split_beta' Let_def)
definition r01_binary_sum :: "(nat ⇒ nat) ⇒ nat ⇒ real" where
"r01_binary_sum a n ≡ (∑i=0..n. real (a i) * ((1/2)^(Suc i)))"
definition r01_binary_sum_lim :: "(nat ⇒ nat) ⇒ real" where
"r01_binary_sum_lim ≡ lim ∘ r01_binary_sum"
definition r01_binary_expression :: "real ⇒ nat ⇒ real" where
"r01_binary_expression ≡ r01_binary_sum ∘ r01_binary_expansion'"
lemma r01_binary_expansion_lr_r_ur:
assumes "0 < r" "r < 1"
shows "(snd (snd (r01_binary_expansion'' r n))) ≤ r ∧
r < (fst (snd (r01_binary_expansion'' r n)))"
using assms by (induction n) (simp_all add:split_beta' Let_def)
text ‹‹0 ≤ lr ∧ lr < ur ∧ ur ≤ 1›.›
lemma r01_binary_expansion_lr_ur_nn:
shows "0 ≤ snd (snd (r01_binary_expansion'' r n)) ∧
snd (snd (r01_binary_expansion'' r n)) < fst (snd (r01_binary_expansion'' r n)) ∧
fst (snd (r01_binary_expansion'' r n)) ≤ 1"
by (induction n) (simp_all add:split_beta' Let_def)
lemma r01_binary_expansion_diff:
shows "(fst (snd (r01_binary_expansion'' r n))) - (snd (snd (r01_binary_expansion'' r n))) = (1/2)^(Suc n)"
proof(induction n)
case (Suc n')
then show ?case
proof(cases "r01_binary_expansion'' r n'")
case 1:(fields a ur lr)
assume "fst (snd (r01_binary_expansion'' r n')) - snd (snd (r01_binary_expansion'' r n')) = (1 / 2) ^ (Suc n')"
then have 2:"ur - lr = (1/2)^(Suc n')" by (simp add: 1)
show ?thesis
proof -
have [simp]:"ur * 4 - (ur * 4 + lr * 4) / 2 = (ur - lr) * 2"
by(simp add: division_ring_class.add_divide_distrib)
have "ur * 4 - (ur * 4 + lr * 4) / 2 = (1 / 2) ^ n'"
by(simp add: 2)
moreover have "(ur * 4 + lr * 4) / 2 - lr * 4 = (1 / 2) ^ n'"
by(simp add: division_ring_class.add_divide_distrib ring_class.right_diff_distrib[symmetric] 2)
ultimately show ?thesis
by(simp add: 1 Let_def)
qed
qed
qed simp
text ‹‹lrn = Sn›.›
lemma r01_binary_expression_eq_lr:
"snd (snd (r01_binary_expansion'' r n)) = r01_binary_expression r n"
proof(induction n)
case 0
then show ?case
by(simp add: r01_binary_expression_def r01_binary_sum_def r01_binary_expansion'_def)
next
case 1:(Suc n')
show ?case
proof (cases "r01_binary_expansion'' r n'")
case 2:(fields a ur lr)
then have ih:"lr = (∑i = 0..n'. real (fst (r01_binary_expansion'' r i)) * (1 / 2) ^ i / 2)"
using 1 by(simp add: r01_binary_expression_def r01_binary_sum_def r01_binary_expansion'_def)
have 3:"(ur + lr) / 2 = lr + (1/2)^(Suc (Suc n'))"
using r01_binary_expansion_diff[of r n'] 2 by simp
show ?thesis
by(simp add: r01_binary_expression_def r01_binary_sum_def r01_binary_expansion'_def 2 Let_def 3) fact
qed
qed
lemma r01_binary_expression'_sum_range:
"∃k::nat. (snd (snd (r01_binary_expansion'' r n))) = real k/2^(Suc n) ∧
k < 2^(Suc n) ∧
((r01_binary_expansion' r n) = 0 ⟶ even k) ∧
((r01_binary_expansion' r n) = 1 ⟶ odd k)"
proof -
have [simp]:"(snd (snd (r01_binary_expansion'' r n))) = (∑i=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i)))"
using r01_binary_expression_eq_lr[of r n] by(simp add: r01_binary_expression_def r01_binary_sum_def)
have "∃k::nat. (∑i=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) = real k/2^(Suc n) ∧
k < 2^(Suc n) ∧
((r01_binary_expansion' r n) = 0 ⟶ even k) ∧
((r01_binary_expansion' r n) = 1 ⟶ odd k)"
proof(induction n)
case 0
consider "r01_binary_expansion' r 0 = 0" | "r01_binary_expansion' r 0 = 1"
using real01_binary_expansion'_0or1[of r 0] by auto
then show ?case
by cases auto
next
case (Suc n')
then obtain k :: nat where ih:
"(∑i = 0..n'. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) = real k / 2^(Suc n') ∧ k < 2^(Suc n')"
by auto
have "(∑i = 0..Suc n'. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) = (∑i = 0..n'. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) + real (r01_binary_expansion' r (Suc n')) * (1 / 2) ^ Suc (Suc n')"
by simp
also have "... = real k / 2^(Suc n') + (real (r01_binary_expansion' r (Suc n')))/ 2^ Suc (Suc n')"
proof -
have "⋀r ra n. (r::real) * (1 / ra) ^ n = r / ra ^ n"
by (simp add: power_one_over)
then show ?thesis
using ih by presburger
qed
also have "... = (2*real k) / 2^(Suc (Suc n')) + (real (r01_binary_expansion' r (Suc n')))/ 2^ Suc (Suc n')"
by simp
also have "... = (2*(real k) + real (r01_binary_expansion' r (Suc n')))/2 ^ Suc (Suc n')"
by (simp add: add_divide_distrib)
also have "... = (real (2*k + r01_binary_expansion' r (Suc n')))/2 ^ Suc (Suc n')"
by simp
finally have "(∑i = 0..Suc n'. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) = real (2 * k + r01_binary_expansion' r (Suc n')) / 2 ^ Suc (Suc n')" .
moreover have "2 * k + r01_binary_expansion' r (Suc n') < 2^Suc (Suc n')"
proof -
have "k + 1 ≤ 2^Suc n'"
using ih by simp
hence "2*k + 2 ≤ 2^Suc (Suc n')"
by simp
thus ?thesis
using real01_binary_expansion'_0or1[of r "Suc n'"]
by auto
qed
moreover have "r01_binary_expansion' r (Suc n') = 0 ⟶ even (2 * k + r01_binary_expansion' r (Suc n'))"
by simp
moreover have "r01_binary_expansion' r (Suc n') = 1 ⟶ odd (2 * k + r01_binary_expansion' r (Suc n'))"
by simp
ultimately show ?case by fastforce
qed
thus ?thesis
by simp
qed
text ‹‹an = bn ↔ Sn = S'n›.›
lemma r01_binary_expansion'_expression_eq:
"r01_binary_expansion' r1 = r01_binary_expansion' r2 ⟷
r01_binary_expression r1 = r01_binary_expression r2"
proof
assume "r01_binary_expansion' r1 = r01_binary_expansion' r2"
then show "r01_binary_expression r1 = r01_binary_expression r2"
by(simp add: r01_binary_expression_def)
next
assume "r01_binary_expression r1 = r01_binary_expression r2"
then have 1:"⋀n. r01_binary_sum (r01_binary_expansion' r1) n = r01_binary_sum (r01_binary_expansion' r2) n"
by(simp add: r01_binary_expression_def)
show "r01_binary_expansion' r1 = r01_binary_expansion' r2"
proof
fix n
show " r01_binary_expansion' r1 n = r01_binary_expansion' r2 n"
proof(cases n)
case 0
then show ?thesis
using 1[of 0] by(simp add: r01_binary_sum_def)
next
fix n'
case (Suc n')
have "r01_binary_sum (r01_binary_expansion' r1) n - r01_binary_sum (r01_binary_expansion' r1) n' = r01_binary_sum (r01_binary_expansion' r2) n - r01_binary_sum (r01_binary_expansion' r2) n'"
by(simp add: 1)
thus ?thesis
using ‹n = Suc n'› by(simp add: r01_binary_sum_def)
qed
qed
qed
lemma power2_e:
"⋀e::real. 0 < e ⟹ ∃n::nat. real_of_rat (1/2)^n < e"
by (simp add: real_arch_pow_inv)
lemma r01_binary_expression_converges_to_r:
assumes "0 < r"
and "r < 1"
shows "LIMSEQ (r01_binary_expression r) r"
proof
fix e :: real
assume "0 < e"
then obtain k :: nat where hk:"real_of_rat (1/2)^k < e"
using power2_e by auto
show "∀⇩F x in sequentially. dist (r01_binary_expression r x) r < e"
proof(rule eventually_sequentiallyI[of k])
fix m
assume "k ≤ m"
have "¦ r - r01_binary_expression r m ¦ < e"
proof (cases "r01_binary_expansion'' r m")
case 1:(fields a ur lr)
then have "¦r - r01_binary_expression r m¦ = ¦r - lr¦"
by (metis r01_binary_expression_eq_lr snd_conv)
also have "... = r - lr"
using r01_binary_expansion_lr_r_ur[OF assms] 1
by (metis abs_of_nonneg diff_ge_0_iff_ge snd_conv)
also have "... < e"
proof -
have "r - lr ≤ ur - lr"
using r01_binary_expansion_lr_r_ur[of r] assms 1
by (metis diff_right_mono fst_conv less_imp_le snd_conv)
also have "... = (1/2)^(Suc m)"
using r01_binary_expansion_diff[of r m]
by(simp add: 1)
also have "... ≤ (1/2)^(Suc k)"
using ‹k ≤ m› by simp
also have "... < (1/2)^k" by simp
finally show ?thesis
using hk by (simp add: of_rat_divide)
qed
finally show ?thesis .
qed
then show "dist (r01_binary_expression r m) r < e"
by (simp add: dist_real_def)
qed
qed
lemma r01_binary_expression_correct:
assumes "0 < r"
and "r < 1"
shows "r = (∑n. real (r01_binary_expansion' r n) * (1/2)^(Suc n))"
proof -
have "(λn. (λn. ∑i<n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) (Suc n)) = r01_binary_expression r"
proof -
have "⋀n. {..<Suc n} = {0..n}" by auto
thus ?thesis
by(auto simp add: r01_binary_expression_def r01_binary_sum_def)
qed
hence "LIMSEQ (λn. ∑i<n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) r"
using r01_binary_expression_converges_to_r[OF assms] LIMSEQ_imp_Suc[of "λn. ∑i<n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i" r]
by simp
thus ?thesis
using suminf_eq_lim[of "λn. real (r01_binary_expansion' r n) * (1/2)^(Suc n)"] assms limI[of "(λn. ∑i<n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i)" r]
by simp
qed
text ‹‹S0 ≤ S1 ≤ S2 ≤ ...›.›
lemma binary_sum_incseq:
"incseq (r01_binary_sum a)"
by(simp add: incseq_Suc_iff r01_binary_sum_def)
lemma r01_eq_iff:
assumes "0 < r1" "r1 < 1"
"0 < r2" "r2 < 1"
shows "r1 = r2 ⟷ r01_binary_expansion' r1 = r01_binary_expansion' r2"
proof auto
assume "r01_binary_expansion' r1 = r01_binary_expansion' r2"
then have 1:"r01_binary_expression r1 = r01_binary_expression r2"
using r01_binary_expansion'_expression_eq[of r1 r2] by simp
have "r1 = lim (r01_binary_expression r1)"
using limI[of _ r1] r01_binary_expression_converges_to_r[of r1] assms(1,2)
by simp
also have "... = lim (r01_binary_expression r2)"
by (simp add: 1)
also have "... = r2"
using limI[of _ r2] r01_binary_expression_converges_to_r[of r2] assms(3,4)
by simp
finally show "r1 = r2" .
qed
lemma power_half_summable:
"summable (λn. ((1::real) / 2) ^ Suc n)"
using power_half_series summable_def by blast
lemma binary_expression_summable:
assumes "⋀n. a n ∈ {0,1 :: nat}"
shows "summable (λn. real (a n) * (1/2)^(Suc n))"
proof -
have "summable (λn::nat. ¦real (a n) * ((1::real) / (2::real)) ^ Suc n¦)"
proof(rule summable_rabs_comparison_test[of "λn. real (a n) * (1/2)^(Suc n)" "λn. (1/2)^(Suc n)"])
have "⋀n. ¦real (a n) * (1 / 2) ^ Suc n¦ ≤ (1 / 2)^(Suc n)"
proof -
fix n
have "¦real (a n) * (1 / 2) ^ Suc n¦ = real (a n) * (1 / 2) ^ Suc n"
using assms by simp
also have "... ≤ (1 / 2) ^ Suc n"
proof -
consider "a n = 0" | "a n = 1"
using assms by (meson insertE singleton_iff)
then show ?thesis
by(cases,auto)
qed
finally show "¦real (a n) * (1 / 2) ^ Suc n¦ ≤ (1 / 2)^(Suc n)" .
qed
thus "∃N. ∀n≥N. ¦real (a n) * (1 / 2) ^ Suc n¦ ≤ (1 / 2) ^ Suc n"
by simp
next
show "summable (λn. ((1::real) / 2) ^ Suc n)"
using power_half_summable by simp
qed
thus ?thesis by simp
qed
lemma binary_expression_gteq0:
assumes "⋀n. a n ∈ {0,1 :: nat}"
shows "0 ≤ (∑n. real (a (n + k)) * (1 / 2) ^ Suc (n + k))"
proof -
have "(∑n. 0) ≤ (∑n. real (a (n + k)) * (1 / 2) ^ Suc (n + k))"
using binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" k] suminf_le[of "λn. 0" "λn. real (a (n + k)) * (1 / 2) ^ Suc (n + k)"] assms
by simp
thus ?thesis by simp
qed
lemma binary_expression_leeq1:
assumes "⋀n. a n ∈ {0,1 :: nat}"
shows "(∑n. real (a (n + k)) * (1 / 2) ^ Suc (n + k)) ≤ 1"
proof -
have "(∑n. real (a (n + k)) * (1 / 2) ^ Suc (n + k)) ≤ (∑n. (1/2)^(Suc n))"
proof(rule suminf_le)
fix n
have 1:"real (a (n + k)) * (1 / 2) ^ Suc (n + k) ≤ (1 / 2) ^ Suc (n + k)"
using assms[of "n+k"] by auto
have 2:"((1::real) / 2) ^ Suc (n + k) ≤ (1 / 2) ^ Suc n"
by simp
show "real (a (n + k)) * (1 / 2) ^ Suc (n + k) ≤ (1 / 2) ^ Suc n"
by(rule order.trans[OF 1 2])
next
show "summable (λn. real (a (n + k)) * (1 / 2) ^ Suc (n + k))"
using binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" k] assms
by simp
next
show "summable (λn. ((1::real) / 2) ^ Suc n)"
using power_half_summable by simp
qed
thus ?thesis
using power_half_series sums_unique by fastforce
qed
lemma binary_expression_less_than:
assumes "⋀n. a n ∈ {0,1 :: nat}"
shows "(∑n. real (a (n + k)) * (1 / 2) ^ Suc (n + k)) ≤ (∑n. (1 / 2) ^ Suc (n + k))"
proof(rule suminf_le)
fix n
show "real (a (n + k)) * (1 / 2) ^ Suc (n + k) ≤ (1 / 2) ^ Suc (n + k)"
using assms[of "n + k"] by auto
next
show "summable (λn. real (a (n + k)) * (1 / 2) ^ Suc (n + k))"
using summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" k] binary_expression_summable[of a] assms
by simp
next
show "summable (λn. ((1::real) / 2) ^ Suc (n + k))"
using power_half_summable summable_iff_shift[of "λn. ((1::real) / 2) ^ Suc n" k]
by simp
qed
lemma lim_sum_ai:
assumes "⋀n. a n ∈ {0,1 :: nat}"
shows "lim (λn. (∑i=0..n. real (a i) * (1/2)^(Suc i))) = (∑n::nat. real (a n) * (1/2)^(Suc n))"
proof -
have "⋀n::nat. {0..n} = {..n}" by auto
hence "LIMSEQ (λn. ∑i=0..n. real (a i) * (1 / 2) ^ Suc i) (∑n. real (a n) * (1 / 2) ^ Suc n)"
using summable_LIMSEQ'[of "λn. real (a n) * (1/2)^(Suc n)"] binary_expression_summable[of a] assms
by simp
thus "lim (λn. (∑i=0..n. real (a i) * (1/2)^(Suc i))) = (∑n. real (a n) * (1 / 2) ^ Suc n)"
using limI by simp
qed
lemma half_1_minus_sum:
"1 - (∑i<k. ((1::real) / 2) ^ Suc i) = (1/2)^k"
by(induction k) auto
lemma half_sum:
"(∑n. ((1::real) / 2) ^ (Suc (n + k))) = (1/2)^k"
using suminf_split_initial_segment[of "λn. ((1::real) / 2) ^ (Suc n)" k] half_1_minus_sum[of k] power_half_series sums_unique[of "λn. (1 / 2) ^ Suc n" 1] power_half_summable
by fastforce
lemma ai_exists0_less_than_sum:
assumes "⋀n. a n ∈ {0,1}"
"i ≥ m"
and "a i = 0"
shows "(∑n::nat. real (a (n + m)) * (1/2)^(Suc (n + m))) < (1 / 2) ^ m"
proof -
have "(∑n::nat. real (a (n + m)) * (1/2)^(Suc (n + m))) = (∑n<i-m. real (a (n + m)) * (1/2)^(Suc (n + m))) + (∑n::nat. real (a (n + i)) * (1/2)^(Suc (n + i)))"
using suminf_split_initial_segment[of "λn. real (a (n + m)) * (1/2)^(Suc (n + m))" "i-m"] assms(1) binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" m] assms(2)
by simp
also have "... < (1 / 2) ^ m"
proof -
have "(∑n. real (a (n + i)) * (1 / 2) ^ Suc (n + i)) ≤ (1 / 2) ^ Suc i"
proof -
have "(∑n::nat. real (a (n + i)) * (1/2)^(Suc (n + i))) = (∑n::nat. real (a (Suc n + i)) * (1/2)^(Suc (Suc n + i)))"
using suminf_split_head[of "λn. real (a (n + i)) * (1/2)^(Suc (n + i))"] assms(1,3) binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" i]
by simp
also have "... = (∑n::nat. real (a (n + Suc i)) * (1/2)^(Suc n + Suc i))"
by simp
also have "... ≤ (∑n::nat. (1/2)^(Suc n + Suc i))"
using binary_expression_less_than[of a "Suc i"] assms(1)
by simp
also have "... = (1/2)^(Suc i)"
using half_sum[of "Suc i"] by simp
finally show ?thesis .
qed
moreover have "(∑n<i - m. real (a (n + m)) * (1 / 2) ^ Suc (n + m)) ≤ (1/2)^m - (1/2)^i"
proof -
have "(∑n<i - m. real (a (n + m)) * (1 / 2) ^ Suc (n + m)) ≤ (∑n<i - m. (1 / 2) ^ Suc (n + m))"
proof -
have "real (a i) * (1 / 2) ^ Suc i ≤ (1 / 2) ^ Suc i" for i
using assms(1)[of i] by auto
thus ?thesis
by (simp add: sum_mono)
qed
also have "... = (∑n. (1 / 2) ^ Suc (n + m)) - (∑n. (1 / 2) ^ Suc (n + (i - m) + m))"
using suminf_split_initial_segment[of "λn. (1 / 2) ^ Suc (n + m)" "i-m"] power_half_summable summable_iff_shift[of "λn. ((1::real) / 2) ^ Suc n" m]
by fastforce
also have "... = (∑n. (1 / 2) ^ Suc (n + m)) - (∑n. (1 / 2) ^ Suc (n + i))"
using assms(2) by simp
also have "... = (1/2)^m - (1/2)^i"
using half_sum by fastforce
finally show ?thesis .
qed
ultimately have "(∑n<i - m. real (a (n + m)) * (1 / 2) ^ Suc (n + m)) + (∑n. real (a (n + i)) * (1 / 2) ^ Suc (n + i)) ≤ (1 / 2) ^ Suc i + (1 / 2) ^ m - (1 / 2) ^ i"
by linarith
also have "... < (1 / 2) ^ m "
by simp
finally show ?thesis .
qed
finally show ?thesis .
qed
lemma ai_exists0_less_than1:
assumes "⋀n. a n ∈ {0,1}"
and "∃i. a i = 0"
shows "(∑n::nat. real (a n) * (1/2)^(Suc n)) < 1"
using ai_exists0_less_than_sum[of a 0] assms
by auto
lemma ai_1_gt:
assumes "⋀n. a n ∈ {0,1}"
and "a i = 1"
shows "(1/2)^(Suc i) ≤ (∑n::nat. real (a (n+i)) * (1/2)^(Suc (n+i)))"
proof -
have 1:"(∑n::nat. real (a (n+i)) * (1/2)^(Suc (n+i))) = (1 / 2) ^ Suc (0 + i) + (∑n. real (a (Suc n + i)) * (1 / 2) ^ Suc (Suc n + i))"
using suminf_split_head[of "λn. real (a (n+i)) * (1/2)^(Suc (n+i))"] binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" i] assms
by simp
show ?thesis
using 1 binary_expression_gteq0[of a "Suc i"] assms(1)
by simp
qed
lemma ai_exists1_gt0:
assumes "⋀n. a n ∈ {0,1}"
and "∃i. a i = 1"
shows "0 < (∑n::nat. real (a n) * (1/2)^(Suc n))"
proof -
obtain k where h1: "a k = 1"
using assms(2) by auto
have "(1/2)^(Suc k) = (∑n::nat. (if n = k then (1/2)^(Suc k) else (0::real)))"
proof -
have "(λn. if n ∈ {k} then (1 / 2) ^ Suc k else (0::real)) = (λn. if n = k then (1/2)^(Suc k) else 0)"
by simp
moreover have "(λn. if n ∈ {k} then (1 / 2) ^ Suc k else (0::real)) sums (∑r∈{k}. (1 / 2) ^ Suc k)"
using sums_If_finite_set[of "{k}" "λn. ((1::real)/2)^(Suc k)"] by simp
ultimately have "(λn. if n = k then (1 / 2) ^ Suc k else (0::real)) sums (1/2)^(Suc k)"
by simp
thus ?thesis
using sums_unique[of "λn. if n = k then (1 / 2) ^ Suc k else (0::real)" "(1/2)^(Suc k)"]
by simp
qed
also have "(∑n::nat. (if n = k then (1/2)^(Suc k) else 0)) ≤ (∑n::nat. real (a n) * (1/2)^(Suc n))"
proof(rule suminf_le)
show "⋀n. (if n = k then (1 / 2) ^ Suc k else 0) ≤ real (a n) * (1 / 2) ^ Suc n"
proof -
fix n
show "(if n = k then (1 / 2) ^ Suc k else 0) ≤ real (a n) * (1 / 2) ^ Suc n"
by(cases "n = k"; simp add: h1)
qed
next
show "summable (λn. if n = k then (1 / 2) ^ Suc k else (0::real))"
using summable_single[of k "λn. ((1::real) / 2) ^ Suc k"]
by simp
next
show "summable (λn. real (a n) * (1 / 2) ^ Suc n)"
using binary_expression_summable[of a] assms(1)
by simp
qed
finally have "(1 / 2) ^ Suc k ≤ (∑n. real (a n) * (1 / 2) ^ Suc n)" .
moreover have "0 < ((1::real) / 2) ^ Suc k" by simp
ultimately show ?thesis by linarith
qed
lemma r01_binary_expression_ex0:
assumes "0 < r" "r < 1"
shows "∃i. r01_binary_expansion' r i = 0"
proof (rule ccontr)
assume "¬ (∃ i. r01_binary_expansion' r i = 0)"
then have "⋀i. r01_binary_expansion' r i = 1"
using real01_binary_expansion'_0or1[of r] by blast
hence 1:"r01_binary_expression r = (λn. ∑i=0..n. ((1/2)^(Suc i)))"
by(auto simp: r01_binary_expression_def r01_binary_sum_def)
have "LIMSEQ (r01_binary_expression r) 1"
proof -
have "LIMSEQ (λn. ∑i=0..n. (((1::real)/2)^(Suc i))) 1"
using power_half_series sums_def'[of "λn. ((1::real)/2)^(Suc n)" 1]
by simp
thus ?thesis
using 1 by simp
qed
moreover have "LIMSEQ (r01_binary_expression r) r"
using r01_binary_expression_converges_to_r[of r] assms
by simp
ultimately have "r = 1"
using LIMSEQ_unique by auto
thus False
using assms by simp
qed
lemma r01_binary_expression_ex1:
assumes "0 < r" "r < 1"
shows "∃i. r01_binary_expansion' r i = 1"
proof (rule ccontr)
assume "¬ (∃i. r01_binary_expansion' r i = 1)"
then have "⋀i. r01_binary_expansion' r i = 0"
using real01_binary_expansion'_0or1[of r] by blast
hence 1:"r01_binary_expression r = (λn. ∑i=0..n. 0)"
by(auto simp add: r01_binary_expression_def r01_binary_sum_def)
hence "LIMSEQ (r01_binary_expression r) 0"
by simp
moreover have "LIMSEQ (r01_binary_expression r) r"
using r01_binary_expression_converges_to_r[of r] assms
by simp
ultimately have "r = 0"
using LIMSEQ_unique by auto
thus False
using assms by simp
qed
lemma r01_binary_expansion'_gt1:
"1 ≤ r ⟷ (∀n. r01_binary_expansion' r n = 1)"
proof auto
fix n
assume h:"1 ≤ r"
show "r01_binary_expansion' r n = Suc 0"
unfolding r01_binary_expansion'_def
proof(cases n)
case 0
then show "fst (r01_binary_expansion'' r n) = Suc 0"
using h by simp
next
case 2:(Suc n')
show "fst (r01_binary_expansion'' r n) = Suc 0"
proof(cases "r01_binary_expansion'' r n'")
case 3:(fields a ur lr)
then have "(ur + lr) / 2 ≤ 1"
using r01_binary_expansion_lr_ur_nn[of r "Suc n'"]
by (cases "((ur + lr) / 2) ≤ r") (auto simp: Let_def)
thus "fst (r01_binary_expansion'' r n) = Suc 0"
using h by(simp add: 2 3 Let_def)
qed
qed
next
assume h:"∀n. r01_binary_expansion' r n = Suc 0"
show "1 ≤ r"
proof(rule ccontr)
assume "¬ 1 ≤ r"
then consider "r ≤ 0" | "0 < r ∧ r < 1"
by linarith
then show "False"
proof cases
case 1
then have "r01_binary_expansion' r 0 = 0"
by(simp add: r01_binary_expansion'_def)
then show ?thesis
using h by simp
next
case 2
then have "∃i. r01_binary_expansion' r i = 0"
using r01_binary_expression_ex0[of r] by simp
then show ?thesis
using h by simp
qed
qed
qed
lemma r01_binary_expansion'_lt0:
"r ≤ 0 ⟷ (∀n. r01_binary_expansion' r n = 0)"
proof auto
fix n
assume h:"r ≤ 0"
show "r01_binary_expansion' r n = 0"
proof(cases n)
case 0
then show ?thesis
using h by(simp add: r01_binary_expansion'_def)
next
case hn:(Suc n')
then show ?thesis
unfolding r01_binary_expansion'_def
proof(cases "r01_binary_expansion'' r n'")
case 1:(fields a ur lr)
then have "0 < ((ur + lr) / 2)"
using r01_binary_expansion_lr_ur_nn[of r n']
by simp
hence "r < ..."
using h by linarith
then show "fst (r01_binary_expansion'' r n) = 0 "
by(simp add: 1 hn Let_def)
qed
qed
next
assume h:"∀n. r01_binary_expansion' r n = 0"
show "r ≤ 0"
proof(rule ccontr)
assume "¬ r ≤ 0"
then consider "0 < r ∧ r < 1" | "1 ≤ r" by linarith
thus False
proof cases
case 1
then have "∃i. r01_binary_expansion' r i = 1"
using r01_binary_expression_ex1[of r] by simp
then show ?thesis
using h by simp
next
case 2
then show ?thesis
using r01_binary_expansion'_gt1[of r] h by simp
qed
qed
qed
text ‹The sequence $111111\dots$ does not appear in $r = 0.a_1 a_2\dots$. ›
lemma r01_binary_expression_ex0_strong:
assumes "0 < r" "r < 1"
shows "∃i≥n. r01_binary_expansion' r i = 0"
proof(cases "r01_binary_expansion'' r n")
case 1:(fields a ur lr)
show ?thesis
proof(rule ccontr)
assume "¬ (∃i≥n. r01_binary_expansion' r i = 0)"
then have h:"∀i≥n. r01_binary_expansion' r i = 1"
using real01_binary_expansion'_0or1[of r] by blast
have "r = (∑i=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) + (∑i::nat. real (r01_binary_expansion' r (i + (Suc n))) * ((1/2)^(Suc (i + (Suc n)))))"
proof -
have "r = (∑l. real (r01_binary_expansion' r l) * (1 / 2) ^ Suc l)"
using r01_binary_expression_correct[of r] assms by simp
also have "... = (∑l. real (r01_binary_expansion' r (l + Suc n)) * (1 / 2) ^ Suc (l + Suc n)) + (∑i<Suc n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i)"
apply(rule suminf_split_initial_segment)
apply(rule binary_expression_summable)
using real01_binary_expansion'_0or1[of r] by simp
also have "... = (∑i=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) + (∑i::nat. real (r01_binary_expansion' r (i + (Suc n))) * ((1/2)^(Suc (i + (Suc n)))))"
proof -
have "⋀n. {..<Suc n} = {0..n}" by auto
thus ?thesis by simp
qed
finally show ?thesis .
qed
also have "... = (∑i=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) + (∑i::nat. ((1/2)^(Suc (i + (Suc n)))))"
using h by simp
also have "... = (∑i=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) + (1/2)^(Suc n)"
using half_sum[of "Suc n"] by simp
also have "... = lr + (1/2)^(Suc n)"
using 1 r01_binary_expression_eq_lr[of r n]
by(simp add: r01_binary_expression_def r01_binary_sum_def)
also have "... = ur"
using r01_binary_expansion_diff[of r n]
by(simp add: 1)
finally have "r = ur" .
moreover have "r < ur"
using r01_binary_expansion_lr_r_ur[of r n] assms 1
by simp
ultimately show False
by simp
qed
qed
text ‹ A binary expression is well-formed when $111\dots$ does not appear in the tail of the sequence ›
definition biexp01_well_formed :: "(nat ⇒ nat) ⇒ bool" where
"biexp01_well_formed a ≡ (∀n. a n ∈ {0,1}) ∧ (∀n. ∃m≥n. a m = 0)"
lemma biexp01_well_formedE:
assumes "biexp01_well_formed a"
shows "(∀n. a n ∈ {0,1}) ∧ (∀n. ∃m≥n. a m = 0)"
using assms by(simp add: biexp01_well_formed_def)
lemma biexp01_well_formedI:
assumes "⋀n. a n ∈ {0,1}"
and "⋀n. ∃m≥n. a m = 0"
shows "biexp01_well_formed a"
using assms by(simp add: biexp01_well_formed_def)
lemma r01_binary_expansion_well_formed:
assumes "0 < r" "r < 1"
shows "biexp01_well_formed (r01_binary_expansion' r)"
using r01_binary_expression_ex0_strong[of r] assms real01_binary_expansion'_0or1[of r]
by(simp add: biexp01_well_formed_def)
lemma biexp01_well_formed_comb:
assumes "biexp01_well_formed a"
and "biexp01_well_formed b"
shows "biexp01_well_formed (λn. if even n then a (n div 2)
else b ((n-1) div 2))"
proof(rule biexp01_well_formedI)
show "⋀n. (if even n then a (n div 2) else b ((n - 1) div 2)) ∈ {0, 1}"
using assms biexp01_well_formedE by simp
next
fix n
obtain m where 1:"m≥n ∧ a m = 0"
using assms biexp01_well_formedE by blast
then have "a ((2*m) div 2) = 0" by simp
hence "(if even (2*m) then a (2*m div 2) else b ((2*m - 1) div 2)) = 0"
by simp
moreover have "2*m ≥ n" using 1 by simp
ultimately show "∃m≥n. (if even m then a (m div 2) else b ((m - 1) div 2)) = 0"
by auto
qed
lemma nat_complete_induction:
assumes "P (0 :: nat)"
and "⋀n. (⋀m. m ≤ n ⟹ P m) ⟹ P (Suc n)"
shows "P n"
proof(cases n)
case 0
then show ?thesis
using assms(1) by simp
next
case h:(Suc n')
have "P (Suc n')"
proof(rule assms(2))
show "⋀m. m ≤ n' ⟹ P m"
proof(induction n')
case 0
then show ?case
using assms(1) by simp
next
case (Suc n'')
then show ?case
by (metis assms(2) le_SucE)
qed
qed
thus ?thesis
using h by simp
qed
text ‹ ‹(∑m. real (a m) * (1 / 2) ^ Suc m) n = a n›.›
lemma biexp01_well_formed_an:
assumes "biexp01_well_formed a"
shows "r01_binary_expansion' (∑m. real (a m) * (1 / 2) ^ Suc m) n = a n"
proof(rule nat_complete_induction[of _ n])
show "r01_binary_expansion' (∑m. real (a m) * (1 / 2) ^ Suc m) 0 = a 0"
proof (auto simp add: r01_binary_expansion'_def)
assume h:"1 ≤ (∑m. real (a m) * (1 / 2) ^ m / 2) * 2"
show "Suc 0 = a 0"
proof(rule ccontr)
assume "Suc 0 ≠ a 0"
then have "a 0 = 0"
using assms(1) biexp01_well_formedE[of a] by auto
hence "(∑m. real (a m) * (1 / 2) ^ (Suc m)) = (∑m. real (a (Suc m)) * (1 / 2) ^ (Suc (Suc m)))"
using suminf_split_head[of "λm. real (a m) * (1 / 2) ^ (Suc m)"] binary_expression_summable[of a] assms biexp01_well_formedE
by simp
also have "... < 1/2"
using ai_exists0_less_than_sum[of a 1] assms biexp01_well_formedE[of a]
by auto
finally have "(∑m. real (a m) * (1 / 2) ^ m / 2) < 1/2"
by simp
thus False
using h by simp
qed
next
assume h:"¬ 1 ≤ (∑m. real (a m) * (1 / 2) ^ m / 2) * 2"
show "a 0 = 0"
proof(rule ccontr)
assume "a 0 ≠ 0"
then have "a 0 = 1"
using assms(1) biexp01_well_formedE[of a]
by (meson insertE singletonD)
hence "1/2 ≤ (∑m. real (a m) * (1 / 2) ^ (Suc m))"
using ai_1_gt[of a 0] assms(1) biexp01_well_formedE[of a]
by auto
thus False
using h by simp
qed
qed
next
fix n :: nat
assume ih:"(⋀m. m ≤ n ⟹ r01_binary_expansion' (∑m. real (a m) * (1 / 2) ^ Suc m) m = a m)"
show "r01_binary_expansion' (∑m. real (a m) * (1 / 2) ^ Suc m) (Suc n) = a (Suc n)"
proof(cases "r01_binary_expansion'' (∑m. real (a m) * (1 / 2) ^ Suc m) n")
case h:(fields bn ur lr)
then have hlr:"lr = (∑k=0..n. real (a k) * (1 / 2) ^ Suc k)"
using r01_binary_expression_eq_lr[of "∑m. real (a m) * (1 / 2) ^ Suc m" n] ih
by(simp add: r01_binary_expression_def r01_binary_sum_def)
have hlr2:"(ur + lr) / 2 = lr + (1/2)^(Suc (Suc n))"
proof -
have "(ur + lr) / 2 = lr + (1/2)^(Suc (Suc n))"
using r01_binary_expansion_diff[of "∑m. real (a m) * (1 / 2) ^ Suc m" n] h by simp
show ?thesis
by (simp add: ‹(ur + lr) / 2 = lr + (1 / 2) ^ Suc (Suc n)› of_rat_add of_rat_divide of_rat_power)
qed
show ?thesis
using h
proof(auto simp add: r01_binary_expansion'_def Let_def)
assume h1: "(ur + lr) ≤ (∑m. real (a m) * (1 / 2) ^ m / 2) * 2"
show "Suc 0 = a (Suc n)"
proof(rule ccontr)
assume "Suc 0 ≠ a (Suc n)"
then have "a (Suc n) = 0"
using assms(1) biexp01_well_formedE[of a] by auto
have "(∑m. real (a m) * (1 / 2) ^ m / 2) < (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (1/2)^(Suc (Suc n))"
proof -
have "(∑m. real (a m) * (1 / 2) ^ (Suc m)) = (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (∑m. real (a (m+Suc n)) * (1 / 2) ^ Suc (m + Suc n))"
proof -
have "{0..n} = {..<Suc n}" by auto
thus ?thesis
using suminf_split_initial_segment[of "λm. real (a m) * (1 / 2) ^ (Suc m)" "Suc n"] binary_expression_summable[of a] assms(1) biexp01_well_formedE[of a]
by simp
qed
also have "... = (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (∑m. real (a (Suc m + Suc n)) * (1 / 2) ^ Suc (Suc m + Suc n))"
using suminf_split_head[of "λm. real (a (m + Suc n)) * (1 / 2) ^ (Suc (m + Suc n))"] binary_expression_summable[of a] assms(1) biexp01_well_formedE[of a] Series.summable_iff_shift[of "λm. real (a m) * (1 / 2) ^ (Suc m)" "Suc n"] ‹a (Suc n) = 0›
by simp
also have "... = (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (∑m. real (a (m + Suc (Suc n))) * (1 / 2) ^ Suc (m + Suc (Suc n)))"
by simp
also have "... < (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (1/2)^Suc (Suc n)"
using ai_exists0_less_than_sum[of a "Suc (Suc n)"] assms(1) biexp01_well_formedE[of a]
by auto
finally show ?thesis by simp
qed
thus False
using h1 hlr2 hlr by simp
qed
next
assume h2:"¬ ur + lr ≤ (∑m. real (a m) * (1 / 2) ^ m / 2) * 2"
show "a (Suc n) = 0"
proof(rule ccontr)
assume "a (Suc n) ≠ 0"
then have "a (Suc n) = 1"
using biexp01_well_formedE[OF assms(1)]
by (meson insertE singletonD)
have "(∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (1/2)^(Suc (Suc n)) ≤ (∑m. real (a m) * (1 / 2) ^ m / 2)"
proof -
have "(∑m. real (a m) * (1 / 2) ^ (Suc m)) = (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (∑m. real (a (m+Suc n)) * (1 / 2) ^ Suc (m + Suc n))"
proof -
have "{0..n} = {..<Suc n}" by auto
thus ?thesis
using suminf_split_initial_segment[of "λm. real (a m) * (1 / 2) ^ (Suc m)" "Suc n"] binary_expression_summable[of a] assms(1) biexp01_well_formedE[of a]
by simp
qed
also have "... = (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (∑m. real (a (Suc m + Suc n)) * (1 / 2) ^ Suc (Suc m + Suc n)) + (1 / 2) ^ Suc (Suc n)"
using suminf_split_head[of "λm. real (a (m + Suc n)) * (1 / 2) ^ (Suc (m + Suc n))"] binary_expression_summable[of a] assms(1) biexp01_well_formedE[of a] Series.summable_iff_shift[of "λm. real (a m) * (1 / 2) ^ (Suc m)" "Suc n"] ‹a (Suc n) = 1›
by simp
also have "... = (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (∑m. real (a (m + Suc (Suc n))) * (1 / 2) ^ Suc (m + (Suc (Suc n)))) + (1 / 2) ^ Suc (Suc n)"
by simp
also have "... ≥ (∑k=0..n. real (a k) * (1 / 2) ^ Suc k) + (1 / 2) ^ Suc (Suc n)"
using binary_expression_gteq0[of a "Suc (Suc n)"] assms(1) biexp01_well_formedE[of a] by simp
finally show ?thesis by simp
qed
thus False
using h2 hlr2 hlr by simp
qed
qed
qed
qed
lemma f01_borel_measurable:
assumes "f -` {0::real} ∈ sets real_borel"
"f -` {1} ∈ sets borel"
and "⋀r::real. f r ∈ {0,1}"
shows "f ∈ borel_measurable real_borel"
proof(rule measurableI)
fix U :: "real set"
assume "U ∈ sets borel"
consider "1 ∈ U ∧ 0 ∈ U" | "1 ∈ U ∧ 0 ∉ U" | "1 ∉ U ∧ 0 ∈ U" | "1 ∉ U ∧ 0 ∉ U"
by auto
then show "f -` U ∩ space real_borel ∈ sets borel"
proof cases
case 1
then have "f -` U = UNIV"
using assms(3) by auto
then show ?thesis by simp
next
case 2
then have "f -` U = f -` {1}"
using assms(3) by fastforce
then show ?thesis
using assms(2) by simp
next
case 3
then have "f -` U = f -` {0}"
using assms(3) by fastforce
then show ?thesis
using assms(1) by simp
next
case 4
then have "f -` U = {}"
using assms(3) by (metis all_not_in_conv insert_iff vimage_eq)
then show ?thesis by simp
qed
qed simp
lemma r01_binary_expansion'_measurable:
"(λr. real (r01_binary_expansion' r n)) ∈ borel_measurable (borel :: real measure)"
proof -
have "(λr. real (r01_binary_expansion' r n)) -`{0} ∈ sets borel ∧ (λr. real (r01_binary_expansion' r n)) -`{1} ∈ sets borel"
proof -
let ?A = "{..0::real} ∪ (⋃i∈{l::nat. l < 2^(Suc n) ∧ even l} . {i/2^(Suc n)..<(Suc i)/2^(Suc n)})"
let ?B = "{1::real..} ∪ (⋃i∈{l::nat. l < 2^(Suc n) ∧ odd l} . {i/2^(Suc n)..<(Suc i)/2^(Suc n)})"
have "?A ∈ sets borel" by simp
have "?B ∈ sets borel" by simp
have hE:"?A ∩ ?B = {}"
proof auto
fix r :: real
fix l :: nat
assume h: "r ≤ 0"
"odd l"
"real l / (2 * 2 ^ n) ≤ r"
then have "0 < l" by(cases l; auto)
hence "0 < real l / (2 * 2 ^ n)" by simp
thus False
using h by simp
next
fix r :: real
fix l :: nat
assume h: "l < 2 * 2 ^ n"
"even l"
"1 ≤ r"
"r < (1 + real l) / (2 * 2 ^ n)"
then have "1 + real l ≤ 2 * 2 ^ n"
by (simp add: nat_less_real_le)
moreover have "1 + real l ≠ 2 * 2 ^ n"
using h by auto
ultimately have "1 + real l < 2 * 2 ^ n" by simp
hence "(1 + real l) / (2 * 2 ^ n) < 1" by simp
thus False using h by linarith
next
fix r :: real
fix l1 l2 :: nat
assume h: "even l1" "odd l2"
"real l1 / (2 * 2 ^ n) ≤ r" "r < (1 + real l1) / (2 * 2 ^ n)"
"real l2 / (2 * 2 ^ n) ≤ r" "r < (1 + real l2) / (2 * 2 ^ n)"
then consider "l1 < l2" | "l2 < l1" by fastforce
thus False
proof cases
case 1
then have "(1 + real l1) / (2 * 2 ^ n) ≤ real l2 / (2 * 2 ^ n)"
by (simp add: frac_le)
then show ?thesis
using h by simp
next
case 2
then have "(1 + real l2) / (2 * 2 ^ n) ≤ real l1 / (2 * 2 ^ n)"
by (simp add: frac_le)
then show ?thesis
using h by simp
qed
qed
have hU:"?A ∪ ?B = UNIV"
proof
show "?A ∪ ?B ⊆ UNIV" by simp
next
show "UNIV ⊆ ?A ∪ ?B"
proof
fix r :: real
consider "r ≤ 0" | "0 < r ∧ r < 1" | "1 ≤ r" by linarith
then show "r ∈ ?A ∪ ?B"
proof cases
case 1
then show ?thesis by simp
next
case 2
show ?thesis
proof(cases "r01_binary_expansion'' r n")
case hc:(fields a ur lr)
then have hlu:"lr ≤ r ∧ r < ur"
using 2 r01_binary_expansion_lr_r_ur[of r n] by simp
obtain k :: nat where hk:
"lr = real k / 2 ^ Suc n ∧ k < 2 ^ Suc n"
using r01_binary_expression'_sum_range[of r n] hc
by auto
hence "ur = real (Suc k) / 2^Suc n"
using r01_binary_expansion_diff[of r n] hc
by (simp add: add_divide_distrib power_one_over)
thus ?thesis
using hlu hk by auto
qed
next
case 3
then show ?thesis by simp
qed
qed
qed
have hi1:"- ?A = ?B"
proof -
have "?B ⊆ - ?A"
using hE by blast
moreover have "-?A ⊆ ?B"
proof -
have "-(?A ∪ ?B) = {}"
using hU by simp
hence "(-?A) ∩ (-?B) = {}" by simp
thus ?thesis
by blast
qed
ultimately show ?thesis
by blast
qed
have hi2: "?A = -?B"
using hi1 by blast
let ?U0 = "(λr. real (r01_binary_expansion' r n)) -`{0}"
let ?U1 = "(λr. real (r01_binary_expansion' r n)) -`{1}"
have hU':"?U0 ∪ ?U1 = UNIV"
proof -
have "?U0 ∪ ?U1 = (λr. real (r01_binary_expansion' r n)) -`{0,1}"
by auto
thus ?thesis
using real01_binary_expansion'_0or1[of _ n] by auto
qed
have hE':"?U0 ∩ ?U1 = {}"
by auto
have hiu1:"- ?U0 = ?U1"
using hE' hU' by fastforce
have hiu2:"- ?U1 = ?U0"
using hE' hU' by fastforce
have "?U0 ⊆ ?A"
proof
fix r
assume "r ∈ ?U0"
then have h1:"r01_binary_expansion' r n = 0"
by simp
then consider "r ≤ 0" | "0 < r ∧ r < 1"
using r01_binary_expansion'_gt1[of r] by fastforce
thus "r ∈ ?A"
proof cases
case 1
then show ?thesis by simp
next
case 2
then have 3:"(snd (snd (r01_binary_expansion'' r n))) ≤ r ∧
r < (fst (snd (r01_binary_expansion'' r n)))"
using r01_binary_expansion_lr_r_ur[of r n] by simp
obtain k where 4:
"(snd (snd (r01_binary_expansion'' r n))) =
real k / 2 ^ Suc n ∧
k < 2 ^ Suc n ∧ even k"
using r01_binary_expression'_sum_range[of r n] h1
by auto
have "(fst (snd (r01_binary_expansion'' r n))) = real (Suc k) / 2 ^ Suc n"
proof -
have "(fst (snd (r01_binary_expansion'' r n))) = (snd (snd (r01_binary_expansion'' r n))) + (1/2)^Suc n"
using r01_binary_expansion_diff[of r n] by linarith
thus ?thesis
using 4
by (simp add: add_divide_distrib power_one_over)
qed
thus ?thesis
using 3 4 by auto
qed
qed
have "?U1 ⊆ ?B"
proof
fix r
assume "r ∈ ?U1"
then have h1:"r01_binary_expansion' r n = 1"
by simp
then consider "1 ≤ r" | "0 < r ∧ r < 1"
using r01_binary_expansion'_lt0[of r] by fastforce
thus "r ∈ ?B"
proof cases
case 1
then show ?thesis by simp
next
case 2
then have 3:"(snd (snd (r01_binary_expansion'' r n))) ≤ r ∧
r < (fst (snd (r01_binary_expansion'' r n)))"
using r01_binary_expansion_lr_r_ur[of r n] by simp
obtain k where 4:
"(snd (snd (r01_binary_expansion'' r n))) =
real k / 2 ^ Suc n ∧
k < 2 ^ Suc n ∧ odd k"
using StandardBorel.r01_binary_expression'_sum_range[of r n] h1
by auto
have "(fst (snd (r01_binary_expansion'' r n))) = real (Suc k) / 2 ^ Suc n"
proof -
have "(fst (snd (r01_binary_expansion'' r n))) = (snd (snd (r01_binary_expansion'' r n))) + (1/2)^Suc n"
using r01_binary_expansion_diff[of r n] by simp
thus ?thesis
using 4
by (simp add: add_divide_distrib power_one_over)
qed
thus ?thesis
using 3 4 by auto
qed
qed
have "?U0 = ?A"
proof
show "?U0 ⊆ ?A" by fact
next
show "?A ⊆ ?U0"
using ‹?U1 ⊆ ?B› Compl_subset_Compl_iff[of ?U0 ?A] hi1 hiu1
by blast
qed
have "?U1 = ?B"
using ‹?U0 = ?A› hi1 hiu1 by auto
show ?thesis
using ‹?U0 = ?A› ‹?U1 = ?B› ‹?A ∈ sets borel› ‹?B ∈ sets borel›
by simp
qed
thus ?thesis
using f01_borel_measurable[of "(λr. real (r01_binary_expansion' r n))"] real01_binary_expansion'_0or1[of _ n]
by simp
qed
definition r01_to_r01_r01_fst' :: "real ⇒ nat ⇒ nat" where
"r01_to_r01_r01_fst' r n ≡ r01_binary_expansion' r (2*n)"
lemma r01_to_r01_r01_fst'in01:
"⋀n. r01_to_r01_r01_fst' r n ∈ {0,1}"
using real01_binary_expansion'_0or1 by (simp add: r01_to_r01_r01_fst'_def)
definition r01_to_r01_r01_fst_sum :: "real ⇒ nat ⇒ real" where
"r01_to_r01_r01_fst_sum ≡ r01_binary_sum ∘ r01_to_r01_r01_fst'"
definition r01_to_r01_r01_fst :: "real ⇒ real" where
"r01_to_r01_r01_fst = lim ∘ r01_to_r01_r01_fst_sum"
lemma r01_to_r01_r01_fst_def':
"r01_to_r01_r01_fst r = (∑n. real (r01_binary_expansion' r (2*n)) * (1/2)^(n+1))"
proof -
have "r01_to_r01_r01_fst_sum r = (λn. ∑i=0..n. real (r01_binary_expansion' r (2*i)) * (1/2)^(i+1))"
by(auto simp add: r01_to_r01_r01_fst_sum_def r01_binary_sum_def r01_to_r01_r01_fst'_def)
thus ?thesis
using lim_sum_ai real01_binary_expansion'_0or1
by(simp add: r01_to_r01_r01_fst_def)
qed
lemma r01_to_r01_r01_fst_measurable:
"r01_to_r01_r01_fst ∈ borel_measurable borel"
unfolding r01_to_r01_r01_fst_def'
using r01_binary_expansion'_measurable by auto
definition r01_to_r01_r01_snd' :: "real ⇒ nat ⇒ nat" where
"r01_to_r01_r01_snd' r n = r01_binary_expansion' r (2*n + 1)"
lemma r01_to_r01_r01_snd'in01:
"⋀n. r01_to_r01_r01_snd' r n ∈ {0,1}"
using real01_binary_expansion'_0or1 by (simp add: r01_to_r01_r01_snd'_def)
definition r01_to_r01_r01_snd_sum :: "real ⇒ nat ⇒ real" where
"r01_to_r01_r01_snd_sum ≡ r01_binary_sum ∘ r01_to_r01_r01_snd'"
definition r01_to_r01_r01_snd :: "real ⇒ real" where
"r01_to_r01_r01_snd = lim ∘ r01_to_r01_r01_snd_sum"
lemma r01_to_r01_r01_snd_def':
"r01_to_r01_r01_snd r = (∑n. real (r01_binary_expansion' r (2*n + 1)) * (1/2)^(n+1))"
proof -
have "r01_to_r01_r01_snd_sum r = (λn. ∑i=0..n. real (r01_binary_expansion' r (2*i + 1)) * (1/2)^(i+1))"
by(auto simp add: r01_to_r01_r01_snd_sum_def r01_binary_sum_def r01_to_r01_r01_snd'_def)
thus ?thesis
using lim_sum_ai real01_binary_expansion'_0or1
by(simp add: r01_to_r01_r01_snd_def)
qed
lemma r01_to_r01_r01_snd_measurable:
"r01_to_r01_r01_snd ∈ borel_measurable borel"
unfolding r01_to_r01_r01_snd_def'
using r01_binary_expansion'_measurable by auto
definition r01_to_r01_r01 :: "real ⇒ real × real" where
"r01_to_r01_r01 r = (r01_to_r01_r01_fst r,r01_to_r01_r01_snd r)"
lemma r01_to_r01_r01_image:
"r01_to_r01_r01 r ∈ {0..1}×{0..1}"
using r01_to_r01_r01_fst_def'[of r] r01_to_r01_r01_snd_def'[of r] real01_binary_expansion'_0or1
binary_expression_gteq0[of "λn. r01_binary_expansion' r (2*n)" 0] binary_expression_leeq1[of "λn. r01_binary_expansion' r (2*n)" 0] binary_expression_gteq0[of "λn. r01_binary_expansion' r (2*n+1)" 0] binary_expression_leeq1[of "λn. r01_binary_expansion' r (2*n+1)" 0]
by(simp add: r01_to_r01_r01_def)
lemma r01_to_r01_r01_measurable:
"r01_to_r01_r01 ∈ real_borel →⇩M real_borel ⨂⇩M real_borel"
unfolding r01_to_r01_r01_def
using borel_measurable_Pair[of r01_to_r01_r01_fst borel r01_to_r01_r01_snd] r01_to_r01_r01_fst_measurable r01_to_r01_r01_snd_measurable
by(simp add: borel_prod)
lemma r01_to_r01_r01_3over4:
"r01_to_r01_r01 (3/4) = (1/2,1/2)"
proof -
have h0:"r01_binary_expansion' (3/4) 0 = 1"
by (simp add: r01_binary_expansion'_def)
have h1:"r01_binary_expansion' (3/4) 1 = 1"
by (simp add: r01_binary_expansion'_def Let_def of_rat_divide)
have hn:"⋀n. n>1⟹ r01_binary_expansion' (3/4) n = 0"
proof -
fix n :: nat
assume h:"1 < n"
show "r01_binary_expansion' (3 / 4) n = 0"
proof(rule ccontr)
assume "r01_binary_expansion' (3 / 4) n ≠ 0"
have "3/4 < (∑i=0..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))"
proof -
have "(∑i=0..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)) = real (r01_binary_expansion' (3/4) 0) * (1/2)^(Suc 0) + (∑i=(Suc 0)..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))"
by(rule sum.atLeast_Suc_atMost) (simp add: h)
also have "... = real (r01_binary_expansion' (3/4) 0) * (1/2)^(Suc 0) + (real (r01_binary_expansion' (3/4) 1) * (1/2)^(Suc 1) + (∑i=(Suc (Suc 0))..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)))"
using sum.atLeast_Suc_atMost[OF order.strict_implies_order[OF h],of "λi. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)"]
by simp
also have "... = 3/4 + (∑i=2..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))"
using h0 h1 by(simp add: numeral_2_eq_2)
also have "... > 3/4"
proof -
have "(∑i=2..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)) = (∑i=2..n-1. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)) + real (r01_binary_expansion' (3/4) n) * (1/2)^Suc n"
by (metis (no_types, lifting) h One_nat_def Suc_pred less_2_cases_iff less_imp_add_positive order_less_irrefl plus_1_eq_Suc sum.cl_ivl_Suc zero_less_Suc)
hence "real (r01_binary_expansion' (3/4) n) * (1/2)^Suc n ≤ (∑i=2..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))"
using ordered_comm_monoid_add_class.sum_nonneg[of "{2..n-1}" "λi. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)"]
by simp
moreover have "0 < real (r01_binary_expansion' (3/4) n) * (1/2)^Suc n"
using ‹r01_binary_expansion' (3 / 4) n ≠ 0› by simp
ultimately have "0 < (∑i=2..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))"
by simp
thus ?thesis by simp
qed
finally show "3 / 4 < (∑i = 0..n. real (r01_binary_expansion' (3 / 4) i) * (1 / 2) ^ Suc i)" .
qed
moreover have "(∑i=0..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)) ≤ 3/4"
using r01_binary_expansion_lr_r_ur[of "3/4" n] r01_binary_expression_eq_lr[of "3/4" n]
by(simp add: r01_binary_expression_def r01_binary_sum_def)
ultimately show False by simp
qed
qed
show ?thesis
proof
have "fst (r01_to_r01_r01 (3 / 4)) = (∑n. real (r01_binary_expansion' (3 / 4) (2 * n)) * (1 / 2) ^ Suc n)"
by(simp add: r01_to_r01_r01_def r01_to_r01_r01_fst_def')
also have "... = 1/2 + (∑n. real (r01_binary_expansion' (3 / 4) (2 * Suc n)) * (1 / 2) ^ Suc (Suc n))"
using suminf_split_head[of "λn. real (r01_binary_expansion' (3 / 4) (2 * n)) * (1 / 2) ^ Suc n"] binary_expression_summable[of "λn. r01_binary_expansion' (3/4) (2*n)"] real01_binary_expansion'_0or1[of "3/4"] h0
by simp
also have "... = 1/2"
proof -
have "∀n. real (r01_binary_expansion' (3 / 4) (2 * Suc n)) * (1 / 2) ^ Suc (Suc n) = 0"
using hn by simp
hence "(∑n. real (r01_binary_expansion' (3 / 4) (2 * Suc n)) * (1 / 2) ^ Suc (Suc n)) = 0"
by simp
thus ?thesis
by simp
qed
finally show "fst (r01_to_r01_r01 (3 / 4)) = fst (1 / 2, 1 / 2)"
by simp
next
have "snd (r01_to_r01_r01 (3 / 4)) = (∑n. real (r01_binary_expansion' (3 / 4) (2 * n + 1)) * (1 / 2) ^ Suc n)"
by(simp add: r01_to_r01_r01_def r01_to_r01_r01_snd_def')
also have "... = 1/2 + (∑n. real (r01_binary_expansion' (3 / 4) (2 * Suc n + 1)) * (1 / 2) ^ Suc (Suc n))"
using suminf_split_head[of "λn. real (r01_binary_expansion' (3 / 4) (2 * n + 1)) * (1 / 2) ^ Suc n"] binary_expression_summable[of "λn. r01_binary_expansion' (3/4) (2*n + 1)"] real01_binary_expansion'_0or1[of "3/4"] h1
by simp
also have "... = 1/2"
proof -
have "∀n. real (r01_binary_expansion' (3 / 4) (2 * Suc n + 1)) * (1 / 2) ^ Suc (Suc n) = 0"
using hn by simp
hence "(∑n. real (r01_binary_expansion' (3 / 4) (2 * Suc n + 1)) * (1 / 2) ^ Suc (Suc n)) = 0"
by simp
thus ?thesis
by simp
qed
finally show "snd (r01_to_r01_r01 (3 / 4)) = snd (1 / 2, 1 / 2)"
by simp
qed
qed
definition r01_r01_to_r01' :: "real × real ⇒ nat ⇒ nat" where
"r01_r01_to_r01' rs ≡ (λn. if even n then r01_binary_expansion' (fst rs) (n div 2)
else r01_binary_expansion' (snd rs) ((n-1) div 2))"
lemma r01_r01_to_r01'in01:
"⋀n. r01_r01_to_r01' rs n ∈ {0,1}"
using real01_binary_expansion'_0or1 by (simp add: r01_r01_to_r01'_def)
lemma r01_r01_to_r01'_well_formed:
assumes "0 < r1" "r1 < 1"
and "0 < r2" "r2 < 1"
shows "biexp01_well_formed (r01_r01_to_r01' (r1,r2))"
using biexp01_well_formed_comb[of "r01_binary_expansion' (fst (r1,r2))" "r01_binary_expansion' (snd (r1,r2))"] r01_binary_expansion_well_formed[of r1] r01_binary_expansion_well_formed[of r2] assms
by (auto simp add: r01_r01_to_r01'_def)
definition r01_r01_to_r01_sum :: "real × real ⇒ nat ⇒ real" where
"r01_r01_to_r01_sum ≡ r01_binary_sum ∘ r01_r01_to_r01'"
definition r01_r01_to_r01 :: "real × real ⇒ real" where
"r01_r01_to_r01 ≡ lim ∘ r01_r01_to_r01_sum"
lemma r01_r01_to_r01_def':
"r01_r01_to_r01 (r1,r2) = (∑n. real (r01_r01_to_r01' (r1,r2) n) * (1/2)^(n+1))"
proof -
have "r01_r01_to_r01_sum (r1,r2) = (λn. (∑i = 0..n. real (r01_r01_to_r01' (r1,r2) i) * (1 / 2) ^ Suc i))"
by(auto simp add: r01_r01_to_r01_sum_def r01_binary_sum_def)
thus ?thesis
using lim_sum_ai[of "λn. r01_r01_to_r01' (r1,r2) n"] r01_r01_to_r01'in01
by(simp add: r01_r01_to_r01_def)
qed
lemma r01_r01_to_r01_measurable:
"r01_r01_to_r01 ∈ real_borel ⨂⇩M real_borel →⇩M real_borel"
proof -
have "r01_r01_to_r01 = (λx. ∑n. real (r01_r01_to_r01' x n) * (1/2)^(n+1))"
using r01_r01_to_r01_def' by auto
also have "... ∈ real_borel ⨂⇩M real_borel →⇩M real_borel"
proof(rule borel_measurable_suminf)
fix n :: nat
have "(λx. real (r01_r01_to_r01' x n) * (1 / 2) ^ (n + 1)) = (λr. r * (1/2)^(n+1)) ∘ (λx. real (r01_r01_to_r01' x n))"
by auto
also have "... ∈ borel_measurable (borel ⨂⇩M borel)"
proof(rule measurable_comp[of _ _ borel])
have "(λx. real (r01_r01_to_r01' x n))
= (λx. if even n then real (r01_binary_expansion' (fst x) (n div 2)) else real (r01_binary_expansion' (snd x) ((n - 1) div 2)))"
by (auto simp add: r01_r01_to_r01'_def)
also have "... ∈ borel_measurable (borel ⨂⇩M borel)"
using r01_binary_expansion'_measurable by simp
finally show "(λx. real (r01_r01_to_r01' x n)) ∈ borel_measurable (borel ⨂⇩M borel)" .
next
show "(λr::real. r * (1 / 2) ^ (n + 1)) ∈ borel_measurable borel"
by simp
qed
finally show "(λx. real (r01_r01_to_r01' x n) * (1 / 2) ^ (n + 1)) ∈ borel_measurable (borel ⨂⇩M borel)" .
qed
finally show ?thesis .
qed
lemma r01_r01_to_r01_image:
assumes "0 < r1" "r1 < 1"
shows "r01_r01_to_r01 (r1,r2) ∈ {0<..<1}"
proof -
obtain i where "r01_binary_expansion' r1 i = 1"
using r01_binary_expression_ex1[of r1] assms(1,2)
by auto
hence hi:"r01_r01_to_r01' (r1,r2) (2*i) = 1"
by(simp add: r01_r01_to_r01'_def)
obtain j where "r01_binary_expansion' r1 j = 0"
using r01_binary_expression_ex0[of r1] assms(1,2)
by auto
hence hj:"r01_r01_to_r01' (r1,r2) (2*j) = 0"
by(simp add: r01_r01_to_r01'_def)
show ?thesis
using ai_exists1_gt0[of "r01_r01_to_r01' (r1,r2)"] ai_exists0_less_than1[of "r01_r01_to_r01' (r1,r2)"] r01_r01_to_r01'in01[of "(r1,r2)"] r01_r01_to_r01_def'[of r1 r2] hi hj
by auto
qed
lemma r01_r01_to_r01_image':
assumes "0 < r2" "r2 < 1"
shows "r01_r01_to_r01 (r1,r2) ∈ {0<..<1}"
proof -
obtain i where "r01_binary_expansion' r2 i = 1"
using r01_binary_expression_ex1[of r2] assms(1,2)
by auto
hence hi:"r01_r01_to_r01' (r1,r2) (2*i + 1) = 1"
by(simp add: r01_r01_to_r01'_def)
obtain j where "r01_binary_expansion' r2 j = 0"
using r01_binary_expression_ex0[of r2] assms(1,2)
by auto
hence hj:"r01_r01_to_r01' (r1,r2) (2*j + 1) = 0"
by(simp add: r01_r01_to_r01'_def)
show ?thesis
using ai_exists1_gt0[of "r01_r01_to_r01' (r1,r2)"] ai_exists0_less_than1[of "r01_r01_to_r01' (r1,r2)"] r01_r01_to_r01'in01[of "(r1,r2)"] r01_r01_to_r01_def'[of r1 r2] hi hj
by auto
qed
lemma r01_r01_to_r01_binary_nth:
assumes "0 < r1" "r1 < 1"
and "0 < r2" "r2 < 1"
shows "r01_binary_expansion' r1 n = r01_binary_expansion' (r01_r01_to_r01 (r1,r2)) (2*n) ∧
r01_binary_expansion' r2 n = r01_binary_expansion' (r01_r01_to_r01 (r1,r2)) (2*n + 1)"
proof -
have "⋀n. r01_binary_expansion' (r01_r01_to_r01 (r1,r2)) n = r01_r01_to_r01' (r1,r2) n"
using r01_r01_to_r01_def'[of r1 r2] biexp01_well_formed_an[of "r01_r01_to_r01' (r1,r2)"] r01_r01_to_r01'_well_formed[of r1 r2] assms
by simp
thus ?thesis
by(simp add: r01_r01_to_r01'_def)
qed
lemma r01_r01__r01__r01_r01_id:
assumes "0 < r1" "r1 < 1"
"0 < r2" "r2 < 1"
shows "(r01_to_r01_r01 ∘ r01_r01_to_r01) (r1,r2) = (r1,r2)"
proof
show "fst ((r01_to_r01_r01 ∘ r01_r01_to_r01) (r1, r2)) = fst (r1, r2)"
proof -
have "fst ((r01_to_r01_r01 ∘ r01_r01_to_r01) (r1, r2)) = r01_to_r01_r01_fst (r01_r01_to_r01 (r1,r2))"
by(simp add: r01_to_r01_r01_def)
also have "... = (∑n. real (r01_binary_expansion' (r01_r01_to_r01 (r1, r2)) (2 * n)) * (1 / 2) ^ (n + 1))"
using r01_to_r01_r01_fst_def'[of "r01_r01_to_r01 (r1,r2)"] by simp
also have "... = (∑n. real (r01_binary_expansion' r1 n) * (1 / 2) ^ (n + 1))"
using r01_r01_to_r01_binary_nth[of r1 r2] assms by simp
also have "... = r1"
using r01_binary_expression_correct[of r1] assms(1,2)
by simp
finally show ?thesis by simp
qed
next
show "snd ((r01_to_r01_r01 ∘ r01_r01_to_r01) (r1, r2)) = snd (r1, r2)"
proof -
have "snd ((r01_to_r01_r01 ∘ r01_r01_to_r01) (r1, r2)) = r01_to_r01_r01_snd (r01_r01_to_r01 (r1,r2))"
by(simp add: r01_to_r01_r01_def)
also have "... = (∑n. real (r01_binary_expansion' (r01_r01_to_r01 (r1, r2)) (2 * n + 1)) * (1 / 2) ^ (n + 1))"
using r01_to_r01_r01_snd_def'[of "r01_r01_to_r01 (r1,r2)"] by simp
also have "... = (∑n. real (r01_binary_expansion' r2 n) * (1 / 2) ^ (n + 1))"
using r01_r01_to_r01_binary_nth[of r1 r2] assms by simp
also have "... = r2"
using r01_binary_expression_correct[of r2] assms(3,4)
by simp
finally show ?thesis by simp
qed
qed
text ‹ We first show that ‹M ⨂⇩M N› is a standard Borel space for standard Borel spaces ‹M› and ‹N›.›
lemma pair_measurable[measurable]:
assumes "f ∈ X →⇩M Y"
and "g ∈ X' →⇩M Y'"
shows "map_prod f g ∈ X ⨂⇩M X' →⇩M Y ⨂⇩M Y'"
using assms by(auto simp add: measurable_pair_iff)
lemma pair_standard_borel_standard:
assumes "standard_borel M"
and "standard_borel N"
shows "standard_borel (M ⨂⇩M N)"
proof -
define rr_to_r :: "real × real ⇒ real"
where "rr_to_r ≡ real_to_01open_inverse ∘ r01_r01_to_r01 ∘ (λ(x,y). (real_to_01open x, real_to_01open y))"
have 1[measurable]: "rr_to_r ∈ real_borel ⨂⇩M real_borel →⇩M real_borel"
proof -
have "(λ(x,y). (real_to_01open x, real_to_01open y)) ∈ real_borel ⨂⇩M real_borel →⇩M real_borel ⨂⇩M real_borel"
using borel_measurable_continuous_onI[OF real_to_01open_continuous]
by simp
from measurable_restrict_space2[OF _ this,of "{0<..<1}×{0<..<1}"]
have [measurable]:"(λ(x,y). (real_to_01open x, real_to_01open y)) ∈ real_borel ⨂⇩M real_borel →⇩M restrict_space (real_borel ⨂⇩M real_borel) ({0<..<1}×{0<..<1})"
by(simp add: split_beta' real_to_01open_01)
have [measurable]: "r01_r01_to_r01 ∈ restrict_space (real_borel ⨂⇩M real_borel) ({0<..<1}×{0<..<1}) →⇩M restrict_space real_borel {0<..<1}"
using r01_r01_to_r01_image' by(auto intro!: measurable_restrict_space3[OF r01_r01_to_r01_measurable])
thus ?thesis
using borel_measurable_continuous_on_restrict[OF real_to_01open_inverse_continuous]
by(simp add: rr_to_r_def)
qed
define r_to_01 :: "real ⇒ real"
where "r_to_01 ≡ (λr. if r ∈ real_to_01open -` (r01_to_r01_r01 -` ({0<..<1}×{0<..<1})) then real_to_01open r else 3/4)"
define r01_to_r01_r01' :: "real ⇒ real × real"
where "r01_to_r01_r01' ≡ (λr. if r ∈ r01_to_r01_r01 -` ({0<..<1}×{0<..<1}) then r01_to_r01_r01 r else (1/2,1/2))"
define r_to_rr :: "real ⇒ real × real"
where "r_to_rr ≡ (λ(x,y). (real_to_01open_inverse x, real_to_01open_inverse y)) ∘ r01_to_r01_r01' ∘ r_to_01"
have 2[measurable]: "r_to_rr ∈ real_borel →⇩M real_borel ⨂⇩M real_borel"
proof -
have 1: "{0<..<1}×{0<..<1} ∈ sets (restrict_space (real_borel ⨂⇩M real_borel) ({0..1}×{0..1}))"
by(auto simp: sets_restrict_space_iff)
have 2[measurable]: "real_to_01open ∈ real_borel →⇩M restrict_space real_borel {0<..<1}"
using measurable_restrict_space2[OF _ borel_measurable_continuous_onI[OF real_to_01open_continuous] ,of "{0<..<1}"]
by(simp add: real_to_01open_01)
have 3: "real_to_01open -` space (restrict_space real_borel {0<..<1}) = UNIV"
using real_to_01open_01 by auto
have "r01_to_r01_r01 ∈ restrict_space real_borel {0<..<1} →⇩M restrict_space (real_borel ⨂⇩M real_borel) ({0..1}×{0..1})"
using r01_to_r01_r01_image measurable_restrict_space3[OF r01_to_r01_r01_measurable] by simp
note 4 = measurable_sets[OF this 1]
note 5 = measurable_sets[OF 2 4,simplified vimage_Int 3,simplified]
have [measurable]:"r_to_01 ∈ real_borel →⇩M restrict_space real_borel {0<..<1}"
unfolding r_to_01_def
by(rule measurable_If_set) (auto intro!: measurable_restrict_space2 simp: 5)
have [measurable]: "r01_to_r01_r01' ∈ restrict_space real_borel {0<..<1} →⇩M restrict_space (real_borel ⨂⇩M real_borel) ({0<..<1}×{0<..<1})"
using 4 r01_to_r01_r01_measurable
by(auto intro!: measurable_restrict_space3 simp: r01_to_r01_r01'_def)
have [measurable]: "(λ(x,y). (real_to_01open_inverse x, real_to_01open_inverse y)) ∈ restrict_space (real_borel ⨂⇩M real_borel) ({0<..<1}×{0<..<1}) →⇩M real_borel ⨂⇩M real_borel"
using borel_measurable_continuous_on_restrict[OF continuous_on_Pair[OF continuous_on_compose[of "{0<..<1::real}×{0<..<1::real}",OF continuous_on_fst[OF continuous_on_id'],simplified,OF real_to_01open_inverse_continuous] continuous_on_compose[of "{0<..<1::real}×{0<..<1::real}",OF continuous_on_snd[OF continuous_on_id'],simplified,OF real_to_01open_inverse_continuous]]]
by(simp add: split_beta' borel_prod)
show ?thesis
by(simp add: r_to_rr_def)
qed
have 3: "⋀x. r_to_rr (rr_to_r x) = x"
using r01_to_r01_r01_image r01_r01_to_r01_image r01_r01__r01__r01_r01_id real_to_01open_01 real_to_01open_inverse_correct' fun_cong[OF real_to_01open_inverse_correct]
by(auto simp add: r01_to_r01_r01'_def r_to_01_def comp_def split_beta' r_to_rr_def rr_to_r_def)
interpret s1: standard_borel M by fact
interpret s2: standard_borel N by fact
show ?thesis
by(auto intro!: standard_borelI[where f="rr_to_r ∘ map_prod s1.f s2.f" and g="map_prod s1.g s2.g ∘ r_to_rr"] simp: 3 space_pair_measure)
qed
lemma pair_standard_borel_spaceUNIV:
assumes "standard_borel_space_UNIV M"
and "standard_borel_space_UNIV N"
shows "standard_borel_space_UNIV (M ⨂⇩M N)"
apply(rule standard_borel_space_UNIVI')
using assms pair_standard_borel_standard[of M N]
by(auto simp add: standard_borel_space_UNIV_def standard_borel_space_UNIV_axioms_def space_pair_measure)
locale pair_standard_borel = s1: standard_borel M + s2: standard_borel N
for M :: "'a measure" and N :: "'b measure"
begin
sublocale standard_borel "M ⨂⇩M N"
by(auto intro!: pair_standard_borel_standard)
end
locale pair_standard_borel_space_UNIV = s1: standard_borel_space_UNIV M + s2: standard_borel_space_UNIV N
for M :: "'a measure" and N :: "'b measure"
begin
sublocale pair_standard_borel M N
by standard
sublocale standard_borel_space_UNIV "M ⨂⇩M N"
by(auto intro!: pair_standard_borel_spaceUNIV
simp: s1.standard_borel_space_UNIV_axioms s2.standard_borel_space_UNIV_axioms)
end
text ‹$\mathbb{R}\times\mathbb{R}$ is a standard Borel space.›
interpretation real_real : pair_standard_borel_space_UNIV real_borel real_borel
by(auto intro!: pair_standard_borel_spaceUNIV simp: real.standard_borel_space_UNIV_axioms pair_standard_borel_space_UNIV_def)
subsection ‹ $\mathbb{N}\times\mathbb{R}$ ›
text ‹ $\mathbb{N}\times\mathbb{R}$ is a standard Borel space. ›
interpretation nat_real: pair_standard_borel_space_UNIV nat_borel real_borel
by(auto intro!: pair_standard_borel_spaceUNIV
simp: real.standard_borel_space_UNIV_axioms nat.standard_borel_space_UNIV_axioms pair_standard_borel_space_UNIV_def)
end