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)