Showing that the sum of squares is non-negative

Stream: general

[Eric Chen]

Hey all,

I was wondering if there is a nice Lean theorem/tactic that I could utilize to show that the sum of squares is positive?

As a simple application, I want to rewrite the expression

$$2a^2 - 2ab - 2ac + b^2 + c^2 = (a-b)^2 + (a-c)^2$$

so that I can deduce

$$2a^2 - 2ab - 2ac + b^2 + c^2 \geq 0, \forall a,b,c \in \mathbb{R}.$$

I could probably show the first equality using ring, but after that, what should I do?

Thanks!

[Kevin Buzzard]

positivity? But you don't say what the types of your terms are. Writing a #mwe would probably get you a better answer.

[Eric Chen]

It looks like positivity solves it. Thanks so much!

For those who are curious, here's the solved code for this proof:

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Modeq
import Mathlib.Data.Int.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Divisibility.Basic
import Mathlib.Tactic.Ring
import Mathlib.Data.Nat.Prime
import Mathlib.Algebra.Group.Defs
import Mathlib.Algebra.EuclideanDomain.Defs
import Mathlib.Algebra.GroupPower.Basic
import Mathlib.Algebra.Field.Basic
import Mathlib.Tactic.Zify

theorem sum_of_squares_is_positive(a b c : ℝ):2*a^2 - 2*a*b - 2*a*c + b^2 + c^2 ≥ 0:= by
  have h1: 2*a^2 - 2*a*b - 2*a*c + b^2 + c^2 = (a - b)^2 + (a-c)^2 := by
    ring
  rw[h1]
  positivity

[Jireh Loreaux]

Surely Mathlib.Data.Real.Basic is the only import you need there?

[Kevin Buzzard]

Good to see that they were real numbers after all, not complex numbers :-)