mathlib3documentation

mathlib-archive / imo.imo2006_q3

IMO 2006 Q3 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Determine the least real number $M$ such that $$\left| ab(a^2 - b^2) + bc(b^2 - c^2) + ca(c^2 - a^2) \right| ≤ M (a^2 + b^2 + c^2)^2$$ for all real numbers $a$, $b$, $c$.

Solution #

The answer is $M = \frac{9 \sqrt 2}{32}$.

This is essentially a translation of the solution in https://web.evanchen.cc/exams/IMO-2006-notes.pdf.

It involves making the substitution x = a - b, y = b - c, z = c - a, s = a + b + c.

theorem imo2006_q3.lhs_ineq {x y : } (hxy : 0 x * y) :
16 * x ^ 2 * y ^ 2 * (x + y) ^ 2 ((x + y) ^ 2) ^ 3

Replacing x and y with their average increases the left side.

theorem imo2006_q3.mid_ineq {s t : } :
s * t ^ 3 (3 * t + s) ^ 4 / 4 ^ 4
theorem imo2006_q3.rhs_ineq {x y : } :
3 * (x + y) ^ 2 2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2)

Replacing x and y with their average decreases the right side.

theorem imo2006_q3.zero_lt_32  :
0 < 32
theorem imo2006_q3.subst_wlog {x y z s : } (hxy : 0 x * y) (hxyz : x + y + z = 0) :
32 * |x * y * z * s| 2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
theorem imo2006_q3.subst_proof₁ (x y z s : ) (hxyz : x + y + z = 0) :
|x * y * z * s| 2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2

Proof that M = 9 * sqrt 2 / 32 works with the substitution.

theorem imo2006_q3.lhs_identity (a b c : ) :
a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2) = (a - b) * (b - c) * (c - a) * -(a + b + c)
theorem imo2006_q3.proof₁ {a b c : } :
|a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| 9 * 2 / 32 * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
theorem imo2006_q3.proof₂ (M : ) (h : (a b c : ), |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2) :
9 * 2 / 32 M
theorem imo2006_q3 (M : ) :
( (a b c : ), |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2) 9 * 2 / 32 M