lean_workbook_plus_5606
ProvedProve that $ \dfrac{1}{2a^2+b^2+3} + \dfrac{1}{2b^2+c^2+3} + \dfrac{1}{2c^2+a^2+3} \le \dfrac{1}{2} $ for positive real numbers $ a,b,c $ such that $ abc = 1 $
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_5606 (a b c : ℝ) (habc : a * b * c = 1) : 1 / (2 * a ^ 2 + b ^ 2 + 3) + 1 / (2 * b ^ 2 + c ^ 2 + 3) + 1 / (2 * c ^ 2 + a ^ 2 + 3) ≤ 1 / 2 := by sorry
Source