mathlib3 documentation

number_theory.liouville.liouville_with

Liouville numbers with a given exponent #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 liouville_with any real exponent, see forall_liouville_with_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 liouville_with.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 liouville_with and prove some basic facts about this predicate.

Tags #

Liouville number, irrational, irrationality exponent

def liouville_with (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 liouville_with any real exponent.

Equations

liouville_with p x = ∃ (C : ℝ), ∃ᶠ (n : ℕ) in filter.at_top , ∃ (m : ℤ), x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p

theorem liouville_with_one (x : ℝ) :

liouville_with 1 x

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

theorem liouville_with.exists_pos {p x : ℝ} (h : liouville_with p x) :

∃ (C : ℝ) (h₀ : 0 < C), ∃ᶠ (n : ℕ) in filter.at_top , 1 ≤ n ∧ ∃ (m : ℤ), x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p

The constant C provided by the definition of liouville_with 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 liouville_with.mono {p q x : ℝ} (h : liouville_with p x) (hle : q ≤ p) :

liouville_with q x

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

theorem liouville_with.frequently_lt_rpow_neg {p q x : ℝ} (h : liouville_with p x) (hlt : q < p) :

∃ᶠ (n : ℕ) in filter.at_top , ∃ (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 liouville_with.mul_rat {p x : ℝ} {r : ℚ} (h : liouville_with p x) (hr : r ≠ 0) :

liouville_with p (x * ↑r)

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

theorem liouville_with.mul_rat_iff {p x : ℝ} {r : ℚ} (hr : r ≠ 0) :

liouville_with p (x * ↑r) ↔ liouville_with 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 liouville_with.rat_mul_iff {p x : ℝ} {r : ℚ} (hr : r ≠ 0) :

liouville_with p (↑r * x) ↔ liouville_with 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 liouville_with.rat_mul {p x : ℝ} {r : ℚ} (h : liouville_with p x) (hr : r ≠ 0) :

liouville_with p (↑r * x)

theorem liouville_with.mul_int_iff {p x : ℝ} {m : ℤ} (hm : m ≠ 0) :

liouville_with p (x * ↑m) ↔ liouville_with p x

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

liouville_with p (x * ↑m)

theorem liouville_with.int_mul_iff {p x : ℝ} {m : ℤ} (hm : m ≠ 0) :

liouville_with p (↑m * x) ↔ liouville_with p x

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

liouville_with p (↑m * x)

theorem liouville_with.mul_nat_iff {p x : ℝ} {n : ℕ} (hn : n ≠ 0) :

liouville_with p (x * ↑n) ↔ liouville_with p x

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

liouville_with p (x * ↑n)

theorem liouville_with.nat_mul_iff {p x : ℝ} {n : ℕ} (hn : n ≠ 0) :

liouville_with p (↑n * x) ↔ liouville_with p x

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

liouville_with p (↑n * x)

theorem liouville_with.add_rat {p x : ℝ} (h : liouville_with p x) (r : ℚ) :

liouville_with p (x + ↑r)

@[simp]

theorem liouville_with.add_rat_iff {p x : ℝ} {r : ℚ} :

liouville_with p (x + ↑r) ↔ liouville_with p x

@[simp]

theorem liouville_with.rat_add_iff {p x : ℝ} {r : ℚ} :

liouville_with p (↑r + x) ↔ liouville_with p x

theorem liouville_with.rat_add {p x : ℝ} (h : liouville_with p x) (r : ℚ) :

liouville_with p (↑r + x)

@[simp]

theorem liouville_with.add_int_iff {p x : ℝ} {m : ℤ} :

liouville_with p (x + ↑m) ↔ liouville_with p x

@[simp]

theorem liouville_with.int_add_iff {p x : ℝ} {m : ℤ} :

liouville_with p (↑m + x) ↔ liouville_with p x

@[simp]

theorem liouville_with.add_nat_iff {p x : ℝ} {n : ℕ} :

liouville_with p (x + ↑n) ↔ liouville_with p x

@[simp]

theorem liouville_with.nat_add_iff {p x : ℝ} {n : ℕ} :

liouville_with p (↑n + x) ↔ liouville_with p x

theorem liouville_with.add_int {p x : ℝ} (h : liouville_with p x) (m : ℤ) :

liouville_with p (x + ↑m)

theorem liouville_with.int_add {p x : ℝ} (h : liouville_with p x) (m : ℤ) :

liouville_with p (↑m + x)

theorem liouville_with.add_nat {p x : ℝ} (h : liouville_with p x) (n : ℕ) :

liouville_with p (x + ↑n)

theorem liouville_with.nat_add {p x : ℝ} (h : liouville_with p x) (n : ℕ) :

liouville_with p (↑n + x)

@[protected]

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

liouville_with p (-x)

@[simp]

theorem liouville_with.neg_iff {p x : ℝ} :

liouville_with p (-x) ↔ liouville_with p x

@[simp]

theorem liouville_with.sub_rat_iff {p x : ℝ} {r : ℚ} :

liouville_with p (x - ↑r) ↔ liouville_with p x

theorem liouville_with.sub_rat {p x : ℝ} (h : liouville_with p x) (r : ℚ) :

liouville_with p (x - ↑r)

@[simp]

theorem liouville_with.sub_int_iff {p x : ℝ} {m : ℤ} :

liouville_with p (x - ↑m) ↔ liouville_with p x

theorem liouville_with.sub_int {p x : ℝ} (h : liouville_with p x) (m : ℤ) :

liouville_with p (x - ↑m)

@[simp]

theorem liouville_with.sub_nat_iff {p x : ℝ} {n : ℕ} :

liouville_with p (x - ↑n) ↔ liouville_with p x

theorem liouville_with.sub_nat {p x : ℝ} (h : liouville_with p x) (n : ℕ) :

liouville_with p (x - ↑n)

@[simp]

theorem liouville_with.rat_sub_iff {p x : ℝ} {r : ℚ} :

liouville_with p (↑r - x) ↔ liouville_with p x

theorem liouville_with.rat_sub {p x : ℝ} (h : liouville_with p x) (r : ℚ) :

liouville_with p (↑r - x)

@[simp]

theorem liouville_with.int_sub_iff {p x : ℝ} {m : ℤ} :

liouville_with p (↑m - x) ↔ liouville_with p x

theorem liouville_with.int_sub {p x : ℝ} (h : liouville_with p x) (m : ℤ) :

liouville_with p (↑m - x)

@[simp]

theorem liouville_with.nat_sub_iff {p x : ℝ} {n : ℕ} :

liouville_with p (↑n - x) ↔ liouville_with p x

theorem liouville_with.nat_sub {p x : ℝ} (h : liouville_with p x) (n : ℕ) :

liouville_with p (↑n - x)

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

@[protected]

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

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.at_top , ∃ (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.

@[protected]

theorem liouville.liouville_with {x : ℝ} (hx : liouville x) (p : ℝ) :

liouville_with p x

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

theorem forall_liouville_with_iff {x : ℝ} :

(∀ (p : ℝ), liouville_with p x) ↔ liouville x

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