IMO 2001 Q2

Let $a$, $b$, $c$ be positive reals. Prove that $$ \frac{a}{\sqrt{a^2 + 8bc}} + \frac{b}{\sqrt{b^2 + 8ca}} + \frac{c}{\sqrt{c^2 + 8ab}} ≥ 1. $$

Solution

This proof is based on the bound $$ \frac{a}{\sqrt{a^2 + 8bc}} ≥ \frac{a^{\frac43}}{a^{\frac43} + b^{\frac43} + c^{\frac43}}. $$

theorem Imo2001Q2.bound {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ 4 / (a ^ 4 + b ^ 4 + c ^ 4) ≤ a ^ 3 / √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)

theorem Imo2001Q2.imo2001_q2' {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : 1 ≤ a ^ 3 / √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) + b ^ 3 / √((b ^ 3) ^ 2 + 8 * c ^ 3 * a ^ 3) + c ^ 3 / √((c ^ 3) ^ 2 + 8 * a ^ 3 * b ^ 3)

theorem imo2001_q2 {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : 1 ≤ a / √(a ^ 2 + 8 * b * c) + b / √(b ^ 2 + 8 * c * a) + c / √(c ^ 2 + 8 * a * b)