Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1984P3

module

public import Mathlib.Tactic
public import Mathlib.Analysis.SpecialFunctions.Complex.Arg
public import Mathlib.Analysis.Complex.Trigonometric
public import Mathlib.Analysis.Real.Pi.Bounds
public import Mathlib.Data.Fintype.Pigeonhole

public section


/-!
# International Mathematical Olympiad 1984, Problem 3

In the plane two different points O and A are given. For each point X of the plane,
other than O, denote by a(X) the measure of the angle between OA and OX in radians,
counterclockwise from OA (0 ≤ a(X) < 2π). Let C(X) be the circle with center O and
radius of length OX + a(X)/OX. Each point of the plane is colored by one of a finite
number of colors. Prove that there exists a point Y for which a(Y) > 0 such that its
color appears on the circumference of the circle C(Y).
-/

namespace Imo1984P3

/-- The angle `a(X)` from the problem statement: the measure in radians, counterclockwise
from `OA`, of the angle between `OA` and `OX`, taking values in `[0, 2 * π)`.
(The problem only uses this for `X ≠ O`; we define it for all `X`.) -/
noncomputable def aang (O A X : ℂ) : ℝ :=
  if 0 ≤ Complex.arg ((X - O) / (A - O)) then Complex.arg ((X - O) / (A - O))
    else Complex.arg ((X - O) / (A - O)) + 2 * Real.pi

theorem imo1984_p3 {ι : Type*} [Fintype ι] (O A : ℂ) (hOA : O ≠ A) (color : ℂ → ι) :
    ∃ Y : ℂ, Y ≠ O ∧ 0 < aang O A Y ∧
      ∃ Z : ℂ, ‖Z - O‖ = ‖Y - O‖ + aang O A Y / ‖Y - O‖ ∧ color Z = color Y := sorry

end Imo1984P3

File author(s): Kimi K3

This problem has a complete formalized solution.