Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1985P3

module

public import Mathlib.Algebra.CharP.Lemmas
public import Mathlib.Algebra.Field.ZMod
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.RingTheory.Polynomial.Basic
public import Mathlib.Tactic.NormNum

public section


/-!
# International Mathematical Olympiad 1985, Problem 3

For any polynomial $P(x) = a_0 + a_1x + \dots + a_kx^k$ with integer coefficients, the
number of odd coefficients is denoted by $o(P)$. For $i = 0, 1, 2, \dots$ let
$Q_i(x) = (1 + x)^i$. Prove that if $i_1, i_2, \dots, i_n$ are integers satisfying
$0 \le i_1 < i_2 < \dots < i_n$, then
$$o(Q_{i_1} + Q_{i_2} + \dots + Q_{i_n}) \ge o(Q_{i_1}).$$
-/

namespace Imo1985P3

open Polynomial

/-- The number of odd coefficients of a polynomial with integer coefficients. -/
noncomputable def oddCount (P : ℤ[X]) : ℕ :=
  (P.support.filter fun n => Odd (P.coeff n)).card

theorem imo1985_p3 (S : Finset ℕ) (hS : S.Nonempty) :
    oddCount ((1 + X : ℤ[X]) ^ S.min' hS) ≤
      oddCount (∑ i ∈ S, (1 + X : ℤ[X]) ^ i) := sorry

end Imo1985P3

File author(s): Kimi K3

This problem has a complete formalized solution.