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

source

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

|x| = 1

source

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