/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import Mathlib.Algebra.Module.NatInt
public import Mathlib.Data.ENat.Lattice
public import Mathlib.Data.Set.Card
import Mathlib.Tactic.IntervalCases@[expose] public sectionArithmetic 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.
variable {α : Type*} [AddCommMonoid α]
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 s.IsAPOfLengthWith l a d, where l : ℕ∞ may take the infinite
value ⊤.
def Set.IsAPOfLengthWith (s : Set α) (l : ℕ∞) (a d : α) : Prop :=
ENat.card s = l ∧ s = {a + n • d | (n : ℕ) (_ : n < l)}
A list version of Set.IsAPOfLengthWith. Useful when order preservation is required, for example
when considering images under arbitrary functions.
def List.IsAPOfLengthWith (s : List α) (l : ℕ) (a d : α) : Prop :=
s = (List.range l).map (fun n ↦ a + n • d) ∨ s = (List.range l).reverse.map (fun n ↦ a + n • d)namespace Set.IsAPOfLengthWithvariable {s : Set α} {l : ℕ∞} {a d : α}theorem card (h : s.IsAPOfLengthWith l a d) : ENat.card s = l := h.1theorem eq (h : s.IsAPOfLengthWith l a d) : s = {a + n • d | (n : ℕ) (_ : n < l)} := h.2
An arithmetic progression with first term a and difference d is of length zero if and only
if s is empty.
@[simp]
theorem zero : s.IsAPOfLengthWith 0 a d ↔ s = ∅ := α:Type u_1inst✝:AddCommMonoid αs:Set αa:αd:α⊢ s.IsAPOfLengthWith 0 a d ↔ s = ∅ All goals completed! 🐙
An arithmetic progression with first term a and difference d is of length one if and only
if s is a singleton.
@[simp]
theorem one : s.IsAPOfLengthWith 1 a d ↔ s = {a} := α:Type u_1inst✝:AddCommMonoid αs:Set αa:αd:α⊢ s.IsAPOfLengthWith 1 a d ↔ s = {a} All goals completed! 🐙end Set.IsAPOfLengthWithnamespace List.IsAPOfLengthWithvariable {s : List α} {l : ℕ} {a d : α}theorem length (h : s.IsAPOfLengthWith l a d) : s.length = l := α:Type u_1inst✝:AddCommMonoid αs:List αl:ℕa:αd:αh:s.IsAPOfLengthWith l a d⊢ s.length = l
α:Type u_1inst✝:AddCommMonoid αs:List αl:ℕa:αd:αh✝:s = map (fun n ↦ a + n • d) (range l)⊢ s.length = lα:Type u_1inst✝:AddCommMonoid αs:List αl:ℕa:αd:αh✝:s = map (fun n ↦ a + n • d) (range l).reverse⊢ s.length = l α:Type u_1inst✝:AddCommMonoid αs:List αl:ℕa:αd:αh✝:s = map (fun n ↦ a + n • d) (range l)⊢ s.length = lα:Type u_1inst✝:AddCommMonoid αs:List αl:ℕa:αd:αh✝:s = map (fun n ↦ a + n • d) (range l).reverse⊢ s.length = l All goals completed! 🐙
An arithmetic progression with first term a and difference d is of length zero if and only
if s is empty.
@[simp]
theorem zero : s.IsAPOfLengthWith 0 a d ↔ s = [] := α:Type u_1inst✝:AddCommMonoid αs:List αa:αd:α⊢ s.IsAPOfLengthWith 0 a d ↔ s = []
All goals completed! 🐙
An arithmetic progression with first term a and difference d is of length one if and only
if s is a singleton.
@[simp]
theorem one : s.IsAPOfLengthWith 1 a d ↔ s = [a] := α:Type u_1inst✝:AddCommMonoid αs:List αa:αd:α⊢ s.IsAPOfLengthWith 1 a d ↔ s = [a]
All goals completed! 🐙end List.IsAPOfLengthWith
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.
α:Type u_2inst✝¹:DecidableEq αinst✝:AddCommGroup αa:αb:αhab:a ≠ b⊢ ↑({b}.card + 1) = 2 ∧ {a, b} = {x | ∃ n ≤ 1, a + n • (b - a) = x}
α:Type u_2inst✝¹:DecidableEq αinst✝:AddCommGroup αa:αb:αhab:a ≠ b⊢ {a, b} = {x | ∃ n ≤ 1, a + n • (b - a) = x}
refine Set.ext fun x => ⟨fun h ↦ ?_, fun ⟨n, ⟨_, _⟩⟩ ↦ α:Type u_2inst✝¹:DecidableEq αinst✝:AddCommGroup αa:αb:αhab:a ≠ bx:αx✝:x ∈ {x | ∃ n ≤ 1, a + n • (b - a) = x}n:ℕleft✝:n ≤ 1right✝:a + n • (b - a) = x⊢ x ∈ {a, b} α:Type u_2inst✝¹:DecidableEq αinst✝:AddCommGroup αa:αb:αhab:a ≠ bx:αx✝:x ∈ {x | ∃ n ≤ 1, a + n • (b - a) = x}n:ℕleft✝:0 ≤ 1right✝:a + 0 • (b - a) = x⊢ x ∈ {a, b}α:Type u_2inst✝¹:DecidableEq αinst✝:AddCommGroup αa:αb:αhab:a ≠ bx:αx✝:x ∈ {x | ∃ n ≤ 1, a + n • (b - a) = x}n:ℕleft✝:1 ≤ 1right✝:a + 1 • (b - a) = x⊢ x ∈ {a, b} α:Type u_2inst✝¹:DecidableEq αinst✝:AddCommGroup αa:αb:αhab:a ≠ bx:αx✝:x ∈ {x | ∃ n ≤ 1, a + n • (b - a) = x}n:ℕleft✝:0 ≤ 1right✝:a + 0 • (b - a) = x⊢ x ∈ {a, b}α:Type u_2inst✝¹:DecidableEq αinst✝:AddCommGroup αa:αb:αhab:a ≠ bx:αx✝:x ∈ {x | ∃ n ≤ 1, a + n • (b - a) = x}n:ℕleft✝:1 ≤ 1right✝:a + 1 • (b - a) = x⊢ x ∈ {a, b} All goals completed! 🐙⟩
cases h with
α:Type u_2inst✝¹:DecidableEq αinst✝:AddCommGroup αa:αb:αhab:a ≠ bx:αhl:x = a⊢ x ∈ {x | ∃ n ≤ 1, a + n • (b - a) = x} α:Type u_2inst✝¹:DecidableEq αinst✝:AddCommGroup αa:αb:αhab:a ≠ bx:αhl:x = a⊢ 0 ≤ 1 ∧ a + 0 • (b - a) = x; All goals completed! 🐙
α:Type u_2inst✝¹:DecidableEq αinst✝:AddCommGroup αa:αb:αhab:a ≠ bx:αhr:x ∈ {b}⊢ x ∈ {x | ∃ n ≤ 1, a + n • (b - a) = x} exact ⟨1, α:Type u_2inst✝¹:DecidableEq αinst✝:AddCommGroup αa:αb:αhab:a ≠ bx:αhr:x ∈ {b}⊢ 1 ≤ 1 All goals completed! 🐙, α:Type u_2inst✝¹:DecidableEq αinst✝:AddCommGroup αa:αb:αhab:a ≠ bx:αhr:x ∈ {b}⊢ a + 1 • (b - a) = x All goals completed! 🐙⟩
The set {a, b} : Set ℕ 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) :
Set.IsAPOfLengthWith {a, b} 2 a (b - a) := a:ℕb:ℕhab:a < b⊢ {a, b}.IsAPOfLengthWith 2 a (b - a)
a:ℕb:ℕhab:a < bn:ℕh:b = a + n + 1⊢ {a, b}.IsAPOfLengthWith 2 a (b - a)
a:ℕb:ℕhab:a < bn:ℕh:b = a + n + 1⊢ {a, a + (n + 1)} = {x | ∃ n_1 ≤ 1, a + n_1 * (n + 1) = x}
exact Set.ext fun x => ⟨fun a => a✝:ℕb:ℕhab:a < bn:ℕh:b = a + n + 1x:ℕa:x ∈ {a✝, a✝ + (n + 1)}⊢ x ∈ {x | ∃ n_1 ≤ 1, a✝ + n_1 * (n + 1) = x} All goals completed! 🐙, fun ⟨w, ⟨_, _⟩⟩ => a:ℕb:ℕhab:a < bn:ℕh:b = a + n + 1x:ℕx✝:x ∈ {x | ∃ n_1 ≤ 1, a✝ + n_1 * (n + 1) = x}w:ℕleft✝:w ≤ 1right✝:a + w * (n + 1) = x⊢ x ∈ {a✝, a✝ + (n + 1)} a:ℕb:ℕhab:a < bn:ℕh:b = a + n + 1x:ℕx✝:x ∈ {x | ∃ n_1 ≤ 1, a✝ + n_1 * (n + 1) = x}w:ℕleft✝:0 ≤ 1right✝:a + 0 * (n + 1) = x⊢ x ∈ {a✝, a✝ + (n + 1)}a:ℕb:ℕhab:a < bn:ℕh:b = a + n + 1x:ℕx✝:x ∈ {x | ∃ n_1 ≤ 1, a✝ + n_1 * (n + 1) = x}w:ℕleft✝:1 ≤ 1right✝:a + 1 * (n + 1) = x⊢ x ∈ {a✝, a✝ + (n + 1)} a:ℕb:ℕhab:a < bn:ℕh:b = a + n + 1x:ℕx✝:x ∈ {x | ∃ n_1 ≤ 1, a✝ + n_1 * (n + 1) = x}w:ℕleft✝:0 ≤ 1right✝:a + 0 * (n + 1) = x⊢ x ∈ {a✝, a✝ + (n + 1)}a:ℕb:ℕhab:a < bn:ℕh:b = a + n + 1x:ℕx✝:x ∈ {x | ∃ n_1 ≤ 1, a✝ + n_1 * (n + 1) = x}w:ℕleft✝:1 ≤ 1right✝:a + 1 * (n + 1) = x⊢ x ∈ {a✝, a✝ + (n + 1)} All goals completed! 🐙⟩
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.
def Set.IsAPOfLength (s : Set α) (l : ℕ∞) : Prop :=
∃ a d : α, s.IsAPOfLengthWith l a d
A list version of Set.IsAPOfLength. Useful when order preservation is required, for example
when considering images under arbitrary functions.
def List.IsAPOfLength (s : List α) (l : ℕ) : Prop :=
∃ a d : α, s.IsAPOfLengthWith l a dnamespace Set.IsAPOfLengthopen Set.IsAPOfLengthWithvariable {s : Set α} {l : ℕ∞}theorem card (h : s.IsAPOfLength l) : ENat.card s = l := h.choose_spec.choose_spec.1theorem eq (h : s.IsAPOfLength l) : ∃ a d : α, s = {a + n • d | (n : ℕ) (_ : n < l)} :=
⟨h.choose, h.choose_spec.choose, h.choose_spec.choose_spec.2⟩Only the empty set is a finite arithmetic progression of length $0$.
@[simp] theorem zero : s.IsAPOfLength 0 ↔ s = ∅ := α:Type u_1inst✝:AddCommMonoid αs:Set α⊢ s.IsAPOfLength 0 ↔ s = ∅ All goals completed! 🐙Only singletons are finite arithmetic progressions of length $1$.
@[simp] theorem one : s.IsAPOfLength 1 ↔ ∃ a, s = {a} := α:Type u_1inst✝:AddCommMonoid αs:Set α⊢ s.IsAPOfLength 1 ↔ ∃ a, s = {a} All goals completed! 🐙
If a set is an arithmetic progression of lengths l₁ and l₂, then the lengths are
equal.
All goals completed! 🐙end Set.IsAPOfLengthnamespace List.IsAPOfLengthopen List.IsAPOfLengthWithvariable {s : List α} {l : ℕ}theorem length (h : s.IsAPOfLength l) : s.length = l := α:Type u_1inst✝:AddCommMonoid αs:List αl:ℕh:s.IsAPOfLength l⊢ s.length = l
α:Type u_1inst✝:AddCommMonoid αs:List αl:ℕw✝¹:αw✝:αh:s.IsAPOfLengthWith l w✝¹ w✝⊢ s.length = l
All goals completed! 🐙Only the empty list is a finite arithmetic progression of length $0$.
@[simp] theorem zero : s.IsAPOfLength 0 ↔ s = [] := α:Type u_1inst✝:AddCommMonoid αs:List α⊢ s.IsAPOfLength 0 ↔ s = [] All goals completed! 🐙Only singletons are finite arithmetic progressions of length $1$.
@[simp] theorem one : s.IsAPOfLength 1 ↔ ∃ a, s = [a] := α:Type u_1inst✝:AddCommMonoid αs:List α⊢ s.IsAPOfLength 1 ↔ ∃ a, s = [a] All goals completed! 🐙
If a list is an arithmetic progression of lengths l₁ and l₂, then the lengths are
equal.
All goals completed! 🐙end List.IsAPOfLengththeorem Set.isAPOfLength_pair {α : Type*} [DecidableEq α] [AddCommGroup α] {a b : α} (hab : a ≠ b) :
Set.IsAPOfLength {a, b} 2 :=
⟨a, b - a, Set.isAPOfLengthWith_pair hab⟩theorem Nat.isAPOfLength_pair {a b : ℕ} (hab : a < b) :
Set.IsAPOfLength {a, b} 2 :=
⟨a, b - a, Nat.isAPOfLengthWith_pair hab⟩The empty set is not an arithmetic progression of positive length.
theorem Set.not_isAPOfLength_empty {l : ℕ∞} (hl : 0 < l) :
¬Set.IsAPOfLength (∅ : Set α) l :=
fun h ↦ α:Type u_1inst✝:AddCommMonoid αl:ℕ∞hl:0 < lh:∅.IsAPOfLength l⊢ False All goals completed! 🐙
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. -
def Set.IsAPOfLengthFree (s : Set α) (l : ℕ∞) : Prop :=
∀ t ⊆ s, t.IsAPOfLength l → l ≤ 1
Any set is free of arithmetic progressions of length 1, because such APs are all trivial.
theorem Set.isAPOfLengthFree_one (s : Set α) : s.IsAPOfLengthFree 1 := α:Type u_1inst✝:AddCommMonoid αs:Set α⊢ s.IsAPOfLengthFree 1
All goals completed! 🐙
Any set is free of arithmetic progressions of length 0, because such APs are all trivial.
theorem Set.isAPOfLengthFree_zero (s : Set α) : s.IsAPOfLengthFree 0 := α:Type u_1inst✝:AddCommMonoid αs:Set α⊢ s.IsAPOfLengthFree 0
All goals completed! 🐙Any non-trivial arithmetic progression cannot be free of arithmetic progressions.
theorem Set.IsAPOfLength.not_isAPOfLengthFree {s : Set α} {l : ℕ∞}
(hs : s.IsAPOfLength l) (hl : 1 < l) : ¬s.IsAPOfLengthFree l := α:Type u_1inst✝:AddCommMonoid αs:Set αl:ℕ∞hs:s.IsAPOfLength lhl:1 < l⊢ ¬s.IsAPOfLengthFree l
All goals completed! 🐙Define the largest possible size of a subset of ${1, \dots, N}$ that does not contain any non-trivial $k$-term arithmetic progression.
noncomputable def Set.IsAPOfLengthFree.maxCard (k : ℕ) (N : ℕ) : ℕ :=
sSup {Finset.card S | (S) (_ : S ⊆ Finset.Icc 1 N) (_ : (S : Set ℕ).IsAPOfLengthFree k)}theorem Set.IsAPOfLengthFree.maxCard_zero (N : ℕ) : maxCard 0 N = N := N:ℕ⊢ maxCard 0 N = N
N:ℕ⊢ sSup {x | ∃ S ⊆ Finset.Icc 1 N, S.card = x} = N
N:ℕ⊢ IsGreatest {x | ∃ S ⊆ Finset.Icc 1 N, S.card = x} N
N:ℕ⊢ N ∈ upperBounds {x | ∃ S ⊆ Finset.Icc 1 N, S.card = x}
N:ℕS:Finset ℕhS:S ⊆ Finset.Icc 1 N⊢ S.card ≤ N
All goals completed! 🐙theorem Set.IsAPOfLengthFree.maxCard_one (N : ℕ) : maxCard 1 N = N := N:ℕ⊢ maxCard 1 N = N
nth_rw 2 [N:ℕ⊢ maxCard 1 N = maxCard 0 NN:ℕ⊢ maxCard 1 N = maxCard 0 N
All goals completed! 🐙
A set A contains an arithmetic progression of length k with difference d.
def Set.ContainsAP (A : Set α) (k : ℕ) (d : α) : Prop :=
∃ a, ∃ s, s ⊆ A ∧ s.IsAPOfLengthWith (k : ℕ∞) a ddef ContainsMonoAPofLength {κ : Type} [Finite κ] {M : Set α}
(coloring : M → κ) (k : ℕ) : Prop :=
∃ c : κ, ∃ ap : Set M, ((·.1) '' ap).IsAPOfLength k ∧
∀ m ∈ ap, coloring m = c
A function f : β → α has a monotone k-term arithmetic progression if there exists a choice
of indices b 1 < b 2 < ... < b k such that the subsequence f (b i) forms an increasing or
decreasing arithmetic progression of length k.
def HasMonotoneAP {β : Type*} [Preorder β] (f : β → α) (k : ℕ) : Prop :=
∃ l : List β, (l.map f).IsAPOfLength k ∧ l.Pairwise (· < ·)
Define the largest possible size of a subset of a finset s that does not contain
any non-trivial k-term arithmetic progression.
noncomputable def Finset.maxAPFreeCard (k : ℕ) (s : Finset α) : ℕ :=
open scoped Classical in
(s.powerset.filter fun t : Finset α ↦ (t : Set α).IsAPOfLengthFree k).sup Finset.card