Arithmetic Progressions

Main definitions:

• Set.IsAPOfLengthWith (s : Set α) (l : ℕ∞) (a d : α) : predicate asserting that s is the set consisting of an arithmetic progression of length l (possibly infinite) with first term a and difference d. Useful for cases in which additional conditions need to be applied to the individual terms and/or difference.
• Set.IsAPOfLength (s : Set α) (l : ℕ∞) : predicate asserting that s is the set consisting of an arithmetic progression of length l, for some some first term and difference.

def Set.IsAPOfLengthWith {α : Type u_1} [AddCommMonoid α] (s : Set α) (l : ℕ∞) (a d : α) : Prop

A set $S$ is an arithmetic progression of length $l$ with first term $a$ and difference $d$ if $S = \{a, a + d, ..., a + (l - 1)d\}$, if $l$ if finite, else $S = {a, a + d, a + 2d, ...}. This can be written as Set.IsAPOfLengthWith a l a d, where l : ℕ∞ may take the infinite value ⊤.

Equations

• s.IsAPOfLengthWith l a d = (ENat.card ↑s = l ∧ s = {x : α | ∃ (n : ℕ) (_ : ↑n < l), a + n • d = x})

theorem Set.IsAPOfLengthWith.card {α : Type u_1} [AddCommMonoid α] {s : Set α} {l : ℕ∞} {a d : α} (h : s.IsAPOfLengthWith l a d) : ENat.card ↑s = l

theorem Set.IsAPOfLengthWith.eq {α : Type u_1} [AddCommMonoid α] {s : Set α} {l : ℕ∞} {a d : α} (h : s.IsAPOfLengthWith l a d) : s = {x : α | ∃ (n : ℕ) (_ : ↑n < l), a + n • d = x}

@[simp]

theorem Set.IsAPOfLengthWith.zero {α : Type u_1} [AddCommMonoid α] {s : Set α} {a d : α} : s.IsAPOfLengthWith 0 a d ↔ s = ∅

An arithmetic progression with first term a and difference d is of length zero if and only if the difference is non-zero and s is empty.

@[simp]

theorem Set.IsAPOfLengthWith.one {α : Type u_1} [AddCommMonoid α] {s : Set α} {a d : α} : s.IsAPOfLengthWith 1 a d ↔ s = {a}

An arithmetic progression with first term a and difference d is of length one if and only if s is a singleton.

theorem Set.isAPOfLengthWith_pair {α : Type u_2} [DecidableEq α] [AddCommGroup α] {a b : α} (hab : a ≠ b) : {a, b}.IsAPOfLengthWith 2 a (b - a)

In an abelian additive group α, the set {a, b} with a ≠ b is an arithmetic progression of length 2 with first term a and difference b - a.

theorem Nat.isAPOfLengthWith_pair {a b : ℕ} (hab : a < b) : {a, b}.IsAPOfLengthWith 2 a (b - a)

The set {a, b} : Set ℕ with a < b is an arithmetic progression of length 2 with first term a and difference b - a.

def Set.IsAPOfLength {α : Type u_1} [AddCommMonoid α] (s : Set α) (l : ℕ∞) : Prop

The predicate that a set s is an arithmetic progression of length l (possibly infinite). This predicate does not assert a specific value for the first term or the difference of the arithmetic progression.

Equations

• s.IsAPOfLength l = ∃ (a : α) (d : α), s.IsAPOfLengthWith l a d

theorem Set.IsAPOfLength.card {α : Type u_1} [AddCommMonoid α] {s : Set α} {l : ℕ∞} (h : s.IsAPOfLength l) : ENat.card ↑s = l

theorem Set.IsAPOfLength.eq {α : Type u_1} [AddCommMonoid α] {s : Set α} {l : ℕ∞} (h : s.IsAPOfLength l) : ∃ (a : α) (d : α), s = {x : α | ∃ (n : ℕ) (_ : ↑n < l), a + n • d = x}

@[simp]

theorem Set.IsAPOfLength.zero {α : Type u_1} [AddCommMonoid α] {s : Set α} : s.IsAPOfLength 0 ↔ s = ∅

Only the empty set is a finite arithmetic progression of length $0$.

@[simp]

theorem Set.IsAPOfLength.one {α : Type u_1} [AddCommMonoid α] {s : Set α} : s.IsAPOfLength 1 ↔ ∃ (a : α), s = {a}

Only singletons are finite arithmetic progressions of length $1$.

theorem Set.IsAPOfLength.congr {α : Type u_1} [AddCommMonoid α] {s : Set α} {l₁ l₂ : ℕ∞} (h₁ : s.IsAPOfLength l₁) (h₂ : s.IsAPOfLength l₂) : l₁ = l₂

If a set is an arithmetic progression of lengths l₁ and l₂, then the lengths are equal.

theorem Set.isAPOfLength_pair {α : Type u_2} [DecidableEq α] [AddCommGroup α] {a b : α} (hab : a ≠ b) : {a, b}.IsAPOfLength 2

theorem Nat.isAPOfLength_pair {a b : ℕ} (hab : a < b) : {a, b}.IsAPOfLength 2

theorem Set.not_isAPOfLength_empty {α : Type u_1} [AddCommMonoid α] {l : ℕ∞} (hl : 0 < l) : ¬∅.IsAPOfLength l

The empty set is not an arithmetic progression of positive length.

def Set.IsAPOfLengthFree {α : Type u_1} [AddCommMonoid α] (s : Set α) (l : ℕ∞) : Prop

We say that a set s is free of arithmetic progressions of length l if s contains no non-trivial arithmetic progressions of length l. Written as Set.IsAPOfLengthFree s l. -

Equations

• s.IsAPOfLengthFree l = ∀ t ⊆ s, t.IsAPOfLength l → l ≤ 1

theorem Set.isAPOfLengthFree_one {α : Type u_1} [AddCommMonoid α] (s : Set α) : s.IsAPOfLengthFree 1

Any set is free of arithmetic progressions of length 1, because such APs are all trivial.

theorem Set.isAPOfLengthFree_zero {α : Type u_1} [AddCommMonoid α] (s : Set α) : s.IsAPOfLengthFree 0

Any set is free of arithmetic progressions of length 0, because such APs are all trivial.

theorem Set.IsAPOfLength.not_isAPOfLengthFree {α : Type u_1} [AddCommMonoid α] {s : Set α} {l : ℕ∞} (hs : s.IsAPOfLength l) (hl : 1 < l) : ¬s.IsAPOfLengthFree l

Any non-trivial arithmetic progression cannot be free of arithmetic progressions.

noncomputable def Set.IsAPOfLengthFree.maxCard (k N : ℕ) : ℕ

Define the largest possible size of a subset of $\{1, \dots, N\}$ that does not contain any non-trivial $k$-term arithmetic progression.

Equations

• Set.IsAPOfLengthFree.maxCard k N = sSup {x : ℕ | ∃ (S : Finset ℕ) (_ : S ⊆ Finset.Icc 1 N) (_ : (↑S).IsAPOfLengthFree ↑k), S.card = x}