Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(archive/imo): formalize IMO 2005 Q3 (#6984)
feat(archive/imo): formalize IMO 2005 Q3 Co-authored-by: Manuel Candales <manuelcandales@gmail.com>
- Loading branch information
1 parent
b05affb
commit 89ea423
Showing
1 changed file
with
68 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,68 @@ | ||
/- | ||
Copyright (c) 2021 Manuel Candales. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Manuel Candales | ||
-/ | ||
import data.real.basic | ||
|
||
/-! | ||
# IMO 2005 Q3 | ||
Let `x`, `y` and `z` be positive real numbers such that `xyz ≥ 1`. Prove that: | ||
`(x^5 - x^2)/(x^5 + y^2 + z^2) + (y^5 - y^2)/(y^5 + z^2 + x^2) + (z^5 - z^2)/(z^5 + x^2 + y^2) ≥ 0` | ||
# Solution | ||
The solution by Iurie Boreico from Moldova is presented, which won a special prize during the exam. | ||
The key insight is that `(x^5-x^2)/(x^5+y^2+z^2) ≥ (x^2-y*z)/(x^2+y^2+z^2)`, which is proven by | ||
factoring `(x^5-x^2)/(x^5+y^2+z^2) - (x^5-x^2)/(x^3*(x^2+y^2+z^2))` into a non-negative expression | ||
and then making use of `xyz ≥ 1` to show `(x^5-x^2)/(x^3*(x^2+y^2+z^2)) ≥ (x^2-y*z)/(x^2+y^2+z^2)`. | ||
-/ | ||
|
||
lemma key_insight (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x*y*z ≥ 1) : | ||
(x^5-x^2)/(x^5+y^2+z^2) ≥ (x^2-y*z)/(x^2+y^2+z^2) := | ||
begin | ||
have h₁ : x^5+y^2+z^2 > 0, linarith [pow_pos hx 5, pow_pos hy 2, pow_pos hz 2], | ||
have h₂ : x^3 > 0, exact pow_pos hx 3, | ||
have h₃ : x^2+y^2+z^2 > 0, linarith [pow_pos hx 2, pow_pos hy 2, pow_pos hz 2], | ||
have h₄ : x^3*(x^2+y^2+z^2) > 0, exact mul_pos h₂ h₃, | ||
|
||
have key : (x^5-x^2)/(x^5+y^2+z^2) - (x^5-x^2)/(x^3*(x^2+y^2+z^2)) | ||
= ((x^3 - 1)^2*x^2*(y^2 + z^2))/((x^5+y^2+z^2)*(x^3*(x^2+y^2+z^2))), | ||
calc (x^5-x^2)/(x^5+y^2+z^2) - (x^5-x^2)/(x^3*(x^2+y^2+z^2)) | ||
= ((x^5-x^2)*(x^3*(x^2+y^2+z^2))-(x^5+y^2+z^2)*(x^5-x^2))/((x^5+y^2+z^2)*(x^3*(x^2+y^2+z^2))): | ||
by exact div_sub_div _ _ (ne_of_gt h₁) (ne_of_gt h₄) -- a/b - c/d = (a*d-b*c)/(b*d) | ||
... = ((x^3 - 1)^2*x^2*(y^2 + z^2))/((x^5+y^2+z^2)*(x^3*(x^2+y^2+z^2))) : | ||
by ring, | ||
|
||
have h₅ : ((x^3 - 1)^2*x^2*(y^2 + z^2))/((x^5+y^2+z^2)*(x^3*(x^2+y^2+z^2))) ≥ 0, | ||
{ refine div_nonneg _ _, | ||
refine mul_nonneg (mul_nonneg (pow_two_nonneg _) (pow_two_nonneg _)) _, | ||
exact add_nonneg (pow_two_nonneg _) (pow_two_nonneg _), | ||
exact le_of_lt (mul_pos h₁ h₄) }, | ||
|
||
calc (x^5-x^2)/(x^5+y^2+z^2) | ||
≥ (x^5-x^2)/(x^3*(x^2+y^2+z^2)) : by linarith [key, h₅] | ||
... ≥ (x^5-x^2*(x*y*z))/(x^3*(x^2+y^2+z^2)) : | ||
by { refine (div_le_div_right h₄).mpr _, simp, | ||
exact (le_mul_iff_one_le_right (pow_pos hx 2)).mpr h } | ||
... = (x^2-y*z)/(x^2+y^2+z^2) : | ||
by { field_simp [ne_of_gt h₂, ne_of_gt h₃], ring }, | ||
end | ||
|
||
theorem imo2005_q3 (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x*y*z ≥ 1) : | ||
(x^5-x^2)/(x^5+y^2+z^2) + (y^5-y^2)/(y^5+z^2+x^2) + (z^5-z^2)/(z^5+x^2+y^2) ≥ 0 := | ||
begin | ||
calc (x^5-x^2)/(x^5+y^2+z^2) + (y^5-y^2)/(y^5+z^2+x^2) + (z^5-z^2)/(z^5+x^2+y^2) | ||
≥ (x^2-y*z)/(x^2+y^2+z^2) + (y^2-z*x)/(y^2+z^2+x^2) + (z^2-x*y)/(z^2+x^2+y^2) : | ||
by { linarith [key_insight x y z hx hy hz h, | ||
key_insight y z x hy hz hx (by linarith [h]), | ||
key_insight z x y hz hx hy (by linarith [h])] } | ||
... = (x^2 + y^2 + z^2 - y*z - z*x - x*y) / (x^2+y^2+z^2) : | ||
by { have h₁ : y^2+z^2+x^2 = x^2+y^2+z^2, linarith, | ||
have h₂ : z^2+x^2+y^2 = x^2+y^2+z^2, linarith, | ||
rw [h₁, h₂], ring } | ||
... = 1/2*( (x-y)^2 + (y-z)^2 + (z-x)^2 ) / (x^2+y^2+z^2) : by ring | ||
... ≥ 0 : | ||
by { exact div_nonneg | ||
(by linarith [pow_two_nonneg (x-y), pow_two_nonneg (y-z), pow_two_nonneg (z-x)]) | ||
(by linarith [pow_two_nonneg x, pow_two_nonneg y, pow_two_nonneg z]) }, | ||
end |