# Documentation

Archive.Imo.Imo2013Q5

# IMO 2013 Q5 #

Let ℚ>₀ be the positive rational numbers. Let f : ℚ>₀ → ℝ be a function satisfying the conditions

1. f(x) * f(y) ≥ f(x * y)
2. f(x + y) ≥ f(x) + f(y)

for all x, y ∈ ℚ>₀. Given that f(a) = a for some rational a > 1, prove that f(x) = x for all x ∈ ℚ>₀.

# Solution #

We provide a direct translation of the solution found in https://www.imo-official.org/problems/IMO2013SL.pdf

theorem Imo2013Q5.le_of_all_pow_lt_succ {x : } {y : } (hx : 1 < x) (hy : 1 < y) (h : ∀ (n : ), 0 < nx ^ n - 1 < y ^ n) :
x y
theorem Imo2013Q5.le_of_all_pow_lt_succ' {x : } {y : } (hx : 1 < x) (hy : 0 < y) (h : ∀ (n : ), 0 < nx ^ n - 1 < y ^ n) :
x y

Like le_of_all_pow_lt_succ, but with a weaker assumption for y.

theorem Imo2013Q5.f_pos_of_pos {f : } {q : } (hq : 0 < q) (H1 : ∀ (x y : ), 0 < x0 < yf (x * y) f x * f y) (H4 : ∀ (n : ), 0 < nn f n) :
0 < f q
theorem Imo2013Q5.fx_gt_xm1 {f : } {x : } (hx : 1 x) (H1 : ∀ (x y : ), 0 < x0 < yf (x * y) f x * f y) (H2 : ∀ (x y : ), 0 < x0 < yf x + f y f (x + y)) (H4 : ∀ (n : ), 0 < nn f n) :
x - 1 < f x
theorem Imo2013Q5.pow_f_le_f_pow {f : } {n : } (hn : 0 < n) {x : } (hx : 1 < x) (H1 : ∀ (x y : ), 0 < x0 < yf (x * y) f x * f y) (H4 : ∀ (n : ), 0 < nn f n) :
f (x ^ n) f x ^ n
theorem Imo2013Q5.fixed_point_of_pos_nat_pow {f : } {n : } (hn : 0 < n) (H1 : ∀ (x y : ), 0 < x0 < yf (x * y) f x * f y) (H4 : ∀ (n : ), 0 < nn f n) (H5 : ∀ (x : ), 1 < xx f x) {a : } (ha1 : 1 < a) (hae : f a = a) :
f (a ^ n) = ↑(a ^ n)
theorem Imo2013Q5.fixed_point_of_gt_1 {f : } {x : } (hx : 1 < x) (H1 : ∀ (x y : ), 0 < x0 < yf (x * y) f x * f y) (H2 : ∀ (x y : ), 0 < x0 < yf x + f y f (x + y)) (H4 : ∀ (n : ), 0 < nn f n) (H5 : ∀ (x : ), 1 < xx f x) {a : } (ha1 : 1 < a) (hae : f a = a) :
f x = x
theorem imo2013_q5 (f : ) (H1 : ∀ (x y : ), 0 < x0 < yf (x * y) f x * f y) (H2 : ∀ (x y : ), 0 < x0 < yf x + f y f (x + y)) (H_fixed_point : a, 1 < a f a = a) (x : ) :
0 < xf x = x