The irrationality exponent

This file defines the irrationality exponent of a real number as the supremum of the exponents for which it satisfies Mathlib's LiouvilleWith predicate. It establishes the order-theoretic API of this definition, identifies infinite irrationality exponent with the Liouville property, computes the exponent of rational numbers, and records its invariance under rational Möbius transformations ξ ↦ (a ξ + b) / (c ξ + d) with a d - b c ≠ 0 (irrationalityExponent_mul_add_div_mul_add). The new ingredient beyond Mathlib's affine API for LiouvilleWith is inversion, LiouvilleWith.inv; the general transformation is a composition of affine maps and one inversion.

It then relates the exponent to approximation by reduced fractions: irrationalityExponent ξ is the supremum of the p for which infinitely many r : ℚ satisfy |ξ - r| < r.den ^ (-p) (irrationalityExponent_eq_iSup_infinite). Dirichlet's approximation theorem makes every irrational number a Liouville number with exponent two, so the exponent is at least two exactly on the irrational numbers (two_le_irrationalityExponent_iff), and Mathlib's measure estimate for LiouvilleWith gives exponent two for almost every real number (ae_irrationalityExponent_eq_two).

The definition follows Sondow, Irrationality measures, irrationality bases, and a theorem of Jarnik, Definition 2. The invariance under rational Möbius transformations is classical; see Bugeaud, Approximation by Algebraic Numbers, Cambridge Tracts in Mathematics 160 (2004).

noncomputable def TauCeti.irrationalityExponent (ξ : ℝ) : ENNReal

The irrationality exponent of ξ is the supremum of the real exponents p for which LiouvilleWith p ξ holds.

theorem TauCeti.irrationalityExponent_def (ξ : ℝ) : irrationalityExponent ξ = ⨆ (p : ℝ), ⨆ (_ : LiouvilleWith p ξ), ENNReal.ofReal p

The irrationality exponent is the supremum of ENNReal.ofReal p over the exponents p for which LiouvilleWith p ξ holds.

theorem TauCeti.le_irrationalityExponent_of_liouvilleWith {p ξ : ℝ} (h : LiouvilleWith p ξ) : ENNReal.ofReal p ≤ irrationalityExponent ξ

An exponent satisfying LiouvilleWith is at most the irrationality exponent.

theorem TauCeti.one_le_irrationalityExponent (ξ : ℝ) : 1 ≤ irrationalityExponent ξ

The irrationality exponent of every real number is at least one.

theorem TauCeti.liouvilleWith_of_lt_irrationalityExponent {p ξ : ℝ} (h : ENNReal.ofReal p < irrationalityExponent ξ) : LiouvilleWith p ξ

A real exponent strictly below the irrationality exponent satisfies LiouvilleWith.

theorem TauCeti.irrationalityExponent_le_iff {ξ : ℝ} {a : ENNReal} : irrationalityExponent ξ ≤ a ↔ ∀ (p : ℝ), LiouvilleWith p ξ → ENNReal.ofReal p ≤ a

The irrationality exponent is bounded by a exactly when every exponent satisfying LiouvilleWith maps below a.

theorem TauCeti.irrationalityExponent_eq_top_iff (ξ : ℝ) : irrationalityExponent ξ = ⊤ ↔ Liouville ξ

A real number has infinite irrationality exponent exactly when it is a Liouville number.

@[simp]

theorem TauCeti.irrationalityExponent_ratCast (q : ℚ) : irrationalityExponent ↑q = 1

The irrationality exponent of a rational number is one.

@[simp]

theorem TauCeti.irrationalityExponent_add_ratCast (ξ : ℝ) (q : ℚ) : irrationalityExponent (ξ + ↑q) = irrationalityExponent ξ

Adding a rational number does not change the irrationality exponent.

@[simp]

theorem TauCeti.irrationalityExponent_ratCast_mul (q : ℚ) (ξ : ℝ) (hq : q ≠ 0) : irrationalityExponent (↑q * ξ) = irrationalityExponent ξ

Multiplying by a nonzero rational number does not change the irrationality exponent.

@[simp]

theorem TauCeti.irrationalityExponent_neg (ξ : ℝ) : irrationalityExponent (-ξ) = irrationalityExponent ξ

Negation does not change the irrationality exponent.

theorem TauCeti.irrational_of_one_lt_irrationalityExponent {ξ : ℝ} (hξ : 1 < irrationalityExponent ξ) : Irrational ξ

An irrationality exponent strictly greater than one forces irrationality.

Inversion and Möbius transformations

theorem LiouvilleWith.inv {p x : ℝ} (h : LiouvilleWith p x) : LiouvilleWith p x⁻¹

The reciprocal of a Liouville number with exponent p is a Liouville number with exponent p.

@[simp]

theorem LiouvilleWith.inv_iff {p x : ℝ} : LiouvilleWith p x⁻¹ ↔ LiouvilleWith p x

A real number is a Liouville number with exponent p exactly when its reciprocal is.

theorem LiouvilleWith.mul_add_div_mul_add_iff {p x : ℝ} {a b c d : ℚ} (h : a * d - b * c ≠ 0) : LiouvilleWith p ((↑a * x + ↑b) / (↑c * x + ↑d)) ↔ LiouvilleWith p x

A real number is a Liouville number with exponent p exactly when its image under a Möbius transformation x ↦ (a x + b) / (c x + d) with rational coefficients and nonzero determinant a d - b c is.

@[simp]

theorem TauCeti.irrationalityExponent_inv (ξ : ℝ) : irrationalityExponent ξ⁻¹ = irrationalityExponent ξ

The irrationality exponent is invariant under inversion.

theorem TauCeti.irrationalityExponent_mul_add_div_mul_add (ξ : ℝ) {a b c d : ℚ} (h : a * d - b * c ≠ 0) : irrationalityExponent ((↑a * ξ + ↑b) / (↑c * ξ + ↑d)) = irrationalityExponent ξ

The irrationality exponent is invariant under a Möbius transformation ξ ↦ (a ξ + b) / (c ξ + d) with rational coefficients and nonzero determinant a d - b c.

Approximation by reduced fractions

theorem Set.Infinite.liouvilleWith_of_abs_sub_lt_rpow_neg {p ξ : ℝ} (h : {r : ℚ | |ξ - ↑r| < ↑r.den ^ (-p)}.Infinite) : LiouvilleWith p ξ

If infinitely many rational numbers r satisfy |ξ - r| < r.den ^ (-p), then ξ is a Liouville number with exponent p.

theorem TauCeti.exists_le_den_of_infinite {p ξ : ℝ} (hS : {r : ℚ | |ξ - ↑r| < ↑r.den ^ (-p)}.Infinite) (N : ℕ) : ∃ (r : ℚ), |ξ - ↑r| < ↑r.den ^ (-p) ∧ N ≤ r.den

An infinite set of rationals r with |ξ - r| < r.den ^ (-p) contains members of arbitrarily large denominator.

theorem LiouvilleWith.infinite_setOf_abs_sub_lt_rpow_neg {p q ξ : ℝ} (h : LiouvilleWith p ξ) (hq : q < p) : {r : ℚ | |ξ - ↑r| < ↑r.den ^ (-q)}.Infinite

A Liouville number with exponent p has, for every q < p, infinitely many rational approximations r with |ξ - r| < r.den ^ (-q).

theorem TauCeti.irrationalityExponent_eq_iSup_infinite (ξ : ℝ) : irrationalityExponent ξ = ⨆ (p : ℝ), ⨆ (_ : {r : ℚ | |ξ - ↑r| < ↑r.den ^ (-p)}.Infinite), ENNReal.ofReal p

The irrationality exponent of ξ is the supremum of the exponents p for which infinitely many rational numbers r satisfy |ξ - r| < r.den ^ (-p).

Irrational numbers and almost every real number

theorem Irrational.liouvilleWith_two {ξ : ℝ} (hξ : Irrational ξ) : LiouvilleWith 2 ξ

Every irrational number is a Liouville number with exponent 2, by Dirichlet's approximation theorem.

@[simp]

theorem TauCeti.two_le_irrationalityExponent_iff (ξ : ℝ) : 2 ≤ irrationalityExponent ξ ↔ Irrational ξ

A real number has irrationality exponent at least two exactly when it is irrational.

theorem TauCeti.irrationalityExponent_le_two_iff (ξ : ℝ) : irrationalityExponent ξ ≤ 2 ↔ ∀ p > 2, ¬LiouvilleWith p ξ

The irrationality exponent of ξ is at most two exactly when ξ is not a Liouville number with any exponent greater than two.

theorem TauCeti.ae_irrationalityExponent_eq_two : ∀ᵐ (ξ : ℝ), irrationalityExponent ξ = 2

Almost every real number has irrationality exponent two.