Erdős Problem 139

Reference: erdosproblems.com/139

instance instInhabitedOfAddMonoid_formalConjectures {M : Type u_1} [AddMonoid M] : Inhabited M

Equations

• instInhabitedOfAddMonoid_formalConjectures = { default := 0 }

def IsArithmeticProgression {M : Type u_1} [Add M] (l : List M) : Prop

Equations

• IsArithmeticProgression l = ∃ (step : M), List.Chain' (fun (s t : M) => t = s + step) l

noncomputable def IsArithmeticProgression.step {M : Type u_1} [Add M] {l : List M} (hl : IsArithmeticProgression l) : M

Equations

• hl.step = Exists.choose hl

theorem IsArithmeticProgression.step_def {M : Type u_1} [Add M] {l : List M} (hl : IsArithmeticProgression l) : hl.step = Exists.choose hl

theorem IsArithmeticProgression.step_unique {M : Type u_1} [AddCancelMonoid M] {l : List M} (hl : IsArithmeticProgression l) (hl' : 1 < l.length) (u : M) (hu : List.Chain' (fun (s t : M) => t = s + u) l) : u = hl.step

theorem IsArithmeticProgression.step_zero {M : Type u_1} [AddMonoid M] [Inhabited M] {l : List M} (hl : IsArithmeticProgression l) (hl' : hl.step = 0) : l = List.replicate l.length l.headI

@[simp]

theorem IsArithmeticProgression_nil {M : Type u_1} [AddMonoid M] : IsArithmeticProgression []

theorem IsArithmeticProgression_singleton {M : Type u_1} [AddMonoid M] (a : M) : IsArithmeticProgression [a]

theorem IsArithmeticProgression_map_range {M : Type u_1} [AddCommMonoid M] (a b : M) (n : ℕ) : IsArithmeticProgression (List.map (fun (i : ℕ) => a + i • b) (List.range n))

theorem IsArithmeticProgression_pair {M : Type u_1} [AddCommGroup M] (a b : M) : IsArithmeticProgression [a, b]

def NonArithmeticSubset {M : Type u_1} [AddCommMonoid M] (k : ℕ) (A : Set M) : Prop

Say a set A is a k-non-arithmetic subset if it contains non non-trivial arithmetic progressions of length k.

Equations

• NonArithmeticSubset k A = ∀ (AP : List M) (hAP : IsArithmeticProgression AP), AP.length = k → {x : M | x ∈ AP} ⊆ A → hAP.step = 0

@[reducible, inline]

noncomputable abbrev r (k N : ℕ) : ℕ

Denote by $r_k(N)$ the size of the largest k-non-arithmetic subset of ${1,...,N}$

Equations

• r k N = (Finset.filter (fun (S : Finset ℤ) => NonArithmeticSubset k ↑S) (Finset.Icc 1 ↑N).powerset).sup Finset.card

theorem erdos_139 (k : ℕ) (hk : 1 ≤ k) : Filter.Tendsto (fun (N : ℕ) => ↑(r k N) / ↑N) Filter.atTop (nhds 0)

Erdős Problem 139: Let $r_k(N)$ be the size of the largest subset of ${1,...,N}$ which does not contain a non-trivial $k$-step arithmetic progression. Prove that $r_k(N) = o(N)$.