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 IsEquidistributed (a b : ℝ) (s : ℕ → ℝ) : Prop

A sequence (s_1, s_2, s_3, ...) of real numbers is said to be equidistributed on an interval [a, b] if for every subinterval [c, d] of [a, b] we have lim_{n→ ∞} |{s_1, ..., s_n} ∩ [c, d]| / n = (d - c)/(b-a)

Equations

• One or more equations did not get rendered due to their size.

def IsEquidistributedModuloOne (s : ℕ → ℝ) : Prop

A sequence (s_1, s_2, s_3, ...) of real numbers is said to be equidistributed modulo 1 or uniformly distributed modulo 1 if the sequence of the fractional parts of a_n, denoted by (a_n) or by a_n − ⌊a_n⌋, is equidistributed in the interval [0, 1].

Equations

• IsEquidistributedModuloOne s = IsEquidistributed 0 1 fun (n : ℕ) => Int.fract (s n)

def 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

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

def 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 isEquidistributedModuloOne_three_halves_pow : IsEquidistributedModuloOne fun (n : ℕ) => (3 / 2) ^ n

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

theorem 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 isAccumulationPoint_three_halves_pow : IsAccumulationPoint sorry fun (n : ℕ) => (3 / 2) ^ n

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