IMO 2026 Q5

Let ℝ₊ be the set of positive real numbers. Determine all functions f : ℝ₊ → ℝ₊ such that √((x ^ 2 + f y ^ 2) / 2) ≥ (f x + y) / 2 ≥ √(x * f y) for all x, y ∈ ℝ₊.

The solutions are the translations f x = x + c, where c ≥ 0.

Solution

For an informal version of the iteration argument below, see the iterated solution in Section 2.2 of Evan Chen's IMO 2026 solution notes.

Write d x = f x - x for the displacement of x. Squaring the upper inequality bounds (f x + y) ^ 2 - (x + f y) ^ 2 by (x - f y) ^ 2, while squaring the lower inequality gives the same bound for its negation. Factoring the difference of squares gives the key estimate |d x - d y| * (f x + y + x + f y) ≤ (x - f y) ^ 2.

Substituting x = f y into the original inequalities shows that d (f y) = d y. Consequently, the iterates of f form the arithmetic progression f^[n] x = x + n * d x. Since all these iterates are positive, d x cannot be negative.

Next suppose that a = d x and b = d y are both positive but unequal. Choose n sufficiently large and set m = ⌊(f^[n + 1] y - x) / a⌋. Since f^[m] x = x + m * a, the definition of the floor ensures 0 ≤ f^[n + 1] y - f^[m] x < a. Applying the key estimate to f^[m] x and f^[n] y now makes its right-hand side less than a ^ 2; the choice of n makes its left-hand side greater than a ^ 2, a contradiction. Thus all positive displacements have the same value.

Finally, the key estimate shows that a point with positive displacement a has distance at least a from every point with zero displacement. Hence the displacement is locally constant on the positive reals. Since the positive reals are connected, the displacement is constant, giving f x = x + c with c ≥ 0. A direct calculation verifies that every such translation is a solution.

def Imo2026Q5.IsSolution (f : ℝ → ℝ) : Prop

The pair of inequalities in the problem. Positivity of f on positive inputs is kept as a separate hypothesis because f is represented as a function on all of ℝ.

Equations

• Imo2026Q5.IsSolution f = ∀ x > 0, ∀ y > 0, √((x ^ 2 + f y ^ 2) / 2) ≥ (f x + y) / 2 ∧ (f x + y) / 2 ≥ √(x * f y)

theorem Imo2026Q5.displacement_control {f : ℝ → ℝ} {x y : ℝ} (hf : ∀ x > 0, 0 < f x) (h : IsSolution f) (hx : 0 < x) (hy : 0 < y) : |f x - x - (f y - y)| * (f x + y + x + f y) ≤ (x - f y) ^ 2

The key estimate: the two inequalities in the problem control the difference between the displacements at two positive inputs.

theorem Imo2026Q5.iterate_pos {f : ℝ → ℝ} {x : ℝ} (hf : ∀ x > 0, 0 < f x) (hx : 0 < x) (n : ℕ) : 0 < f^[n] x

Every iterate of a positive input remains positive.

theorem Imo2026Q5.iterate_eq_add_mul_displacement {f : ℝ → ℝ} {x : ℝ} (hf : ∀ x > 0, 0 < f x) (h : IsSolution f) (hx : 0 < x) (n : ℕ) : f^[n] x = x + ↑n * (f x - x)

The iterates of a positive input form an arithmetic progression whose common difference is f x - x.

theorem Imo2026Q5.displacement_nonneg {f : ℝ → ℝ} {x : ℝ} (hf : ∀ x > 0, 0 < f x) (h : IsSolution f) (hx : 0 < x) : 0 ≤ f x - x

The displacement f x - x is nonnegative at every positive input.

theorem Imo2026Q5.displacement_iterate_eq {f : ℝ → ℝ} {x : ℝ} (hf : ∀ x > 0, 0 < f x) (h : IsSolution f) (hx : 0 < x) (n : ℕ) : f (f^[n] x) - f^[n] x = f x - x

The displacement is constant along the forward orbit of a positive input.

theorem Imo2026Q5.displacement_eq_of_pos {f : ℝ → ℝ} {x y : ℝ} (hf : ∀ x > 0, 0 < f x) (h : IsSolution f) (hx : 0 < x) (hy : 0 < y) (hfx : 0 < f x - x) (hfy : 0 < f y - y) : f x - x = f y - y

Any two strictly positive displacements are equal.

theorem Imo2026Q5.displacement_le_dist_of_eq_zero {f : ℝ → ℝ} (hf : ∀ x > 0, 0 < f x) (h : IsSolution f) {p q a : ℝ} (hp : 0 < p) (hq : 0 < q) (ha : 0 < a) (hp' : f p - p = a) (hq' : f q - q = 0) : a ≤ dist p q

A point with positive displacement a is at least distance a from every point with zero displacement.

theorem Imo2026Q5.displacement_eq {f : ℝ → ℝ} {x y : ℝ} (hf : ∀ x > 0, 0 < f x) (h : IsSolution f) (hx : 0 < x) (hy : 0 < y) : f x - x = f y - y

The displacement f x - x is constant on the positive reals.

theorem Imo2026Q5.imo2026_q5 {f : ℝ → ℝ} (hf : ∀ x > 0, 0 < f x) : IsSolution f ↔ ∃ c ≥ 0, ∀ x > 0, f x = x + c

The solutions to IMO 2026 Q5 are precisely the nonnegative translations on ℝ₊.