Erdős Problem 330

Reference: erdosproblems.com/330

def Erdos330.Rep (A : Set ℕ) (m h : ℕ) : Prop

Rep A m h means m is a sum of at most h elements of Ax.

Equations

• Erdos330.Rep A m h = ∃ k ≤ h, ∃ (f : Fin k → ℕ), (∀ (i : Fin k), f i ∈ A) ∧ ∑ i : Fin k, f i = m

def Erdos330.UnrepWithout (A : Set ℕ) (n h : ℕ) : Set ℕ

Integers not representable as a finite sum of elements with at most h terms of A while avoiding n.

Equations

• Erdos330.UnrepWithout A n h = {m : ℕ | ¬Erdos330.Rep (A \ {n}) m h}

def Erdos330.MinAsymptoticAddBasisOfOrder (A : Set ℕ) (h : ℕ) : Prop

An asymptotic additive basis of order h is minimal when one cannot obtain an asymptotic additive basis by removing any element from it.

Equations

• Erdos330.MinAsymptoticAddBasisOfOrder A h = (A.IsAsymptoticAddBasisOfOrder h ∧ ∀ n ∈ A, ¬(A \ {n}).IsAsymptoticAddBasisOfOrder h)

theorem Erdos330.erdos_330_statement : sorry ↔ ∃ (A : Set ℕ) (h : ℕ), MinAsymptoticAddBasisOfOrder A h ∧ A.HasPosDensity ∧ ∀ n ∈ A, (UnrepWithout A n h).HasPosDensity

Does there exist a minimal basis $A \subset \mathbb{N}$ with positive density such that, for any $n \in A$, the (upper) density of integers which cannot be represented without using $n$ is positive?