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

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

Equations

• M.spanCoeffs v = ⋯.spanCoeffs v

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

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

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

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

Equations

• M.spanContains v = ⋯.spanContains v

@[simp]

theorem Hex.Matrix.spanContains_eq_isSome {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (v : Vector R m) : M.spanContains v = (M.spanCoeffs v).isSome

Hex.Matrix.spanContains is the Boolean isSome view of Hex.Matrix.spanCoeffs.

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

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

theorem Hex.Matrix.spanCoeffs_eq_none_iff {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (v : Vector R m) : M.spanCoeffs v = none ↔ ¬∃ (c : Vector R n), 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.rowReduce_rank {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) : Nat

The rank returned by Hex.Matrix.rowReduce.

Equations

• M.rowReduce_rank = M.rowReduce.rank

theorem Hex.Matrix.rowReduce_rank_eq_n_of_rightInverse {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (Q : Matrix R m n) (hMQ : M * Q = Matrix.identity n) : M.rowReduce_rank = n

A matrix with a right inverse has full row rank.

theorem Hex.Matrix.takeRows_mul {R : Type u} {n m k : Nat} [Lean.Grind.Field R] [DecidableEq R] (A : Matrix R n m) (B : Matrix R m k) (r : Nat) (hr : r ≤ n) : (A * B).takeRows r hr = A.takeRows r hr * B

theorem Hex.Matrix.rowReduce_takeRows_echelon_eq_identity {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (hm : m ≤ n) (hrank : M.rowReduce_rank = m) : M.rowReduce.echelon.takeRows m hm = Matrix.identity m

If row reduction finds full column rank, the leading square block of the reduced echelon form is the identity.

theorem Hex.Matrix.rowReduce_rank_le_of_eq_mul {R : Type u} {n m k : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (C : Matrix R n k) (B : Matrix R k m) (hM : M = C * B) : M.rowReduce_rank ≤ k

The computed rank is no larger than the middle dimension of any matrix factorization.

theorem Hex.Matrix.rowReduce_rank_le_of_rows_span {R : Type u} {n m k : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (B : Matrix R k m) (hspan : ∀ (i : Fin n), ∃ (c : Vector R k), vecMul c B = M.row i) : M.rowReduce_rank ≤ k

A spanning family bounds the computed rank: if every row of M is a combination of the rows of B, then M has rank at most the row count of B.

theorem Hex.Matrix.rowReduce_rank_ge_of_rightInverse {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (Q : Matrix R m n) (hMQ : M * Q = Matrix.identity n) : n ≤ M.rowReduce_rank

A right inverse supplies the matching lower rank bound.

theorem Hex.Matrix.rowReduce_rank_factorization {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) : ∃ (C : Matrix R n M.rowReduce_rank), ∃ (B : Matrix R M.rowReduce_rank m), M = C * B

The computed rank supplies an explicit factorization through that many coordinates.

theorem Hex.Matrix.rowReduce_rank_transpose {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) : M.transpose.rowReduce_rank = M.rowReduce_rank

Row reduction computes the same rank for a matrix and its transpose.

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

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

Equations

• M.nullspaceBasisMatrix = ⋯.nullspaceMatrix

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

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

Equations

• M.nullspace = ⋯.nullspace

theorem Hex.Matrix.nullspaceBasisMatrix_col {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (k : Fin (m - M.rowReduce_rank)) : M.nullspaceBasisMatrix.col k = M.nullspace.get k

The k-th column of Hex.Matrix.nullspaceBasisMatrix is the k-th vector in Hex.Matrix.nullspace.

theorem Hex.Matrix.nullspace_sound {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : 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_ne_zero {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (k : Fin (m - M.rowReduce_rank)) : M.nullspace.get k ≠ 0

Every vector in the computed nullspace basis is nonzero.

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

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