Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 6585eff

Browse files
dwrenshabryangingechen
dwrensha
and
bryangingechen
committed
feat(archive/imo): formalize IMO 2013 problem Q5 (#5787)
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
1 parent 3e59960 commit 6585eff

File tree

1 file changed

+333
-0
lines changed

1 file changed

+333
-0
lines changed

‎archive/imo/imo2013_q5.lean

Lines changed: 333 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,333 @@
1+
/-
2+
Copyright (c) 2021 David Renshaw. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: David Renshaw
5+
-/
6+
7+
import algebra.geom_sum
8+
import data.rat.basic
9+
import data.real.basic
10+
11+
/-!
12+
# IMO 2013 Q5
13+
14+
Let ℚ>₀ be the set of positive rational numbers. Let f: ℚ>₀ → ℝ be a function satisfying
15+
the conditions
16+
17+
(1) f(x) * f(y) ≥ f(x * y)
18+
(2) f(x + y) ≥ f(x) + f(y)
19+
20+
for all x,y ∈ ℚ>₀. Given that f(a) = a for some rational a > 1, prove that f(x) = x for
21+
all x ∈ ℚ>₀.
22+
23+
# Solution
24+
25+
We provide a direct translation of the solution found in
26+
https://www.imo-official.org/problems/IMO2013SL.pdf
27+
-/
28+
29+
open_locale big_operators
30+
31+
lemma le_of_all_pow_lt_succ {x y : ℝ} (hx : 1 < x) (hy : 1 < y)
32+
(h : ∀ n : ℕ, 0 < n → x^n - 1 < y^n) :
33+
x ≤ y :=
34+
begin
35+
by_contra hxy,
36+
push_neg at hxy,
37+
have hxmy : 0 < x - y := sub_pos.mpr hxy,
38+
have hn : ∀ n : ℕ, 0 < n → (x - y) * (n : ℝ) ≤ x^n - y^n,
39+
{ intros n hn,
40+
have hterm : ∀ i : ℕ, i ∈ finset.range n → 1 ≤ x^i * y^(n - 1 - i),
41+
{ intros i hi,
42+
have hx' : 1 ≤ x ^ i := one_le_pow_of_one_le hx.le i,
43+
have hy' : 1 ≤ y ^ (n - 1 - i) := one_le_pow_of_one_le hy.le (n - 1 - i),
44+
calc 1 ≤ x^i : hx'
45+
... = x^i * 1 : (mul_one _).symm
46+
... ≤ x^i * y^(n-1-i) : mul_le_mul_of_nonneg_left hy' (zero_le_one.trans hx') },
47+
48+
calc (x - y) * (n : ℝ)
49+
= (n : ℝ) * (x - y) : mul_comm _ _
50+
... = (∑ (i : ℕ) in finset.range n, (1 : ℝ)) * (x - y) :
51+
by simp only [mul_one, finset.sum_const, nsmul_eq_mul,
52+
finset.card_range]
53+
... ≤ (∑ (i : ℕ) in finset.range n, x ^ i * y ^ (n - 1 - i)) * (x-y) :
54+
(mul_le_mul_right hxmy).mpr (finset.sum_le_sum hterm)
55+
... = x^n - y^n : geom_sum₂_mul x y n, },
56+
57+
-- Choose n larger than 1 / (x - y).
58+
obtain ⟨N, hN⟩ := exists_nat_gt (1 / (x - y)),
59+
have hNp : 0 < N, { exact_mod_cast (one_div_pos.mpr hxmy).trans hN },
60+
61+
have := calc 1 = (x - y) * (1 / (x - y)) : by field_simp [ne_of_gt hxmy]
62+
... < (x - y) * N : (mul_lt_mul_left hxmy).mpr hN
63+
... ≤ x^N - y^N : hn N hNp,
64+
linarith [h N hNp]
65+
end
66+
67+
/--
68+
Like le_of_all_pow_lt_succ, but with a weaker assumption for y.
69+
-/
70+
lemma le_of_all_pow_lt_succ' {x y : ℝ} (hx : 1 < x) (hy : 0 < y)
71+
(h : ∀ n : ℕ, 0 < n → x^n - 1 < y^n) :
72+
x ≤ y :=
73+
begin
74+
refine le_of_all_pow_lt_succ hx _ h,
75+
by_contra hy'',
76+
push_neg at hy'', -- hy'' : y ≤ 1.
77+
78+
-- Then there exists y' such that 0 < y ≤ 1 < y' < x.
79+
let y' := (x + 1) / 2,
80+
have h_y'_lt_x : y' < x,
81+
{ have hh : (x + 1)/2 < (x * 2) / 2, { linarith },
82+
calc y' < (x * 2) / 2 : hh
83+
... = x : by field_simp },
84+
have h1_lt_y' : 1 < y',
85+
{ have hh' : 1 * 2 / 2 < (x + 1) / 2, { linarith },
86+
calc 1 = 1 * 2 / 2 : by field_simp
87+
... < y' : hh' },
88+
have h_y_lt_y' : y < y' := hy''.trans_lt h1_lt_y',
89+
have hh : ∀ n, 0 < n → x^n - 1 < y'^n,
90+
{ intros n hn,
91+
calc x^n - 1 < y^n : h n hn
92+
... ≤ y'^n : pow_le_pow_of_le_left hy.le h_y_lt_y'.le n },
93+
exact h_y'_lt_x.not_le (le_of_all_pow_lt_succ hx h1_lt_y' hh)
94+
end
95+
96+
lemma f_pos_of_pos {f : ℚ → ℝ} {q : ℚ} (hq : 0 < q)
97+
(H1 : ∀ x y, 0 < x → 0 < y → f (x * y) ≤ f x * f y)
98+
(H4 : ∀ n : ℕ, 0 < n → (n : ℝ) ≤ f n) :
99+
0 < f q :=
100+
begin
101+
have hfqn := calc f q.num = f (q * q.denom) : by rw ←rat.mul_denom_eq_num
102+
... ≤ f q * f q.denom : H1 q q.denom hq (nat.cast_pos.mpr q.pos),
103+
104+
-- Now we just need to show that `f q.num` and `f q.denom` are positive.
105+
-- Then nlinarith will be able to close the goal.
106+
107+
have num_pos : 0 < q.num := rat.num_pos_iff_pos.mpr hq,
108+
have hqna : (q.num.nat_abs : ℤ) = q.num := int.nat_abs_of_nonneg num_pos.le,
109+
have hqfn' :=
110+
calc (q.num : ℝ)
111+
= ((q.num.nat_abs : ℤ) : ℝ) : congr_arg coe (eq.symm hqna)
112+
... ≤ f q.num.nat_abs : H4 q.num.nat_abs
113+
(int.nat_abs_pos_of_ne_zero (ne_of_gt num_pos))
114+
... = f q.num : by exact_mod_cast congr_arg f (congr_arg coe hqna),
115+
116+
have f_num_pos := calc (0 : ℝ) < q.num : int.cast_pos.mpr num_pos
117+
... ≤ f q.num : hqfn',
118+
have f_denom_pos := calc (0 : ℝ) < q.denom : nat.cast_pos.mpr q.pos
119+
... ≤ f q.denom : H4 q.denom q.pos,
120+
nlinarith
121+
end
122+
123+
lemma fx_gt_xm1 {f : ℚ → ℝ} {x : ℚ} (hx : 1 ≤ x)
124+
(H1 : ∀ x y, 0 < x → 0 < y → f (x * y) ≤ f x * f y)
125+
(H2 : ∀ x y, 0 < x → 0 < y → f x + f y ≤ f (x + y))
126+
(H4 : ∀ n : ℕ, 0 < n → (n : ℝ) ≤ f n) :
127+
((x - 1 : ℚ) : ℝ) < f x :=
128+
begin
129+
have hfe : (⌊x⌋.nat_abs : ℤ) = ⌊x⌋ := int.nat_abs_of_nonneg
130+
(floor_nonneg.mpr (zero_le_one.trans hx)),
131+
have hfe' : (⌊x⌋.nat_abs : ℚ) = ⌊x⌋, { exact_mod_cast hfe },
132+
have h0fx : 0 < ⌊x⌋ := int.cast_pos.mp ((sub_nonneg.mpr hx).trans_lt (sub_one_lt_floor x)),
133+
have h_nat_abs_floor_pos : 0 < ⌊x⌋.nat_abs := int.nat_abs_pos_of_ne_zero (ne_of_gt h0fx),
134+
have hx0 := calc ((x - 1 : ℚ) : ℝ)
135+
< ⌊x⌋ : by exact_mod_cast sub_one_lt_floor x
136+
... = ↑⌊x⌋.nat_abs : by exact_mod_cast hfe.symm
137+
... ≤ f ⌊x⌋.nat_abs : H4 ⌊x⌋.nat_abs h_nat_abs_floor_pos
138+
... = f ⌊x⌋ : by rw hfe',
139+
140+
obtain (h_eq : (⌊x⌋ : ℚ) = x) | (h_lt : (⌊x⌋ : ℚ) < x) := (floor_le x).eq_or_lt,
141+
{ rwa h_eq at hx0 },
142+
143+
calc ((x - 1 : ℚ) : ℝ) < f ⌊x⌋ : hx0
144+
... < f (x - ⌊x⌋) + f ⌊x⌋ : lt_add_of_pos_left (f ↑⌊x⌋)
145+
(f_pos_of_pos (sub_pos.mpr h_lt) H1 H4)
146+
... ≤ f (x - ⌊x⌋ + ⌊x⌋) : H2 (x - ⌊x⌋) ⌊x⌋ (sub_pos.mpr h_lt)
147+
(by exact_mod_cast h0fx)
148+
... = f x : by simp only [sub_add_cancel]
149+
end
150+
151+
lemma pow_f_le_f_pow {f : ℚ → ℝ} {n : ℕ} (hn : 0 < n) {x : ℚ} (hx : 1 < x)
152+
(H1 : ∀ x y, 0 < x → 0 < y → f (x * y) ≤ f x * f y)
153+
(H4 : ∀ n : ℕ, 0 < n → (n : ℝ) ≤ f n) :
154+
f (x^n) ≤ (f x)^n :=
155+
begin
156+
induction n with pn hpn,
157+
{ exfalso, exact nat.lt_asymm hn hn },
158+
cases pn,
159+
{ simp only [pow_one] },
160+
have hpn' := hpn pn.succ_pos,
161+
rw [pow_succ' x (pn + 1), pow_succ' (f x) (pn + 1)],
162+
have hxp : 0 < x := zero_lt_one.trans hx,
163+
calc f ((x ^ (pn+1)) * x)
164+
≤ f (x ^ (pn+1)) * f x : H1 (x ^ (pn+1)) x (pow_pos hxp (pn+1)) hxp
165+
... ≤ (f x) ^ (pn+1) * f x : (mul_le_mul_right (f_pos_of_pos hxp H1 H4)).mpr hpn'
166+
end
167+
168+
lemma fixed_point_of_pos_nat_pow {f : ℚ → ℝ} {n : ℕ} (hn : 0 < n)
169+
(H1 : ∀ x y, 0 < x → 0 < y → f (x * y) ≤ f x * f y)
170+
(H4 : ∀ n : ℕ, 0 < n → (n : ℝ) ≤ f n)
171+
(H5 : ∀ x : ℚ, 1 < x → (x : ℝ) ≤ f x)
172+
{a : ℚ} (ha1 : 1 < a) (hae : f a = a) :
173+
f (a^n) = a^n :=
174+
begin
175+
have hh0 : (a : ℝ) ^ n ≤ f (a ^ n),
176+
{ exact_mod_cast H5 (a ^ n) (one_lt_pow ha1 (nat.succ_le_iff.mpr hn)) },
177+
178+
have hh1 := calc f (a^n) ≤ (f a)^n : pow_f_le_f_pow hn ha1 H1 H4
179+
... = (a : ℝ)^n : by rw ← hae,
180+
181+
exact hh1.antisymm hh0
182+
end
183+
184+
lemma fixed_point_of_gt_1 {f : ℚ → ℝ} {x : ℚ} (hx : 1 < x)
185+
(H1 : ∀ x y, 0 < x → 0 < y → f (x * y) ≤ f x * f y)
186+
(H2 : ∀ x y, 0 < x → 0 < y → f x + f y ≤ f (x + y))
187+
(H4 : ∀ n : ℕ, 0 < n → (n : ℝ) ≤ f n)
188+
(H5 : ∀ x : ℚ, 1 < x → (x : ℝ) ≤ f x)
189+
{a : ℚ} (ha1 : 1 < a) (hae : f a = a) :
190+
f x = x :=
191+
begin
192+
-- Choose n such that 1 + x < a^n.
193+
have hbound : ∀ m : ℕ, 1 + (m : ℚ) * (a - 1) ≤ a^m,
194+
{ intros m,
195+
have ha : -1 ≤ a := le_of_lt (lt_trans (neg_one_lt_zero.trans zero_lt_one) ha1),
196+
exact one_add_mul_sub_le_pow ha m },
197+
198+
-- Choose N greater than x / (a - 1).
199+
obtain ⟨N, hN⟩ := exists_nat_gt (max 0 (x / (a - 1))),
200+
have hN' := calc x / (a - 1) ≤ max 0 (x / (a - 1)) : le_max_right _ _
201+
... < N : hN,
202+
have h_big_enough :=
203+
calc (1 : ℚ)
204+
= (1 + N * (a - 1)) - N * (a - 1) : by ring
205+
... ≤ a^N - N * (a - 1) : sub_le_sub_right (hbound N) (↑N * (a - 1))
206+
... < a^N - (x / (a - 1)) * (a - 1) : sub_lt_sub_left
207+
((mul_lt_mul_right (sub_pos.mpr ha1)).mpr hN') (a^N)
208+
... = a^N - x : by field_simp [ne_of_gt (sub_pos.mpr ha1)],
209+
210+
have h1 := calc (x : ℝ) + ((a^N - x) : ℚ)
211+
≤ f x + ((a^N - x) : ℚ) : add_le_add_right (H5 x hx) _
212+
... ≤ f x + f (a^N - x) : add_le_add_left (H5 _ h_big_enough) _,
213+
214+
have hxp : 0 < x := zero_lt_one.trans hx,
215+
216+
have hNp : 0 < N,
217+
{ exact_mod_cast calc ((0 : ℕ) : ℚ) = (0 : ℚ) : nat.cast_zero
218+
... ≤ max 0 (x / (a - 1)) : le_max_left 0 _
219+
... < N : hN, },
220+
221+
have h2 := calc f x + f (a^N - x)
222+
≤ f (x + (a^N - x)) : H2 x (a^N - x) hxp (zero_lt_one.trans h_big_enough)
223+
... = f (a^N) : by ring
224+
... = a^N : fixed_point_of_pos_nat_pow hNp H1 H4 H5 ha1 hae
225+
... = x + (a^N - x) : by ring,
226+
227+
have heq := h1.antisymm (by exact_mod_cast h2),
228+
linarith [H5 x hx, H5 _ h_big_enough]
229+
end
230+
231+
theorem imo2013_q5
232+
(f : ℚ → ℝ)
233+
(H1 : ∀ x y, 0 < x → 0 < y → f (x * y) ≤ f x * f y)
234+
(H2 : ∀ x y, 0 < x → 0 < y → f x + f y ≤ f (x + y))
235+
(H_fixed_point : ∃ a, 1 < a ∧ f a = a) :
236+
∀ x, 0 < x → f x = x :=
237+
begin
238+
obtain ⟨a, ha1, hae⟩ := H_fixed_point,
239+
have H3 : ∀ x : ℚ, 0 < x → ∀ n : ℕ, 0 < n → ↑n * f x ≤ f (n * x),
240+
{ intros x hx n hn,
241+
cases n,
242+
{ exfalso, exact nat.lt_asymm hn hn },
243+
induction n with pn hpn,
244+
{ simp only [one_mul, nat.cast_one] },
245+
calc (↑pn + 1 + 1) * f x
246+
= ((pn : ℝ) + 1) * f x + 1 * f x : add_mul (↑pn + 1) 1 (f x)
247+
... = (↑pn + 1) * f x + f x : by rw one_mul
248+
... ≤ f ((↑pn.succ) * x) + f x : by exact_mod_cast add_le_add_right
249+
(hpn pn.succ_pos) (f x)
250+
... ≤ f ((↑pn + 1) * x + x) : by exact_mod_cast H2 _ _
251+
(mul_pos pn.cast_add_one_pos hx) hx
252+
... = f ((↑pn + 1) * x + 1 * x) : by rw one_mul
253+
... = f ((↑pn + 1 + 1) * x) : congr_arg f (add_mul (↑pn + 1) 1 x).symm },
254+
have H4 : ∀ n : ℕ, 0 < n → (n : ℝ) ≤ f n,
255+
{ intros n hn,
256+
have hf1 : 1 ≤ f 1,
257+
{ have a_pos : (0 : ℝ) < a := rat.cast_pos.mpr (zero_lt_one.trans ha1),
258+
suffices : ↑a * 1 ≤ ↑a * f 1, from (mul_le_mul_left a_pos).mp this,
259+
calc ↑a * 1 = ↑a : mul_one ↑a
260+
... = f a : hae.symm
261+
... = f (a * 1) : by rw mul_one
262+
... ≤ f a * f 1 : (H1 a 1) (zero_lt_one.trans ha1) zero_lt_one
263+
... = ↑a * f 1 : by rw hae },
264+
265+
calc (n : ℝ) = (n : ℝ) * 1 : (mul_one _).symm
266+
... ≤ (n : ℝ) * f 1 : (mul_le_mul_left (nat.cast_pos.mpr hn)).mpr hf1
267+
... ≤ f (n * 1) : H3 1 zero_lt_one n hn
268+
... = f n : by rw mul_one },
269+
270+
have H5 : ∀ x : ℚ, 1 < x → (x : ℝ) ≤ f x,
271+
{ intros x hx,
272+
have hxnm1 : ∀ n : ℕ, 0 < n → (x : ℝ)^n - 1 < (f x)^n,
273+
{ intros n hn,
274+
calc (x : ℝ)^n - 1 < f (x^n) : by exact_mod_cast fx_gt_xm1 (one_le_pow_of_one_le hx.le n)
275+
H1 H2 H4
276+
... ≤ (f x)^n : pow_f_le_f_pow hn hx H1 H4 },
277+
have hx' : 1 < (x : ℝ) := by exact_mod_cast hx,
278+
have hxp : 0 < x := zero_lt_one.trans hx,
279+
exact le_of_all_pow_lt_succ' hx' (f_pos_of_pos hxp H1 H4) hxnm1 },
280+
281+
have h_f_commutes_with_pos_nat_mul : ∀ n : ℕ, 0 < n → ∀ x : ℚ, 0 < x → f (n * x) = n * f x,
282+
{ intros n hn x hx,
283+
have h2 : f (n * x) ≤ n * f x,
284+
{ cases n,
285+
{ exfalso, exact nat.lt_asymm hn hn },
286+
cases n,
287+
{ simp only [one_mul, nat.cast_one] },
288+
have hfneq : f (n.succ.succ) = n.succ.succ,
289+
{ have := fixed_point_of_gt_1
290+
(nat.one_lt_cast.mpr (nat.succ_lt_succ n.succ_pos)) H1 H2 H4 H5 ha1 hae,
291+
rwa (rat.cast_coe_nat n.succ.succ) at this },
292+
rw ← hfneq,
293+
exact H1 (n.succ.succ : ℚ) x (nat.cast_pos.mpr hn) hx },
294+
exact h2.antisymm (H3 x hx n hn) },
295+
296+
-- For the final calculation, we expand x as (2*x.num) / (2*x.denom), because
297+
-- we need the top of the fraction to be strictly greater than 1 in order
298+
-- to apply fixed_point_of_gt_1.
299+
intros x hx,
300+
let x2denom := 2 * x.denom,
301+
let x2num := 2 * x.num,
302+
303+
have hx2pos := calc 0 < x.denom : x.pos
304+
... < x.denom + x.denom : lt_add_of_pos_left x.denom x.pos
305+
... = 2 * x.denom : by ring,
306+
307+
have hxcnez : (x.denom : ℚ) ≠ (0 : ℚ) := ne_of_gt (nat.cast_pos.mpr x.pos),
308+
have hx2cnezr : (x2denom : ℝ) ≠ (0 : ℝ) := nat.cast_ne_zero.mpr (ne_of_gt hx2pos),
309+
310+
have hrat_expand2 := calc x = x.num / x.denom : by exact_mod_cast rat.num_denom.symm
311+
... = x2num / x2denom : by { field_simp, linarith [hxcnez] },
312+
313+
have h_denom_times_fx :=
314+
calc (x2denom : ℝ) * f x = f (x2denom * x) : (h_f_commutes_with_pos_nat_mul
315+
x2denom hx2pos x hx).symm
316+
... = f (x2denom * (x2num / x2denom)) : by rw hrat_expand2
317+
... = f x2num : by { congr, field_simp, ring },
318+
319+
have h_fx2num_fixed : f x2num = x2num,
320+
{ have hx2num_gt_one : (1 : ℚ) < (2 * x.num : ℤ),
321+
{ norm_cast, linarith [rat.num_pos_iff_pos.mpr hx] },
322+
have hh := fixed_point_of_gt_1 hx2num_gt_one H1 H2 H4 H5 ha1 hae,
323+
rwa (rat.cast_coe_int x2num) at hh },
324+
325+
calc f x = f x * 1 : (mul_one (f x)).symm
326+
... = f x * (x2denom / x2denom) : by rw ←(div_self hx2cnezr)
327+
... = (f x * x2denom) / x2denom : mul_div_assoc' (f x) _ _
328+
... = (x2denom * f x) / x2denom : by rw mul_comm
329+
... = f x2num / x2denom : by rw h_denom_times_fx
330+
... = x2num / x2denom : by rw h_fx2num_fixed
331+
... = (((x2num : ℚ) / (x2denom : ℚ) : ℚ) : ℝ) : by norm_cast
332+
... = x : by rw ←hrat_expand2
333+
end

0 commit comments

Comments
 (0)