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 < n → x ^ 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 < n → x ^ 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 < x → 0 < y → f (x * y) ≤ f x * f y) (H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n) : 0 < f q

theorem Imo2013Q5.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 Imo2013Q5.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 Imo2013Q5.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 Imo2013Q5.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