Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.LogPowerBounds

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

AnalyticNumberTheory.LargeSieve.log_pow_le_sqrt_eventually · compiled type and proof/definition references.