IMO 1986 Q5

Find all functions f, defined on the non-negative real numbers and taking nonnegative real values, such that:

• $f(xf(y))f(y) = f(x + y)$ for all $x, y \ge 0$,
• $f(2) = 0$,
• $f(x) \ne 0$ for $0 \le x < 2$.

We formalize the assumptions on f in Imo1986Q5.IsGood predicate, then prove Imo1986Q5.IsGood f ↔ f = fun x ↦ 2 / (2 - x).

Note that this formalization relies on the fact that Mathlib uses 0 as the "garbage value", namely for 2 ≤ x we have 2 - x = 0 and 2 / (2 - x) = 0.

Formalization is based on Art of Problem Solving with minor modifications.

structure Imo1986Q5.IsGood (f : NNReal → NNReal) : Prop

• map_add_rev : ∀ (x y : NNReal), f (x * f y) * f y = f (x + y)
• map_two : f 2 = 0
• map_ne_zero : ∀ x < 2, f x ≠ 0

theorem Imo1986Q5.IsGood.map_add_rev {f : NNReal → NNReal} (self : Imo1986Q5.IsGood f) (x : NNReal) (y : NNReal) : f (x * f y) * f y = f (x + y)

theorem Imo1986Q5.IsGood.map_two {f : NNReal → NNReal} (self : Imo1986Q5.IsGood f) : f 2 = 0

theorem Imo1986Q5.IsGood.map_ne_zero {f : NNReal → NNReal} (self : Imo1986Q5.IsGood f) (x : NNReal) : x < 2 → f x ≠ 0

theorem Imo1986Q5.IsGood.map_add {f : NNReal → NNReal} (hf : Imo1986Q5.IsGood f) (x : NNReal) (y : NNReal) : f (x + y) = f (x * f y) * f y

theorem Imo1986Q5.IsGood.map_eq_zero {f : NNReal → NNReal} (hf : Imo1986Q5.IsGood f) {x : NNReal} : f x = 0 ↔ 2 ≤ x

theorem Imo1986Q5.IsGood.map_ne_zero_iff {f : NNReal → NNReal} (hf : Imo1986Q5.IsGood f) {x : NNReal} : f x ≠ 0 ↔ x < 2

theorem Imo1986Q5.IsGood.map_of_lt_two {f : NNReal → NNReal} (hf : Imo1986Q5.IsGood f) {x : NNReal} (hx : x < 2) : f x = 2 / (2 - x)

theorem Imo1986Q5.IsGood.map_eq {f : NNReal → NNReal} (hf : Imo1986Q5.IsGood f) (x : NNReal) : f x = 2 / (2 - x)

theorem Imo1986Q5.isGood_iff {f : NNReal → NNReal} : Imo1986Q5.IsGood f ↔ f = fun (x : NNReal) => 2 / (2 - x)