Skip to content

Erdős problem 951

Start work

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

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

951.lean

Retained formal statement3 of 3

If a has property Erdos951Prop and 1 < a 0, then a is a set of Beurling prime numbers.

FormalConjectures/ErdosProblems/951.leanErdos951.erdos_951.variants.isBeurlingPrimes1 lineExact file
∀ {a : ℕ → ℝ}, 1 < a 0 → StrictMono a → Erdos951.Erdos951Prop a → IsBeurlingPrimes a
APIStatement only, no proof