Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2013P4

module

public import Mathlib.Tactic

public section


/-!
# USA Mathematical Olympiad 2013, Problem 4

Find all real numbers x, y, z ≥ 1 satisfying

  min(√(x + xyz), √(y + xyz), √(z + xyz)) = √(x - 1) + √(y - 1) + √(z - 1).
-/

namespace Usa2013P4

open Real

/-- The condition that `x` is the "distinguished" coordinate of a solution
(the coordinate at which the minimum of the left-hand side is attained):
the other two shifted coordinates `y - 1`, `z - 1` multiply to `1`, and
`x - 1` is the reciprocal of `(√(y - 1) + √(z - 1))²`. -/
def Distinguished (x y z : ℝ) : Prop :=
  (y - 1) * (z - 1) = 1 ∧ (x - 1) * (√(y - 1) + √(z - 1)) ^ 2 = 1

/- determine -/ abbrev solution_set : Set (ℝ × ℝ × ℝ) := sorry

theorem usa2013_p4 (x y z : ℝ) :
    1 ≤ x ∧ 1 ≤ y ∧ 1 ≤ z ∧
      min (min (√(x + x * y * z)) (√(y + x * y * z))) (√(z + x * y * z)) =
        √(x - 1) + √(y - 1) + √(z - 1) ↔ (x, y, z) ∈ solution_set := sorry

end Usa2013P4

File author(s): Kimi K3

This problem has a complete formalized solution.