Square-sum-free sets

DefinitionSquare-sum-free sets#✓fully proved

A finite set \(A\) of natural numbers is square-sum-free if for all \(a, b \in A\), not necessarily distinct, the sum \(a + b\) is not a perfect square.

def IsSquareSumFree (A : Finset ℕ) : Prop :=
  ∀ a ∈ A, ∀ b ∈ A, ¬ IsSquare (a + b)

Used by 1

Used byMaximum size of a square-sum-free set

DefinitionMaximum size of a square-sum-free set#✓fully proved

For a natural number \(N\), the largest size of a set \(A \subseteq \{1, \dots, N\}\) such that no sum \(a + b\) with \(a, b \in A\), not necessarily distinct, is a perfect square.

noncomputable def maxSquareSumFreeSize (N : ℕ) : ℕ :=
  sSup {k : ℕ | ∃ A : Finset ℕ, A ⊆ Finset.Icc 1 N ∧ IsSquareSumFree A ∧ A.card = k}

Uses 1 · Used by 1

Statement usesSquare-sum-free sets

Used byErdős Problem 438 (statement)

DefinitionErdős Problem 438 (statement)#✓fully proved

For a natural number \(N\), let \(M(N)\) be the largest size of a set \(A \subseteq \{1, \dots, N\}\) such that no sum \(a + b\) with \(a, b \in A\), not necessarily distinct, is a perfect square. This is the statement that \(M(N) / N \to 11/32\) as \(N \to \infty\).

def maxSquareSumFreeDensity : Prop :=
  Filter.Tendsto (fun N : ℕ => (maxSquareSumFreeSize N : ℝ) / N) Filter.atTop (nhds (11 / 32))

Uses 1 · Used by 1

Statement usesMaximum size of a square-sum-free set

Used byMaximal density of square-sum-free sets (Erdős Problem 438)

TheoremMaximal density of square-sum-free sets (Erdős Problem 438)#●ready to prove

For a natural number \(N\), let \(M(N)\) be the largest size of a set \(A \subseteq \{1, \dots, N\}\) such that no sum \(a + b\) with \(a, b \in A\), not necessarily distinct, is a perfect square. Then \(M(N) / N \to 11/32\) as \(N \to \infty\).

Khalfalah, Lodha and Szemerédi proved \(M(N) \le (11/32 + o(1)) N\), and Massias's example (the integers congruent to one of \(1, 5, 9, 13, 14, 17, 21, 25, 26, 29, 30\) modulo \(32\)) gives \(M(N) \ge 11N/32 + O(1)\).

public theorem_wanted maxSquareSumFreeDensity_holds : maxSquareSumFreeDensity

Sources

• T. F. Bloom, Erdős Problems, Problem #438, https://www.erdosproblems.com/438 (status SOLVED); resolution: A. Khalfalah, S. Lodha and E. Szemerédi, Tight bound for the density of sequence of integers the sum of no two of which is a perfect square, Discrete Math. (2002), 243-255, max |A| ≤ (11/32 + o(1)) N; Massias's residues mod 32 give the lower bound (erdosproblems.com/438).

Uses 1

Statement usesErdős Problem 438 (statement)

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.