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.
theorem
Imo1986Q5.IsGood.map_ne_zero
{f : NNReal → NNReal}
(self : Imo1986Q5.IsGood f)
(x : NNReal)
:
theorem
Imo1986Q5.IsGood.map_ne_zero_iff
{f : NNReal → NNReal}
(hf : Imo1986Q5.IsGood f)
{x : NNReal}
:
theorem
Imo1986Q5.IsGood.map_of_lt_two
{f : NNReal → NNReal}
(hf : Imo1986Q5.IsGood f)
{x : NNReal}
(hx : x < 2)
: