lean_workbook_plus_27362
ProvedNow, by Cauchy-Schwarz, we have ${(am_{a}+bm_{b}+cm_{c})}^{2}\le (a^{2}+b^{2}+c^{2})(m_{a}^{2}+m_{b}^{2}+m_{c}^{2})
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_27362 (a b c : ℝ) (ma mb mc : ℝ) : (a * ma + b * mb + c * mc)^2 ≤ (a^2 + b^2 + c^2) * (ma^2 + mb^2 + mc^2) := by sorry
Source