Erdős problem 951 · problems.science

If 1 < a 0 < ... has property Erdos951Prop, is it true that #{a i ≤ x} ≤ π x?

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

951.lean

Retained formal statement1 of 3

If 1 < a 0 < ... has property Erdos951Prop, is it true that #{a i ≤ x} ≤ π x?

FormalConjectures/ErdosProblems/951.leanErdos951.erdos_9514 linesExact file

1sorry ↔2  ∀ (a : ℕ → ℝ),3    1 < a 0 →4      StrictMono a → Erdos951.Erdos951Prop a → ∀ᶠ (x : ℝ) in Filter.atTop, {i | a i ≤ x}.ncard ≤ ⌊x⌋₊.primeCounting

OpenStatement only, no proof

Sources

Search problems.science