Chunks of matrix index pairs

Main definitions

• pairIndex, rankIn: row-major index and rank in a finite set.
• chunk, numChunks: consecutive chunks and their number.

Main results

• card_chunk_le: each chunk has at most the capacity many pairs.
• biUnion_chunk: all chunks cover the input finite set.

References

Adapted from Chunks.lean and the minimal definitions in PaperStatements.lean at anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5. There are no graph or weight assumptions.

def Cslib.Matrix.pairIndex {n : ℕ} (q : Fin n × Fin n) : ℕ

The position of the pair (a, b) in the row-major order of A × B.

def Cslib.Matrix.rankIn {n : ℕ} (S : Finset (Fin n × Fin n)) (q : Fin n × Fin n) : ℕ

The number of pairs of S that come before q in row-major order.

def Cslib.Matrix.chunk {n : ℕ} (S : Finset (Fin n × Fin n)) (cap j : ℕ) : Finset (Fin n × Fin n)

The j-th chunk (j = 0, 1, …) of S when S is cut, in row-major order, into chunks of cap pairs each (the last one may be smaller).

def Cslib.Matrix.numChunks {n : ℕ} (S : Finset (Fin n × Fin n)) (cap : ℕ) : ℕ

The number ⌈|S| / cap⌉ of nonempty chunks of S (for cap ≥ 1).

Ranks

theorem Cslib.Matrix.pairIndex_injective {n : ℕ} : Function.Injective pairIndex

The position in row-major order determines the pair.

theorem Cslib.Matrix.rankIn_lt_rankIn {n : ℕ} {S : Finset (Fin n × Fin n)} {q r : Fin n × Fin n} (hq : q ∈ S) (h : pairIndex q < pairIndex r) : rankIn S q < rankIn S r

Among the pairs of S, a pair that comes earlier in row-major order has a smaller rank.

theorem Cslib.Matrix.rankIn_injOn {n : ℕ} (S : Finset (Fin n × Fin n)) : Set.InjOn (rankIn S) ↑S

Different pairs of S have different ranks.

theorem Cslib.Matrix.rankIn_lt_card {n : ℕ} {S : Finset (Fin n × Fin n)} {q : Fin n × Fin n} (hq : q ∈ S) : rankIn S q < S.card

The rank of a pair of S is less than the number of pairs of S.

theorem Cslib.Matrix.rankIn_univ {n : ℕ} (q : Fin n × Fin n) : rankIn Finset.univ q = pairIndex q

In the full matrix, row-major rank is the row-major index itself. This avoids enumerating all preceding pairs when applying the chunk API to a full matrix.

Chunks

theorem Cslib.Matrix.card_chunk_le {n cap : ℕ} (S : Finset (Fin n × Fin n)) (hcap : 1 ≤ cap) (j : ℕ) : (chunk S cap j).card ≤ cap

A chunk has at most cap pairs: their ranks are different numbers in [j cap, (j + 1) cap).

theorem Cslib.Matrix.biUnion_chunk {n cap : ℕ} (S : Finset (Fin n × Fin n)) (hcap : 1 ≤ cap) : ((Finset.range (numChunks S cap)).biUnion fun (j : ℕ) => chunk S cap j) = S

The first ⌈|S|/cap⌉ chunks cover S, because |S| ≤ ⌈|S|/cap⌉ cap.