Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2006P2

module

public import Mathlib.Algebra.BigOperators.Intervals
public import Mathlib.Algebra.BigOperators.Ring.Finset
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Linarith.Lemmas
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.LinearCombination.Lemmas
public import Mathlib.Tactic.NormNum.Ineq
public import Mathlib.Tactic.Ring.Basic
public import Mathlib.Tactic.Zify

public section


/-!
# USA Mathematical Olympiad 2006, Problem 2

For a given positive integer k find, in terms of k, the minimum value
of N for which there is a set of 2k + 1 distinct positive integers
that has sum greater than N but every subset of size k has sum at
most N / 2.
-/

namespace Usa2006P2

/- determine -/ abbrev solution : ℕ → ℕ := sorry

-- We formalise "every subset of size k has sum at most N / 2" as
-- `2 * ∑ x ∈ t, x ≤ N`, which is equivalent for natural numbers.
theorem usa2006_p2 (k : ℕ) (hk : 0 < k) :
    IsLeast {N : ℕ | ∃ s : Finset ℕ, s.card = 2 * k + 1 ∧ (∀ x ∈ s, 0 < x) ∧
        N < ∑ x ∈ s, x ∧ ∀ t ⊆ s, t.card = k → 2 * ∑ x ∈ t, x ≤ N}
      (solution k) := sorry

end Usa2006P2

File author(s): Kimi K3

This problem has a complete formalized solution.