mathlib documentation

number_theory.liouville.liouville_with

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 liouville_with any real exponent, see forall_liouville_with_iff.

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
theorem liouville_with_one (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) :

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) :

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) :

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) :

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) :
theorem liouville_with.mul_int_iff {p x : } {m : } (hm : m 0) :
theorem liouville_with.mul_int {p x : } {m : } (h : liouville_with p x) (hm : m 0) :
theorem liouville_with.int_mul_iff {p x : } {m : } (hm : m 0) :
theorem liouville_with.int_mul {p x : } {m : } (h : liouville_with p x) (hm : m 0) :
theorem liouville_with.mul_nat_iff {p x : } {n : } (hn : n 0) :
theorem liouville_with.mul_nat {p x : } {n : } (h : liouville_with p x) (hn : n 0) :
theorem liouville_with.nat_mul_iff {p x : } {n : } (hn : n 0) :
theorem liouville_with.nat_mul {p x : } {n : } (h : liouville_with p x) (hn : n 0) :
theorem liouville_with.add_rat {p x : } (h : liouville_with p x) (r : ) :
@[simp]
theorem liouville_with.add_rat_iff {p x : } {r : } :
@[simp]
theorem liouville_with.rat_add_iff {p x : } {r : } :
theorem liouville_with.rat_add {p x : } (h : liouville_with p x) (r : ) :
@[simp]
theorem liouville_with.add_int_iff {p x : } {m : } :
@[simp]
theorem liouville_with.int_add_iff {p x : } {m : } :
@[simp]
theorem liouville_with.add_nat_iff {p x : } {n : } :
@[simp]
theorem liouville_with.nat_add_iff {p x : } {n : } :
theorem liouville_with.add_int {p x : } (h : liouville_with p x) (m : ) :
theorem liouville_with.int_add {p x : } (h : liouville_with p x) (m : ) :
theorem liouville_with.add_nat {p x : } (h : liouville_with p x) (n : ) :
theorem liouville_with.nat_add {p x : } (h : liouville_with p x) (n : ) :
@[protected]
theorem liouville_with.neg {p x : } (h : liouville_with p x) :
@[simp]
@[simp]
theorem liouville_with.sub_rat_iff {p x : } {r : } :
theorem liouville_with.sub_rat {p x : } (h : liouville_with p x) (r : ) :
@[simp]
theorem liouville_with.sub_int_iff {p x : } {m : } :
theorem liouville_with.sub_int {p x : } (h : liouville_with p x) (m : ) :
@[simp]
theorem liouville_with.sub_nat_iff {p x : } {n : } :
theorem liouville_with.sub_nat {p x : } (h : liouville_with p x) (n : ) :
@[simp]
theorem liouville_with.rat_sub_iff {p x : } {r : } :
theorem liouville_with.rat_sub {p x : } (h : liouville_with p x) (r : ) :
@[simp]
theorem liouville_with.int_sub_iff {p x : } {m : } :
theorem liouville_with.int_sub {p x : } (h : liouville_with p x) (m : ) :
@[simp]
theorem liouville_with.nat_sub_iff {p x : } {n : } :
theorem liouville_with.nat_sub {p x : } (h : liouville_with p x) (n : ) :
theorem liouville_with.ne_cast_int {p x : } (h : liouville_with p x) (hp : 1 < p) (m : ) :
x 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 : ) :

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.