Sums of squares

We introduce sums of squares in a type R endowed with an [Add R], [Zero R] and [Mul R] instances. Sums of squares in R are defined by an inductive predicate isSumSq : R → Prop: 0 : R is a sum of squares and if S is a sum of squares, then for all a : R, a * a + S is a sum of squares in R.

Main declaration

• The predicate isSumSq : R → Prop, defining the property of being a sum of squares in R.

Auxiliary declarations

• The type SumSqIn R : in an additive monoid with multiplication R, we introduce the type SumSqIn R as the submonoid of R whose carrier is the subset {S : R | isSumSq S}.

Theorems

• isSumSq.add: if S1 and S2 are sums of squares in R, then so is S1 + S2.
• SumSq.nonneg: in a linearly ordered semiring R with an [ExistsAddOfLE R] instance, sums of squares are non-negative.
• SquaresInSumSq: a square is a sum of squares.
• SquaresAddClosure: the submonoid of R generated by the squares in R is the set of sums of squares in R.

theorem isSumSq_iff {R : Type u_1} [Mul R] [Add R] [Zero R] : ∀ (a : R), isSumSq a ↔ a = 0 ∨ ∃ (a_1 : R) (S : R), isSumSq S ∧ a = a_1 * a_1 + S

inductive isSumSq {R : Type u_1} [Mul R] [Add R] [Zero R] : R → Prop

In a type R with an addition, a zero element and a multiplication, the property of being a sum of squares is defined by an inductive predicate: 0 : R is a sum of squares and if S is a sum of squares, then for all a : R, a * a + S is a sum of squares in R.

• zero: ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R], isSumSq 0
• sq_add: ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R] (a S : R), isSumSq S → isSumSq (a * a + S)

theorem isSumSq.add {R : Type u_1} [Mul R] [AddMonoid R] {S1 : R} {S2 : R} (p1 : isSumSq S1) (p2 : isSumSq S2) : isSumSq (S1 + S2)

If S1 and S2 are sums of squares in a semiring R, then S1 + S2 is a sum of squares in R.

def SumSqIn (R : Type u_1) [Mul R] [AddMonoid R] : AddSubmonoid R

In an additive monoid with multiplication R, the type SumSqIn R is the submonoid of sums of squares in R.

Equations

• SumSqIn R = { carrier := {S : R | isSumSq S}, add_mem' := ⋯, zero_mem' := ⋯ }

theorem SquaresInSumSq {R : Type u_1} [Mul R] [AddMonoid R] {x : R} (px : IsSquare x) : x ∈ SumSqIn R

In an additive monoid with multiplication, every square is a sum of squares. By definition, a square in R is a term x : R such that x = y * y for some y : R and in Mathlib this is known as IsSquare R (see Mathlib.Algebra.Group.Even).

theorem SquaresAddClosure {R : Type u_1} [Mul R] [AddMonoid R] : AddSubmonoid.closure IsSquare = SumSqIn R

In an additive monoid with multiplication R, the submonoid generated by the squares is the set of sums of squares.

theorem isSumSq.nonneg {R : Type u_2} [LinearOrderedSemiring R] [ExistsAddOfLE R] {S : R} (pS : isSumSq S) : 0 ≤ S

Let R be a linearly ordered semiring in which the property a ≤ b → ∃ c, a + c = b holds (e.g. R = ℕ). If S : R is a sum of squares in R, then 0 ≤ S. This is used in Mathlib.Algebra.Ring.Semireal.Defs to show that linearly ordered fields are semireal.