# Theory StandardBorel

(*  Title:   StandardBorel.thy
Author:  Michikazu Hirata, Tokyo Institute of Technology
*)

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

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

lemma f_inj':
"inj f"

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"
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"
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"
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"
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
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
next
case 3
then show ?thesis
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
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"
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"
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"
next
show "continuous_on (range arctan) (λx. x / pi + 1 / 2)"
qed
thus ?thesis
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)

(* S_n = a_0 + ... + a_n *)
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"
have "ur * 4 - (ur * 4 + lr * 4) / 2 = (1 / 2) ^ n'"
moreover have "(ur * 4 + lr * 4) / 2 - lr * 4 = (1 / 2) ^ n'"
ultimately show ?thesis
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
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"
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')"
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"
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"
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'"
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"

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]
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"
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
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)"

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)"
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
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)"
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"
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
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 "
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]
also have "... = ur"
using r01_binary_expansion_diff[of r n]
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)"

lemma biexp01_well_formedI:
assumes "⋀n. a n ∈ {0,1}"
and "⋀n. ∃m≥n. a m = 0"
shows "biexp01_well_formed a"

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]

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