feat(archive/imo): formalize IMO 2011 problem Q3 (#5842)

archive/imo/imo2011_q3.lean

@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2021 David Renshaw. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Renshaw
+-/
+
+import data.real.basic
+
+/-!
+# IMO 2011 Q3
+
+Let f : ℝ → ℝ be a function that satisfies
+
+   f(x + y) ≤ y * f(x) + f(f(x))
+
+for all x and y. Prove that f(x) = 0 for all x ≤ 0.
+
+# Solution
+
+Direct translation of the solution found in https://www.imo-official.org/problems/IMO2011SL.pdf
+-/
+
+theorem imo2011_q3 (f : ℝ → ℝ) (hf : ∀ x y, f (x + y) ≤ y * f x + f (f x)) :
+  ∀ x ≤ 0, f x = 0 :=
+begin
+  -- reparameterize
+  have hxt : ∀ x t, f t ≤ t * f x - x * f x + f (f x),
+  { intros x t,
+    calc f t = f (x + (t - x))             : by rw (add_eq_of_eq_sub' rfl)
+         ... ≤ (t - x) * f x + f (f x)     : hf x (t - x)
+         ... = t * f x - x * f x + f (f x) : by rw sub_mul },
+
+  have h_ab_combined : ∀ a b, a * f a + b * f b ≤ 2 * f a * f b,
+  { intros a b,
+    linarith [hxt b (f a), hxt a (f b)] },
+
+  have h_f_nonneg_of_pos : ∀ a < 0, 0 ≤ f a,
+  { intros a han,
+    suffices : a * f a ≤ 0, from nonneg_of_mul_nonpos_right this han,
+    exact add_le_iff_nonpos_left.mp (h_ab_combined a (2 * f a)) },
+
+  have h_f_nonpos : ∀ x, f x ≤ 0,
+  { intros x,
+    by_contra h_suppose_not,
+    -- If we choose a small enough argument for f, then we get a contradiction.
+    let s := (x * f x - f (f x)) / (f x),
+    have hm : min 0 s - 1 < s := (sub_one_lt _).trans_le (min_le_right 0 s),
+    have hml : min 0 s - 1 < 0 := (sub_one_lt _).trans_le (min_le_left 0 s),
+
+    suffices : f (min 0 s - 1) < 0, from not_le.mpr this (h_f_nonneg_of_pos (min 0 s - 1) hml),
+
+    have hp : 0 < f x := not_le.mp h_suppose_not,
+    calc f (min 0 s - 1)
+           ≤ (min 0 s - 1) * f x - x * f x + f (f x) : hxt x (min 0 s - 1)
+      ...  < s * f x - x * f x + f (f x) : by linarith [(mul_lt_mul_right hp).mpr hm]
+      ...  = 0 : by { rw [(eq_div_iff hp.ne.symm).mp rfl], linarith } },
+
+  have h_fx_zero_of_neg : ∀ x < 0, f x = 0,
+  { intros x hxz,
+    exact (h_f_nonpos x).antisymm (h_f_nonneg_of_pos x hxz) },
+
+  intros x hx,
+  obtain (h_x_neg : x < 0) | (rfl : x = 0) := hx.lt_or_eq,
+  { exact h_fx_zero_of_neg _ h_x_neg },
+  { suffices : 0 ≤ f 0, from le_antisymm (h_f_nonpos 0) this,
+    have hno : f (-1) = 0 := h_fx_zero_of_neg (-1) neg_one_lt_zero,
+    have hp := hxt (-1) (-1),
+    rw hno at hp,
+    linarith },
+end