Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1995P2

module

public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

public section


/-!
# USA Mathematical Olympiad 1995, Problem 2

A trigonometric map is any one of sin, cos, tan, arcsin, arccos and arctan.
Show that given any positive rational number x, one can find a finite
sequence of trigonometric maps which take 0 to x. [So we need to show that
we can always find a sequence of trigonometric maps tᵢ so that:
x₁ = t₀(0), x₂ = t₁(x₁), ..., xₙ = tₙ₋₁(xₙ₋₁), x = tₙ(xₙ).]
-/

namespace Usa1995P2

/-- The six trigonometric maps allowed by the problem. -/
inductive TrigMap where
  | sin | cos | tan | arcsin | arccos | arctan

/-- Evaluate a trigonometric map at a real number. -/
noncomputable def TrigMap.apply : TrigMap → ℝ → ℝ
  | .sin => Real.sin
  | .cos => Real.cos
  | .tan => Real.tan
  | .arcsin => Real.arcsin
  | .arccos => Real.arccos
  | .arctan => Real.arctan

/-- Apply a finite sequence of trigonometric maps to a starting value. -/
noncomputable def run (l : List TrigMap) (x : ℝ) : ℝ := l.foldl (fun a f => f.apply a) x

theorem usa1995_p2 (x : ℚ) (hx : 0 < x) :
    ∃ l : List TrigMap, run l 0 = (x : ℝ) := sorry

end Usa1995P2

File author(s): Kimi K3

This problem has a complete formalized solution.