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 groupA
, givenn : ℕ
andδ : ℝ
,approxOrderOf A n δ
is the set of elements within a distanceδ
of a point of ordern
.wellApproximable
: in a seminormed groupA
, given a sequence of distancesδ₁, δ₂, ...
,wellApproximable A δ
is the limsup asn → ∞
of the setsapproxOrderOf A n δₙ
. Thus, it is the set of points that lie in infinitely many of the setsapproxOrderOf A n δₙ
.AddCircle.addWellApproximable_ae_empty_or_univ
: Gallagher's ergodic theorem says that for the (additive) circle𝕊
, for any sequence of distancesδ
, the setaddWellApproximable 𝕊 δ
is almost empty or almost full.NormedAddCommGroup.exists_norm_nsmul_le
: a general version of Dirichlet's approximation theoremAddCircle.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
).
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}
Instances For
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}
Instances For
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
Instances For
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
Instances For
Gallagher's ergodic theorem on Diophantine approximation.
A general version of Dirichlet's approximation theorem.
See also AddCircle.exists_norm_nsmul_le
.