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})

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

A list version of Set.IsAPOfLengthWith. Useful when order preservation is required, for example when considering images under arbitrary functions.

Equations

• s.IsAPOfLengthWith l a d = (s = List.map (fun (n : ℕ) => a + n • d) (List.range l))

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 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 List.IsAPOfLengthWith.length {α : Type u_1} [AddCommMonoid α] {s : List α} {l : ℕ} {a d : α} (h : s.IsAPOfLengthWith l a d) : s.length = l

@[simp]

theorem List.IsAPOfLengthWith.zero {α : Type u_1} [AddCommMonoid α] {s : List α} {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 s is empty.

@[simp]

theorem List.IsAPOfLengthWith.one {α : Type u_1} [AddCommMonoid α] {s : List α} {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

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

A list version of Set.IsAPOfLength. Useful when order preservation is required, for example when considering images under arbitrary functions.

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 List.IsAPOfLength.length {α : Type u_1} [AddCommMonoid α] {s : List α} {l : ℕ} (h : s.IsAPOfLength l) : s.length = l

@[simp]

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

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

@[simp]

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

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

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

If a list 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}

theorem Set.IsAPOfLengthFree.maxCard_zero (N : ℕ) : maxCard 0 N = N

theorem Set.IsAPOfLengthFree.maxCard_one (N : ℕ) : maxCard 1 N = N

def ContainsMonoAPofLength {α : Type u_1} [AddCommMonoid α] {κ : Type} [Finite κ] {M : Set α} (coloring : ↑M → κ) (k : ℕ) : Prop

Equations

• ContainsMonoAPofLength coloring k = ∃ (c : κ) (ap : Set ↑M), ((fun (x : ↑M) => ↑x) '' ap).IsAPOfLength ↑k ∧ ∀ m ∈ ap, coloring m = c