Erdős Problem 168

Reference: erdosproblems.com/168

def Erdos168.NonTernary (S : Finset ℕ) : Prop

Say a finite set of natural numbers is non ternary if it contains no 3-term arithmetic progression of the form n, 2n, 3n.

Equations

• Erdos168.NonTernary S = ∀ (n : ℕ), n ∉ S ∨ 2 * n ∉ S ∨ 3 * n ∉ S

def Erdos168.IntervalNonTernarySets (N : ℕ) : Finset (Finset ℕ)

IntervalNonTernarySets N is the (fin)set of non ternary subsets of {1,...,N}. The advantage of defining it as below is that some proofs (e.g. that of F 3 = 2) become rfl.

Equations

• Erdos168.IntervalNonTernarySets N = Finset.filter (fun (S : Finset ℕ) => ∀ n ∈ Finset.Icc 1 (N / 3), n ∉ S ∨ 2 * n ∉ S ∨ 3 * n ∉ S) (Finset.Icc 1 N).powerset

theorem Erdos168.F_0 : Erdos168.F✝ 0 = 0

theorem Erdos168.F_1 : Erdos168.F✝ 1 = 1

theorem Erdos168.F_2 : Erdos168.F✝ 2 = 2

theorem Erdos168.F_3 : Erdos168.F✝ 3 = 2

theorem Erdos168.mem_IntervalNonTernarySets_iff (N : ℕ) (S : Finset ℕ) : S ∈ IntervalNonTernarySets N ↔ NonTernary S ∧ S ⊆ Finset.Icc 1 N

Sanity check: elements of IntervalNonTernarySets N are precisely non ternary subsets of {1,...,N}

theorem Erdos168.F_eq_card (N : ℕ) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 N) (hS' : NonTernary S) (hS'' : ∀ T ⊆ Finset.Icc 1 N, NonTernary T → S.card ≤ T.card → T.card = S.card) : Erdos168.F✝ N = S.card

Sanity check: if S is a maximal non ternary subset of {1,..., N} then F N is given by the cardinality of S

theorem Erdos168.erdos_168.parts.i : Filter.Tendsto (fun (N : ℕ) => ↑(Erdos168.F✝ N) / ↑N) Filter.atTop (nhds sorry)

What is the limit $F(N)/N$ as $N \to \infty$?

theorem Erdos168.erdos_168.parts.ii : Irrational (Filter.limsup (fun (N : ℕ) => ↑(Erdos168.F✝ N) / ↑N) Filter.atTop) ↔ sorry

Is the limit $F(N)/N$ as $N \to \infty$ irrational?

theorem Erdos168.erdos_168.variants.limit_exists : ∃ (x : ℝ), Filter.Tendsto (fun (N : ℕ) => ↑(Erdos168.F✝ N) / ↑N) Filter.atTop (nhds x)

The limit $F(N)/N$ as $N \to \infty$ exists. (proved by Graham, Spencer, and Witsenhausen)