Documentation

FormalConjectures.ErdosProblems.«168»

Erdős Problem 168 #

Reference: erdosproblems.com/168

source
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
Instances For
    source
    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
    Instances For
      source
      @[reducible, inline]
      abbrev Erdos168.F (N : ℕ) :
      ℕ

      F N is the size of the largest non ternary subset of {1,...,N}.

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

        source
        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) :
        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 Erdos168.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 Erdos168.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 Erdos168.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)