Erdős Problem 318

References:

• erdosproblems.com/318
• [ErSt75] Erdős, P. and Straus, E. G., Solution to Problem 387. Nieuw Arch. Wisk. (1975), 183.
• [Sa75] Sattler, R., Solution to Problem 387. Nieuw Arch. Wisk. (1975), 184-189.
• [Sa82b] Sattler, R., On Erdős property P₁ for the arithmetical sequence. Nederl. Akad. Wetensch. Indag. Math. (1982), 347--352.
• [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

def Erdos318.P₁ (A : Set ℕ) : Prop

A set A : Set ℕ is said to have propery P₁ if for any nonconstant sequence f : A → {-1, 1}, one can always select a finite, nonempty subset S ⊆ A \ {0} such that ∑ n ∈ S, fₙ / n = 0. This is defined in [Sa82b].

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos318.erdos_318.univ : P₁ Set.univ

ℕ has property P₁. This is proved in [ErSt75].

theorem Erdos318.erdos_318.odd : P₁ {n : ℕ | Odd n}

Sattler proved in [Sa75] that the set of odd numbers has property P₁.

theorem Erdos318.erdos_318.squares : ¬P₁ {n : ℕ | IsSquare n}

The set of squares does not have property P₁.

theorem Erdos318.erdos_318.contain_single_even {A : Set ℕ} (hA : {n : ℕ | n ∈ A ∧ Even n}.ncard = 1) : ¬P₁ {n : ℕ | IsSquare n}

For any set A containing exactly one even number, A does not have property P₁. Sattler [Sa82] credits this observation to Erdős, who presumably found this after [ErGr80].

theorem Erdos318.erdos_318.posDensity : ∃ (A : Set ℕ), A.HasPosDensity ∧ ¬P₁ A

There exists a set A with positive density that does not have property P₁. #TODO: prove this lemma by assuming erdos_318.contain_single_even.

theorem Erdos318.erdos_318.infinite_AP {A : Set ℕ} (hA : A.IsAPOfLength ⊤) : P₁ A

Every infinite arithmetic progression has property P₁. This is proved in [Sa82b].

theorem Erdos318.erdos_318.square_excluding_one : sorry ↔ P₁ ({n : ℕ | IsSquare n} \ {1})

Does the set of squares excluding 1 have property P₁?