Sums of squares - Basic properties of lists

import SumSq.Defs
import Batteries.Data.List.Basic
import Mathlib.Data.List.Perm
import Mathlib.Tactic.FieldSimp

import Mathlib.Data.Multiset.Basic

#check Multiset

#check List.Perm

Appended lists

Recall from #List.append that L1 ++ L2 (which is notation for List.append L1 L2) is defined as follows, by pattern matching on L1 (see Init.Data.List.Basic for details).

def List.append : (L1 L2 : List R) → List R
  | [], L2 => L2
  | a::l1, L2 => a :: List.append l1 L2

We now prove that the sum of squares of the list L1 ++ L2 is equal to the sum of squares of L1 plus the sum of squares of L2.

SumSq (L1 ++ L2) = SumSq L1 + SumSq L2

theorem SumSqAppend {R : Type} [Semiring R] (L1 L2 : List R) : SumSq (L1 ++ L2) = SumSq L1 + SumSq L2 := by
  induction L1 with -- we prove the result by induction on the list L1
  | nil => -- case when L1 is the empty list
    simp only [SumSq, zero_add, List.nil_append L2] -- since [] ++ L2 = L2 by definition of ++, the result follows by definition of SumSq
  | cons a l1 ih => -- case when L1 = (a :: L)
    simp [SumSq] -- by [`List.cons_append](https://leanprover-community.github.io/mathlib4_docs/Init/Data/List/Basic.html#List.cons_append) (a :: L) ++ L2 = a :: (L ++ L2), so SumSq (a :: (L ++ L2)) = a ^ 2  + SumSq (L ++ L2)
    rw [ih] -- recall that ih : SumSq (L ++ L2) = SumSq L + SumSq L2
    rw [add_assoc] -- the two terms are now equal up to associativity of addition

Permuted lists

Recall from #List.Perm that the relation L1 ~ L2 (which is notation for List.Perm L1 L2) is defined inductively using pairwise swaps.

inductive Perm : List R → List R → Prop
  | nil : Perm [] []
  | cons (a : R) {l₁ l₂ : List R} : Perm l₁ l₂ → Perm (a :: l₁) (a :: l₂)
  | swap (a₁ a₂ : R) (l : List R) : Perm (a₂ :: a₁ :: l) (a₁ :: a₂ :: l)
  | trans {L₁ L₂ L₃ : List R} : Perm L₁ L₂ → Perm L₂ L₃ → Perm L₁ L₃

So we wee that List.Perm is an inductive type: a list L2 is a permutation of the list L1 if and only if one of four cases occurs.

We can now prove that a sum of squares is invariant under permutations:

L1 ~ L2 → SumSq L1 = SumSq L2

Note that, since List.Perm uses implicit variables for the constructors cons and trans, we choose to write the proof by indution with a slighty different syntax (using case), to make the Lean infoview rendering more readable (for more on this, see Exercise 1 below).

theorem SumSqPermut {R : Type} [Semiring R] {L1 L2 : List R} (H : L1.Perm L2) : SumSq L1 = SumSq L2 := by
  induction H -- we prove the result by induction on `H`, which is a term of type `L1 ~ L2` (and the latter is indeed inductively defined)
  · case nil => -- case when L1 L2 are both empty
    rfl -- equality holds by definition
  · case cons x l1 l2 Hl Sum12 => -- case when L1 = (x :: l1) and L2 = (x :: l2) with l1 ~ l2
    simp only [SumSq] -- by definition, SumSq (x :: lj) = x ^ 2  + SumSq lj for j = 1, 2
    rw [Sum12] -- by induction, SumSq l1 = SumSq l2
  · case swap a b L => -- case when L1 = (b :: (a :: L)) and L2 = (a :: (b :: L))
    simp only [SumSq] -- by definition, SumSq (b :: (a :: L)) = b ^ 2  + (a ^ 2  + SumSq L)
    rw [← add_assoc, ← add_assoc, add_comm (b ^ 2) (a ^ 2)] -- the two expressions are equal in R
  · case trans L1 L L2 H1 H2 Sum1 Sum2 => -- case when L1 ~ L and L ~ L2
    rw [Sum1, Sum2] -- by induction SumSq L1 = SumSq L and SumSq L = SumSq L2

Erasing an entry

The function List.erase can erase an entry of a list. It is defined as follows in #List.erase.

def List.erase {R : Type} [BEq R] : List R → R → List R
  | [], _ => []
  | a::l, b => match a == b with
    | true  => l
    | false => a :: List.erase l b

Note that this declaration uses Boolean equality. It could be written using decidable equality, in the following way.

def List.erase' {R : Type} [DecidableEq R] : List R → R → List R
  | [], _ => []
  | a::l, b => if a = b then l else List.erase' l b

Whichever definition of erase we choose, we need to assume that the type R has decidable equality in order to be able to use it (and the same goes for the function #List.perm_cons_erase, also used below).

We now prove that, if a term a : R is an entry of a list L : List R, then we can compute SumSq L from a and SumSq (L.erase a). More precisely:

a ∈ L → SumSq L = a ^ 2 + SumSq (L.erase a)

The type a ∈ L is defined in #List.Mem. It is an inductive type: a term a : R belongs to a list L : List R if and only if L = (a :: l) or L = (b :: l) with b ∈ l.

theorem SumSqErase {R : Type} [Semiring R] [DecidableEq R] (L : List R) (a : R) (h : a ∈ L) : SumSq L = a ^ 2 + SumSq (L.erase a) := by
  have H : L.Perm (a :: (L.erase a)) := L.perm_cons_erase h -- this is the Mathlib proof that, if a ∈ L, then L ~ (a :: (L.erase a)), see also the exercises section below
  rw [SumSqPermut H] -- since we have a proof that L ~ (a :: (L.erase a)), we can use the SumSq_permut function that we defined earlier to conclude that the two sums of squares are equal
  rw [SumSq]  -- the last simplification follows by definition of `SumSq`

Multiplication by a scalar

Let L be a list with entries in a semiring R. If c is a term of type R, we can multiply each entry of L by c to define a new list, that we shall denote c • L. For instance, if L = [x, y, z], we should have:

c • [x, y, z] = [c * x, c * y, c * z]

Let us define this formally and take a look at a few examples. As we shall see, one has to be precise in the notation, in order for Lean to interpret the command correctly.

def ListSmul {R : Type} [Semiring R] (c : R) : List R → List R
  | [] => []
  | a :: l => (c * a) :: ListSmul c l

infixl:50 " • " => ListSmul

theorem ListSmulMap {R : Type} [Semiring R] (c : R) (L : List R) : (c • L) = L.map (c * .) := by
  induction L with
  | nil => simp [ListSmul]  -- the case of the empty list is trivial
  | cons a l ih =>  simp [ListSmul, ih]  -- the case of a list of the form (a :: l) reduces immediately to the induction hypothesis

#eval ListSmul 2 [1, -2, 3]  --[2, -4, 6]
#eval ((2 : ℤ) • [1, -2, 3])

example : ListSmul 2 [1, -2, 3] = [2, -4, 6] := by rfl

#eval SumSq (ListSmul 2 [1, -2, 3])  -- 56
#eval SumSq ((2 : ℤ) • [1, -2, 3])  -- 56

example : SumSq (ListSmul 2 [1, -2, 3]) = 4 * SumSq [1, -2, 3] := by rfl

#eval SumSq [2, -4, 6]
#eval 4 * SumSq [1, -2, 3]  -- 56

example (a x y : ℚ) : (ListSmul a [x, y]) = [a * x, a * y] := by rfl
example (a x y : ℚ) : SumSq (ListSmul a [x, y]) = a ^ 2 * SumSq [x, y] := by simp [SumSq, mul_pow, mul_add, ListSmul]

The result we expect is then the following:

SumSq (c • L) = c ^ 2 * SumSq L

We will see below that this result holds when R is a commutative semiring.

Indeed, in order to be able to apply lemmas such as #mul_pow in the proof, we need to assume that the semiring R is commutative.

Before proving the result that is relevant result, we prove an easier one, of possibly greater general interest, with SumSq replaced by List.sum.

theorem SumSmul {R : Type} [Semiring R] (c : R) (L : List R) : List.sum (c • L) = c * (List.sum L) := by
  induction L with
  | nil => simp only [ListSmul, List.sum_nil, mul_zero]
  | cons a l ih => simp [ListSmul, mul_add, ih]

theorem SumSqSmul {R : Type} [CommSemiring R] (c : R) (L : List R) : SumSq (c • L) = c ^ 2 * SumSq L := by
    induction L with -- we prove the result by induction on L
    | nil => simp only [SumSq, mul_zero, ListSmul]  -- the case of the empty list is trivial
    | cons a l ih => simp only [ListSmul, SumSq, mul_add, ih, mul_pow] -- the case of a list of the form (a :: l) follows from simplifications and the use of the induction hypothesis

If we assume that the semiring R is in fact a semifield, then we can also consider the list from L obtained by dividing each entry by a term c such that `c ≠ 0’.

theorem SumSqDiv {F : Type} [Semifield F]
  (L : List F) (c : F) : SumSq (L.map (. / c)) = (1 / c ^ 2) * SumSq L := by
    -- this will be an application of mul_sum_sq2, using the fact that . / c = . * c⁻¹
    have aux : (fun x => x / c) = (fun x => c⁻¹ * x) := by field_simp
    simp only [aux, ← ListSmulMap, SumSqSmul]
    field_simp

Note that no assumption (hc : c ≠ 0) has been used because Lean gives a value to division by c in F even if c = 0 and that the equality remains true in this case.

example [Semifield F] (x : F) : x / 0 = 0 := by field_simp

More computations

Before moving on to the exercises, we give another proof of theorem SumSqSmul, seen in the section on Multiplication by a scalar.

It is a direct, more computational proof, harder to follow than the original proof (by induction).

lemma SumSmul2 {R : Type} [Semiring R]  (c : R) (L : List R) : (L.map (c * .)).sum = c * L.sum := by
  induction L with
  | nil => simp
  | cons a l ih => simp [mul_add, ih]

theorem SumSqSmul2 {R : Type} [CommSemiring R] (L : List R) (c : R) : ((L.map (c * .)).map (. ^2)).sum = c ^ 2 * (L.map (. ^ 2)).sum := by
    simp [mul_add, mul_pow, ← SumSmul2]  -- we simplify the statement
    have aux : ((fun x => x ^ 2) ∘ fun x => c * x) = ((fun x => c ^ 2 * x) ∘ fun x => x ^ 2)
      := by simp [Function.funext_iff, mul_pow]  -- we prove an auxiliary result in order to incorporate it in the goal
    rw [aux]

Exercises

Exercise 1

Modify the syntax of the induction tactic in SumSqPermut to make it look more similar to that of SumSqAppend. This means: in SumSqPermut, replace induction H by induction H with and make the proof syntactically correct after that (start by changing ⬝ case nil to | nil).

Exercise 2

Let R be a type with decidable equality. Let a be a term of type R and let L be a term of type List R. Prove that, if a ∈ L, then the list a :: L.erase a is a permutation of L (we have used this standard result here).

Exercise 3

Prove that the statement of theorem SumSqSmul2 is indeed equivalent to the statement of theorem SumSqSmul.