theorem AnalyticNumberTheory.LargeSieve.log_pow_le_sqrt_eventually (k : ℕ) : ∀ᶠ (N : ℕ) in Filter.atTop, Real.log ↑N ^ k ≤ √↑N