Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1994P5

module

public import Mathlib.Algebra.BigOperators.Ring.Finset
public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.Order.ConditionallyCompleteLattice.Basic
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Linarith.Lemmas
public import Mathlib.Tactic.Ring
public import Mathlib.Tactic.Ring.Basic

public section


/-!
# USA Mathematical Olympiad 1994, Problem 5

Let |U|, σ(U) and π(U) denote the number of elements, the sum, and the
product, respectively, of a finite set U of positive integers. (If U is the
empty set, |U| = 0, σ(U) = 0, π(U) = 1.) Let S be a finite set of positive
integers. As usual, we define (n k) = n! / (k! (n-k)!) for 0 ≤ k ≤ n and
(n k) = 0 otherwise. Prove that

  ∑_{U ⊆ S} (-1)^{|U|} (m - σ(U) choose |S|) = π(S)

for all integers m ≥ σ(S).
-/

namespace Usa1994P5

theorem usa1994_p5 (S : Finset ℕ) (hS : ∀ s ∈ S, 0 < s) (m : ℕ) (hm : ∑ s ∈ S, s ≤ m) :
    ∑ U ∈ S.powerset, (-1 : ℤ) ^ U.card * ((m - ∑ s ∈ U, s).choose S.card : ℤ)
      = ∏ s ∈ S, s := sorry

end Usa1994P5

File author(s): Kimi K3

This problem has a complete formalized solution.