sorry ↔ ∃ 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))