Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2018P2

module

public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.EuclideanDomain.Basic
public import Mathlib.Algebra.EuclideanDomain.Field
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.Analysis.Normed.Field.Basic
public import Mathlib.Tactic.IntervalCases

public section


/-!
# United States of America Mathematical Olympiad 2018, Problem 2

Find all functions $f : (0, \infty) \to (0, \infty)$ such that
$$f\left(x + \frac{1}{y}\right) + f\left(y + \frac{1}{z}\right) +
  f\left(z + \frac{1}{x}\right) = 1$$
for all $x, y, z > 0$ with $xyz = 1$.
-/

namespace Usa2018P2

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

theorem usa2018_p2 (f : ℝ → ℝ) :
    f ∈ solution_set ↔
      (∀ x : ℝ, 0 < x → 0 < f x) ∧
        (∀ x y z : ℝ, 0 < x → 0 < y → 0 < z → x * y * z = 1 →
          f (x + 1 / y) + f (y + 1 / z) + f (z + 1 / x) = 1) := sorry

end Usa2018P2

File author(s): Kimi K3

This problem has a complete formalized solution.