Sets without arithmetic progressions of length three and Roth numbers #
This file defines sets without arithmetic progressions of length three, aka 3AP-free sets, and the Roth number of a set.
The corresponding notion, sets without geometric progressions of length three, are called 3GP-free sets.
The Roth number of a finset is the size of its biggest 3AP-free subset. This is a more general
definition than the one often found in mathematical literature, where the n
-th Roth number is
the size of the biggest 3AP-free subset of {0, ..., n - 1}
.
Main declarations #
ThreeGPFree
: Predicate for a set to be 3GP-free.ThreeAPFree
: Predicate for a set to be 3AP-free.mulRothNumber
: The multiplicative Roth number of a finset.addRothNumber
: The additive Roth number of a finset.rothNumberNat
: The Roth number of a natural, namelyaddRothNumber (Finset.range n)
.
TODO #
- Can
threeAPFree_iff_eq_right
be made more general? - Generalize
ThreeGPFree.image
to Freiman homs
References #
Tags #
3AP-free, Salem-Spencer, Roth, arithmetic progression, average, three-free
A set is 3AP-free if it does not contain any non-trivial arithmetic progression of length three.
This is also sometimes called a non averaging set or Salem-Spencer set.
Equations
Instances For
Whether a given finset is 3AP-free is decidable.
Whether a given finset is 3GP-free is decidable.
Arithmetic progressions of length three are reflected under 2
-Freiman homomorphisms.
Geometric progressions of length three are reflected under 2
-Freiman homomorphisms.
Arithmetic progressions of length three are unchanged under 2
-Freiman isomorphisms.
Geometric progressions of length three are unchanged under 2
-Freiman isomorphisms.
Alias of the reverse direction of threeGPFree_image
.
Geometric progressions of length three are unchanged under 2
-Freiman isomorphisms.
Arithmetic progressions of length three are reflected under 2
-Freiman homomorphisms.
Geometric progressions of length three are reflected under 2
-Freiman homomorphisms.
Arithmetic progressions of length three are unchanged under 2
-Freiman isomorphisms.
Geometric progressions of length three are unchanged under 2
-Freiman isomorphisms.
Arithmetic progressions of length three are preserved under semigroup homomorphisms.
Geometric progressions of length three are preserved under semigroup homomorphisms.
The additive Roth number of a finset is the cardinality of its biggest 3AP-free subset.
The usual Roth number corresponds to addRothNumber (Finset.range n)
, see rothNumberNat
.
Equations
- addRothNumber = { toFun := fun (s : Finset α) => Nat.findGreatest (fun (m : ℕ) => ∃ t ⊆ s, t.card = m ∧ ThreeAPFree ↑t) s.card, monotone' := ⋯ }
Instances For
The multiplicative Roth number of a finset is the cardinality of its biggest 3GP-free subset.
Equations
- mulRothNumber = { toFun := fun (s : Finset α) => Nat.findGreatest (fun (m : ℕ) => ∃ t ⊆ s, t.card = m ∧ ThreeGPFree ↑t) s.card, monotone' := ⋯ }
Instances For
Arithmetic progressions can be pushed forward along bijective 2-Freiman homs.
Arithmetic progressions can be pushed forward along bijective 2-Freiman homs.
Arithmetic progressions are preserved under 2-Freiman isos.
Arithmetic progressions are preserved under 2-Freiman isos.
The Roth number of a natural N
is the largest integer m
for which there is a subset of
range N
of size m
with no arithmetic progression of length 3.
Trivially, rothNumberNat N ≤ N
, but Roth's theorem (proved in 1953) shows that
rothNumberNat N = o(N)
and the construction by Behrend gives a lower bound of the form
N * exp(-C sqrt(log(N))) ≤ rothNumberNat N
.
A significant refinement of Roth's theorem by Bloom and Sisask announced in 2020 gives
rothNumberNat N = O(N / (log N)^(1+c))
for an absolute constant c
.
Equations
- rothNumberNat = { toFun := fun (n : ℕ) => addRothNumber (Finset.range n), monotone' := rothNumberNat.proof_1 }
Instances For
A verbose specialization of threeAPFree.le_addRothNumber
, sometimes convenient in
practice.
The Roth number is a subadditive function. Note that by Fekete's lemma this shows that
the limit rothNumberNat N / N
exists, but Roth's theorem gives the stronger result that this
limit is actually 0
.