lean_workbook_plus_10318
ProvedProve: $( (\frac{1}{\sqrt{3}})^2 + (\frac{1}{\sqrt{3}})^2 + (\frac{1}{\sqrt{3}})^2 ) * ( (3 - a)^2 + (3 - b)^2 + (3 - c)^2 ) \geq (\frac{3 - a}{\sqrt{3}} + \frac{3 - b}{\sqrt{3}} + \frac{3 - c}{\sqrt{3}})^2
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10318 {a b c : ℝ} : (1 / Real.sqrt 3 ^ 2 + 1 / Real.sqrt 3 ^ 2 + 1 / Real.sqrt 3 ^ 2) * ((3 - a) ^ 2 + (3 - b) ^ 2 + (3 - c) ^ 2) ≥ (1 / Real.sqrt 3 * (3 - a) + 1 / Real.sqrt 3 * (3 - b) + 1 / Real.sqrt 3 * (3 - c)) ^ 2 := by sorrySource