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.four_pow_four_pos : 0 < 4 ^ 4

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.zero_lt_32 : 0 < 32

theorem Imo2006Q3.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 Imo2006Q3.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 Imo2006Q3.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 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 * √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