# mathlib3documentation

mathlib-archive / imo.imo2013_q5

# IMO 2013 Q5 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 imo2013_q5.le_of_all_pow_lt_succ {x y : } (hx : 1 < x) (hy : 1 < y) (h : (n : ), 0 < n x ^ n - 1 < y ^ n) :
x y
theorem imo2013_q5.le_of_all_pow_lt_succ' {x y : } (hx : 1 < x) (hy : 0 < y) (h : (n : ), 0 < n x ^ n - 1 < y ^ n) :
x y

Like le_of_all_pow_lt_succ, but with a weaker assumption for y.

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