IMO 2011 Q3 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Let f : ℝ → ℝ be a function that satisfies

f(x + y) ≤ y * f(x) + f(f(x))

for all x and y. Prove that f(x) = 0 for all x ≤ 0.

Solution #

theorem imo2011_q3 (f : ℝ → ℝ) (hf : ∀ (x y : ℝ), f (x + y) ≤ y * f x + f (f x)) (x : ℝ) (H : x ≤ 0) :

f x = 0