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 $| a b (a^{2} - b^{2}) + b c (b^{2} - c^{2}) + c a (c^{2} - a^{2}) | \leq 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.

source

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.

source

theorem imo2006_q3.four_pow_four_pos :

0 < 4 ^ 4

source

theorem imo2006_q3.mid_ineq {s t : ℝ} :

s * t ^ 3 ≤ (3 * t + s) ^ 4 / 4 ^ 4

source

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.

source

theorem imo2006_q3.zero_lt_32 :

0 < 32

source

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

source

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.

source

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)

source

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

source

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

source

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