Erdős problem 1002

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?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1002.lean

Retained formal statement2 of 2

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.

FormalConjectures/ErdosProblems/1002.leanErdos1002.erdos_1002.variants.kesten10 linesExact file

1∃ ρ > 0,2  have g := fun c => 1 / Real.pi * ∫ (t : ℝ) in Set.Iic (ρ * c), 1 / (1 + t ^ 2);3  ∀ (c : ℝ),4    Filter.Tendsto5      (fun n =>6        (MeasureTheory.volume7            {(α, β) |8              α ∈ Set.Icc 0 1 ∧9                β ∈ Set.Icc 0 1 ∧ 1 / Real.log ↑n * ∑ k ∈ Finset.Icc 1 n, (1 / 2 - Int.fract (β + α * ↑k)) ≤ c}).toReal)10      Filter.atTop (nhds (g c))

SolvedStatement only, no proof