Progression-free sets meeting every infinite progression
DefinitionErdős Problem 199#✓fully proved
The statement that for every set \(A \subseteq \mathbb{R}\) containing no three-term arithmetic progression (no \(x, y, z \in A\) with \(x + z = 2y\) and \(x \ne y\)) there are reals \(a\) and \(d \ne 0\) with \(a + nd \notin A\) for every natural number \(n\), that is, the complement \(\mathbb{R} \setminus A\) contains the infinite arithmetic progression \(a, a + d, a + 2d, \dots\).
def threeAPFreeComplementContainsProgression : Prop :=
∀ A : Set ℝ, ThreeAPFree A → ∃ a d : ℝ, d ≠ 0 ∧ ∀ n : ℕ, a + n * d ∉ AUsed by 1
TheoremErdős Problem 199 is false#●ready to prove
There is a set \(A \subseteq \mathbb{R}\) containing no three-term arithmetic progression (no \(x, y, z \in A\) with \(x + z = 2y\) and \(x \ne y\)) such that for all reals \(a\) and \(d \ne 0\) some term \(a + nd\), with \(n\) a natural number, lies in \(A\): the complement \(\mathbb{R} \setminus A\) contains no infinite arithmetic progression \(a, a + d, a + 2d, \dots\) with \(d \ne 0\).
Baumgartner constructed such a set with the axiom of choice, from a basis of \(\mathbb{R}\) over \(\mathbb{Q}\).
public theorem_wanted threeAPFreeComplementContainsProgression_refuted :
¬ threeAPFreeComplementContainsProgressiondef threeAPFreeComplementContainsProgression : Prop :=
∀ A : Set ℝ, ThreeAPFree A → ∃ a d : ℝ, d ≠ 0 ∧ ∀ n : ℕ, a + n * d ∉ AWantedExt/Combinatorics/ThreeAPFreeComplementProgressionErdosProblem199Wanted.lean:38
Sources
- T. F. Bloom, Erdős Problems, Problem #199, https://www.erdosproblems.com/199 (status DISPROVED (LEAN)); resolution: J. E. Baumgartner, Partitioning vector spaces, J. Combin. Theory Ser. A 18 (1975), 231-233; formal proof plby/lean-proofs, erdosproblems.com/199: answered no by Baumgartner (construction using a Hamel basis), https://doi.org/10.1016/0097-3165(75)90011-8.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.