Erdős Problem 170

Reference: erdosproblems.com/170

@[reducible]

def Erdos170.PerfectRuler (N : ℕ) (A : Finset ℕ) : Prop

An $N$-perfect ruler is a finite subset $A \subseteq \mathbb{N}$ (the marks), such that each positive integer $k \leq N$ can be measured, that is, expressed as a difference $k = a_1 - a_0$ with $a_0, a_1 \in A$. The set $A$ is then also called a difference basis w.r.t. $N$.

Equations

• Erdos170.PerfectRuler N A = ∀ k ∈ Finset.range (N + 1), ∃ a₀ ∈ A, ∃ a₁ ∈ A, k = a₁ - a₀

def Erdos170.PerfectRulersLengthN (N : ℕ) : Finset (Finset ℕ)

We define the set of all $N$-perfect rulers $A$ of length $N$, i.e. subsets $A \subseteq \{0, \dots, N\}$, s.t. $A$ is $N$-perfect. This is also called a restricted difference basis w.r.t. $N$.

Equations

• Erdos170.PerfectRulersLengthN N = Finset.filter (Erdos170.PerfectRuler N) (Finset.range (N + 1)).powerset

@[reducible, inline]

abbrev Erdos170.TrivialRuler (N : ℕ) : Finset ℕ

The trivial ruler with all marks $\{0, \dots, N\}$.

Equations

• Erdos170.TrivialRuler N = Finset.range (N + 1)

theorem Erdos170.trivial_ruler_is_perfect (N : ℕ) : TrivialRuler N ∈ PerfectRulersLengthN N

Sanity Check: the trivial ruler is actually a perfect ruler if $K \geq N$

def Erdos170.F (N : ℕ) : ℕ

We define a function F N as the minimum cardinality of an N-perfect ruler of length N.

Equations

• Erdos170.F N = (Finset.image Finset.card (Erdos170.PerfectRulersLengthN N)).min' ⋯

theorem Erdos170.erdos170 : Filter.Tendsto (fun (N : ℕ) => ↑(F N) / √↑N) Filter.atTop (nhds sorry)

The problem is to determine the limit of the sequence $\frac{F(N)}{\sqrt{N}}$ as $N \to \infty$.

@[reducible, inline]

noncomputable abbrev Erdos170.lower_bound : ℝ

A known lower bound to the limit by Leech [Le56], which is $1.56\dots$.

Equations

• Erdos170.lower_bound = √(sSup {x : ℝ | ∃ (θ : ℝ), θ ≠ 0 ∧ 2 * (1 - Real.sin θ / θ) = x})

@[reducible, inline]

noncomputable abbrev Erdos170.upper_bound : ℝ

A known upper bound obtained by constructing Wichmann's Rulers [Wi63].

Equations

• Erdos170.upper_bound = √3

theorem Erdos170.erdos170.existing_bounds : ∃ x ∈ Set.Icc lower_bound upper_bound, Filter.Tendsto (fun (N : ℕ) => ↑(F N) / √↑N) Filter.atTop (nhds x)

The existence of the limit has been proved by Erdős and Gál [ErGa48]. The lower bound has been proven by Leech [Le56], who refined an argument of Rédei and Rényi. The upper bound is due to Wichmann [Wi63].