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}$.
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.
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
- liouville.liouville_number_initial_terms m k = (finset.range (k + 1)).sum (λ (i : ℕ), 1 / m ^ i.factorial)
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!}}.
$$
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.
Starting from here, we specialize to the case in which m is a natural number.