Theory Liouville_Numbers
theory Liouville_Numbers
imports
Complex_Main
"HOL-Computational_Algebra.Polynomial"
Liouville_Numbers_Misc
begin
text ‹
A Liouville number is a real number that can be approximated well -- but not perfectly --
by a sequence of rational numbers. ``Well``, in this context, means that the error of the
$n$-th rational in the sequence is bounded by the $n$-th power of its denominator.
Our approach will be the following:
\begin{itemize}
\item Liouville numbers cannot be rational.
\item Any irrational algebraic number cannot be approximated in the Liouville sense
\item Therefore, all Liouville numbers are transcendental.
\item The standard construction fulfils all the properties of Liouville numbers.
\end{itemize}
›
subsection ‹Definition of Liouville numbers›
text ‹
The following definitions and proofs are largely adapted from those in the Wikipedia
article on Liouville numbers.~\<^cite>‹"wikipedia"›
›
text ‹
A Liouville number is a real number that can be approximated well -- but not perfectly --
by a sequence of rational numbers. The error of the $n$-th term $\frac{p_n}{q_n}$ is at most
$q_n^{-n}$, where $p_n\in\isasymint$ and $q_n \in\isasymint_{\geq 2}$.
We will say that such a number can be approximated in the Liouville sense.
›
locale liouville =
fixes x :: real and p q :: "nat ⇒ int"
assumes approx_int_pos: "abs (x - p n / q n) > 0"
and denom_gt_1: "q n > 1"
and approx_int: "abs (x - p n / q n) < 1 / of_int (q n) ^ n"
text ‹
First, we show that any Liouville number is irrational.
›
lemma (in liouville) irrational: "x ∉ ℚ"
proof
assume "x ∈ ℚ"
then obtain c d :: int where d: "x = of_int c / of_int d" "d > 0"
by (elim Rats_cases') simp
define n where "n = Suc (nat ⌈log 2 d⌉)"
note q_gt_1 = denom_gt_1[of n]
have neq: "c * q n ≠ d * p n"
proof
assume "c * q n = d * p n"
hence "of_int (c * q n) = of_int (d * p n)" by (simp only: )
with approx_int_pos[of n] d q_gt_1 show False by (auto simp: field_simps)
qed
hence abs_pos: "0 < abs (c * q n - d * p n)" by simp
from q_gt_1 d have "of_int d = 2 powr log 2 d" by (subst powr_log_cancel) simp_all
also from d have "log 2 (of_int d) ≥ log 2 1" by (subst log_le_cancel_iff) simp_all
hence "2 powr log 2 d ≤ 2 powr of_nat (nat ⌈log 2 d⌉)"
by (intro powr_mono) simp_all
also have "… = of_int (2 ^ nat ⌈log 2 d⌉)"
by (subst powr_realpow) simp_all
finally have "d ≤ 2 ^ nat ⌈log 2 (of_int d)⌉"
by (subst (asm) of_int_le_iff)
also have "… * q n ≤ q n ^ Suc (nat ⌈log 2 (of_int d)⌉)"
by (subst power_Suc, subst mult.commute, intro mult_left_mono power_mono,
insert q_gt_1) simp_all
also from q_gt_1 have "… = q n ^ n" by (simp add: n_def)
finally have "1 / of_int (q n ^ n) ≤ 1 / real_of_int (d * q n)" using q_gt_1 d
by (intro divide_left_mono Rings.mult_pos_pos of_int_pos, subst of_int_le_iff) simp_all
also have "… ≤ of_int (abs (c * q n - d * p n)) / real_of_int (d * q n)" using q_gt_1 d abs_pos
by (intro divide_right_mono) (linarith, simp)
also have "… = abs (x - of_int (p n) / of_int (q n))" using q_gt_1 d(2)
by (simp_all add: divide_simps d(1) mult_ac)
finally show False using approx_int[of n] by simp
qed
text ‹
Next, any irrational algebraic number cannot be approximated with rational
numbers in the Liouville sense.
›
lemma liouville_irrational_algebraic:
fixes x :: real
assumes irrationsl: "x ∉ ℚ" and "algebraic x"
obtains c :: real and n :: nat
where "c > 0" and "⋀(p::int) (q::int). q > 0 ⟹ abs (x - p / q) > c / of_int q ^ n"
proof -
from ‹algebraic x› obtain p where p: "⋀i. coeff p i ∈ ℤ" "p ≠ 0" "poly p x = 0"
by (elim algebraicE) blast
define n where "n = degree p"
let ?f = "λt. ¦poly (pderiv p) t¦"
define M where "M = (SUP t∈{x-1..x+1}. ?f t)"
define roots where "roots = {x. poly p x = 0} - {x}"
define A_set where "A_set = {1, 1/M} ∪ {abs (x' - x) |x'. x' ∈ roots}"
define A' where "A' = Min A_set"
define A where "A = A' / 2"
have "∃s∈{x-1..x+1}. ∀y∈{x-1..x+1}. ?f s ≥ ?f y"
by (intro continuous_attains_sup) (auto intro!: continuous_intros)
hence bdd: "bdd_above (?f ` {x-1..x+1})" by auto
have M_pos: "M > 0"
proof -
from p have "pderiv p ≠ 0" by (auto dest!: pderiv_iszero)
hence "finite {x. poly (pderiv p) x = 0}" using poly_roots_finite by blast
moreover have "¬finite {x-1..x+1}" by (simp add: infinite_Icc)
ultimately have "¬finite ({x-1..x+1} - {x. poly (pderiv p) x = 0})" by simp
hence "{x-1..x+1} - {x. poly (pderiv p) x = 0} ≠ {}" by (intro notI) simp
then obtain t where t: "t ∈ {x-1..x+1}" and "poly (pderiv p) t ≠ 0" by blast
hence "0 < ?f t" by simp
also from t and bdd have "… ≤ M" unfolding M_def by (rule cSUP_upper)
finally show "M > 0" .
qed
have M_sup: "?f t ≤ M" if "t ∈ {x-1..x+1}" for t
proof -
from that and bdd show "?f t ≤ M"
unfolding M_def by (rule cSUP_upper)
qed
from p poly_roots_finite[of p] have "finite A_set"
unfolding A_set_def roots_def by simp
have "x ∉ roots" unfolding roots_def by auto
hence "A' > 0" using Min_gr_iff[OF ‹finite A_set›, folded A'_def, of 0]
by (auto simp: A_set_def M_pos)
hence A_pos: "A > 0" by (simp add: A_def)
from ‹A' > 0› have "A < A'" by (simp add: A_def)
moreover from Min_le[OF ‹finite A_set›, folded A'_def]
have "A' ≤ 1" "A' ≤ 1/M" "⋀x'. x' ≠ x ⟹ poly p x' = 0 ⟹ A' ≤ abs (x' - x)"
unfolding A_set_def roots_def by auto
ultimately have A_less: "A < 1" "A < 1/M" "⋀x'. x' ≠ x ⟹ poly p x' = 0 ⟹ A < abs (x' - x)"
by fastforce+
have "∀(a::int) (b :: int). b > 0 ⟶ ¦x - of_int a / of_int b¦ > A / of_int b ^ n"
proof (intro allI impI, rule ccontr)
fix a b :: int
assume b: "b > 0" and "¬(A / of_int b ^ n < ¦x - of_int a / of_int b¦)"
hence ab: "abs (x - of_int a / of_int b) ≤ A / of_int b ^ n" by simp
also from A_pos b have "A / of_int b ^ n ≤ A / 1"
by (intro divide_left_mono) simp_all
finally have ab': "abs (x - a / b) ≤ A" by simp
also have "… ≤ 1" using A_less by simp
finally have ab'': "a / b ∈ {x-1..x+1}" by auto
have no_root: "poly p (a / b) ≠ 0"
proof
assume "poly p (a / b) = 0"
moreover from ‹x ∉ ℚ› have "x ≠ a / b" by auto
ultimately have "A < abs (a / b - x)" using A_less(3) by simp
with ab' show False by simp
qed
have "∃x0∈{x-1..x+1}. poly p (a / b) - poly p x = (a / b - x) * poly (pderiv p) x0"
using ab'' by (intro poly_MVT') (auto simp: min_def max_def)
with p obtain x0 :: real where x0:
"x0 ∈ {x-1..x+1}" "poly p (a / b) = (a / b - x) * poly (pderiv p) x0" by auto
from x0(2) no_root have deriv_pos: "poly (pderiv p) x0 ≠ 0" by auto
from b p no_root have p_ab: "abs (poly p (a / b)) ≥ 1 / of_int b ^ n"
unfolding n_def by (intro int_poly_rat_no_root_ge)
note ab
also from A_less b have "A / of_int b ^ n < (1/M) / of_int b ^ n"
by (intro divide_strict_right_mono) simp_all
also have "… = (1 / b ^ n) / M" by simp
also from M_pos ab p_ab have "… ≤ abs (poly p (a / b)) / M"
by (intro divide_right_mono) simp_all
also from deriv_pos M_pos x0(1)
have "… ≤ abs (poly p (a / b)) / abs (poly (pderiv p) x0)"
by (intro divide_left_mono M_sup) simp_all
also have "¦poly p (a / b)¦ = ¦a / b - x¦ * ¦poly (pderiv p) x0¦"
by (subst x0(2)) (simp add: abs_mult)
with deriv_pos have "¦poly p (a / b)¦ / ¦poly (pderiv p) x0¦ = ¦x - a / b¦"
by (subst nonzero_divide_eq_eq) simp_all
finally show False by simp
qed
with A_pos show ?thesis using that[of A n] by blast
qed
text ‹
Since Liouville numbers are irrational, but can be approximated well by rational
numbers in the Liouville sense, they must be transcendental.
›
lemma (in liouville) transcendental: "¬algebraic x"
proof
assume "algebraic x"
from liouville_irrational_algebraic[OF irrational this]
obtain c n where cn:
"c > 0" "⋀p q. q > 0 ⟹ c / real_of_int q ^ n < ¦x - real_of_int p / real_of_int q¦"
by auto
define r where "r = nat ⌈log 2 (1 / c)⌉"
define m where "m = n + r"
from cn(1) have "(1/c) = 2 powr log 2 (1/c)" by (subst powr_log_cancel) simp_all
also have "log 2 (1/c) ≤ of_nat (nat ⌈log 2 (1/c)⌉)" by linarith
hence "2 powr log 2 (1/c) ≤ 2 powr …" by (intro powr_mono) simp_all
also have "… = 2 ^ r" unfolding r_def by (simp add: powr_realpow)
finally have "1 / (2^r) ≤ c" using cn(1) by (simp add: field_simps)
have "abs (x - p m / q m) < 1 / of_int (q m) ^ m" by (rule approx_int)
also have "… = (1 / of_int (q m) ^ r) * (1 / real_of_int (q m) ^ n)"
by (simp add: m_def power_add)
also from denom_gt_1[of m] have "1 / real_of_int (q m) ^ r ≤ 1 / 2 ^ r"
by (intro divide_left_mono power_mono) simp_all
also have "… ≤ c" by fact
finally have "abs (x - p m / q m) < c / of_int (q m) ^ n"
using denom_gt_1[of m] by - (simp_all add: divide_right_mono)
with cn(2)[of "q m" "p m"] denom_gt_1[of m] show False by simp
qed
subsection ‹Standard construction for Liouville numbers›
text ‹
We now define the standard construction for Liouville numbers.
›
definition standard_liouville :: "(nat ⇒ int) ⇒ int ⇒ real" where
"standard_liouville p q = (∑k. p k / of_int q ^ fact (Suc k))"
lemma standard_liouville_summable:
fixes p :: "nat ⇒ int" and q :: int
assumes "q > 1" "range p ⊆ {0..<q}"
shows "summable (λk. p k / of_int q ^ fact (Suc k))"
proof (rule summable_comparison_test')
from assms(1) show "summable (λn. (1 / q) ^ n)"
by (intro summable_geometric) simp_all
next
fix n :: nat
from assms have "p n ∈ {0..<q}" by blast
with assms(1) have "norm (p n / of_int q ^ fact (Suc n)) ≤
q / of_int q ^ (fact (Suc n))" by (auto simp: field_simps)
also from assms(1) have "… = 1 / of_int q ^ (fact (Suc n) - 1)"
by (subst power_diff) (auto simp del: fact_Suc)
also have "Suc n ≤ fact (Suc n)" by (rule fact_ge_self)
with assms(1) have "1 / real_of_int q ^ (fact (Suc n) - 1) ≤ 1 / of_int q ^ n"
by (intro divide_left_mono power_increasing)
(auto simp del: fact_Suc simp add: algebra_simps)
finally show "norm (p n / of_int q ^ fact (Suc n)) ≤ (1 / q) ^ n"
by (simp add: power_divide)
qed
lemma standard_liouville_sums:
assumes "q > 1" "range p ⊆ {0..<q}"
shows "(λk. p k / of_int q ^ fact (Suc k)) sums standard_liouville p q"
using standard_liouville_summable[OF assms] unfolding standard_liouville_def
by (simp add: summable_sums)
text ‹
Now we prove that the standard construction indeed yields Liouville numbers.
›
lemma standard_liouville_is_liouville:
assumes "q > 1" "range p ⊆ {0..<q}" "frequently (λn. p n ≠ 0) sequentially"
defines "b ≡ λn. q ^ fact (Suc n)"
defines "a ≡ λn. (∑k≤n. p k * q ^ (fact (Suc n) - fact (Suc k)))"
shows "liouville (standard_liouville p q) a b"
proof
fix n :: nat
from assms(1) have "1 < q ^ 1" by simp
also from assms(1) have "… ≤ b n" unfolding b_def
by (intro power_increasing) (simp_all del: fact_Suc)
finally show "b n > 1" .
note summable = standard_liouville_summable[OF assms(1,2)]
let ?S = "∑k. p (k + n + 1) / of_int q ^ (fact (Suc (k + n + 1)))"
let ?C = "(q - 1) / of_int q ^ (fact (n+2))"
have "a n / b n = (∑k≤n. p k * (of_int q ^ (fact (n+1) - fact (k+1)) / of_int q ^ (fact (n+1))))"
by (simp add: a_def b_def sum_divide_distrib of_int_sum)
also have "… = (∑k≤n. p k / of_int q ^ (fact (Suc k)))"
by (intro sum.cong refl, subst inverse_divide [symmetric], subst power_diff [symmetric])
(insert assms(1), simp_all add: divide_simps fact_mono_nat del: fact_Suc)
also have "standard_liouville p q - … = ?S" unfolding standard_liouville_def
by (subst diff_eq_eq) (intro suminf_split_initial_segment' summable)
finally have "abs (standard_liouville p q - a n / b n) = abs ?S" by (simp only: )
moreover from assms have "?S ≥ 0"
by (intro suminf_nonneg allI divide_nonneg_pos summable_ignore_initial_segment summable) force+
ultimately have eq: "abs (standard_liouville p q - a n / b n) = ?S" by simp
also have "?S ≤ (∑k. ?C * (1 / q) ^ k)"
proof (intro suminf_le allI summable_ignore_initial_segment summable)
from assms show "summable (λk. ?C * (1 / q) ^ k)"
by (intro summable_mult summable_geometric) simp_all
next
fix k :: nat
from assms have "p (k + n + 1) ≤ q - 1" by force
with ‹q > 1› have "p (k + n + 1) / of_int q ^ fact (Suc (k + n + 1)) ≤
(q - 1) / of_int q ^ (fact (Suc (k + n + 1)))"
by (intro divide_right_mono) (simp_all del: fact_Suc)
also from ‹q > 1› have "… ≤ (q - 1) / of_int q ^ (fact (n+2) + k)"
using fact_ineq[of "n+2" k]
by (intro divide_left_mono power_increasing) (simp_all add: add_ac)
also have "… = ?C * (1 / q) ^ k"
by (simp add: field_simps power_add del: fact_Suc)
finally show "p (k + n + 1) / of_int q ^ fact (Suc (k + n + 1)) ≤ …" .
qed
also from assms have "… = ?C * (∑k. (1 / q) ^ k)"
by (intro suminf_mult summable_geometric) simp_all
also from assms have "(∑k. (1 / q) ^ k) = 1 / (1 - 1 / q)"
by (intro suminf_geometric) simp_all
also from assms(1) have "?C * … = of_int q ^ 1 / of_int q ^ fact (n + 2)"
by (simp add: field_simps)
also from assms(1) have "… ≤ of_int q ^ fact (n + 1) / of_int q ^ fact (n + 2)"
by (intro divide_right_mono power_increasing) (simp_all add: field_simps del: fact_Suc)
also from assms(1) have "… = 1 / (of_int q ^ (fact (n + 2) - fact (n + 1)))"
by (subst power_diff) simp_all
also have "fact (n + 2) - fact (n + 1) = (n + 1) * fact (n + 1)" by (simp add: algebra_simps)
also from assms(1) have "1 / (of_int q ^ …) < 1 / (real_of_int q ^ (fact (n + 1) * n))"
by (intro divide_strict_left_mono power_increasing mult_right_mono) simp_all
also have "… = 1 / of_int (b n) ^ n"
by (simp add: power_mult b_def power_divide del: fact_Suc)
finally show "¦standard_liouville p q - a n / b n¦ < 1 / of_int (b n) ^ n" .
from assms(3) obtain k where k: "k ≥ n + 1" "p k ≠ 0"
by (auto simp: frequently_def eventually_at_top_linorder)
define k' where "k' = k - n - 1"
from assms k have "p k ≥ 0" by force
with k assms have k': "p (k' + n + 1) > 0" unfolding k'_def by force
with assms(1,2) have "?S > 0"
by (intro suminf_pos2[of _ k'] summable_ignore_initial_segment summable)
(force intro!: divide_pos_pos divide_nonneg_pos)+
with eq show "¦standard_liouville p q - a n / b n¦ > 0" by (simp only: )
qed
text ‹
We can now show our main result: any standard Liouville number is transcendental.
›
theorem transcendental_standard_liouville:
assumes "q > 1" "range p ⊆ {0..<q}" "frequently (λk. p k ≠ 0) sequentially"
shows "¬algebraic (standard_liouville p q)"
proof -
from assms interpret
liouville "standard_liouville p q"
"λn. (∑k≤n. p k * q ^ (fact (Suc n) - fact (Suc k)))"
"λn. q ^ fact (Suc n)"
by (rule standard_liouville_is_liouville)
from transcendental show ?thesis .
qed
text ‹
In particular: The the standard construction for constant sequences, such as the
``classic'' Liouville constant $\sum_{n=1}^\infty 10^{-n!} = 0.11000100\ldots$,
are transcendental.
This shows that Liouville numbers exists and therefore gives a concrete and
elementary proof that transcendental numbers exist.
›
corollary transcendental_standard_standard_liouville:
"a ∈ {0<..<b} ⟹ ¬algebraic (standard_liouville (λ_. int a) (int b))"
by (intro transcendental_standard_liouville) auto
corollary transcendental_liouville_constant:
"¬algebraic (standard_liouville (λ_. 1) 10)"
by (intro transcendental_standard_liouville) auto
end