Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1996P2

module

public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Data.Finset.Sort

public section


/-!
# USA Mathematical Olympiad 1996, Problem 2

Let S be a set of n positive integers. Let P be the set of all integers which
are the sum of one or more distinct elements of S. Show that we can find n
subsets of P whose union is P such that if a, b belong to the same subset,
then a ≤ 2b.
-/

namespace Usa1996P2

/-- The set of all sums of one or more distinct elements of `S`. -/
def SubsetSums (S : Finset ℕ) : Set ℕ :=
  {x | ∃ A : Finset ℕ, A ⊆ S ∧ A.Nonempty ∧ x = A.sum id}

theorem usa1996_p2 (S : Finset ℕ) (hS : ∀ s ∈ S, 0 < s) :
    ∃ T : Fin S.card → Set ℕ,
      (∀ i, T i ⊆ SubsetSums S) ∧
        (⋃ i, T i = SubsetSums S) ∧
          ∀ i, ∀ a ∈ T i, ∀ b ∈ T i, a ≤ 2 * b := sorry

end Usa1996P2

File author(s): Kimi K3

This problem has a complete formalized solution.