# Documentation

Archive.Imo.Imo2006Q3

# IMO 2006 Q3 #

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 Imo2006Q3.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 Imo2006Q3.mid_ineq {s : } {t : } :
s * t ^ 3 (3 * t + s) ^ 4 / 4 ^ 4
theorem Imo2006Q3.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 Imo2006Q3.subst_wlog {x : } {y : } {z : } {s : } (hxy : 0 x * y) (hxyz : x + y + z = 0) :
32 * |x * y * z * s| * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
theorem Imo2006Q3.subst_proof₁ (x : ) (y : ) (z : ) (s : ) (hxyz : x + y + z = 0) :
|x * y * z * s| / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2

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

theorem Imo2006Q3.proof₁ {a : } {b : } {c : } :
|a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| 9 * / 32 * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
theorem Imo2006Q3.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 * / 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 * / 32 M