Grace/Cumulus/LinearAlgebra/Matrix.g17

Open in Workbench Download source

Imports

FiniteDimensional

Declarations

Source

1-- Matrices as set-theoretic functions on pairs of natural indices.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.LinearAlgebra.Matrix8import FiniteDimensional910-- Dimensions are cutoffs on a total array, so one matrix can be reused at11-- several finite sizes without changing its underlying set-theoretic graph.12predicate RealMatrix (M : Set) := FunctionBetween(M, ℕ × ℕ, ℝ)1314-- Coordinates are uniquely determined on the Cartesian product.15-- Extracting them needs only ZF and supports matrix graphs over index pairs.16defunique matrixFirstIndex (p : Set) (i ∈ ℕ) :=17  ∃ j ∈ ℕ, p = (i, j)18requires pair : p ∈ ℕ × ℕ19proof20  have shape := product.membership.forward at ℕ, ℕ, p with pair21  rcases shape with ⟨bound, i, naturalI, j, naturalJ, equation⟩22  witness i23  refine ⟨naturalI, j, naturalJ, equation⟩2425uniqueness26  intros a aMember first c cMember second27  obtain ⟨b, bMember, firstPair⟩ := first28  obtain ⟨d, dMember, secondPair⟩ := second29  have same : (a, b) = (c, d)30    cc31  have coordinates := orderedPair.injective at a, b, c, d with same32  tauto3334defunique matrixSecondIndex (p : Set) (j ∈ ℕ) :=35  ∃ i ∈ ℕ, p = (i, j)36requires pair : p ∈ ℕ × ℕ37proof38  have shape := product.membership.forward at ℕ, ℕ, p with pair39  rcases shape with ⟨bound, i, naturalI, j, naturalJ, equation⟩40  witness j41  refine ⟨naturalJ, i, naturalI, equation⟩4243uniqueness44  intros b bMember first d dMember second45  obtain ⟨a, aMember, firstPair⟩ := first46  obtain ⟨c, cMember, secondPair⟩ := second47  have same : (a, b) = (c, d)48    cc49  have coordinates := orderedPair.injective at a, b, c, d with same50  tauto5152theorem matrixFirstIndex.pair (i j : Nat)53  shows matrixFirstIndex((i, j)) = i54proof55  have naturalI : i ∈ ℕ by simp [Nat]56  have naturalJ : j ∈ ℕ by simp [Nat]57  have pair := product.pair with naturalI, naturalJ58  obtain ⟨natural, k, naturalK, shape⟩ := matrixFirstIndex.selected with pair59  obtain ⟨first, second⟩ := orderedPair.injective with shape60  rw ←first61  rfl6263theorem matrixSecondIndex.pair (i j : Nat)64  shows matrixSecondIndex((i, j)) = j65proof66  have naturalI : i ∈ ℕ by simp [Nat]67  have naturalJ : j ∈ ℕ by simp [Nat]68  have pair := product.pair with naturalI, naturalJ69  obtain ⟨natural, k, naturalK, shape⟩ := matrixSecondIndex.selected with pair70  obtain ⟨first, second⟩ := orderedPair.injective with shape71  rw ←second72  rfl7374theorem RealMatrix.entry (M : Set, i j : Nat)75  requires matrix : RealMatrix(M)76  shows Real(M[i, j])77proof78  unfold RealMatrix at matrix79  have iNatural : i ∈ ℕ by simp [Nat]80  have jNatural : j ∈ ℕ by simp [Nat]81  have pair := product.pair with iNatural, jNatural82  exact FunctionBetween.apply_closed with matrix, pair8384defgraph matrixTranspose (M : Set) (p ∈ ℕ × ℕ) : ℝ :=85  M[matrixSecondIndex(p), matrixFirstIndex(p)]86requires matrix : RealMatrix(M)87proof88  have first := matrixFirstIndex.selected with member89  have second := matrixSecondIndex.selected with member90  rcases first with ⟨naturalFirst, j, naturalJ, shapeFirst⟩91  rcases second with ⟨naturalSecond, i, naturalI, shapeSecond⟩92  have typedFirst := nat.omega.backward with naturalFirst93  have typedSecond := nat.omega.backward with naturalSecond94  exact RealMatrix.entry at95    M, matrixSecondIndex(p), matrixFirstIndex(p) with matrix9697theorem matrixTranspose.matrix (M : Set)98  requires matrix : RealMatrix(M)99  shows RealMatrix(matrixTranspose(M))100proof101  unfold RealMatrix102  exact matrixTranspose.function with matrix103104theorem matrixTranspose.entry (M : Set, i j : Nat)105  requires matrix : RealMatrix(M)106  shows matrixTranspose(M)[i, j] = M[j, i]107proof108  have naturalI : i ∈ ℕ by simp [Nat]109  have naturalJ : j ∈ ℕ by simp [Nat]110  have pair := product.pair with naturalI, naturalJ111  have value := matrixTranspose.value with matrix112  rw [value, matrixFirstIndex.pair, matrixSecondIndex.pair]113  rfl114115defgraph matrixAdd (A B : Set) (p ∈ ℕ × ℕ) : ℝ :=116  call2(realAdd, A[matrixFirstIndex(p), matrixSecondIndex(p)],117    B[matrixFirstIndex(p), matrixSecondIndex(p)])118requires matrixA : RealMatrix(A)119requires matrixB : RealMatrix(B)120proof121  have first := matrixFirstIndex.selected with member122  have second := matrixSecondIndex.selected with member123  rcases first with ⟨naturalFirst, j, naturalJ, shapeFirst⟩124  rcases second with ⟨naturalSecond, i, naturalI, shapeSecond⟩125  have typedFirst := nat.omega.backward with naturalFirst126  have typedSecond := nat.omega.backward with naturalSecond127  have left := RealMatrix.entry at A, matrixFirstIndex(p), matrixSecondIndex(p) with matrixA128  have right := RealMatrix.entry at B, matrixFirstIndex(p), matrixSecondIndex(p) with matrixB129  exact realAddValue.real with left, right130131theorem matrixAdd.matrix (A B : Set)132  requires matrixA : RealMatrix(A)133  requires matrixB : RealMatrix(B)134  shows RealMatrix(matrixAdd(A, B))135proof136  unfold RealMatrix137  exact matrixAdd.function with matrixA, matrixB138139theorem matrixAdd.entry (A B : Set, i j : Nat)140  requires matrixA : RealMatrix(A)141  requires matrixB : RealMatrix(B)142  shows matrixAdd(A, B)[i, j] = (A[i, j]:R) + (B[i, j]:R)143proof144  have naturalI : i ∈ ℕ by simp [Nat]145  have naturalJ : j ∈ ℕ by simp [Nat]146  have pair := product.pair with naturalI, naturalJ147  have value := matrixAdd.value with matrixA, matrixB148  rw [value, matrixFirstIndex.pair, matrixSecondIndex.pair]149  rfl150151defgraph matrixScale (C : Real, M : Set) (p ∈ ℕ × ℕ) : ℝ :=152  realMul(C, M[matrixFirstIndex(p), matrixSecondIndex(p)])153requires matrix : RealMatrix(M)154proof155  have first := matrixFirstIndex.selected with member156  have second := matrixSecondIndex.selected with member157  rcases first with ⟨naturalFirst, j, naturalJ, shapeFirst⟩158  rcases second with ⟨naturalSecond, i, naturalI, shapeSecond⟩159  have typedFirst := nat.omega.backward with naturalFirst160  have typedSecond := nat.omega.backward with naturalSecond161  have entry := RealMatrix.entry at M, matrixFirstIndex(p), matrixSecondIndex(p) with matrix162  have scaled := realMulValue.real at C,163    M[matrixFirstIndex(p), matrixSecondIndex(p)] with assumption, entry164  exact scaled165166theorem matrixScale.matrix (C : Real, M : Set)167  requires matrix : RealMatrix(M)168  shows RealMatrix(matrixScale(C, M))169proof170  unfold RealMatrix171  exact matrixScale.function with matrix172173theorem matrixScale.entry (C : Real, M : Set, i j : Nat)174  requires matrix : RealMatrix(M)175  shows matrixScale(C, M)[i, j] = C * (M[i, j]:R)176proof177  have naturalI : i ∈ ℕ by simp [Nat]178  have naturalJ : j ∈ ℕ by simp [Nat]179  have pair := product.pair with naturalI, naturalJ180  have value := matrixScale.value with matrix181  rw [value, matrixFirstIndex.pair, matrixSecondIndex.pair]182  rfl183184-- Equality of indices uniquely determines the diagonal coefficient in ZF.185defunique diagonalCoefficient (i j : Nat) (X ∈ ℝ) :=186  (i = j → X = (1:R)) ∧ (i ≠ j → X = (0:R))187proof188  have alternatives : i = j ∨ i ≠ j by tauto189  cases alternatives with equal | distinct190  . witness (1:R)191    constructor192    . exact realOne.real193    . constructor194      . intro same195        rfl196      . intro impossible197        exfalso198        exact impossible with equal199  . witness (0:R)200    constructor201    . exact realZero.real202    . constructor203      . intro impossible204        exfalso205        exact distinct with impossible206      . intro different207        rfl208209uniqueness210  intros u uMember first v vMember second211  have alternatives : i = j ∨ ¬(i = j) by tauto212  cases alternatives with present | absent213  . have uValue : u = (1:R)214      tauto215    have vValue : v = (1:R) by tauto216    cc217  . have uValue : u = (0:R)218      tauto219    have vValue : v = (0:R) by tauto220    cc221222theorem diagonalCoefficient.same (i : Nat)223  shows diagonalCoefficient(i, i) = (1:R)224proof225  have selected := diagonalCoefficient.selected at i, i with *226  rcases selected with ⟨real, diagonal, offDiagonal⟩227  have self : i = i by rfl228  exact diagonal with self229230theorem diagonalCoefficient.distinct (i j : Nat)231  requires different : i ≠ j232  shows diagonalCoefficient(i, j) = (0:R)233proof234  have selected := diagonalCoefficient.selected at i, j with *235  rcases selected with ⟨real, diagonal, offDiagonal⟩236  exact offDiagonal with different237238defgraph identityMatrix (n : Nat) (p ∈ ℕ × ℕ) : ℝ :=239  diagonalCoefficient(matrixFirstIndex(p), matrixSecondIndex(p))240proof241  have first := matrixFirstIndex.selected with member242  have second := matrixSecondIndex.selected with member243  rcases first with ⟨naturalFirst, j, naturalJ, shapeFirst⟩244  rcases second with ⟨naturalSecond, i, naturalI, shapeSecond⟩245  have typedFirst := nat.omega.backward with naturalFirst246  have typedSecond := nat.omega.backward with naturalSecond247  obtain ⟨real, diagonal, offDiagonal⟩ := diagonalCoefficient.selected with typedFirst, typedSecond248  exact real249250theorem identityMatrix.matrix (n : Nat)251  shows RealMatrix(identityMatrix(n))252proof253  unfold RealMatrix254  exact identityMatrix.function with assumption255256theorem identityMatrix.entry (n i j : Nat)257  shows identityMatrix(n)[i, j] = diagonalCoefficient(i, j)258proof259  have naturalI : i ∈ ℕ by simp [Nat]260  have naturalJ : j ∈ ℕ by simp [Nat]261  have pair := product.pair with naturalI, naturalJ262  have value := identityMatrix.value at n, (i, j)263  rw [value, matrixFirstIndex.pair, matrixSecondIndex.pair]264  rfl265266theorem identityMatrix.diagonal (n i : Nat)267  shows identityMatrix(n)[i, i] = (1:R)268proof269  rw identityMatrix.entry270  exact diagonalCoefficient.same with assumption271272theorem identityMatrix.off_diagonal (n i j : Nat)273  requires different : i ≠ j274  shows identityMatrix(n)[i, j] = (0:R)275proof276  rw identityMatrix.entry277  exact diagonalCoefficient.distinct with *278279theorem matrixAdd.commutative_entry (A B : Set, i j : Nat)280  requires matrixA : RealMatrix(A)281  requires matrixB : RealMatrix(B)282  shows matrixAdd(A, B)[i, j] = matrixAdd(B, A)[i, j]283proof284  have typedA := RealMatrix.entry at A, i, j with matrixA285  have typedB := RealMatrix.entry at B, i, j with matrixB286  rw [matrixAdd.entry, matrixAdd.entry]287  ring288289theorem matrixAdd.associative_entry (A B C : Set, i j : Nat)290  requires matrixA : RealMatrix(A)291  requires matrixB : RealMatrix(B)292  requires matrixC : RealMatrix(C)293  shows matrixAdd(matrixAdd(A, B), C)[i, j] =294    matrixAdd(A, matrixAdd(B, C))[i, j]295proof296  have typedAB := matrixAdd.matrix with matrixA, matrixB297  have typedBC := matrixAdd.matrix with matrixB, matrixC298  have typedA := RealMatrix.entry at A, i, j with matrixA299  have typedB := RealMatrix.entry at B, i, j with matrixB300  have typedC := RealMatrix.entry at C, i, j with matrixC301  rw [matrixAdd.entry, matrixAdd.entry, matrixAdd.entry, matrixAdd.entry]302  ring303304theorem matrixScale.add_entry (A B : Set, C : Real, i j : Nat)305  requires matrixA : RealMatrix(A)306  requires matrixB : RealMatrix(B)307  shows matrixScale(C, matrixAdd(A, B))[i, j] =308    matrixAdd(matrixScale(C, A), matrixScale(C, B))[i, j]309proof310  have combined := matrixAdd.matrix with matrixA, matrixB311  have scaledA := matrixScale.matrix with matrixA312  have scaledB := matrixScale.matrix with matrixB313  have typedA := RealMatrix.entry at A, i, j with matrixA314  have typedB := RealMatrix.entry at B, i, j with matrixB315  rw [matrixScale.entry, matrixAdd.entry, matrixAdd.entry, matrixScale.entry, matrixScale.entry]316  ring317318theorem matrixTranspose.add_entry (A B : Set, i j : Nat)319  requires matrixA : RealMatrix(A)320  requires matrixB : RealMatrix(B)321  shows matrixTranspose(matrixAdd(A, B))[i, j] =322    matrixAdd(matrixTranspose(A), matrixTranspose(B))[i, j]323proof324  have combined := matrixAdd.matrix with matrixA, matrixB325  have transposedA := matrixTranspose.matrix with matrixA326  have transposedB := matrixTranspose.matrix with matrixB327  rw [matrixTranspose.entry, matrixAdd.entry, matrixAdd.entry, matrixTranspose.entry, matrixTranspose.entry]328  rfl329330theorem matrixTranspose.scale_entry (C : Real, M : Set, i j : Nat)331  requires matrix : RealMatrix(M)332  shows matrixTranspose(matrixScale(C, M))[i, j] =333    matrixScale(C, matrixTranspose(M))[i, j]334proof335  have scaled := matrixScale.matrix with matrix336  have transposed := matrixTranspose.matrix with matrix337  rw [matrixTranspose.entry, matrixScale.entry, matrixScale.entry, matrixTranspose.entry]338  rfl339340defgraph matrixRow (M : Set, i : Nat) (j ∈ ℕ) : ℝ := M[i, j]341requires matrix : RealMatrix(M)342proof343  have typedJ := nat.omega.backward with member344  exact RealMatrix.entry at M, i, j with matrix345346theorem matrixRow.sequence (M : Set, i : Nat)347  requires matrix : RealMatrix(M)348  shows RealSequence(matrixRow(M, i))349proof350  unfold RealSequence351  exact matrixRow.function with matrix352353defgraph matrixColumn (M : Set, j : Nat) (i ∈ ℕ) : ℝ := M[i, j]354requires matrix : RealMatrix(M)355proof356  have typedI := nat.omega.backward with member357  exact RealMatrix.entry at M, i, j with matrix358359theorem matrixColumn.sequence (M : Set, j : Nat)360  requires matrix : RealMatrix(M)361  shows RealSequence(matrixColumn(M, j))362proof363  unfold RealSequence364  exact matrixColumn.function with matrix365366theorem matrixTranspose.involutive_entry (M : Set, i j : Nat)367  requires matrix : RealMatrix(M)368  shows matrixTranspose(matrixTranspose(M))[i, j] = M[i, j]369proof370  have transposed := matrixTranspose.matrix with matrix371  have outer := matrixTranspose.entry at matrixTranspose(M), i, j with transposed372  have inner := matrixTranspose.entry at M, j, i with matrix373  rwa outer374375theorem matrixTranspose.row_column (M : Set, i j : Nat)376  requires matrix : RealMatrix(M)377  shows matrixRow(matrixTranspose(M), i)[j] = matrixColumn(M, i)[j]378proof379  have transposed := matrixTranspose.matrix with matrix380  have entry := matrixTranspose.entry at M, i, j with matrix381  rwa [matrixRow.value, matrixColumn.value]382383defgraph matrixProduct (A B : Set, n : Nat) (p ∈ ℕ × ℕ) : ℝ :=384  dotProduct(matrixRow(A, matrixFirstIndex(p)),385    matrixColumn(B, matrixSecondIndex(p)), n)386requires matrixA : RealMatrix(A)387requires matrixB : RealMatrix(B)388proof389  have first := matrixFirstIndex.selected with member390  have second := matrixSecondIndex.selected with member391  rcases first with ⟨naturalFirst, j, naturalJ, shapeFirst⟩392  rcases second with ⟨naturalSecond, i, naturalI, shapeSecond⟩393  have typedFirst := nat.omega.backward with naturalFirst394  have typedSecond := nat.omega.backward with naturalSecond395  have row := matrixRow.sequence at A, matrixFirstIndex(p) with matrixA396  have column := matrixColumn.sequence at B, matrixSecondIndex(p) with matrixB397  have value := dotProduct.real at matrixRow(A, matrixFirstIndex(p)),398    matrixColumn(B, matrixSecondIndex(p)), n with row, column399  exact value400401theorem matrixProduct.matrix (A B : Set, n : Nat)402  requires matrixA : RealMatrix(A)403  requires matrixB : RealMatrix(B)404  shows RealMatrix(matrixProduct(A, B, n))405proof406  unfold RealMatrix407  exact matrixProduct.function with matrixA, matrixB408409theorem matrixProduct.entry (A B : Set, n i j : Nat)410  requires matrixA : RealMatrix(A)411  requires matrixB : RealMatrix(B)412  shows matrixProduct(A, B, n)[i, j] =413    dotProduct(matrixRow(A, i), matrixColumn(B, j), n)414proof415  have naturalI : i ∈ ℕ by simp [Nat]416  have naturalJ : j ∈ ℕ by simp [Nat]417  have pair := product.pair with naturalI, naturalJ418  have value := matrixProduct.value at A, B, n, (i, j) with matrixA, matrixB419  rw [value, matrixFirstIndex.pair, matrixSecondIndex.pair]420  rfl421422theorem matrixProduct.zero (A B : Set, i j : Nat)423  requires matrixA : RealMatrix(A)424  requires matrixB : RealMatrix(B)425  shows matrixProduct(A, B, 0)[i, j] = (0:R)426proof427  have value := matrixProduct.entry at A, B, 0, i, j with matrixA, matrixB428  rw value429  exact dotProduct.zero430431theorem matrixProduct.succ (A B : Set, n i j : Nat)432  requires matrixA : RealMatrix(A)433  requires matrixB : RealMatrix(B)434  shows matrixProduct(A, B, succ(n))[i, j] =435    (matrixProduct(A, B, n)[i, j]:R) + (A[i, n]:R) * (B[n, j]:R)436proof437  have row := matrixRow.sequence at A, i with matrixA438  have column := matrixColumn.sequence at B, j with matrixB439  have step := dotProduct.succ at matrixRow(A, i), matrixColumn(B, j), n with row, column440  rw [matrixRow.value, matrixColumn.value] at step441  have next := matrixProduct.entry at A, B, succ(n), i, j with matrixA, matrixB442  have previous := matrixProduct.entry at A, B, n, i, j with matrixA, matrixB443  rwa [next, previous]444445theorem matrixProduct.transpose_entry (A B : Set, n i j : Nat)446  requires matrixA : RealMatrix(A)447  requires matrixB : RealMatrix(B)448  shows matrixTranspose(matrixProduct(A, B, n))[i, j] =449    matrixProduct(matrixTranspose(B), matrixTranspose(A), n)[i, j]450proof451  induction n452  | zero =>453    have transposedA := matrixTranspose.matrix with matrixA454    have transposedB := matrixTranspose.matrix with matrixB455    have product := matrixProduct.matrix at A, B, 0 with matrixA, matrixB456    have flip := matrixTranspose.entry at matrixProduct(A, B, 0), i, j with product457    have left := matrixProduct.zero at A, B, j, i with matrixA, matrixB458    have right := matrixProduct.zero at matrixTranspose(B), matrixTranspose(A), i, j with459      transposedB, transposedA460    rw [flip, left, right]461    rfl462  | succ(k) using ih =>463    have transposedA := matrixTranspose.matrix with matrixA464    have transposedB := matrixTranspose.matrix with matrixB465    have product := matrixProduct.matrix at A, B, succ(k) with matrixA, matrixB466    have flip := matrixTranspose.entry at matrixProduct(A, B, succ(k)), i, j with product467    have left := matrixProduct.succ at A, B, k, j, i with matrixA, matrixB468    have right := matrixProduct.succ at469      matrixTranspose(B), matrixTranspose(A), k, i, j with transposedB, transposedA470    have oldProduct := matrixProduct.matrix at A, B, k with matrixA, matrixB471    have oldFlip := matrixTranspose.entry at matrixProduct(A, B, k), i, j with oldProduct472    have Bentry := matrixTranspose.entry at B, i, k with matrixB473    have Aentry := matrixTranspose.entry at A, k, j with matrixA474    have realA := RealMatrix.entry at A, j, k with matrixA475    have realB := RealMatrix.entry at B, k, i with matrixB476    have realOld := RealMatrix.entry at matrixProduct(A, B, k), j, i with oldProduct477    have reverseProduct := matrixProduct.matrix at matrixTranspose(B),478      matrixTranspose(A), k with transposedB, transposedA479    have realReverse := RealMatrix.entry at480      matrixProduct(matrixTranspose(B), matrixTranspose(A), k), i, j with reverseProduct481    rw [flip, left, right, Bentry, Aentry, ←oldFlip, ih]482    ring483484theorem matrixProduct.add_right_entry (A B C : Set, i j n : Nat)485  requires matrixA : RealMatrix(A)486  requires matrixB : RealMatrix(B)487  requires matrixC : RealMatrix(C)488  shows matrixProduct(A, matrixAdd(B, C), n)[i, j] =489    matrixAdd(matrixProduct(A, B, n), matrixProduct(A, C, n))[i, j]490proof491  induction n492  | zero =>493    have combined := matrixAdd.matrix with matrixB, matrixC494    have productB := matrixProduct.matrix at A, B, 0 with matrixA, matrixB495    have productC := matrixProduct.matrix at A, C, 0 with matrixA, matrixC496    have left := matrixProduct.zero at A, matrixAdd(B, C), i, j with matrixA, combined497    have rightB := matrixProduct.zero at A, B, i, j with matrixA, matrixB498    have rightC := matrixProduct.zero at A, C, i, j with matrixA, matrixC499    rw [left, matrixAdd.entry, rightB, rightC]500    ring501  | succ(k) using ih =>502    have combined := matrixAdd.matrix with matrixB, matrixC503    have nextB := matrixProduct.matrix at A, B, succ(k) with matrixA, matrixB504    have nextC := matrixProduct.matrix at A, C, succ(k) with matrixA, matrixC505    have oldB := matrixProduct.matrix at A, B, k with matrixA, matrixB506    have oldC := matrixProduct.matrix at A, C, k with matrixA, matrixC507    have oldCombined := matrixProduct.matrix at A, matrixAdd(B, C), k with matrixA, combined508    have left := matrixProduct.succ at A, matrixAdd(B, C), k, i, j with matrixA, combined509    have rightB := matrixProduct.succ at A, B, k, i, j with matrixA, matrixB510    have rightC := matrixProduct.succ at A, C, k, i, j with matrixA, matrixC511    have entry := matrixAdd.entry at B, C, k, j with matrixB, matrixC512    have previous := matrixAdd.entry at matrixProduct(A, B, k),513      matrixProduct(A, C, k), i, j with oldB, oldC514    have realA := RealMatrix.entry at A, i, k with matrixA515    have realB := RealMatrix.entry at B, k, j with matrixB516    have realC := RealMatrix.entry at C, k, j with matrixC517    have realOldB := RealMatrix.entry at matrixProduct(A, B, k), i, j with oldB518    have realOldC := RealMatrix.entry at matrixProduct(A, C, k), i, j with oldC519    have realOldCombined := RealMatrix.entry at matrixProduct(A, matrixAdd(B, C), k),520      i, j with oldCombined521    rw [left, entry, matrixAdd.entry, rightB, rightC]522    rw previous at ih523    rw ih524    ring525526theorem matrixProduct.add_left_entry (A B C : Set, i j n : Nat)527  requires matrixA : RealMatrix(A)528  requires matrixB : RealMatrix(B)529  requires matrixC : RealMatrix(C)530  shows matrixProduct(matrixAdd(A, B), C, n)[i, j] =531    matrixAdd(matrixProduct(A, C, n), matrixProduct(B, C, n))[i, j]532proof533  induction n534  | zero =>535    have combined := matrixAdd.matrix with matrixA, matrixB536    have productA := matrixProduct.matrix at A, C, 0 with matrixA, matrixC537    have productB := matrixProduct.matrix at B, C, 0 with matrixB, matrixC538    have left := matrixProduct.zero at matrixAdd(A, B), C, i, j with combined, matrixC539    have rightA := matrixProduct.zero at A, C, i, j with matrixA, matrixC540    have rightB := matrixProduct.zero at B, C, i, j with matrixB, matrixC541    rw [left, matrixAdd.entry, rightA, rightB]542    ring543  | succ(k) using ih =>544    have combined := matrixAdd.matrix with matrixA, matrixB545    have nextA := matrixProduct.matrix at A, C, succ(k) with matrixA, matrixC546    have nextB := matrixProduct.matrix at B, C, succ(k) with matrixB, matrixC547    have oldA := matrixProduct.matrix at A, C, k with matrixA, matrixC548    have oldB := matrixProduct.matrix at B, C, k with matrixB, matrixC549    have left := matrixProduct.succ at matrixAdd(A, B), C, k, i, j with combined, matrixC550    have rightA := matrixProduct.succ at A, C, k, i, j with matrixA, matrixC551    have rightB := matrixProduct.succ at B, C, k, i, j with matrixB, matrixC552    have entry := matrixAdd.entry at A, B, i, k with matrixA, matrixB553    have previous := matrixAdd.entry at matrixProduct(A, C, k),554      matrixProduct(B, C, k), i, j with oldA, oldB555    have realA := RealMatrix.entry at A, i, k with matrixA556    have realB := RealMatrix.entry at B, i, k with matrixB557    have realC := RealMatrix.entry at C, k, j with matrixC558    have realOldA := RealMatrix.entry at matrixProduct(A, C, k), i, j with oldA559    have realOldB := RealMatrix.entry at matrixProduct(B, C, k), i, j with oldB560    rw [left, entry, matrixAdd.entry, rightA, rightB]561    rw previous at ih562    rw ih563    ring564565-- A matrix with n columns acts on a vector by the dot product with each row.566defgraph matrixVectorProduct (M u : Set, n : Nat) (i ∈ ℕ) : ℝ :=567  dotProduct(matrixRow(M, i), u, n)568requires matrix : RealMatrix(M)569requires vector : RealSequence(u)570proof571  have typedI := nat.omega.backward with member572  have row := matrixRow.sequence at M, i with matrix573  exact dotProduct.real at matrixRow(M, i), u, n with row, vector574575theorem matrixVectorProduct.sequence (M u : Set, n : Nat)576  requires matrix : RealMatrix(M)577  requires vector : RealSequence(u)578  shows RealSequence(matrixVectorProduct(M, u, n))579proof580  unfold RealSequence581  exact matrixVectorProduct.function with matrix, vector582583theorem matrixProduct.column_action (A B : Set, n i j : Nat)584  requires matrixA : RealMatrix(A)585  requires matrixB : RealMatrix(B)586  shows matrixProduct(A, B, n)[i, j] =587    matrixVectorProduct(A, matrixColumn(B, j), n)[i]588proof589  have column := matrixColumn.sequence at B, j with matrixB590  have product := matrixProduct.entry at A, B, n, i, j with matrixA, matrixB591  rw [product, matrixVectorProduct.value]592  rfl593594theorem matrixVectorProduct.zero (M u : Set, i : Nat)595  requires matrix : RealMatrix(M)596  requires vector : RealSequence(u)597  shows matrixVectorProduct(M, u, 0)[i] = (0:R)598proof599  rw matrixVectorProduct.value600  exact dotProduct.zero601602theorem matrixVectorProduct.succ (M u : Set, n i : Nat)603  requires matrix : RealMatrix(M)604  requires vector : RealSequence(u)605  shows matrixVectorProduct(M, u, succ(n))[i] =606    (matrixVectorProduct(M, u, n)[i]:R) + (M[i, n]:R) * (u[n]:R)607proof608  have row := matrixRow.sequence at M, i with matrix609  have step := dotProduct.succ at matrixRow(M, i), u, n with row, vector610  rw matrixRow.value at step611  rwa [matrixVectorProduct.value, matrixVectorProduct.value]612613theorem matrixVectorProduct.add (M u v : Set, n i : Nat)614  requires matrix : RealMatrix(M)615  requires vectorU : RealSequence(u)616  requires vectorV : RealSequence(v)617  shows matrixVectorProduct(M, addSequence(u, v), n)[i] =618    (matrixVectorProduct(M, u, n)[i]:R) +619    (matrixVectorProduct(M, v, n)[i]:R)620proof621  have row := matrixRow.sequence at M, i with matrix622  have combined := addSequence.sequence with vectorU, vectorV623  have distributive := dotProduct.add_right at matrixRow(M, i), u, v, n with624    row, vectorU, vectorV625  rwa [matrixVectorProduct.value, matrixVectorProduct.value, matrixVectorProduct.value]626627theorem matrixVectorProduct.add_matrix (A B u : Set, i n : Nat)628  requires matrixA : RealMatrix(A)629  requires matrixB : RealMatrix(B)630  requires vector : RealSequence(u)631  shows matrixVectorProduct(matrixAdd(A, B), u, n)[i] =632    (matrixVectorProduct(A, u, n)[i]:R) + (matrixVectorProduct(B, u, n)[i]:R)633proof634  induction n635  | zero =>636    have combined := matrixAdd.matrix with matrixA, matrixB637    have left := matrixVectorProduct.zero with combined, vector638    have rightA := matrixVectorProduct.zero with matrixA, vector639    have rightB := matrixVectorProduct.zero with matrixB, vector640    rw [left, rightA, rightB]641    ring642  | succ(k) using ih =>643    have combined := matrixAdd.matrix with matrixA, matrixB644    have left := matrixVectorProduct.succ at matrixAdd(A, B), u, k, i with combined, vector645    have rightA := matrixVectorProduct.succ at A, u, k, i with matrixA, vector646    have rightB := matrixVectorProduct.succ at B, u, k, i with matrixB, vector647    have entry := matrixAdd.entry at A, B, i, k with matrixA, matrixB648    have typedA := RealMatrix.entry at A, i, k with matrixA649    have typedB := RealMatrix.entry at B, i, k with matrixB650    have typedU := RealSequence.value at u, k with vector651    have seqA := matrixVectorProduct.sequence at A, u, k with matrixA, vector652    have seqB := matrixVectorProduct.sequence at B, u, k with matrixB, vector653    have oldA := RealSequence.value at matrixVectorProduct(A, u, k), i with seqA654    have oldB := RealSequence.value at matrixVectorProduct(B, u, k), i with seqB655    rw [left, rightA, rightB, entry, ih]656    ring657658theorem matrixVectorProduct.scale_matrix (M u : Set, C : Real, i n : Nat)659  requires matrix : RealMatrix(M)660  requires vector : RealSequence(u)661  shows matrixVectorProduct(matrixScale(C, M), u, n)[i] =662    C * (matrixVectorProduct(M, u, n)[i]:R)663proof664  induction n665  | zero =>666    have scaled := matrixScale.matrix with matrix667    have left := matrixVectorProduct.zero with scaled, vector668    have right := matrixVectorProduct.zero with matrix, vector669    rw [left, right]670    ring671  | succ(k) using ih =>672    have scaled := matrixScale.matrix with matrix673    have left := matrixVectorProduct.succ at matrixScale(C, M), u, k, i with scaled, vector674    have right := matrixVectorProduct.succ at M, u, k, i with matrix, vector675    have entry := matrixScale.entry at C, M, i, k with matrix676    have typedM := RealMatrix.entry at M, i, k with matrix677    have typedU := RealSequence.value at u, k with vector678    have sequence := matrixVectorProduct.sequence at M, u, k with matrix, vector679    have old := RealSequence.value at matrixVectorProduct(M, u, k), i with sequence680    rw [left, right, entry, ih]681    ring682683theorem matrixVectorProduct.scale (M u : Set, C : Real, n i : Nat)684  requires matrix : RealMatrix(M)685  requires vector : RealSequence(u)686  shows matrixVectorProduct(M, mulSequence(constantSequence(C), u), n)[i] =687    C * (matrixVectorProduct(M, u, n)[i]:R)688proof689  have row := matrixRow.sequence at M, i with matrix690  have constants := constantSequence.sequence at C691  have scaled := mulSequence.sequence with constants, vector692  have distributive := dotProduct.scale_right at matrixRow(M, i), u, C, n with row, vector693  rwa [matrixVectorProduct.value, matrixVectorProduct.value]694695theorem matrixVectorProduct.eq_prefix (M u v : Set, n i : Nat)696  requires matrix : RealMatrix(M)697  requires vectorU : RealSequence(u)698  requires vectorV : RealSequence(v)699  requires equal : ∀ k ∈ ℕ, k < n → u[k] = v[k]700  shows matrixVectorProduct(M, u, n)[i] = matrixVectorProduct(M, v, n)[i]701proof702  have row := matrixRow.sequence at M, i with matrix703  have sameRow : ∀ k ∈ ℕ, k < n →704      matrixRow(M, i)[k] = matrixRow(M, i)[k]705    intros k naturalK before706    rfl707  have prefix := dotProduct.eq_prefix with row, vectorU, row, vectorV, sameRow, equal708  rwa [matrixVectorProduct.value, matrixVectorProduct.value]709710theorem matrixVectorProduct.equal_rows (M N u : Set, n i : Nat)711  requires matrixM : RealMatrix(M)712  requires matrixN : RealMatrix(N)713  requires vector : RealSequence(u)714  requires equal : ∀ j ∈ ℕ, j < n → M[i, j] = N[i, j]715  shows matrixVectorProduct(M, u, n)[i] = matrixVectorProduct(N, u, n)[i]716proof717  have rowM := matrixRow.sequence at M, i with matrixM718  have rowN := matrixRow.sequence at N, i with matrixN719  have sameRow : ∀ k ∈ ℕ, k < n →720      matrixRow(M, i)[k] = matrixRow(N, i)[k]721    intros k naturalK before722    have entry := equal with k, naturalK, before723    rwa [matrixRow.value, matrixRow.value]724  have sameVector : ∀ k ∈ ℕ, k < n → u[k] = u[k]725    intros k naturalK before726    rfl727  have prefix := dotProduct.eq_prefix with rowM, vector, rowN, vector, sameRow, sameVector728  rwa [matrixVectorProduct.value, matrixVectorProduct.value]729730-- Before its diagonal coordinate, an identity row contributes only zeros.731theorem identityMatrix.action_before_aux (m : Nat)732  shows ∀ n ∈ ℕ, ∀ i ∈ ℕ, ∀ u, RealSequence(u) → m ≤ i →733    matrixVectorProduct(identityMatrix(n), u, m)[i] = (0:R)734proof735  induction m736  | zero =>737    intros n naturalN i naturalI u sequence outside738    have typedN := nat.omega.backward with naturalN739    have typedI := nat.omega.backward with naturalI740    have matrix := identityMatrix.matrix with typedN741    exact matrixVectorProduct.zero at identityMatrix(n), u, i with matrix, sequence742  | succ(k) using ih =>743    intros n naturalN i naturalI u sequence outside744    have typedN := nat.omega.backward with naturalN745    have typedI := nat.omega.backward with naturalI746    have smaller : k < i by exact outside747    have before := Less.implies_LessEqual at k, i with typedI, smaller748    have different : i ≠ k749      intro equal750      rw equal at smaller751      have impossible := Less.irreflexive at k752      exact impossible with smaller753    have matrix := identityMatrix.matrix with typedN754    have prefix := ih with n, naturalN, i, naturalI, u, sequence, before755    have zeroEntry := identityMatrix.off_diagonal with typedN, typedI, different756    have term := RealSequence.value at u, k with sequence757    have products := matrixVectorProduct.sequence at identityMatrix(n), u, k with matrix, sequence758    have old := RealSequence.value at matrixVectorProduct(identityMatrix(n), u, k), i with products759    rw [matrixVectorProduct.succ, prefix, zeroEntry]760    ring761762theorem identityMatrix.action_before (n m i : Nat, u : Set)763  requires vector : RealSequence(u)764  requires outside : m ≤ i765  shows matrixVectorProduct(identityMatrix(n), u, m)[i] = (0:R)766proof767  exact identityMatrix.action_before_aux at m with768    n, nat.omega.forward at n with assumption,769    i, nat.omega.forward at i with assumption, u, vector, outside770771theorem identityMatrix.action_at_aux (m : Nat)772  shows ∀ n ∈ ℕ, ∀ i ∈ ℕ, ∀ u, RealSequence(u) → i < m →773    matrixVectorProduct(identityMatrix(n), u, m)[i] = u[i]774proof775  induction m776  | zero =>777    intros n naturalN i naturalI u sequence before778    have typedI := nat.omega.backward with naturalI779    have weak := Grace.Core.Nat.Order.LessEqual.zero with typedI780    have typedZero : Nat(0) by typecheck781    have cycle := Less.transitive_LessEqual with typedI, typedZero, typedI, before, weak782    have impossible := Less.irreflexive with typedI783    exfalso784    exact impossible with cycle785  | succ(k) using ih =>786    intros n naturalN i naturalI u sequence before787    have typedN := nat.omega.backward with naturalN788    have typedI := nat.omega.backward with naturalI789    have matrix := identityMatrix.matrix with typedN790    have term := RealSequence.value at u, k with sequence791    have products := matrixVectorProduct.sequence at identityMatrix(n), u, k with matrix, sequence792    have old := RealSequence.value at matrixVectorProduct(identityMatrix(n), u, k), i with products793    have member := membership.of_Less at i, succ(k) with794      typedI, Naturals.constructor.succ at k with assumption, before795    have alternatives := membership.successor_forward{n := k} with member796    cases alternatives with earlier | equal797    . have smaller := Less.of_membership at i, k with typedI, earlier798      have prefix := ih with n, naturalN, i, naturalI, u, sequence, smaller799      have different : i ≠ k800        intro same801        rw same at smaller802        have impossible := Less.irreflexive at k803        exact impossible with smaller804      have zeroEntry := identityMatrix.off_diagonal with typedN, typedI, different805      rw [matrixVectorProduct.succ, prefix, zeroEntry]806      ring807    . rw equal808      have reflexive := LessEqual.reflexive at k809      have prefix := identityMatrix.action_before at n, k, k, u with810        sequence, reflexive811      have diagonal := identityMatrix.diagonal at n, k with typedN812      rw [matrixVectorProduct.succ, prefix, diagonal]813      ring814815theorem identityMatrix.action (n i : Nat, u : Set)816  requires vector : RealSequence(u)817  requires inRange : i < n818  shows matrixVectorProduct(identityMatrix(n), u, n)[i] = u[i]819proof820  exact identityMatrix.action_at_aux at n with821    n, nat.omega.forward at n with assumption,822    i, nat.omega.forward at i with assumption, u, vector, inRange823824theorem matrixProduct.identity_left (A : Set, n i j : Nat)825  requires matrix : RealMatrix(A)826  requires inRange : i < n827  shows matrixProduct(identityMatrix(n), A, n)[i, j] = A[i, j]828proof829  have identity := identityMatrix.matrix at n830  have column := matrixColumn.sequence at A, j with matrix831  have action := identityMatrix.action with column, inRange832  have product := matrixProduct.column_action at identityMatrix(n), A, n, i, j with833    identity, matrix834  rw [product, action, matrixColumn.value]835  rfl836837theorem diagonalCoefficient.not_equal_symmetric (i j : Nat)838  requires different : i ≠ j839  shows j ≠ i840proof841  simp842843theorem diagonalCoefficient.symmetric (i j : Nat)844  shows diagonalCoefficient(i, j) = diagonalCoefficient(j, i)845proof846  have alternatives : i = j ∨ i ≠ j by tauto847  cases alternatives with equal | different848  . rw equal849    rfl850  . have reverse := diagonalCoefficient.not_equal_symmetric with different851    have first := diagonalCoefficient.distinct with different852    have second := diagonalCoefficient.distinct with reverse853    rw [first, second]854    rfl855856theorem identityMatrix.symmetric_entry (n i j : Nat)857  shows identityMatrix(n)[i, j] = identityMatrix(n)[j, i]858proof859  rw [identityMatrix.entry, identityMatrix.entry]860  exact diagonalCoefficient.symmetric with *861862theorem matrixProduct.identity_right (A : Set, n i j : Nat)863  requires matrix : RealMatrix(A)864  requires inRange : j < n865  shows matrixProduct(A, identityMatrix(n), n)[i, j] = A[i, j]866proof867  have identity := identityMatrix.matrix at n868  have rowA := matrixRow.sequence at A, i with matrix869  have rowI := matrixRow.sequence at identityMatrix(n), j with identity870  have colI := matrixColumn.sequence at identityMatrix(n), j with identity871  have equal : ∀ k ∈ ℕ, k < n →872      matrixColumn(identityMatrix(n), j)[k] = matrixRow(identityMatrix(n), j)[k]873    intros k naturalK before874    have typedK := nat.omega.backward with naturalK875    have symmetric := identityMatrix.symmetric_entry at n, k, j with876      assumption, typedK, assumption877    rwa [matrixColumn.value, matrixRow.value]878  have sameRow : ∀ k ∈ ℕ, k < n →879      matrixRow(A, i)[k] = matrixRow(A, i)[k]880    intros k naturalK before881    rfl882  have equalDot := dotProduct.eq_prefix with colI, rowA, rowI, rowA, equal, sameRow883  have swap := dotProduct.symmetric at matrixRow(A, i),884    matrixColumn(identityMatrix(n), j), n with rowA, colI885  have product := matrixProduct.entry at A, identityMatrix(n), n, i, j with matrix, identity886  have action := identityMatrix.action with rowA, inRange887  rw [product, swap, equalDot, ←matrixVectorProduct.value, action, matrixRow.value]888  rfl889890-- The two orders for summing a finite rectangle of a total matrix.891defgraph matrixRowTotals (M : Set, m : Nat) (i ∈ ℕ) : ℝ :=892  realPartialSum(matrixRow(M, i), m)893requires matrix : RealMatrix(M)894proof895  have typedI := nat.omega.backward with member896  have row := matrixRow.sequence at M, i with matrix897  exact realPartialSum.real at matrixRow(M, i), m with row898899theorem matrixRowTotals.sequence (M : Set, m : Nat)900  requires matrix : RealMatrix(M)901  shows RealSequence(matrixRowTotals(M, m))902proof903  unfold RealSequence904  exact matrixRowTotals.function with matrix905906defgraph matrixColumnTotals (M : Set, n : Nat) (j ∈ ℕ) : ℝ :=907  realPartialSum(matrixColumn(M, j), n)908requires matrix : RealMatrix(M)909proof910  have typedJ := nat.omega.backward with member911  have column := matrixColumn.sequence at M, j with matrix912  exact realPartialSum.real at matrixColumn(M, j), n with column913914theorem matrixColumnTotals.sequence (M : Set, n : Nat)915  requires matrix : RealMatrix(M)916  shows RealSequence(matrixColumnTotals(M, n))917proof918  unfold RealSequence919  exact matrixColumnTotals.function with matrix920921theorem matrixColumnTotals.succ (M : Set, n j : Nat)922  requires matrix : RealMatrix(M)923  shows matrixColumnTotals(M, succ(n))[j] =924    (matrixColumnTotals(M, n)[j]:R) + (M[n, j]:R)925proof926  have column := matrixColumn.sequence at M, j with matrix927  have next := matrixColumnTotals.value at M, succ(n), j with matrix928  have previous := matrixColumnTotals.value at M, n, j with matrix929  have entry := matrixColumn.value at M, j, n with matrix930  rw [next, previous, realPartialSum.succ, entry]931  unfold realAddValue932  unfold call2933  rfl934935theorem matrixColumnTotals.empty_sum (M : Set, m : Nat)936  requires matrix : RealMatrix(M)937  shows realPartialSum(matrixColumnTotals(M, 0), m) = (0:R)938proof939  induction m940  | zero =>941    rw realPartialSum.zero942    rfl943  | succ(k) using ih =>944    have value := matrixColumnTotals.value at M, 0, k with matrix945    have zero := realPartialSum.zero at matrixColumn(M, k)946    have sequence := matrixColumnTotals.sequence with matrix947    have term := RealSequence.value with sequence948    rw [realPartialSum.succ, ih, value, zero]949    have unit := realAddValue.zero_right with realZero.real950    unfold realAddValue951    unfold call2 at unit952    exact unit953954theorem matrixTotals.interchange_aux (n : Nat)955  shows ∀ M, RealMatrix(M) → ∀ m ∈ ℕ,956    realPartialSum(matrixRowTotals(M, m), n) =957      realPartialSum(matrixColumnTotals(M, n), m)958proof959  induction n960  | zero =>961    intros M matrix m naturalM962    have typedM := nat.omega.backward with naturalM963    rw realPartialSum.zero964    have empty := matrixColumnTotals.empty_sum with matrix965    rw empty966    rfl967  | succ(k) using ih =>968    intros M matrix m naturalM969    have typedM := nat.omega.backward with naturalM970    have row := matrixRow.sequence at M, k with matrix971    have earlier := matrixColumnTotals.sequence at M, k with matrix972    have later := matrixColumnTotals.sequence at M, succ(k) with matrix973    have combined := addSequence.sequence with earlier, row974    have equal : ∀ j ∈ ℕ, j < m →975        matrixColumnTotals(M, succ(k))[j] =976          addSequence(matrixColumnTotals(M, k), matrixRow(M, k))[j]977      intros j naturalJ before978      have typedJ := nat.omega.backward with naturalJ979      have step := matrixColumnTotals.succ at M, k, j with matrix980      have left := RealSequence.value at matrixColumnTotals(M, k), j with earlier981      have right := RealSequence.value at matrixRow(M, k), j with row982      have value := addSequence.value with earlier, row, left, right983      have entry := matrixRow.value at M, k, j with matrix984      rw [step, value, entry]985      rfl986    have prefix := realPartialSum.eq_prefix with later, combined, equal987    have sumAdd := realPartialSum.add at matrixColumnTotals(M, k),988      matrixRow(M, k), m with earlier, row989    have inductionStep := ih with M, matrix, m, naturalM990    have rowTotal := matrixRowTotals.value at M, m, k with matrix991    rw [realPartialSum.succ, rowTotal, inductionStep, prefix, sumAdd]992    unfold realAddValue993    unfold call2994    rfl995996theorem matrixTotals.interchange (M : Set, n m : Nat)997  requires matrix : RealMatrix(M)998  shows realPartialSum(matrixRowTotals(M, m), n) =999    realPartialSum(matrixColumnTotals(M, n), m)1000proof1001  exact matrixTotals.interchange_aux at n with M, matrix,1002    m, nat.omega.forward at m with assumption1003