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).sqrt

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).sqrt + b ^ 3 / ((b ^ 3) ^ 2 + 8 * c ^ 3 * a ^ 3).sqrt + c ^ 3 / ((c ^ 3) ^ 2 + 8 * a ^ 3 * b ^ 3).sqrt

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