Liouville's theorem #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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|.
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
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
This lemma collects the properties used in the proof of
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
ε is small,
M is a bound on the Lipschitz constant of
the degree of the polynomial