mathlib3 documentation

mathlib-archive / imo.imo2008_q4

IMO 2008 Q4 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. Find all functions f : (0,∞) → (0,∞) (so, f is a function from the positive real numbers to the positive real numbers) such that lean (f(w)^2 + f(x)^2)/(f(y^2) + f(z^2)) = (w^2 + x^2)/(y^2 + z^2) for all positive real numbers w, x, y, z, satisfying wx = yz.

Solution #

The desired theorem is that either f = λ x, x or f = λ x, 1/x

theorem imo2008_q4.abs_eq_one_of_pow_eq_one (x : ) (n : ) (hn : n 0) (h : x ^ n = 1) :
|x| = 1
theorem imo2008_q4 (f : ) (H₁ : (x : ), x > 0 f x > 0) :
( (w x y z : ), 0 < w 0 < x 0 < y 0 < z w * x = y * z (f w ^ 2 + f x ^ 2) / (f (y ^ 2) + f (z ^ 2)) = (w ^ 2 + x ^ 2) / (y ^ 2 + z ^ 2)) ( (x : ), x > 0 f x = x) (x : ), x > 0 f x = 1 / x