Documentation

FormalConjectures.ErdosProblems.«168»

Erdős Problem 168 #

Reference: erdosproblems.com/168

source
def 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
Instances For
    source
    def 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
    Instances For
      source
      theorem F_0 :
      F✝ 0 = 0
      source
      theorem F_1 :
      F✝ 1 = 1
      source
      theorem F_2 :
      F✝ 2 = 2
      source
      theorem F_3 :
      F✝ 3 = 2
      source
      theorem 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}

      source
      theorem F_eq_card (N : ℕ) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 N) (hS' : NonTernary S) (hS'' : ∀ T ⊆ Finset.Icc 1 N, NonTernary T → S ⊆ T → T = S) :
      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

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

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

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

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

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

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