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

Open selected source

FormalConjectures/ErdosProblems/

1002.lean

Retained formal statement1 of 2

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)$ ?

FormalConjectures/ErdosProblems/1002.leanErdos1002.erdos_100214 linesExact file

1sorry ↔2  ∃ g,3    Monotone g ∧4      Filter.Tendsto g Filter.atBot (nhds 0) ∧5        Filter.Tendsto g Filter.atTop (nhds 1) ∧6          ∀ (c : ℝ),7            Filter.Tendsto8              (fun n =>9                (MeasureTheory.volume10                    {α |11                      α ∈ Set.Ioo 0 1 ∧12                        (fun α n => 1 / Real.log ↑n * ∑ k ∈ Finset.Icc 1 n, (1 / 2 - Int.fract (α * ↑k))) α n ≤13                          c}).toReal)14              Filter.atTop (nhds (g c))

OpenStatement only, no proof