Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2026P5

module

public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.Analysis.Normed.Field.Basic

public section


/-!
# International Mathematical Olympiad 2026, Problem 5

Let ℝ_{>0} be the set of positive real numbers. Determine all functions
f : ℝ_{>0} → ℝ_{>0} such that

    √((x² + f(y)²)/2) ≥ (f(x) + y)/2 ≥ √(x·f(y))

for every x, y ∈ ℝ_{>0}.

Statement formalization adapted from AxiomMath/IMO2026; proof adapted from
Humanfia's Kimi-K3 solutions (https://github.com/humanfia/imo2026).
-/

namespace Imo2026P5

/-- The subtype of positive real numbers, representing `\mathbb{R}_{>0}`. -/
abbrev PositiveReal : Type := {x : ℝ // 0 < x}

/-- The two-sided inequality defining admissible functions on positive real numbers. -/
def IsAdmissible (f : PositiveReal → PositiveReal) : Prop :=
  ∀ x y : PositiveReal,
    ((f x : ℝ) + (y : ℝ)) / 2 ≤ Real.sqrt (((x : ℝ) ^ 2 + (f y : ℝ) ^ 2) / 2) ∧
      Real.sqrt ((x : ℝ) * (f y : ℝ)) ≤ ((f x : ℝ) + (y : ℝ)) / 2

/- determine -/ abbrev answer : Set (PositiveReal → PositiveReal) := sorry

/-- The admissible functions are exactly the translations `f(x) = x + c` with a
nonnegative constant `c`. -/
theorem imo2026_p5 (f : PositiveReal → PositiveReal) :
    IsAdmissible f ↔ f ∈ answer := sorry

end Imo2026P5

File author(s): Kimi K3

This problem has a complete formalized solution.

The problem was imported from https://github.com/humanfia/imo2026.