Toeplitz matrices

A Toeplitz matrix is constant along each diagonal: its entry in row i and column j depends only on i - j. An m × n Toeplitz matrix is therefore determined by its first row and its first column, m + n - 1 entries in all (Matrix.toeplitz, Matrix.exists_toeplitz_eq_iff, Matrix.toeplitz_injective).

Over a field, for every nonzero d : Fin n → α, the Toeplitz matrices T reach every vector T d (Matrix.toeplitz_mulVec_surjective). Indeed, if j₀ is the last coordinate with d j₀ ≠ 0, then on Toeplitz matrices supported on the m diagonals through column j₀, the map T ↦ T d is triangular with diagonal d j₀.

Main definitions

• Matrix.toeplitz: the m × n Toeplitz matrix with the given m + n - 1 diagonals.

Main results

• Matrix.exists_toeplitz_eq_iff, Matrix.toeplitz_injective: the matrices with at least one row and one column whose entries depend only on the difference of their indices are exactly the Toeplitz matrices, and each determines its diagonals.
• Matrix.toeplitz_mulVec_surjective: over a field, T ↦ T d maps Toeplitz matrices onto all vectors for every d ≠ 0.

References

• J. Katz, Y. Lindell, Introduction to Modern Cryptography, Section 4.6

def Matrix.toeplitz {α : Type u_1} {m n : ℕ} (a : Fin (m + n - 1) → α) : Matrix (Fin m) (Fin n) α

The m × n Toeplitz matrix with diagonals a: its entry in row i and column j is a (i - j + n - 1). It is constant along each diagonal: a 0 is the top right corner, the first row is a (n - 1), …, a 0, the first column is a (n - 1), …, a (m + n - 2), and the last entry a (m + n - 2) is the bottom left corner [Katz and Lindell, Exercise 4.26] [KL20].

@[simp]

theorem Matrix.toeplitz_apply {α : Type u_1} {m n : ℕ} (a : Fin (m + n - 1) → α) (i : Fin m) (j : Fin n) : toeplitz a i j = a ⟨↑i + (n - 1 - ↑j), ⋯⟩

The entry of toeplitz a in row i and column j is a (i + (n - 1 - j)).

theorem Matrix.toeplitz_apply_eq_of_add_eq {α : Type u_1} {m n : ℕ} (a : Fin (m + n - 1) → α) {i i' : Fin m} {j j' : Fin n} (h : ↑i + ↑j' = ↑i' + ↑j) : toeplitz a i j = toeplitz a i' j'

The entries of a Toeplitz matrix depend only on the difference of their indices.

theorem Matrix.toeplitz_injective {α : Type u_1} {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) : Function.Injective toeplitz

A Toeplitz matrix with at least one row and one column determines its diagonals.

theorem Matrix.exists_toeplitz_eq_iff {α : Type u_1} {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) {A : Matrix (Fin m) (Fin n) α} : (∃ (a : Fin (m + n - 1) → α), toeplitz a = A) ↔ ∀ (i i' : Fin m) (j j' : Fin n), ↑i + ↑j' = ↑i' + ↑j → A i j = A i' j'

A matrix with at least one row and one column is a Toeplitz matrix exactly when its entries depend only on the difference of their indices.

@[simp]

theorem Matrix.toeplitz_zero {α : Type u_1} {m n : ℕ} [Zero α] : toeplitz 0 = 0

The Toeplitz matrix with zero diagonals is zero.

theorem Matrix.toeplitz_add {α : Type u_1} {m n : ℕ} [Add α] (a b : Fin (m + n - 1) → α) : toeplitz (a + b) = toeplitz a + toeplitz b

toeplitz sends sums of diagonals to sums of matrices.

theorem Matrix.toeplitz_neg {α : Type u_1} {m n : ℕ} [Neg α] (a : Fin (m + n - 1) → α) : toeplitz (-a) = -toeplitz a

toeplitz commutes with negation.

theorem Matrix.toeplitz_sub {α : Type u_1} {m n : ℕ} [Sub α] (a b : Fin (m + n - 1) → α) : toeplitz (a - b) = toeplitz a - toeplitz b

toeplitz sends differences of diagonals to differences of matrices.

theorem Matrix.toeplitz_smul {α : Type u_1} {m n : ℕ} {R : Type u_2} [SMul R α] (c : R) (a : Fin (m + n - 1) → α) : toeplitz (c • a) = c • toeplitz a

toeplitz commutes with scalar multiplication.

theorem Matrix.toeplitz_mulVec_surjective {α : Type u_1} {m n : ℕ} [Field α] {d : Fin n → α} (hd : d ≠ 0) : Function.Surjective fun (a : Fin (m + n - 1) → α) => (toeplitz a).mulVec d

Toeplitz matrices reach every vector: over a field, for every nonzero vector d, every vector is T d for some m × n Toeplitz matrix T. If j₀ is the last coordinate with d j₀ ≠ 0, then for a Toeplitz matrix T supported on the m diagonals through column j₀, the i-th coordinate of T d is d j₀ times the entry of T in row i and column j₀, plus entries further down the diagonals; this triangular system can be solved for any T d.