Rectangle covers of matrix support

A finite family of row/column rectangles covers a matrix when every nonzero entry lies in at least one rectangle. We assign an overlapping entry to one covering rectangle, thereby obtaining a supported-block decomposition. This proves the weighted rectangle-cover estimate

rank A ≤ ∑_t min (|rows_t|) (|columns_t|).

The construction is coefficient-agnostic and reusable for every finite matrix flattening.

structure Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Certificate {K I J : Type} [Field K] (matrix : Matrix I J K) : Type

A finite family of combinatorial rectangles covering every nonzero matrix entry. Rectangles may overlap.

• rectangleCount : ℕ

  Number of rectangle occurrences.

• rows : Fin self.rectangleCount → Finset I

  Row side of each rectangle.

• columns : Fin self.rectangleCount → Finset J

  Column side of each rectangle.

• covers_support (row : I) (column : J) : matrix row column ≠ 0 → ∃ (index : Fin self.rectangleCount), row ∈ self.rows index ∧ column ∈ self.columns index

  Every nonzero entry belongs to some rectangle.

noncomputable def Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Certificate.owner {K I J : Type} [Field K] [DecidableEq I] [DecidableEq J] {matrix : Matrix I J K} (certificate : Certificate matrix) (row : I) (column : J) : Option (Fin certificate.rectangleCount)

Choose one covering rectangle for an entry, if one exists.

Equations

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

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Certificate.owner_ne_none_of_ne_zero {K I J : Type} [Field K] [DecidableEq I] [DecidableEq J] {matrix : Matrix I J K} (certificate : Certificate matrix) (row : I) (column : J) (nonzero : matrix row column ≠ 0) : certificate.owner row column ≠ none

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Certificate.mem_of_owner_eq_some {K I J : Type} [Field K] [DecidableEq I] [DecidableEq J] {matrix : Matrix I J K} (certificate : Certificate matrix) (row : I) (column : J) (index : Fin certificate.rectangleCount) (owned : certificate.owner row column = some index) : row ∈ certificate.rows index ∧ column ∈ certificate.columns index

noncomputable def Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Certificate.pieceMatrix {K I J : Type} [Field K] [DecidableEq I] [DecidableEq J] {matrix : Matrix I J K} (certificate : Certificate matrix) (index : Fin certificate.rectangleCount) : Matrix I J K

Entries assigned to one rectangle, with all other entries zeroed out.

Equations

• certificate.pieceMatrix index row column = if certificate.owner row column = some index then matrix row column else 0

noncomputable def Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Certificate.piece {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {matrix : Matrix I J K} (certificate : Certificate matrix) (index : Fin certificate.rectangleCount) : Block.Piece K I J

The assigned entries form a block supported on the chosen rectangle.

Equations

• certificate.piece index = { matrix := certificate.pieceMatrix index, rows := certificate.rows index, columns := certificate.columns index, rows_supported := ⋯, columns_supported := ⋯ }

@[simp]

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Certificate.piece_matrix {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {matrix : Matrix I J K} (certificate : Certificate matrix) (index : Fin certificate.rectangleCount) : (certificate.piece index).matrix = certificate.pieceMatrix index

@[reducible, inline]

noncomputable abbrev Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Certificate.toDecomposition {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {matrix : Matrix I J K} (certificate : Certificate matrix) : Block.Decomposition matrix

Assigning overlaps to one owner turns a rectangle cover into a supported block decomposition.

Equations

• certificate.toDecomposition = { blockCount := certificate.rectangleCount, block := certificate.piece, sum_eq := ⋯ }

def Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Certificate.rankBudget {K I J : Type} [Field K] {matrix : Matrix I J K} (certificate : Certificate matrix) : ℕ

Weighted size of a rectangle cover.

Equations

• certificate.rankBudget = ∑ index : Fin certificate.rectangleCount, min (certificate.rows index).card (certificate.columns index).card

@[simp]

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Certificate.toDecomposition_rankBudget {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {matrix : Matrix I J K} (certificate : Certificate matrix) : certificate.toDecomposition.rankBudget = certificate.rankBudget

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Certificate.rank_toLin'_le_rankBudget {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {matrix : Matrix I J K} (certificate : Certificate matrix) : (Matrix.toLin' matrix).rank ≤ ↑certificate.rankBudget

A rectangle cover bounds flattening rank by its weighted size.

@[reducible, inline]

noncomputable abbrev Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Certificate.single {K I J : Type} [Field K] [Fintype I] [Fintype J] (matrix : Matrix I J K) : Certificate matrix

One rectangle formed by the exact nonzero rows and columns always covers the matrix support.

Equations

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

@[simp]

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Certificate.single_rankBudget {K I J : Type} [Field K] [Fintype I] [Fintype J] (matrix : Matrix I J K) : (single matrix).rankBudget = min (Support.rowSupport matrix).card (Support.columnSupport matrix).card

def Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Certificate.zero {K I J : Type} [Field K] : Certificate 0

Empty rectangle cover of the zero matrix.

Equations

• Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Certificate.zero = { rectangleCount := 0, rows := Fin.elim0, columns := Fin.elim0, covers_support := ⋯ }

@[simp]

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Certificate.zero_rankBudget {K I J : Type} [Field K] : zero.rankBudget = 0