# Liouville's theorem #

This file contains a proof of Liouville's theorem stating that all Liouville numbers are transcendental.

To obtain this result, there is first a proof that Liouville numbers are irrational and two technical lemmas. These lemmas exploit the fact that a polynomial with integer coefficients takes integer values at integers. When evaluating at a rational number, we can clear denominators and obtain precise inequalities that ultimately allow us to prove transcendence of Liouville numbers.

A Liouville number is a real number `x`

such that for every natural number `n`

, there exist
`a, b ∈ ℤ`

with `1 < b`

such that `0 < |x - a/b| < 1/bⁿ`

.
In the implementation, the condition `x ≠ a/b`

replaces the traditional equivalent `0 < |x - a/b|`

.

## Equations

## Instances For

Let `Z, N`

be types, let `R`

be a metric space, let `α : R`

be a point and let
`j : Z → N → R`

be a function. We aim to estimate how close we can get to `α`

, while staying
in the image of `j`

. The points `j z a`

of `R`

in the image of `j`

come with a "cost" equal to
`d a`

. As we get closer to `α`

while staying in the image of `j`

, we are interested in bounding
the quantity `d a * dist α (j z a)`

from below by a strictly positive amount `1 / A`

: the intuition
is that approximating well `α`

with the points in the image of `j`

should come at a high cost. The
hypotheses on the function `f : R → R`

provide us with sufficient conditions to ensure our goal.
The first hypothesis is that `f`

is Lipschitz at `α`

: this yields a bound on the distance.
The second hypothesis is specific to the Liouville argument and provides the missing bound
involving the cost function `d`

.

This lemma collects the properties used in the proof of `exists_pos_real_of_irrational_root`

.
It is stated in more general form than needed: in the intended application, `Z = ℤ`

, `N = ℕ`

,
`R = ℝ`

, `d a = (a + 1) ^ f.nat_degree`

, `j z a = z / (a + 1)`

, `f ∈ ℤ[x]`

, `α`

is an irrational
root of `f`

, `ε`

is small, `M`

is a bound on the Lipschitz constant of `f`

near `α`

, `n`

is
the degree of the polynomial `f`

.

**Liouville's Theorem**