mathlib3 documentation

mathlib-archive / imo.imo2011_q3

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 #

Direct translation of the solution found in https://www.imo-official.org/problems/IMO2011SL.pdf

theorem imo2011_q3 (f : ) (hf : (x y : ), f (x + y) y * f x + f (f x)) (x : ) (H : x 0) :
f x = 0