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

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