12.4. Span and nullspace🔗

From the reduced form we compute the linear combination of the rows, row-span membership with an explicit witness, the Boolean span test, and a nullspace basis. Each has a soundness theorem. The nullspace basis also has a completeness theorem.

def

Hex.Matrix.vecMul.{u} {R : Type u} {n m : ℕ} [Mul R] [Add R] [OfNat R 0]
  (v : Vector R n) (M : Hex.Matrix R n m) : Vector R m
Hex.Matrix.vecMul.{u} {R : Type u}
  {n m : ℕ} [Mul R] [Add R] [OfNat R 0]
  (v : Vector R n)
  (M : Hex.Matrix R n m) : Vector R m

Multiply a row vector by a matrix, v * M. Equal to transpose M * v; the j-th entry is ∑ i, M[i][j] * v[i], the combination of the rows of M with coefficients v.

def

Hex.Matrix.spanCoeffs.{u} {R : Type u} {n m : ℕ} [Lean.Grind.Field R]
  [DecidableEq R] (M : Hex.Matrix R n m) (v : Vector R m) :
  Option (Vector R n)
Hex.Matrix.spanCoeffs.{u} {R : Type u}
  {n m : ℕ} [Lean.Grind.Field R]
  [DecidableEq R] (M : Hex.Matrix R n m)
  (v : Vector R m) : Option (Vector R n)

Compute row-span coefficients using Hex.Matrix.rowReduce internally.

theorem

Hex.Matrix.spanCoeffs_sound.{u} {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R] (M : Hex.Matrix R n m)
  (v : Vector R m) (c : Vector R n) :
  M.spanCoeffs v = some c → Hex.Matrix.vecMul c M = v
Hex.Matrix.spanCoeffs_sound.{u}
  {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R]
  (M : Hex.Matrix R n m) (v : Vector R m)
  (c : Vector R n) :
  M.spanCoeffs v = some c →
    Hex.Matrix.vecMul c M = v

Soundness of Hex.Matrix.spanCoeffs: returned coefficients reconstruct the requested vector.

theorem

Hex.Matrix.spanCoeffs_eq_none_iff.{u} {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R] (M : Hex.Matrix R n m)
  (v : Vector R m) :
  M.spanCoeffs v = none ↔ ¬∃ c, Hex.Matrix.vecMul c M = v
Hex.Matrix.spanCoeffs_eq_none_iff.{u}
  {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R]
  (M : Hex.Matrix R n m)
  (v : Vector R m) :
  M.spanCoeffs v = none ↔
    ¬∃ c, Hex.Matrix.vecMul c M = v

Hex.Matrix.spanCoeffs returns none exactly when v is in no row combination of M, so a none result certifies that v is not in the row span.

def

Hex.Matrix.spanContains.{u} {R : Type u} {n m : ℕ} [Lean.Grind.Field R]
  [DecidableEq R] (M : Hex.Matrix R n m) (v : Vector R m) : Bool
Hex.Matrix.spanContains.{u} {R : Type u}
  {n m : ℕ} [Lean.Grind.Field R]
  [DecidableEq R] (M : Hex.Matrix R n m)
  (v : Vector R m) : Bool

Decide row-span membership using Hex.Matrix.rowReduce internally.

theorem

Hex.Matrix.spanContains_iff.{u} {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R] (M : Hex.Matrix R n m)
  (v : Vector R m) :
  M.spanContains v = true ↔ ∃ c, Hex.Matrix.vecMul c M = v
Hex.Matrix.spanContains_iff.{u}
  {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R]
  (M : Hex.Matrix R n m)
  (v : Vector R m) :
  M.spanContains v = true ↔
    ∃ c, Hex.Matrix.vecMul c M = v

Hex.Matrix.spanContains is exactly row-span membership.

def

Hex.Matrix.nullspace.{u} {R : Type u} {n m : ℕ} [Lean.Grind.Field R]
  [DecidableEq R] (M : Hex.Matrix R n m) :
  Vector (Vector R m) (m - M.rowReduce_rank)
Hex.Matrix.nullspace.{u} {R : Type u}
  {n m : ℕ} [Lean.Grind.Field R]
  [DecidableEq R] (M : Hex.Matrix R n m) :
  Vector (Vector R m)
    (m - M.rowReduce_rank)

Compute the nullspace basis using Hex.Matrix.rowReduce internally.

def

Hex.Matrix.nullspaceBasisMatrix.{u} {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R] (M : Hex.Matrix R n m) :
  Hex.Matrix R m (m - M.rowReduce_rank)
Hex.Matrix.nullspaceBasisMatrix.{u}
  {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R]
  (M : Hex.Matrix R n m) :
  Hex.Matrix R m (m - M.rowReduce_rank)

The public nullspace basis assembled as a matrix of basis columns.

theorem

Hex.Matrix.nullspace_sound.{u} {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R] (M : Hex.Matrix R n m)
  (k : Fin (m - M.rowReduce_rank)) : M * M.nullspace.get k = 0
Hex.Matrix.nullspace_sound.{u}
  {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R]
  (M : Hex.Matrix R n m)
  (k : Fin (m - M.rowReduce_rank)) :
  M * M.nullspace.get k = 0

Every vector returned by Hex.Matrix.nullspace is annihilated by M.

theorem

Hex.Matrix.nullspace_complete.{u} {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R] (M : Hex.Matrix R n m)
  (v : Vector R m) : M * v = 0 → ∃ c, M.nullspaceBasisMatrix * c = v
Hex.Matrix.nullspace_complete.{u}
  {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R]
  (M : Hex.Matrix R n m)
  (v : Vector R m) :
  M * v = 0 →
    ∃ c, M.nullspaceBasisMatrix * c = v

Every vector annihilated by M is generated by the public nullspace basis matrix.