Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1969P2

import Mathlib.Tactic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

/-!
# International Mathematical Olympiad 1969, Problem 2

Let a₁, a₂, ..., aₙ be real constants, x be a real variable, and

  f(x) = cos(a₁ + x) + (1/2)cos(a₂ + x) + (1/4)cos(a₃ + x) + ...
         + (1/2ⁿ⁻¹)cos(aₙ + x).

Given that f(x₁) = f(x₂) = 0 for some x₁, x₂, prove that
x₂ - x₁ = mπ for some integer m.
-/

namespace Imo1969P2

open scoped Real

theorem imo1969_p2
    (x₁ x₂ : ℝ)
    (n : ℕ)
    (a : ℕ → ℝ)
    (f : ℝ → ℝ)
    (h₁ : ∀ x, f x = ∑ i ∈ Finset.range n, (Real.cos (a i + x)) / (2^i))
    (h₂ : f x₂ = 0)
    (h₃ : f x₁ = 0)
    (h₄: ∑ i ∈ Finset.range n, (Real.cos (a i) / (2 ^ i)) ≠ 0) :
    ∃ m : ℤ, x₂ - x₁ = m * π := sorry

end Imo1969P2

File author(s): Roozbeh Yousefzadeh

This problem has a complete formalized solution.

The solution was imported from IMO-Steps/imo_proofs/imo_1969_p2.lean.