Skip to content

Erdős problem 955

If A⊂NA\subset \mathbb{N} has density 00 then s−1(A)s^{-1}(A) must also have density 00.

Sources

The source's own material, retained exactly.

12 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

955.lean

Retained formal statement3 of 12

Pollack, Pomerance, and Thompson [PPT18] prove that if ϵ(x)=o(1)\epsilon(x)=o(1) and A⊂NA\subset \mathbb{N} has size at most x1/2+ϵ(x)x^{1/2+\epsilon(x)} then #{n≤x:s(n)∈A}=o(x)\#\{ n\leq x: s(n)\in A\} =o(x) as x→∞x\to \infty. It follows that (using s(n)≪nlog⁡log⁡ns(n)\ll n\log\log n) if AA grows like ∣A∩[1,x]∣≤x1/2+o(1)\lvert A\cap [1,x]\rvert\leq x^{1/2+o(1)} then s−1(A)s^{-1}(A) has density 00.

FormalConjectures/ErdosProblems/955.leanErdos955.erdos_955.variants.pollack_pomerance_thompson_bound3 linesExact file
∀ (A : Set ℕ) (ε : ℕ → ℝ),  Filter.Tendsto ε Filter.atTop (nhds 0) →    (∀ᶠ (n : ℕ) in Filter.atTop, ↑(Nat.count A n) ≤ ↑n ^ (1 / 2 + ε n)) → {x | Erdos955.s x ∈ A}.HasDensity 0
SolvedStatement only, no proof