Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1995P4

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.LinearAlgebra.Lagrange
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.LinearCombination.Lemmas
public import Mathlib.Tactic.Ring.Compare

public section


/-!
# USA Mathematical Olympiad 1995, Problem 4

a₀, a₁, a₂, ... is an infinite sequence of integers such that aₙ - aₘ is
divisible by n - m for all (unequal) n and m. For some polynomial p(x) we have
p(n) > |aₙ| for all n. Show that there is a polynomial q(x) such that
q(n) = aₙ for all n.
-/

namespace Usa1995P4

open Polynomial

theorem usa1995_p4 (a : ℕ → ℤ)
    (hdiv : ∀ n m : ℕ, ((n : ℤ) - (m : ℤ)) ∣ a n - a m)
    (hp : ∃ p : ℤ[X], ∀ n : ℕ, p.eval (n : ℤ) > |a n|) :
    ∃ q : ℚ[X], ∀ n : ℕ, q.eval (n : ℚ) = (a n : ℚ) := sorry

end Usa1995P4

File author(s): Kimi K3

This problem has a complete formalized solution.