Liouville numbers with a given exponent

We say that a real number x is a Liouville number with exponent p : ℝ if there exists a real number C such that for infinitely many denominators n there exists a numerator m such that x ≠ m / n and |x - m / n| < C / n ^ p. A number is a Liouville number in the sense of Liouville if it is LiouvilleWith any real exponent, see forall_liouvilleWith_iff.

• If p ≤ 1, then this condition is trivial.

• If 1 < p ≤ 2, then this condition is equivalent to Irrational x. The forward implication does not require p ≤ 2 and is formalized as LiouvilleWith.irrational; the other implication follows from approximations by continued fractions and is not formalized yet.

• If p > 2, then this is a non-trivial condition on irrational numbers. In particular, Thue–Siegel–Roth theorem states that such numbers must be transcendental.

In this file we define the predicate LiouvilleWith and prove some basic facts about this predicate.

Tags

Liouville number, irrational, irrationality exponent

def LiouvilleWith (p : ℝ) (x : ℝ) : Prop

We say that a real number x is a Liouville number with exponent p : ℝ if there exists a real number C such that for infinitely many denominators n there exists a numerator m such that x ≠ m / n and |x - m / n| < C / n ^ p.

A number is a Liouville number in the sense of Liouville if it is LiouvilleWith any real exponent.

Equations

• LiouvilleWith p x = ∃ (C : ℝ), ∃ᶠ (n : ℕ) in Filter.atTop, ∃ (m : ℤ), x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p

theorem liouvilleWith_one (x : ℝ) : LiouvilleWith 1 x

For p = 1 (hence, for any p ≤ 1), the condition LiouvilleWith p x is trivial.

theorem LiouvilleWith.exists_pos {p : ℝ} {x : ℝ} (h : LiouvilleWith p x) : ∃ (C : ℝ) (_ : 0 < C), ∃ᶠ (n : ℕ) in Filter.atTop, 1 ≤ n ∧ ∃ (m : ℤ), x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p

The constant C provided by the definition of LiouvilleWith can be made positive. We also add 1 ≤ n to the list of assumptions about the denominator. While it is equivalent to the original statement, the case n = 0 breaks many arguments.

theorem LiouvilleWith.mono {p : ℝ} {q : ℝ} {x : ℝ} (h : LiouvilleWith p x) (hle : q ≤ p) : LiouvilleWith q x

If a number is Liouville with exponent p, then it is Liouville with any smaller exponent.

theorem LiouvilleWith.frequently_lt_rpow_neg {p : ℝ} {q : ℝ} {x : ℝ} (h : LiouvilleWith p x) (hlt : q < p) : ∃ᶠ (n : ℕ) in Filter.atTop, ∃ (m : ℤ), x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)

If x satisfies Liouville condition with exponent p and q < p, then x satisfies Liouville condition with exponent q and constant 1.

theorem LiouvilleWith.mul_rat {p : ℝ} {x : ℝ} {r : ℚ} (h : LiouvilleWith p x) (hr : r ≠ 0) : LiouvilleWith p (x * ↑r)

The product of a Liouville number and a nonzero rational number is again a Liouville number.

theorem LiouvilleWith.mul_rat_iff {p : ℝ} {x : ℝ} {r : ℚ} (hr : r ≠ 0) : LiouvilleWith p (x * ↑r) ↔ LiouvilleWith p x

The product x * r, r : ℚ, r ≠ 0, is a Liouville number with exponent p if and only if x satisfies the same condition.

theorem LiouvilleWith.rat_mul_iff {p : ℝ} {x : ℝ} {r : ℚ} (hr : r ≠ 0) : LiouvilleWith p (↑r * x) ↔ LiouvilleWith p x

The product r * x, r : ℚ, r ≠ 0, is a Liouville number with exponent p if and only if x satisfies the same condition.

theorem LiouvilleWith.rat_mul {p : ℝ} {x : ℝ} {r : ℚ} (h : LiouvilleWith p x) (hr : r ≠ 0) : LiouvilleWith p (↑r * x)

theorem LiouvilleWith.mul_int_iff {p : ℝ} {x : ℝ} {m : ℤ} (hm : m ≠ 0) : LiouvilleWith p (x * ↑m) ↔ LiouvilleWith p x

theorem LiouvilleWith.mul_int {p : ℝ} {x : ℝ} {m : ℤ} (h : LiouvilleWith p x) (hm : m ≠ 0) : LiouvilleWith p (x * ↑m)

theorem LiouvilleWith.int_mul_iff {p : ℝ} {x : ℝ} {m : ℤ} (hm : m ≠ 0) : LiouvilleWith p (↑m * x) ↔ LiouvilleWith p x

theorem LiouvilleWith.int_mul {p : ℝ} {x : ℝ} {m : ℤ} (h : LiouvilleWith p x) (hm : m ≠ 0) : LiouvilleWith p (↑m * x)

theorem LiouvilleWith.mul_nat_iff {p : ℝ} {x : ℝ} {n : ℕ} (hn : n ≠ 0) : LiouvilleWith p (x * ↑n) ↔ LiouvilleWith p x

theorem LiouvilleWith.mul_nat {p : ℝ} {x : ℝ} {n : ℕ} (h : LiouvilleWith p x) (hn : n ≠ 0) : LiouvilleWith p (x * ↑n)

theorem LiouvilleWith.nat_mul_iff {p : ℝ} {x : ℝ} {n : ℕ} (hn : n ≠ 0) : LiouvilleWith p (↑n * x) ↔ LiouvilleWith p x

theorem LiouvilleWith.nat_mul {p : ℝ} {x : ℝ} {n : ℕ} (h : LiouvilleWith p x) (hn : n ≠ 0) : LiouvilleWith p (↑n * x)

theorem LiouvilleWith.add_rat {p : ℝ} {x : ℝ} (h : LiouvilleWith p x) (r : ℚ) : LiouvilleWith p (x + ↑r)

@[simp]

theorem LiouvilleWith.add_rat_iff {p : ℝ} {x : ℝ} {r : ℚ} : LiouvilleWith p (x + ↑r) ↔ LiouvilleWith p x

@[simp]

theorem LiouvilleWith.rat_add_iff {p : ℝ} {x : ℝ} {r : ℚ} : LiouvilleWith p (↑r + x) ↔ LiouvilleWith p x

theorem LiouvilleWith.rat_add {p : ℝ} {x : ℝ} (h : LiouvilleWith p x) (r : ℚ) : LiouvilleWith p (↑r + x)

@[simp]

theorem LiouvilleWith.add_int_iff {p : ℝ} {x : ℝ} {m : ℤ} : LiouvilleWith p (x + ↑m) ↔ LiouvilleWith p x

@[simp]

theorem LiouvilleWith.int_add_iff {p : ℝ} {x : ℝ} {m : ℤ} : LiouvilleWith p (↑m + x) ↔ LiouvilleWith p x

@[simp]

theorem LiouvilleWith.add_nat_iff {p : ℝ} {x : ℝ} {n : ℕ} : LiouvilleWith p (x + ↑n) ↔ LiouvilleWith p x

@[simp]

theorem LiouvilleWith.nat_add_iff {p : ℝ} {x : ℝ} {n : ℕ} : LiouvilleWith p (↑n + x) ↔ LiouvilleWith p x

theorem LiouvilleWith.add_int {p : ℝ} {x : ℝ} (h : LiouvilleWith p x) (m : ℤ) : LiouvilleWith p (x + ↑m)

theorem LiouvilleWith.int_add {p : ℝ} {x : ℝ} (h : LiouvilleWith p x) (m : ℤ) : LiouvilleWith p (↑m + x)

theorem LiouvilleWith.add_nat {p : ℝ} {x : ℝ} (h : LiouvilleWith p x) (n : ℕ) : LiouvilleWith p (x + ↑n)

theorem LiouvilleWith.nat_add {p : ℝ} {x : ℝ} (h : LiouvilleWith p x) (n : ℕ) : LiouvilleWith p (↑n + x)

theorem LiouvilleWith.neg {p : ℝ} {x : ℝ} (h : LiouvilleWith p x) : LiouvilleWith p (-x)

@[simp]

theorem LiouvilleWith.neg_iff {p : ℝ} {x : ℝ} : LiouvilleWith p (-x) ↔ LiouvilleWith p x

@[simp]

theorem LiouvilleWith.sub_rat_iff {p : ℝ} {x : ℝ} {r : ℚ} : LiouvilleWith p (x - ↑r) ↔ LiouvilleWith p x

theorem LiouvilleWith.sub_rat {p : ℝ} {x : ℝ} (h : LiouvilleWith p x) (r : ℚ) : LiouvilleWith p (x - ↑r)

@[simp]

theorem LiouvilleWith.sub_int_iff {p : ℝ} {x : ℝ} {m : ℤ} : LiouvilleWith p (x - ↑m) ↔ LiouvilleWith p x

theorem LiouvilleWith.sub_int {p : ℝ} {x : ℝ} (h : LiouvilleWith p x) (m : ℤ) : LiouvilleWith p (x - ↑m)

@[simp]

theorem LiouvilleWith.sub_nat_iff {p : ℝ} {x : ℝ} {n : ℕ} : LiouvilleWith p (x - ↑n) ↔ LiouvilleWith p x

theorem LiouvilleWith.sub_nat {p : ℝ} {x : ℝ} (h : LiouvilleWith p x) (n : ℕ) : LiouvilleWith p (x - ↑n)

@[simp]

theorem LiouvilleWith.rat_sub_iff {p : ℝ} {x : ℝ} {r : ℚ} : LiouvilleWith p (↑r - x) ↔ LiouvilleWith p x

theorem LiouvilleWith.rat_sub {p : ℝ} {x : ℝ} (h : LiouvilleWith p x) (r : ℚ) : LiouvilleWith p (↑r - x)

@[simp]

theorem LiouvilleWith.int_sub_iff {p : ℝ} {x : ℝ} {m : ℤ} : LiouvilleWith p (↑m - x) ↔ LiouvilleWith p x

theorem LiouvilleWith.int_sub {p : ℝ} {x : ℝ} (h : LiouvilleWith p x) (m : ℤ) : LiouvilleWith p (↑m - x)

@[simp]

theorem LiouvilleWith.nat_sub_iff {p : ℝ} {x : ℝ} {n : ℕ} : LiouvilleWith p (↑n - x) ↔ LiouvilleWith p x

theorem LiouvilleWith.nat_sub {p : ℝ} {x : ℝ} (h : LiouvilleWith p x) (n : ℕ) : LiouvilleWith p (↑n - x)

theorem LiouvilleWith.ne_cast_int {p : ℝ} {x : ℝ} (h : LiouvilleWith p x) (hp : 1 < p) (m : ℤ) : x ≠ ↑m

theorem LiouvilleWith.irrational {p : ℝ} {x : ℝ} (h : LiouvilleWith p x) (hp : 1 < p) : Irrational x

A number satisfying the Liouville condition with exponent p > 1 is an irrational number.

theorem Liouville.frequently_exists_num {x : ℝ} (hx : Liouville x) (n : ℕ) : ∃ᶠ (b : ℕ) in Filter.atTop, ∃ (a : ℤ), x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n

If x is a Liouville number, then for any n, for infinitely many denominators b there exists a numerator a such that x ≠ a / b and |x - a / b| < 1 / b ^ n.

theorem Liouville.liouvilleWith {x : ℝ} (hx : Liouville x) (p : ℝ) : LiouvilleWith p x

A Liouville number is a Liouville number with any real exponent.

theorem forall_liouvilleWith_iff {x : ℝ} : (∀ (p : ℝ), LiouvilleWith p x) ↔ Liouville x

A number satisfies the Liouville condition with any exponent if and only if it is a Liouville number.