# mathlibdocumentation

number_theory.liouville.liouville_constant

# 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 liouville.is_transcendental.

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

noncomputable def liouville.liouville_number (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
noncomputable def liouville.liouville_number_initial_terms (m : ) (k : ) :

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

Equations
noncomputable def liouville.liouville_number_tail (m : ) (k : ) :

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

Equations
theorem liouville.liouville_number_tail_pos {m : } (hm : 1 < m) (k : ) :

Split the sum definining a Liouville number into the first k term and the rest.

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

theorem liouville.tsum_one_div_pow_factorial_lt (n : ) {m : } (m1 : 1 < m) :
∑' (i : ), 1 / m ^ (i + (n + 1))! < (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!)

Partial inequality, works with m ∈ ℝ satisfying 1 < m.

theorem liouville.aux_calc (n : ) {m : } (hm : 2 m) :
(1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) 1 / (m ^ n!) ^ n

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

theorem liouville.liouville_number_rat_initial_terms {m : } (hm : 0 < m) (k : ) :
∃ (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.is_liouville {m : } (hm : 2 m) :
theorem liouville.is_transcendental {m : } (hm : 2 m) :