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.
• IsSumSq.nonneg: in a linearly ordered semiring R with an [ExistsAddOfLE R] instance, sums of squares are non-negative.
• mem_sumSqIn_of_isSquare: a square is a sum of squares.
• AddSubmonoid.closure_isSquare: the submonoid of R generated by the squares in R is the set of sums of squares in R.

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_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

@[deprecated IsSumSq]

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

Alias of IsSumSq.

---

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.

Equations

• @isSumSq = @IsSumSq

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.

@[deprecated IsSumSq.add]

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

Alias of IsSumSq.add.

---

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

theorem isSumSq_sum_mul_self {R : Type u_1} [Mul R] {ι : Type u_2} [AddCommMonoid R] (s : Finset ι) (f : ι → R) : IsSumSq (∑ i ∈ s, f i * f i)

A finite sum of squares is a sum of squares.

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' := ⋯ }

@[deprecated sumSqIn]

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

Alias of sumSqIn.

---

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

Equations

• SumSqIn = sumSqIn

theorem mem_sumSqIn_of_isSquare {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).

@[deprecated mem_sumSqIn_of_isSquare]

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

Alias of mem_sumSqIn_of_isSquare.

---

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 AddSubmonoid.closure_isSquare {R : Type u_1} [Mul R] [AddMonoid R] : AddSubmonoid.closure {x : R | IsSquare x} = sumSqIn R

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

@[deprecated AddSubmonoid.closure_isSquare]

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

Alias of AddSubmonoid.closure_isSquare.

---

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.

@[deprecated IsSumSq.nonneg]

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

Alias of IsSumSq.nonneg.

---

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.