Erdős problem 454

Is it true that `limsup (fun n => (f n - 2 * n.nth Prime : ℕ∞)) atTop = ⊤`?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

454.lean

Retained formal statement1 of 2

Is it true that limsup (fun n => (f n - 2 * n.nth Prime : ℕ∞)) atTop = ⊤?

FormalConjectures/ErdosProblems/454.leanErdos454.erdos_4541 lineExact file

1True ↔ Filter.limsup (fun n => ↑(Erdos454.f n) - 2 * ↑(Nat.nth Prime n)) Filter.atTop = ⊤

OpenStatement only, no proof