The simultaneous Diophantine approximation exponent

For a finite family θ : ι → ℝ, this file defines its simultaneous approximation exponent as the supremum of the real numbers w for which infinitely many positive integers q admit integers pᵢ satisfying

|q θᵢ - pᵢ| ≤ q⁻ʷ

for every i. Using positive denominators instead of arbitrary nonzero integer first coordinates does not change the exponent: negating every coordinate makes the two formulations equivalent. Recording only denominators also does not change infinitude, since for fixed q the displayed bounds leave only finitely many choices for the integer vector.

The main results identify the one-dimensional exponent of an irrational real number with its irrationality exponent, up to the expected shift by one, show that a rational family and an empty family have infinite exponent, and show that forgetting coordinates can only increase the exponent. Dirichlet's theorem gives the lower bound 1 / n for a family of n real numbers (inv_card_le_simultaneousExponent).

References

• Y. Bugeaud, Exponents of Diophantine approximation, in Dynamics and Analytic Number Theory, London Math. Soc. Lecture Note Ser. 437, Cambridge Univ. Press (2016), §2, Definition 2.2. The exponent defined here is that simultaneous exponent, restated with positive denominators as explained above. The lower bound 1 / n is the simultaneous half of Theorem 2.5.

def TauCeti.simultaneousApproximationDenominators {ι : Type u_1} (θ : ι → ℝ) (w : ℝ) : Set ℕ

The positive denominators giving simultaneous approximations to θ with exponent w.

@[simp]

theorem TauCeti.mem_simultaneousApproximationDenominators {ι : Type u_1} {θ : ι → ℝ} {w : ℝ} {q : ℕ} : q ∈ simultaneousApproximationDenominators θ w ↔ 0 < q ∧ ∃ (p : ι → ℤ), ∀ (i : ι), |↑q * θ i - ↑(p i)| ≤ ↑q ^ (-w)

A natural number is an admissible denominator exactly when it is positive and has integer numerators approximating every coordinate to within the exponent bound.

noncomputable def TauCeti.simultaneousExponent {ι : Type u_1} (θ : ι → ℝ) : ENNReal

The simultaneous approximation exponent of a finite family θ.

theorem TauCeti.simultaneousExponent_def {ι : Type u_1} (θ : ι → ℝ) : simultaneousExponent θ = ⨆ (w : ℝ), ⨆ (_ : (simultaneousApproximationDenominators θ w).Infinite), ENNReal.ofReal w

The simultaneous exponent is the supremum of the exponents admitting infinitely many simultaneous approximations.

theorem TauCeti.le_simultaneousExponent_of_infinite {ι : Type u_1} {θ : ι → ℝ} {w : ℝ} (h : (simultaneousApproximationDenominators θ w).Infinite) : ENNReal.ofReal w ≤ simultaneousExponent θ

Every exponent admitting infinitely many simultaneous approximations is bounded by the simultaneous exponent.

theorem TauCeti.simultaneousExponent_le_iff {ι : Type u_1} {θ : ι → ℝ} {a : ENNReal} : simultaneousExponent θ ≤ a ↔ ∀ (w : ℝ), (simultaneousApproximationDenominators θ w).Infinite → ENNReal.ofReal w ≤ a

The simultaneous exponent is at most a exactly when every exponent admitting infinitely many simultaneous approximations is.

theorem TauCeti.simultaneousApproximationDenominators_antitone {ι : Type u_1} (θ : ι → ℝ) : Antitone (simultaneousApproximationDenominators θ)

Increasing the exponent can only shrink the set of admissible denominators.

theorem TauCeti.infinite_simultaneousApproximationDenominators_of_lt_simultaneousExponent {ι : Type u_1} {θ : ι → ℝ} {w : ℝ} (h : ENNReal.ofReal w < simultaneousExponent θ) : (simultaneousApproximationDenominators θ w).Infinite

Every real exponent strictly below the simultaneous exponent admits infinitely many simultaneous approximations.

theorem TauCeti.simultaneousApproximationDenominators_mono_comp {ι : Type u_1} {κ : Type u_2} (θ : ι → ℝ) (f : κ → ι) (w : ℝ) : simultaneousApproximationDenominators θ w ⊆ simultaneousApproximationDenominators (θ ∘ f) w

Restricting a family of simultaneous approximations along any map preserves every admissible denominator.

theorem TauCeti.simultaneousExponent_le_comp {ι : Type u_1} {κ : Type u_2} (θ : ι → ℝ) (f : κ → ι) : simultaneousExponent θ ≤ simultaneousExponent (θ ∘ f)

Forgetting coordinates cannot decrease the simultaneous approximation exponent. The result does not require the reindexing map to be injective.

Rational families

theorem TauCeti.simultaneousExponent_eq_top_of_forall_rat {ι : Type u_1} [Finite ι] {θ : ι → ℝ} (hθ : ∀ (i : ι), ∃ (r : ℚ), ↑r = θ i) : simultaneousExponent θ = ⊤

A finite family of rational real numbers has infinite simultaneous exponent.

@[simp]

theorem TauCeti.simultaneousExponent_of_isEmpty {ι : Type u_1} [IsEmpty ι] (θ : ι → ℝ) : simultaneousExponent θ = ⊤

A family indexed by an empty type has infinite simultaneous exponent.

Dirichlet's lower bound

theorem TauCeti.infinite_simultaneousApproximationDenominators_inv_card {ι : Type u_1} [Fintype ι] (θ : ι → ℝ) : (simultaneousApproximationDenominators θ (↑(Fintype.card ι))⁻¹).Infinite

Dirichlet's theorem, infinitely many denominators. For every finite family θ, infinitely many positive integers q admit integers pᵢ with |q θᵢ - pᵢ| ≤ q ^ (-1 / n) for every i, where n is the number of coordinates.

theorem TauCeti.inv_card_le_simultaneousExponent {ι : Type u_1} [Fintype ι] (θ : ι → ℝ) : (↑(Fintype.card ι))⁻¹ ≤ simultaneousExponent θ

Dirichlet's lower bound for the simultaneous exponent. Every family of n real numbers has simultaneous exponent at least 1 / n. For the empty family both sides are ⊤.

One dimension

theorem Irrational.liouvilleWith_add_one_of_simultaneous_infinite {w ξ : ℝ} (hξ : Irrational ξ) (h : (TauCeti.simultaneousApproximationDenominators ![ξ] w).Infinite) : LiouvilleWith (w + 1) ξ

For an irrational real number ξ, infinitely many one-dimensional simultaneous approximations of exponent w give the LiouvilleWith condition of exponent w + 1.

theorem LiouvilleWith.simultaneous_infinite {p w ξ : ℝ} (h : LiouvilleWith p ξ) (hpw : w + 1 < p) : (TauCeti.simultaneousApproximationDenominators ![ξ] w).Infinite

A LiouvilleWith exponent strictly larger than w + 1 supplies infinitely many one-dimensional simultaneous approximations of exponent w.

theorem Irrational.simultaneousExponent_add_one {ξ : ℝ} (hξ : Irrational ξ) : TauCeti.simultaneousExponent ![ξ] + 1 = TauCeti.irrationalityExponent ξ

For an irrational real number ξ, the one-dimensional simultaneous exponent, shifted by one, is the irrationality exponent of ξ.

Examples