Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1991P2

module

public import Mathlib.Algebra.BigOperators.Group.Finset.Powerset
public import Mathlib.Algebra.BigOperators.Intervals
public import Mathlib.Algebra.BigOperators.Ring.Finset
public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Rat.Star
public import Mathlib.Tactic.FieldSimp
public import Mathlib.Tactic.Positivity.Basic

public section


/-!
# USA Mathematical Olympiad 1991, Problem 2

For each non-empty subset of {1, 2, ... , n} take the sum of the elements
divided by the product. Show that the sum of the resulting quantities is
n² + 2n - (n + 1)sₙ, where sₙ = 1 + 1/2 + 1/3 + ... + 1/n.
-/

namespace Usa1991P2

open Finset

theorem usa1991_p2 (n : ℕ) :
    ∑ S ∈ (Finset.Icc 1 n).powerset.erase ∅, (∑ i ∈ S, (i : ℚ)) / (∏ i ∈ S, (i : ℚ)) =
      (n : ℚ)^2 + 2 * n - (n + 1) * ∑ i ∈ Finset.Icc 1 n, (1 : ℚ) / i := sorry

end Usa1991P2

File author(s): Kimi K3

This problem has a complete formalized solution.