Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2021P5

module

public import Mathlib.Analysis.Normed.Field.Basic
public import Mathlib.Data.ZMod.Defs

public section


/-!
# USA Mathematical Olympiad 2021, Problem 5

Let n ≥ 4 be an integer. Find all positive real solutions to the following
system of 2n equations:

  a₁ = 1/a₂ₙ + 1/a₂,
  a₂ = a₁ + a₃,
  a₃ = 1/a₂ + 1/a₄,
  a₄ = a₃ + a₅,
  a₅ = 1/a₄ + 1/a₆,
  a₆ = a₅ + a₇,
  ⋮
  a₂ₙ₋₁ = 1/a₂ₙ₋₂ + 1/a₂ₙ,
  a₂ₙ = a₂ₙ₋₁ + a₁.
-/

namespace Usa2021P5

/-- The unique solution of the system: the even-indexed terms equal `2` and the
odd-indexed terms equal `1`, i.e. `(a₁, a₂, a₃, a₄, …) = (1, 2, 1, 2, …)`.
The first component is the sequence of even-indexed terms and the second
component is the sequence of odd-indexed terms. -/
/- determine -/ abbrev solution (n : ℕ) : (ZMod n → ℝ) × (ZMod n → ℝ) := sorry

theorem usa2021_p5 (n : ℕ) (hn : 4 ≤ n) (a b : ZMod n → ℝ)
    (ha : ∀ k, 0 < a k) (hb : ∀ k, 0 < b k) :
    ((∀ k, a k = b k + b (k + 1)) ∧
     (∀ k, b k = 1 / a (k - 1) + 1 / a k)) ↔ (a, b) = solution n := sorry

end Usa2021P5

File author(s): Kimi K3

This problem has a complete formalized solution.