Liouville constants

This file contains a construction of a family of Liouville numbers, indexed by a natural number $m$. The most important property is that they are examples of transcendental real numbers. This fact is recorded in transcendental_liouvilleNumber.

More precisely, for a real number $m$, Liouville's constant is $$ \sum_{i=0}^\infty\frac{1}{m^{i!}}. $$ The series converges only for $1 < m$. However, there is no restriction on $m$, since, if the series does not converge, then the sum of the series is defined to be zero.

We prove that, for $m \in \mathbb{N}$ satisfying $2 \le m$, Liouville's constant associated to $m$ is a transcendental number. Classically, the Liouville number for $m = 2$ is the one called ``Liouville's constant''.

Implementation notes

The indexing $m$ is eventually a natural number satisfying $2 ≤ m$. However, we prove the first few lemmas for $m \in \mathbb{R}$.

def liouvilleNumber (m : ℝ) : ℝ

For a real number m, Liouville's constant is $$ \sum_{i=0}^\infty\frac{1}{m^{i!}}. $$ The series converges only for 1 < m. However, there is no restriction on m, since, if the series does not converge, then the sum of the series is defined to be zero.

Equations

• liouvilleNumber m = ∑' (i : ℕ), 1 / m ^ Nat.factorial i

def LiouvilleNumber.partialSum (m : ℝ) (k : ℕ) : ℝ

LiouvilleNumber.partialSum is the sum of the first k + 1 terms of Liouville's constant, i.e. $$ \sum_{i=0}^k\frac{1}{m^{i!}}. $$

Equations

• LiouvilleNumber.partialSum m k = Finset.sum (Finset.range (k + 1)) fun (i : ℕ) => 1 / m ^ Nat.factorial i

def LiouvilleNumber.remainder (m : ℝ) (k : ℕ) : ℝ

LiouvilleNumber.remainder is the sum of the series of the terms in liouvilleNumber m starting from k+1, i.e $$ \sum_{i=k+1}^\infty\frac{1}{m^{i!}}. $$

Equations

• LiouvilleNumber.remainder m k = ∑' (i : ℕ), 1 / m ^ Nat.factorial (i + (k + 1))

We start with simple observations.

theorem LiouvilleNumber.summable {m : ℝ} (hm : 1 < m) : Summable fun (i : ℕ) => 1 / m ^ Nat.factorial i

theorem LiouvilleNumber.remainder_summable {m : ℝ} (hm : 1 < m) (k : ℕ) : Summable fun (i : ℕ) => 1 / m ^ Nat.factorial (i + (k + 1))

theorem LiouvilleNumber.remainder_pos {m : ℝ} (hm : 1 < m) (k : ℕ) : 0 < LiouvilleNumber.remainder m k

theorem LiouvilleNumber.partialSum_succ (m : ℝ) (n : ℕ) : LiouvilleNumber.partialSum m (n + 1) = LiouvilleNumber.partialSum m n + 1 / m ^ Nat.factorial (n + 1)

theorem LiouvilleNumber.partialSum_add_remainder {m : ℝ} (hm : 1 < m) (k : ℕ) : LiouvilleNumber.partialSum m k + LiouvilleNumber.remainder m k = liouvilleNumber m

Split the sum defining a Liouville number into the first k terms and the rest.

We now prove two useful inequalities, before collecting everything together.

theorem LiouvilleNumber.remainder_lt' (n : ℕ) {m : ℝ} (m1 : 1 < m) : LiouvilleNumber.remainder m n < (1 - 1 / m)⁻¹ * (1 / m ^ Nat.factorial (n + 1))

An upper estimate on the remainder. This estimate works with m ∈ ℝ satisfying 1 < m and is stronger than the estimate LiouvilleNumber.remainder_lt below. However, the latter estimate is more useful for the proof.

theorem LiouvilleNumber.aux_calc (n : ℕ) {m : ℝ} (hm : 2 ≤ m) : (1 - 1 / m)⁻¹ * (1 / m ^ Nat.factorial (n + 1)) ≤ 1 / (m ^ Nat.factorial n) ^ n

theorem LiouvilleNumber.remainder_lt (n : ℕ) {m : ℝ} (m2 : 2 ≤ m) : LiouvilleNumber.remainder m n < 1 / (m ^ Nat.factorial n) ^ n

An upper estimate on the remainder. This estimate works with m ∈ ℝ satisfying 2 ≤ m and is weaker than the estimate LiouvilleNumber.remainder_lt' above. However, this estimate is more useful for the proof.

Starting from here, we specialize to the case in which m is a natural number.

theorem LiouvilleNumber.partialSum_eq_rat {m : ℕ} (hm : 0 < m) (k : ℕ) : ∃ (p : ℕ), LiouvilleNumber.partialSum (↑m) k = ↑p / ↑(m ^ Nat.factorial k)

The sum of the k initial terms of the Liouville number to base m is a ratio of natural numbers where the denominator is m ^ k!.

theorem liouville_liouvilleNumber {m : ℕ} (hm : 2 ≤ m) : Liouville (liouvilleNumber ↑m)

theorem transcendental_liouvilleNumber {m : ℕ} (hm : 2 ≤ m) : Transcendental ℤ (liouvilleNumber ↑m)