# Documentation

Mathlib.NumberTheory.Liouville.LiouvilleNumber

# 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}$.

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.

Instances For

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!}}.$$

Instances For

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!}}.$$

Instances For

theorem LiouvilleNumber.summable {m : } (hm : 1 < m) :
Summable fun i => 1 /
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 : ) :
theorem LiouvilleNumber.partialSum_add_remainder {m : } (hm : 1 < m) (k : ) :

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) :
< (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 / () ^ n
theorem LiouvilleNumber.remainder_lt (n : ) {m : } (m2 : 2 m) :
< 1 / () ^ 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, = p / ↑()

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) :
theorem transcendental_liouvilleNumber {m : } (hm : 2 m) :