Erdős Problem 143

Reference: erdosproblems.com/143

def WellSeparatedSet (A : Set ℝ) : Prop

Let $A \subseteq (1, \infty)$ be a countably infinite set such that for all $x\neq y\in A$ and integers $k \geq 1$ we have $|kx - y| \geq 1$.

Equations

• WellSeparatedSet A = (A ⊆ Set.Ioi 1 ∧ A.Infinite ∧ A.Countable ∧ ∀ x ∈ A, ∀ y ∈ A, x ≠ y → ∀ k ≥ 1, 1 ≤ |↑k * x - y|)

theorem erdos_143.parts.i : (∀ (A : Set ℝ), WellSeparatedSet A → Filter.liminf (fun (x : ℝ) => ↑(A ∩ Set.Icc 1 x).ncard / x) Filter.atTop = 0) ↔ sorry

Does this imply that $$ \liminf \frac{|A \cap [1,x]|}{x} = 0? $$

theorem erdos_143.parts.ii (A : Set ℝ) (h : WellSeparatedSet A) : ∃ (s : ℝ), Filter.Tendsto (fun (n : ℕ) => ∑ x ∈ Finset.range n, 1 / (↑x * Real.log ↑x)) Filter.atTop (nhds s)

Or $$ \sum_{x \in A} \frac{1}{x \log x} < \infty, $$