Erdős Problem 434

Reference: erdosproblems.com/434

@[reducible, inline]

abbrev Nat.IsRepresentableAs (n : ℕ) (A : Set ℕ) : Prop

A natural $n$ is representable as a set $A$ if it can be written as the sum of finitely many elements of $A$ (with repetition allowed).

Equations

• n.IsRepresentableAs A = ∃ (S : Multiset ℕ), (∀ a ∈ S, a ∈ A) ∧ S.sum = n

@[reducible, inline]

noncomputable abbrev Nat.NcardUnrepresentable (A : Set ℕ) : ℕ

The number of naturals that cannot be written as the sum of finitely many elements of the set $A$, with repetition allowed.

Equations

• Nat.NcardUnrepresentable A = {n : ℕ | ¬n.IsRepresentableAs A}.ncard

theorem erdos_434.parts.i (n k : ℕ) (hn : 1 ≤ n) (hk : 1 ≤ k) (h : k ≤ n) : IsGreatest {x : ℕ | ∃ (S : Set ℕ) (_ : S ⊆ Set.Icc 1 n) (_ : S.ncard = k), Nat.NcardUnrepresentable S = x} (Nat.NcardUnrepresentable sorry)

Let $k\leq n$. What choice of $A\subseteq\{1, \dots, n\}$ of size $|A| = k$ maximises the number of integers not representable as the sum of finitely many elements from $A$ (with repetitions allowed)? Is it $\{n, n - 1, ..., n - k + 1\}$?

theorem erdos_434.parts.ii : (∀ n ≥ 1, ∀ k ≥ 1, k ≤ n → IsGreatest {x : ℕ | ∃ (S : Set ℕ) (_ : S ⊆ Set.Icc 1 n) (_ : S.ncard = k), Nat.NcardUnrepresentable S = x} (Nat.NcardUnrepresentable (Set.Icc (n - k + 1) n))) ↔ sorry

Let $k\leq n$. Out of all $A\subseteq\{1, \dots, n\}$ of size $|A| = k$, does $A = \{n, n - 1, ..., n - k + 1\}$ maximise the number of integers not representable as the sum of finitely many elements from $A$ (with repetitions allowed)?