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} [Mul R] [Add R] [Zero R] : IsSumSq 0
• sq_add {R : Type u_1} [Mul R] [Add R] [Zero R] (a S : R) (pS : 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 : R) (S : R), IsSumSq S ∧ a✝ = a * a + S

@[deprecated IsSumSq (since := "2024-08-09")]

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 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 (since := "2024-08-09")]

theorem isSumSq.add {R : Type u_1} [Mul R] [AddMonoid R] {S1 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.

@[deprecated IsSumSq.sum_mul_self (since := "2024-12-27")]

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)

Alias of IsSumSq.sum_mul_self.

---

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 (since := "2024-08-09")]

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 (since := "2024-08-09")]

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 (since := "2024-08-09")]

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 (since := "2024-08-09")]

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.