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.

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

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

      Equations
      Instances For

        We start with simple observations.

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

        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 ^ (n + 1).factorial)

        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 ^ (n + 1).factorial) 1 / (m ^ n.factorial) ^ n
        theorem LiouvilleNumber.remainder_lt (n : ) {m : } (m2 : 2 m) :
        LiouvilleNumber.remainder m n < 1 / (m ^ n.factorial) ^ 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 ^ k.factorial)

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