Documentation

Complexitylib.Algebraic.LowerBound.Fusion.SumOfTerms.MatrixRank.Support

Support bounds for matrix flattenings #

The rank of a finite matrix is at most the number of rows or columns on which it is supported. This module converts Mathlib's natural-valued matrix-rank bound to the cardinal-valued rank used by Fusion certificates, and packages canonical finite row and column supports.

Nothing here depends on polynomials or a particular circuit model. Any future matrix-valued feature, including shifted flattenings, can reuse these lemmas.

source
theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Support.rank_toLin'_eq_matrixRank {K I J : Type} [Field K] [Fintype J] [DecidableEq J] (matrix : Matrix I J K) :
(Matrix.toLin' matrix).rank = ↑matrix.rank

On finite index types, the rank of matrix-vector multiplication is the natural-valued matrix rank, coerced to a cardinal.

source
theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Support.rank_toLin'_le_card_of_rowSupport_subset {K I J : Type} [Field K] [Fintype J] [DecidableEq J] (matrix : Matrix I J K) (rows : Finset I) (supported : Function.support matrix.row ⊆ ↑rows) :
(Matrix.toLin' matrix).rank ≤ ↑rows.card

A finite set containing every nonzero row bounds flattening rank.

source
theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Support.rank_toLin'_le_card_of_columnSupport_subset {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq J] (matrix : Matrix I J K) (columns : Finset J) (supported : Function.support matrix.col ⊆ ↑columns) :
(Matrix.toLin' matrix).rank ≤ ↑columns.card

A finite set containing every nonzero column bounds flattening rank.

source
noncomputable def Algebraic.Fusion.SumOfTerms.MatrixRank.Support.rowSupport {K I J : Type} [Zero K] [Fintype I] (matrix : Matrix I J K) :
Finset I

The canonical finite set of nonzero rows.

Equations
Instances For
    source
    @[simp]
    theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Support.mem_rowSupport {K I J : Type} [Zero K] [Fintype I] (matrix : Matrix I J K) (row : I) :
    row ∈ rowSupport matrix ↔ matrix.row row ≠ 0
    source
    noncomputable def Algebraic.Fusion.SumOfTerms.MatrixRank.Support.columnSupport {K I J : Type} [Zero K] [Fintype J] (matrix : Matrix I J K) :
    Finset J

    The canonical finite set of nonzero columns.

    Equations
    Instances For
      source
      @[simp]
      theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Support.mem_columnSupport {K I J : Type} [Zero K] [Fintype J] (matrix : Matrix I J K) (column : J) :
      column ∈ columnSupport matrix ↔ matrix.col column ≠ 0
      source
      theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Support.rank_toLin'_le_card_rowSupport {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq J] (matrix : Matrix I J K) :
      (Matrix.toLin' matrix).rank ≤ ↑(rowSupport matrix).card

      Flattening rank is at most the number of its nonzero rows.

      source
      theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Support.rank_toLin'_le_card_columnSupport {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq J] (matrix : Matrix I J K) :
      (Matrix.toLin' matrix).rank ≤ ↑(columnSupport matrix).card

      Flattening rank is at most the number of its nonzero columns.

      source
      theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Support.rank_toLin'_le_min_support {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq J] (matrix : Matrix I J K) :
      (Matrix.toLin' matrix).rank ≤ ↑(min (rowSupport matrix).card (columnSupport matrix).card)

      Using both sides gives the smaller of the nonzero-row and nonzero-column counts.