Rational approximation measured by height

The denominator and the naive height of a rational approximant give the same irrationality exponent. Near a fixed real number ξ, the numerator of m / n is bounded by a constant times n, so replacing n by max |m| n changes the approximation bound by only a constant.

TauCeti.liouvilleWith_iff_frequently_max makes this comparison without requiring reduced fractions. LiouvilleWith.infinite_setOf_abs_sub_lt_mulHeight₁_rpow_neg absorbs the constant by slightly decreasing the exponent. Real.le_irrationalityExponent_iff characterizes a lower bound on the irrationality exponent by infinitely many rational approximations measured using Height.mulHeight₁. The strict decrease in the exponent is essential: a supremum need not be attained, and a constant cannot in general be removed at the endpoint.

TauCeti.mul_max_abs_rpow_le_norm_sub_of_lt transfers a lower bound on ‖ξ - α‖ for rationals ξ in terms of Height.mulHeight₁ to a lower bound on the integer linear form x - α y when |x| < 2 (‖α‖ + 1) |y|.

References

• Y. Bugeaud, Approximation by Algebraic Numbers, Cambridge University Press (2004), Chapter 3.

The constant-absorption argument follows Mathlib's LiouvilleWith.frequently_lt_rpow_neg; the passage from denominator bounds to height bounds uses LiouvilleWith.infinite_setOf_abs_sub_lt_rpow_neg and the height comparison previously used in IsAlgebraic.not_liouvilleWith.

theorem TauCeti.liouvilleWith_iff_frequently_max {p ξ : ℝ} : LiouvilleWith p ξ ↔ ∃ C > 0, ∃ᶠ (n : ℕ) in Filter.atTop, 0 < n ∧ ∃ (m : ℤ), ξ ≠ ↑m / ↑n ∧ |ξ - ↑m / ↑n| < C / max |↑m| ↑n ^ p

In the Liouville condition, one may replace the denominator by max |m| n, even for fractions that are not reduced.

theorem TauCeti.mul_max_abs_rpow_le_norm_sub_of_lt {α : ℂ} {κ c₀ : ℝ} (hκ : 0 ≤ κ) (hc₀ : 0 ≤ c₀) (h : ∀ (ξ : ℚ), ↑ξ ≠ α → c₀ * Height.mulHeight₁ ξ ^ (-κ) ≤ ‖↑ξ - α‖) {x y : ℤ} (hxy : ↑x - α * ↑y ≠ 0) (hsmall : |↑x| < 2 * (‖α‖ + 1) * |↑y|) : c₀ / (2 * (‖α‖ + 1)) * max |↑x| |↑y| ^ (1 - κ) ≤ ‖↑x - α * ↑y‖

The case |x| < 2 (‖α‖ + 1) |y| of the linear-form bound: if every rational ξ ≠ α satisfies the rational approximation bound c₀ H(ξ) ^ (-κ) ≤ ‖ξ - α‖, then at integers x, y with |x| < 2 (‖α‖ + 1) |y|, x ≠ α y, the linear form satisfies ‖x - α y‖ ≥ c₀ / (2 (‖α‖ + 1)) max(|x|, |y|) ^ (1 - κ).

theorem LiouvilleWith.infinite_setOf_abs_sub_lt_mulHeight₁_rpow_neg {p q ξ : ℝ} (h : LiouvilleWith p ξ) (hqp : q < p) : {r : ℚ | |ξ - ↑r| < Height.mulHeight₁ r ^ (-q)}.Infinite

A Liouville number with exponent p has infinitely many rational approximations measured by their multiplicative height, for every exponent strictly smaller than p.

theorem Real.le_irrationalityExponent_iff (ξ : ℝ) {μ : ENNReal} : μ ≤ TauCeti.irrationalityExponent ξ ↔ ∀ (ν : ℝ), ENNReal.ofReal ν < μ → {r : ℚ | |ξ - ↑r| < Height.mulHeight₁ r ^ (-ν)}.Infinite

An extended nonnegative real μ is at most the irrationality exponent of ξ exactly when, for every real ν with ENNReal.ofReal ν < μ, infinitely many rational numbers approximate ξ within H(r) ^ (-ν). Here H is the rational height max |num r| (den r); the case μ = ⊤ characterizes Liouville numbers.

Boundary checks