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?

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