Equidistributed Sequences

Corollary 4.2 of Chapter 1 states that the sequence $(x^n), n = 1, 2, ... ,$ is equidistributed modulo 1 for almost all x > 1. And a little bit further down: "one does not know whether sequences such as $(e^n)$, $(π^n)$, or even $((\frac 3 2)^n)$" are equidistributed modulo 1 or not.

References:

• Uniform Distribution of Sequences by L. Kuipers and H. Niederreiter, 1974
• Wikipedia

def Equidistribution.IsAccumulationPoint (x : ℝ) (s : ℕ → ℝ) : Prop

A point x is an accumulation point of a sequence s_0, s_1, ... if any neighbourhood of x contains a point of the sequence distinct from x.

Equations

• Equidistribution.IsAccumulationPoint x s = (x ∈ closure (Set.range s \ {x}))

def Equidistribution.isAccumulationPoint_iff_exists_subsequence_tendsto (x : ℝ) (s : ℕ → ℝ) (hx : IsAccumulationPoint x s) : ∃ (u : ℕ → ℕ), StrictMono u ∧ Filter.Tendsto (s ∘ u) Filter.atTop (nhds x)

If a point x is an accumulation point of a sequence s_0, s_1, ... then there is a subsequence of s that tends to x

Equations

• ⋯ = ⋯

theorem Equidistribution.isEquidistributedModuloOne_three_halves_pow : IsEquidistributedModuloOne fun (n : ℕ) => (3 / 2) ^ n

The sequence (3/2)^n is equidistributed modulo 1.

theorem Equidistribution.isEquidistributedModuloOne_transcendental_three_halves_pow (x : ℝ) (hx : Transcendental ℚ x) : IsEquidistributedModuloOne fun (n : ℕ) => x * (3 / 2) ^ n

For any transcendental number x, the sequence x * (3 / 2) ^ n is equidistributed modulo 1.

theorem Equidistribution.isAccumulationPoint_three_halves_pow_infinite : {x : ℝ | IsAccumulationPoint x fun (n : ℕ) => Int.fract ((3 / 2) ^ n)}.Infinite

The sequence (3/2)^n has infinitely many accumulation points modulo 1.

theorem Equidistribution.isAccumulationPoint_three_halves_pow : IsAccumulationPoint sorry fun (n : ℕ) => Int.fract ((3 / 2) ^ n)

Find an accumulation point of the sequence (3/2)^n modulo 1.

theorem Equidistribution.isAccumulationPoint_three_halves_pow_exists : ∃ (p : ℝ), IsAccumulationPoint p fun (n : ℕ) => Int.fract ((3 / 2) ^ n)

There is an accumulation point of the sequence (3/2)^n modulo 1.