Erdős Problem 1002 #
References:
- erdosproblems.com/1002
- [Ke60] Kesten, Harry, Uniform distribution {${\rm mod}\,1$}. Ann. of Math. (2) (1960), 445--471.
theorem
Erdos1002.erdos_1002 :
True ↔ ∃ (g : ℝ → ℝ),
Monotone g ∧ Filter.Tendsto g Filter.atBot (nhds 0) ∧ Filter.Tendsto g Filter.atTop (nhds 1) ∧ ∀ (c : ℝ),
Filter.Tendsto
(fun (n : ℕ) =>
(MeasureTheory.volume
{α : ℝ | α ∈ Set.Ioo 0 1 ∧ (fun (α : ℝ) (n : ℕ) => 1 / Real.log ↑n * ∑ k ∈ Finset.Icc 1 n, (1 / 2 - Int.fract (α * ↑k))) α
n ≤ c}).toReal)
Filter.atTop (nhds (g c))
For any $0<\alpha<1$, let $f(\alpha,n)=\frac{1}{\log n}\sum_{1\leq k\leq n}(\tfrac{1}{2}- \{ \alpha k\})$. Does $f(\alpha,n)$ have an asymptotic distribution function?
In other words, is there a non-decreasing function $g$ such that $g(-\infty)=0$, $g(\infty)=1$, and $\lim_{n\to \infty}\lvert \{ \alpha\in (0,1): f(\alpha,n)\leq c\}\rvert=g(c)$?
theorem
Erdos1002.erdos_1002.variants.kesten :
∃ ρ > 0,
have g := fun (c : ℝ) => 1 / Real.pi * ∫ (t : ℝ) in Set.Iic (ρ * c), 1 / (1 + t ^ 2);
∀ (c : ℝ),
Filter.Tendsto
(fun (n : ℕ) =>
(MeasureTheory.volume
{(α, β) : ℝ × ℝ | α ∈ Set.Icc 0 1 ∧ β ∈ Set.Icc 0 1 ∧ 1 / Real.log ↑n * ∑ k ∈ Finset.Icc 1 n, (1 / 2 - Int.fract (β + α * ↑k)) ≤ c}).toReal)
Filter.atTop (nhds (g c))
Kesten [Ke60] proved that if $f(\alpha,\beta,n)=\frac{1}{\log n}\sum_{1\leq k\leq n}(\tfrac{1}{2}- \{\beta+\alpha k\})$ then $f(\alpha,\beta,n)$ has asymptotic distribution function $g(c)=\frac{1}{\pi}\int_{-\infty}^{\rho c}\frac{1}{1+t^2}\mathrm{d}t$, where $\rho>0$ is an explicit constant.