Discrepancy of fractional parts

DefinitionCounting fractional parts in a rational interval#✓fully proved

For a sequence of integers \((x_n)_{n \ge 0}\), a real number \(\alpha\), a natural number \(N\) and rationals \(p, q\), the number of indices \(n < N\) for which the fractional part \(\{\alpha x_n\}\) lies in the closed interval \([p, q]\).

noncomputable def CountQ (x : ℕ → ℤ) (α : ℝ) (N : ℕ) (p q : ℚ) : ℕ :=
  ((Finset.range N).filter fun n =>
    Int.fract (α * (x n : ℝ)) ∈ Set.Icc (p : ℝ) (q : ℝ)).card

Used by 1

Used byDiscrepancy of fractional parts over rational intervals

DefinitionDiscrepancy of fractional parts over rational intervals#✓fully proved

For a sequence of integers \((x_n)_{n \ge 0}\), a real number \(\alpha\) and a natural number \(N\), the discrepancy \(D(N)\) is the supremum, over rationals \(p, q\) with \(0 \le p \le q \le 1\), of \(\lvert A(p, q) - (q - p) N \rvert\), where \(A(p, q)\) is the number of indices \(n < N\) for which the fractional part \(\{\alpha x_n\}\) lies in the closed interval \([p, q]\).

noncomputable def discrep (x : ℕ → ℤ) (α : ℝ) (N : ℕ) : ℝ :=
  sSup { d : ℝ | ∃ p q : ℚ, 0 ≤ (p : ℝ) ∧ (q : ℝ) ≤ 1 ∧ (p : ℝ) ≤ (q : ℝ) ∧
    d = |(CountQ x α N p q : ℝ) - ((q : ℝ) - (p : ℝ)) * (N : ℝ)| }

Uses 1 · Used by 1

Statement usesCounting fractional parts in a rational interval

Used byErdős Problem 992 on the discrepancy of fractional parts

DefinitionErdős Problem 992 on the discrepancy of fractional parts#✓fully proved

For a strictly increasing sequence of integers \(x_0 < x_1 < \cdots\), a real number \(\alpha\) and a natural number \(N\), let \(D(N)\) be the supremum, over rationals \(p, q\) with \(0 \le p \le q \le 1\), of \(\lvert A(p, q) - (q - p) N \rvert\), where \(A(p, q)\) is the number of indices \(n < N\) for which the fractional part \(\{\alpha x_n\}\) lies in \([p, q]\). The statement is that for every such sequence, for almost every \(\alpha \in [0, 1]\) (Lebesgue measure) and every \(\varepsilon > 0\), there is a real constant \(C\) such that \(D(N) \le C \sqrt{N} (\log N)^{\varepsilon}\) for all sufficiently large \(N\).

def conjecture : Prop :=
  ∀ x : ℕ → ℤ, StrictMono x →
    ∀ᵐ α ∂(volume.restrict (Set.Icc (0 : ℝ) 1)),
      ∀ ε : ℝ, 0 < ε → ∃ C : ℝ,
        ∀ᶠ N : ℕ in atTop,
          discrep x α N ≤ C * Real.sqrt (N : ℝ) * Real.rpow (Real.log (N : ℝ)) ε

Uses 1 · Used by 1

Statement usesDiscrepancy of fractional parts over rational intervals

Used byErdős Problem 992 has a negative answer

TheoremErdős Problem 992 has a negative answer#●ready to prove

For a sequence of integers \((x_n)_{n \ge 0}\), a real number \(\alpha\) and a natural number \(N\), let \(D(N)\) be the supremum, over rationals \(p, q\) with \(0 \le p \le q \le 1\), of \(\lvert A(p, q) - (q - p) N \rvert\), where \(A(p, q)\) is the number of indices \(n < N\) for which the fractional part \(\{\alpha x_n\}\) lies in \([p, q]\). It is not true that for every strictly increasing sequence of integers \(x_0 < x_1 < \cdots\), for almost every \(\alpha \in [0, 1]\) and every \(\varepsilon > 0\) there is a real constant \(C\) with \(D(N) \le C \sqrt{N} (\log N)^{\varepsilon}\) for all sufficiently large \(N\).

Berkes and Philipp construct an increasing integer sequence \((n_k)\) with \(\limsup_N \lvert \sum_{k \le N} \cos(2\pi n_k \alpha) \rvert / \sqrt{N \log N} = \infty\) for almost every \(\alpha\); by Koksma's inequality, \(D(N)\) is then not \(O(\sqrt{N} (\log N)^{\varepsilon})\) for \(\varepsilon < 1/2\).

public theorem_wanted conjecture_refuted : ¬ conjecture

Sources

• C. Aistleitner, I. Berkes, R. Tichy, Lacunary sequences in analysis, probability and number theory, arXiv preprint (2023), arXiv:2301.05561 (reporting I. Berkes, W. Philipp, J. London Math. Soc. (2) 50 (1994), 454-464), https://arxiv.org/abs/2301.05561.

Uses 1

Statement usesErdős Problem 992 on the discrepancy of fractional parts

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.