Erdős Problem 1062

Reference: erdosproblems.com/1062

def Erdos1062.ForkFree (A : Set ℕ) : Prop

A set A of positive integers is fork-free if no element divides two distinct other elements of A.

Equations

• Erdos1062.ForkFree A = ∀ a ∈ A, {b : ℕ | b ∈ A \ {a} ∧ a ∣ b}.Subsingleton

noncomputable def Erdos1062.f (n : ℕ) : ℕ

The extremal function from Erdős problem 1062: the largest size of a fork-free subset of {1,...,n}.

Equations

• Erdos1062.f n = Nat.findGreatest (fun (k : ℕ) => ∃ A ⊆ Set.Icc 1 n, Erdos1062.ForkFree A ∧ A.ncard = k) n

theorem Erdos1062.erdos_1062.lower_bound (n : ℕ) : ⌈2 * ↑n / 3⌉₊ ≤ f n

The interval [⌊n/3⌋, n] is fork-free, and therefore f n is at least ⌈2n / 3⌉.

theorem Erdos1062.erdos_1062.lebensold_bounds : ∀ᶠ (n : ℕ) in Filter.atTop, 0.6725 * ↑n ≤ ↑(f n) ∧ ↑(f n) ≤ 0.6736 * ↑n

Lebensold proved that for large n, the function f n lies between 0.6725 n and 0.6736 n.

theorem Erdos1062.erdos_1062.limit_density : (∃ (l : ℝ), Filter.Tendsto (fun (n : ℕ) => ↑(f n) / ↑n) Filter.atTop (nhds l) ∧ Irrational l) ↔ sorry

Erdős asked whether the limiting density f n / n exists and, if so, whether it is irrational.