← Mathematical handbook

theorem Verification.power_root_gap_limit {u : ℝ} (hu : 0 < u) : Filter.Tendsto (fun (c : ℝ) => c * (1 - u ^ c⁻¹)) Filter.atTop (nhds (-Real.log u))