Skip to content

Erdős problem 158

Start work

Let A be an infinite B₂[2] set. Must liminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) = 0?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

158.lean

Retained formal statement3 of 4

As a corollary of erdos_158.isSidon', we can prove that liminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) = 0 for any infinite Sidon set A.

FormalConjectures/ErdosProblems/158.leanErdos158.erdos_158.variants.isSidon1 lineExact file
∀ {A : Set ℕ}, A.Infinite → IsSidon A → Filter.liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) Filter.atTop = 0
SolvedStatement only, no proof