erdos_434.parts.i

Let $k \le 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, \dots, n - k + 1\}$?

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

Recent Submissions

No submissions yet. Be the first to attempt this problem.