HexRowReduce.Nullspace

Nullspace API over the reduced-row-echelon contract.

From the free columns of an IsRowReduced form this constructs the nullspace basis (nullspaceMatrix, nullspace) and proves it both sound (nullspace_sound: each basis vector is killed by M) and complete (nullspace_complete: every nullspace vector is a combination of the basis).

source

def Hex.Matrix.IsRowReduced.pivotIndex? {R : Type u} {n m : Nat} (D : RowEchelonData R n m) (j : Fin m) :

Option (Fin D.rank)

Find the pivot-row index for column j, if j is a pivot column.

Equations

Hex.Matrix.IsRowReduced.pivotIndex? D j = Hex.Matrix.IsRowReduced.pivotIndexAux✝ D j 0 D.rank

Instances For

source

def Hex.Matrix.IsRowReduced.nullspaceMatrix {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] [Lean.Grind.Ring R] (E : M.IsRowReduced D) :

Matrix R m (m - D.rank)

Nullspace basis vectors assembled as columns indexed by the free variables.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Hex.Matrix.IsRowReduced.nullspaceMatrix_free {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] [Lean.Grind.Ring R] (E : M.IsRowReduced D) (k : Fin (m - D.rank)) :

E.nullspaceMatrix[⋯.freeCols.get k][k] = 1

In the kth nullspace-matrix column, the row for its own free column is 1.

source

theorem Hex.Matrix.IsRowReduced.nullspaceMatrix_free_ne {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] [Lean.Grind.Ring R] (E : M.IsRowReduced D) {k l : Fin (m - D.rank)} (hkl : k ≠ l) :

E.nullspaceMatrix[⋯.freeCols.get l][k] = 0

In the kth nullspace-matrix column, every other free-column row is 0.

source

theorem Hex.Matrix.IsRowReduced.nullspaceMatrix_pivot {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] [Lean.Grind.Ring R] (E : M.IsRowReduced D) (i : Fin D.rank) (k : Fin (m - D.rank)) :

E.nullspaceMatrix[D.pivotCols.get i][k] = -D.echelon[⋯.pivotRow i][⋯.freeCols.get k]

In a pivot-column row, a nullspace-matrix entry is the negative RREF entry in the matching pivot row and free column.

source

def Hex.Matrix.IsRowReduced.nullspace {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] [Lean.Grind.Ring R] (E : M.IsRowReduced D) :

Vector (Vector R m) (m - D.rank)

The individual nullspace basis vectors.

Equations

E.nullspace = Vector.ofFn fun (k : Fin (m - D.rank)) => E.nullspaceMatrix.col k

Instances For

source

theorem Hex.Matrix.IsRowReduced.nullspace_get_free {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] [Lean.Grind.Ring R] (E : M.IsRowReduced D) (k : Fin (m - D.rank)) :

(E.nullspace.get k)[⋯.freeCols.get k] = 1

On its own free column, a nullspace basis vector has entry 1.

source

theorem Hex.Matrix.IsRowReduced.nullspace_get_free_ne {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] [Lean.Grind.Ring R] (E : M.IsRowReduced D) {k l : Fin (m - D.rank)} (hkl : k ≠ l) :

(E.nullspace.get k)[⋯.freeCols.get l] = 0

On every other free column, a nullspace basis vector has entry 0.

source

theorem Hex.Matrix.IsRowReduced.nullspace_get_pivot {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] [Lean.Grind.Ring R] (E : M.IsRowReduced D) (i : Fin D.rank) (k : Fin (m - D.rank)) :

(E.nullspace.get k)[D.pivotCols.get i] = -D.echelon[⋯.pivotRow i][⋯.freeCols.get k]

On a pivot column, a nullspace basis vector is the negative RREF entry in the matching pivot row and free column.

source

theorem Hex.Matrix.IsRowReduced.nullspace_sound {R : Type u} [Lean.Grind.Ring R] {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsRowReduced D) (k : Fin (m - D.rank)) :

M * E.nullspace.get k = 0

Every basis vector returned by nullspace lies in the nullspace of M.

source

theorem Hex.Matrix.IsRowReduced.nullspace_complete {R : Type u} [Lean.Grind.Field R] {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsRowReduced D) (v : Vector R m) :

M * v = 0 → ∃ (c : Vector R (m - D.rank)), E.nullspaceMatrix * c = v

Every nullspace vector is generated by the computed nullspace basis.