Erdős problem 158 · problems.science

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

Sources

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

4 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

158.lean

Retained formal statement4 of 4

Let A be an infinite Sidon set. Then liminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) * (log N) ^ (1 / 2) < ∞. This is proved in [ESS94].

FormalConjectures/ErdosProblems/158.leanErdos158.erdos_158.variants.isSidon'6 linesExact file

1∀ {A : Set ℕ},2  A.Infinite →3    IsSidon A →4      Filter.liminf (fun N => ENNReal.ofReal (↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * Real.log ↑N ^ (1 / 2)))5          Filter.atTop <6        ⊤

SolvedStatement only, no proof

Sources

Search problems.science