Erdős problem 280
Let be an infinite sequence of integers with associated , such that for some we have for all . Then
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/280.leanFalse ↔ ∀ (n a : ℕ → ℕ), StrictMono n → (∀ (i : ℕ), 1 ≤ i → a i < n i) → (∃ ε, 0 < ε ∧ ∀ (k : ℕ), 1 ≤ k → ↑(n k) > (1 + ε) * ↑k * Real.log ↑k) → ¬Filter.Tendsto (fun k => ↑(Erdos280.uncoveredCount n a k) / ↑k) Filter.atTop (nhds 0)Proof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:280 - PLBY Lean proofs
ErdosProblems.Erdos280
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine