Erdős Problem 330

Reference: erdosproblems.com/330

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

Rep A m means m is a sum of finitely many elements of A (i.e., representable by some finite number of terms, not a fixed order).

Equations

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

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

Integers not representable as a finite sum of elements of A while avoiding n.

Equations

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

def Erdos330.MinAsymptoticAddBasis (A : Set ℕ) : Prop

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

Equations

• Erdos330.MinAsymptoticAddBasis A = (A.IsAsymptoticAddBasis ∧ ∀ n ∈ A, ¬(A \ {n}).IsAsymptoticAddBasis)

theorem Erdos330.erdos_330_statement : (∀ (A : Set ℕ), MinAsymptoticAddBasis A → A.HasPosDensity → ∀ n ∈ A, (UnrepWithout A n).HasPosDensity) ↔ sorry

Suppose $A \subset \mathbb{N}$ is a minimal basis with positive density. Is it true that, for any $n \in A$, the (upper) density of integers which cannot be represented without using $n$ is positive?