mathlib3 documentation

number_theory.well_approximable

Well-approximable numbers and Gallagher's ergodic theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 eveywhere 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 add_circle.add_well_approximable_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: #

approx_order_of: in a seminormed group A, given n : ℕ and δ : ℝ, approx_order_of A n δ is the set of elements within a distance δ of a point of order n.
well_approximable: in a seminormed group A, given a sequence of distances δ₁, δ₂, ..., well_approximable A δ is the limsup as n → ∞ of the sets approx_order_of A n δₙ. Thus, it is the set of points that lie in infinitely many of the sets approx_order_of A n δₙ.
add_circle.add_well_approximable_ae_empty_or_univ: Gallagher's ergodic theorem says that for for the (additive) circle 𝕊, for any sequence of distances δ, the set add_well_approximable 𝕊 δ is almost empty or almost full.

TODO: #

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

def approx_add_order_of (A : Type u_1) [seminormed_add_group A] (n : ℕ) (δ : ℝ) :

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

Equations

approx_add_order_of A n δ = metric.thickening δ {y : A | add_order_of y = n}

def approx_order_of (A : Type u_1) [seminormed_group A] (n : ℕ) (δ : ℝ) :

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

Equations

approx_order_of A n δ = metric.thickening δ {y : A | order_of y = n}

theorem mem_approx_order_of_iff {A : Type u_1} [seminormed_group A] {n : ℕ} {δ : ℝ} {a : A} :

a ∈ approx_order_of A n δ ↔ ∃ (b : A), order_of b = n ∧ a ∈ metric.ball b δ

theorem mem_approx_add_order_of_iff {A : Type u_1} [seminormed_add_group A] {n : ℕ} {δ : ℝ} {a : A} :

a ∈ approx_add_order_of A n δ ↔ ∃ (b : A), add_order_of b = n ∧ a ∈ metric.ball b δ

def add_well_approximable (A : Type u_1) [seminormed_add_group A] (δ : ℕ → ℝ) :

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

Equations

add_well_approximable A δ = filter.blimsup (λ (n : ℕ), approx_add_order_of A n (δ n)) filter.at_top (λ (n : ℕ), 0 < n)

def well_approximable (A : Type u_1) [seminormed_group A] (δ : ℕ → ℝ) :

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

Equations

well_approximable A δ = filter.blimsup (λ (n : ℕ), approx_order_of A n (δ n)) filter.at_top (λ (n : ℕ), 0 < n)

theorem mem_add_well_approximable_iff {A : Type u_1} [seminormed_add_group A] {δ : ℕ → ℝ} {a : A} :

a ∈ add_well_approximable A δ ↔ a ∈ filter.blimsup (λ (n : ℕ), approx_add_order_of A n (δ n)) filter.at_top (λ (n : ℕ), 0 < n)

theorem mem_well_approximable_iff {A : Type u_1} [seminormed_group A] {δ : ℕ → ℝ} {a : A} :

a ∈ well_approximable A δ ↔ a ∈ filter.blimsup (λ (n : ℕ), approx_order_of A n (δ n)) filter.at_top (λ (n : ℕ), 0 < n)

theorem approx_add_order_of.image_nsmul_subset_of_coprime {A : Type u_1} [seminormed_add_comm_group A] {m n : ℕ} (δ : ℝ) (hm : 0 < m) (hmn : n.coprime m) :

(λ (y : A), m • y) '' approx_add_order_of A n δ ⊆ approx_add_order_of A n (↑m * δ)

theorem approx_order_of.image_pow_subset_of_coprime {A : Type u_1} [seminormed_comm_group A] {m n : ℕ} (δ : ℝ) (hm : 0 < m) (hmn : n.coprime m) :

(λ (y : A), y ^ m) '' approx_order_of A n δ ⊆ approx_order_of A n (↑m * δ)

theorem approx_add_order_of.image_nsmul_subset {A : Type u_1} [seminormed_add_comm_group A] {m : ℕ} (δ : ℝ) (n : ℕ) (hm : 0 < m) :

(λ (y : A), m • y) '' approx_add_order_of A (n * m) δ ⊆ approx_add_order_of A n (↑m * δ)

theorem approx_order_of.image_pow_subset {A : Type u_1} [seminormed_comm_group A] {m : ℕ} (δ : ℝ) (n : ℕ) (hm : 0 < m) :

(λ (y : A), y ^ m) '' approx_order_of A (n * m) δ ⊆ approx_order_of A n (↑m * δ)

theorem approx_order_of.smul_subset_of_coprime {A : Type u_1} [seminormed_comm_group A] {a : A} {n : ℕ} (δ : ℝ) (han : (order_of a).coprime n) :

a • approx_order_of A n δ ⊆ approx_order_of A (order_of a * n) δ

theorem approx_add_order_of.vadd_subset_of_coprime {A : Type u_1} [seminormed_add_comm_group A] {a : A} {n : ℕ} (δ : ℝ) (han : (add_order_of a).coprime n) :

a +ᵥ approx_add_order_of A n δ ⊆ approx_add_order_of A (add_order_of a * n) δ

theorem approx_order_of.smul_eq_of_mul_dvd {A : Type u_1} [seminormed_comm_group A] {a : A} {n : ℕ} (δ : ℝ) (hn : 0 < n) (han : order_of a ^ 2 ∣ n) :

a • approx_order_of A n δ = approx_order_of A n δ

theorem approx_add_order_of.vadd_eq_of_mul_dvd {A : Type u_1} [seminormed_add_comm_group A] {a : A} {n : ℕ} (δ : ℝ) (hn : 0 < n) (han : add_order_of a ^ 2 ∣ n) :

a +ᵥ approx_add_order_of A n δ = approx_add_order_of A n δ

theorem unit_add_circle.mem_approx_add_order_of_iff {δ : ℝ} {x : unit_add_circle} {n : ℕ} (hn : 0 < n) :

x ∈ approx_add_order_of unit_add_circle n δ ↔ ∃ (m : ℕ) (H : m < n), gcd_monoid.gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ

theorem unit_add_circle.mem_add_well_approximable_iff (δ : ℕ → ℝ) (x : unit_add_circle) :

x ∈ add_well_approximable unit_add_circle δ ↔ {n : ℕ | ∃ (m : ℕ) (H : m < n), gcd_monoid.gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}.infinite

theorem add_circle.add_well_approximable_ae_empty_or_univ {T : ℝ} [hT : fact (0 < T)] (δ : ℕ → ℝ) (hδ : filter.tendsto δ filter.at_top (nhds 0)) :

(∀ᵐ (x : add_circle T), ¬add_well_approximable (add_circle T) δ x) ∨ ∀ᵐ (x : add_circle T), add_well_approximable (add_circle T) δ x

Gallagher's ergodic theorem on Diophantine approximation.