IMO 2008 Q4

Find all functions f : (0,∞) → (0,∞) (so, f is a function from the positive real numbers to the positive real numbers) such that (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 = fun x => x or f = fun x => 1/x

theorem Imo2008Q4.abs_eq_one_of_pow_eq_one (x : ℝ) (n : ℕ) (hn : n ≠ 0) (h : x ^ n = 1) : |x| = 1

theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ 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 > 0, f x = x) ∨ ∀ x > 0, f x = 1 / x