Well-approximable numbers and Gallagher's ergodic theorem

Gallagher's ergodic theorem is a result in metric number theory. It thus belongs to that branch of mathematics concerning arithmetic properties of real numbers which hold almost everywhere with respect to the Lebesgue measure.

Gallagher's theorem concerns the approximation of real numbers by rational numbers. The input is a sequence of distances δ₁, δ₂, ..., and the theorem concerns the set of real numbers x for which there is an infinity of solutions to: $$ |x - m/n| < δₙ, $$ where the rational number m/n is in lowest terms. The result is that for any δ, this set is either almost all x or almost no x.

This result was proved by Gallagher in 1959 P. Gallagher, Approximation by reduced fractions. It is formalised here as AddCircle.addWellApproximable_ae_empty_or_univ except with x belonging to the circle ℝ ⧸ ℤ since this turns out to be more natural.

Given a particular δ, the Duffin-Schaeffer conjecture (now a theorem) gives a criterion for deciding which of the two cases in the conclusion of Gallagher's theorem actually occurs. It was proved by Koukoulopoulos and Maynard in 2019 D. Koukoulopoulos, J. Maynard, On the Duffin-Schaeffer conjecture. We do not include a formalisation of the Koukoulopoulos-Maynard result here.

Main definitions and results:

• approxOrderOf: in a seminormed group A, given n : ℕ and δ : ℝ, approxOrderOf A n δ is the set of elements within a distance δ of a point of order n.
• wellApproximable: in a seminormed group A, given a sequence of distances δ₁, δ₂, ..., wellApproximable A δ is the limsup as n → ∞ of the sets approxOrderOf A n δₙ. Thus, it is the set of points that lie in infinitely many of the sets approxOrderOf A n δₙ.
• AddCircle.addWellApproximable_ae_empty_or_univ: Gallagher's ergodic theorem says that for the (additive) circle 𝕊, for any sequence of distances δ, the set addWellApproximable 𝕊 δ is almost empty or almost full.
• NormedAddCommGroup.exists_norm_nsmul_le: a general version of Dirichlet's approximation theorem
• AddCircle.exists_norm_nsmul_le: Dirichlet's approximation theorem

TODO

The hypothesis hδ in AddCircle.addWellApproximable_ae_empty_or_univ can be dropped. An elementary (non-measure-theoretic) argument shows that if ¬ hδ holds then addWellApproximable 𝕊 δ = univ (provided δ is non-negative).

Use AddCircle.exists_norm_nsmul_le to prove: addWellApproximable 𝕊 (fun n ↦ 1 / n^2) = { ξ | ¬ IsOfFinAddOrder ξ } (which is equivalent to Real.infinite_rat_abs_sub_lt_one_div_den_sq_iff_irrational).

def approxOrderOf (A : Type u_1) [SeminormedGroup A] (n : ℕ) (δ : ℝ) : Set A

In a seminormed group A, given n : ℕ and δ : ℝ, approxOrderOf A n δ is the set of elements within a distance δ of a point of order n.

Equations

• approxOrderOf A n δ = Metric.thickening δ {y : A | orderOf y = n}

def approxAddOrderOf (A : Type u_1) [SeminormedAddGroup A] (n : ℕ) (δ : ℝ) : Set A

In a seminormed additive group A, given n : ℕ and δ : ℝ, approxAddOrderOf A n δ is the set of elements within a distance δ of a point of order n.

Equations

• approxAddOrderOf A n δ = Metric.thickening δ {y : A | addOrderOf y = n}

theorem mem_approxOrderOf_iff {A : Type u_1} [SeminormedGroup A] {n : ℕ} {δ : ℝ} {a : A} : a ∈ approxOrderOf A n δ ↔ ∃ (b : A), orderOf b = n ∧ a ∈ Metric.ball b δ

theorem mem_approx_add_orderOf_iff {A : Type u_1} [SeminormedAddGroup A] {n : ℕ} {δ : ℝ} {a : A} : a ∈ approxAddOrderOf A n δ ↔ ∃ (b : A), addOrderOf b = n ∧ a ∈ Metric.ball b δ

def wellApproximable (A : Type u_1) [SeminormedGroup A] (δ : ℕ → ℝ) : Set A

In a seminormed group A, given a sequence of distances δ₁, δ₂, ..., wellApproximable A δ is the limsup as n → ∞ of the sets approxOrderOf A n δₙ. Thus, it is the set of points that lie in infinitely many of the sets approxOrderOf A n δₙ.

Equations

• wellApproximable A δ = Filter.blimsup (fun (n : ℕ) => approxOrderOf A n (δ n)) Filter.atTop fun (n : ℕ) => 0 < n

def addWellApproximable (A : Type u_1) [SeminormedAddGroup A] (δ : ℕ → ℝ) : Set A

In a seminormed additive group A, given a sequence of distances δ₁, δ₂, ..., addWellApproximable A δ is the limsup as n → ∞ of the sets approxAddOrderOf A n δₙ. Thus, it is the set of points that lie in infinitely many of the sets approxAddOrderOf A n δₙ.

Equations

• addWellApproximable A δ = Filter.blimsup (fun (n : ℕ) => approxAddOrderOf A n (δ n)) Filter.atTop fun (n : ℕ) => 0 < n

theorem mem_wellApproximable_iff {A : Type u_1} [SeminormedGroup A] {δ : ℕ → ℝ} {a : A} : a ∈ wellApproximable A δ ↔ a ∈ Filter.blimsup (fun (n : ℕ) => approxOrderOf A n (δ n)) Filter.atTop fun (n : ℕ) => 0 < n

theorem mem_add_wellApproximable_iff {A : Type u_1} [SeminormedAddGroup A] {δ : ℕ → ℝ} {a : A} : a ∈ addWellApproximable A δ ↔ a ∈ Filter.blimsup (fun (n : ℕ) => approxAddOrderOf A n (δ n)) Filter.atTop fun (n : ℕ) => 0 < n

theorem approxOrderOf.image_pow_subset_of_coprime {A : Type u_1} [SeminormedCommGroup A] {m n : ℕ} (δ : ℝ) (hm : 0 < m) (hmn : n.Coprime m) : (fun (y : A) => y ^ m) '' approxOrderOf A n δ ⊆ approxOrderOf A n (↑m * δ)

theorem approxAddOrderOf.image_nsmul_subset_of_coprime {A : Type u_1} [SeminormedAddCommGroup A] {m n : ℕ} (δ : ℝ) (hm : 0 < m) (hmn : n.Coprime m) : (fun (y : A) => m • y) '' approxAddOrderOf A n δ ⊆ approxAddOrderOf A n (↑m * δ)

theorem approxOrderOf.image_pow_subset {A : Type u_1} [SeminormedCommGroup A] {m : ℕ} (δ : ℝ) (n : ℕ) (hm : 0 < m) : (fun (y : A) => y ^ m) '' approxOrderOf A (n * m) δ ⊆ approxOrderOf A n (↑m * δ)

theorem approxAddOrderOf.image_nsmul_subset {A : Type u_1} [SeminormedAddCommGroup A] {m : ℕ} (δ : ℝ) (n : ℕ) (hm : 0 < m) : (fun (y : A) => m • y) '' approxAddOrderOf A (n * m) δ ⊆ approxAddOrderOf A n (↑m * δ)

theorem approxOrderOf.smul_subset_of_coprime {A : Type u_1} [SeminormedCommGroup A] {a : A} {n : ℕ} (δ : ℝ) (han : (orderOf a).Coprime n) : a • approxOrderOf A n δ ⊆ approxOrderOf A (orderOf a * n) δ

theorem approxAddOrderOf.vadd_subset_of_coprime {A : Type u_1} [SeminormedAddCommGroup A] {a : A} {n : ℕ} (δ : ℝ) (han : (addOrderOf a).Coprime n) : a +ᵥ approxAddOrderOf A n δ ⊆ approxAddOrderOf A (addOrderOf a * n) δ

theorem approxOrderOf.smul_eq_of_mul_dvd {A : Type u_1} [SeminormedCommGroup A] {a : A} {n : ℕ} (δ : ℝ) (hn : 0 < n) (han : orderOf a ^ 2 ∣ n) : a • approxOrderOf A n δ = approxOrderOf A n δ

theorem approxAddOrderOf.vadd_eq_of_mul_dvd {A : Type u_1} [SeminormedAddCommGroup A] {a : A} {n : ℕ} (δ : ℝ) (hn : 0 < n) (han : addOrderOf a ^ 2 ∣ n) : a +ᵥ approxAddOrderOf A n δ = approxAddOrderOf A n δ

theorem UnitAddCircle.mem_approxAddOrderOf_iff {δ : ℝ} {x : UnitAddCircle} {n : ℕ} (hn : 0 < n) : x ∈ approxAddOrderOf UnitAddCircle n δ ↔ ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ

theorem UnitAddCircle.mem_addWellApproximable_iff (δ : ℕ → ℝ) (x : UnitAddCircle) : x ∈ addWellApproximable UnitAddCircle δ ↔ {n : ℕ | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}.Infinite

theorem AddCircle.addWellApproximable_ae_empty_or_univ {T : ℝ} [hT : Fact (0 < T)] (δ : ℕ → ℝ) (hδ : Filter.Tendsto δ Filter.atTop (nhds 0)) : (∀ᵐ (x : AddCircle T), ¬addWellApproximable (AddCircle T) δ x) ∨ ∀ᵐ (x : AddCircle T), addWellApproximable (AddCircle T) δ x

Gallagher's ergodic theorem on Diophantine approximation.

theorem NormedAddCommGroup.exists_norm_nsmul_le {A : Type u_1} [NormedAddCommGroup A] [CompactSpace A] [ConnectedSpace A] [MeasurableSpace A] [BorelSpace A] {μ : MeasureTheory.Measure A} [μ.IsAddHaarMeasure] (ξ : A) {n : ℕ} (hn : 0 < n) (δ : ℝ) (hδ : μ Set.univ ≤ (n + 1) • μ (Metric.closedBall 0 (δ / 2))) : ∃ j ∈ Set.Icc 1 n, ‖j • ξ‖ ≤ δ

A general version of Dirichlet's approximation theorem.

See also AddCircle.exists_norm_nsmul_le.

theorem AddCircle.exists_norm_nsmul_le {T : ℝ} [hT : Fact (0 < T)] (ξ : AddCircle T) {n : ℕ} (hn : 0 < n) : ∃ j ∈ Set.Icc 1 n, ‖j • ξ‖ ≤ T / ↑(n + 1)

Dirichlet's approximation theorem

See also Real.exists_rat_abs_sub_le_and_den_le.