Uniform distribution and metric approximation

Weyl equidistribution, three-gap theorem, Duffin–Schaeffer, normal numbers, Beatty sequences, discrepancy, lattice points and Minkowski-type theorems.

• Beatty sequences
• Discrepancy of fractional parts
• Duffin–Schaeffer conjecture
• Floor and ceiling function sums
• Fractional parts of multiples of primes
• Lattice points in translated discs
• Littlewood conjecture
• Normal numbers
• Reverse Minkowski theorem
• Smallest denominators in intervals
• Square roots of cubic polynomials modulo one
• Three-gap theorem

TheoremWeyl's equidistribution criterion#✓fully proved

Let \((x_n)_{n \ge 0}\) be a sequence of real numbers and write \(\operatorname{frac}(t) = t - \lfloor t \rfloor\) for the fractional part of a real number \(t\). Then the following are equivalent: (i) for all real numbers \(a < b\) with \(0 \le a\) and \(b \le 1\), \(\frac{1}{N} \#\{n < N : a \le \operatorname{frac}(x_n) < b\} \to b - a\) as \(N \to \infty\); (ii) for every nonzero integer \(h\), \(\frac{1}{N} \sum_{n=0}^{N-1} e^{2\pi i h x_n} \to 0\) as \(N \to \infty\).

public theorem weyl_criterion (x : ℕ → ℝ) :
    (∀ a b : ℝ, 0 ≤ a → a < b → b ≤ 1 →
      Tendsto (fun N : ℕ =>
        ((Finset.filter (fun n => a ≤ Int.fract (x n) ∧ Int.fract (x n) < b)
          (Finset.range N)).card : ℝ) / (N : ℝ))
        atTop (nhds (b - a)))
    ↔ ∀ h : ℤ, h ≠ 0 →
      Tendsto (fun N : ℕ =>
        (1 / (N : ℂ)) * ∑ n ∈ Finset.range N,
          Complex.exp (((2 * Real.pi * (h : ℝ) * x n : ℝ) : ℂ) * Complex.I))
        atTop (nhds 0)

Sources

• https://en.wikipedia.org/wiki/Equidistribution_theorem.

Uses 7

Proof usesInterval cutoff · Continuity of the interval cutoff · The interval cutoff equals one on its plateau · The interval cutoff vanishes right of the interval · The interval cutoff vanishes left of the interval · The interval cutoff is at most one · The interval cutoff is nonnegative

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.