Erdős Problem 143

Reference: erdosproblems.com/143

def Erdos143.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

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

theorem Erdos143.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 Erdos143.erdos_143.parts.ii (A : Set ℝ) (h : WellSeparatedSet A) : Summable fun (x : ↑A) => 1 / (↑x * Real.log ↑x)

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