lean_workbook_plus_5361
Proved(4(x^{2}+y^{2}+z^{2}))^{3}\geq 27\prod (2x^{2}+y^{2}+z^{2})$
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_5361 (x y z : ℝ) : (4 * (x ^ 2 + y ^ 2 + z ^ 2)) ^ 3 ≥ 27 * (2 * x ^ 2 + y ^ 2 + z ^ 2) * (2 * y ^ 2 + z ^ 2 + x ^ 2) * (2 * z ^ 2 + x ^ 2 + y ^ 2) := by sorry
Source