Toeplitz Matrices

This module defines Toeplitz matrices, i.e., matrices with constant diagonals.

def Matrix.IsToeplitz {m n : ℕ} {α : Type u_1} (M : Matrix (Fin m) (Fin n) α) : Prop

A (finite) m×n matrix is *Toeplitz if all diagonals are constant.

Equations

• M.IsToeplitz = ∀ {i i' : Fin m} {j j' : Fin n}, ↑i + ↑j' = ↑j + ↑i' → M i j = M i' j'

instance decidablePredMatrixIsToeplitz {m n : ℕ} {α : Type u_1} [DecidableEq α] : DecidablePred fun (M : Matrix (Fin m) (Fin n) α) => M.IsToeplitz

Equations

• decidablePredMatrixIsToeplitz = id inferInstance

def ToeplitzMatrix (m n : ℕ) (α : Type u_1) : Type u_1

The type of (finite-size) Toeplitz matrices

Equations

• ToeplitzMatrix m n α = { M : Matrix (Fin m) (Fin n) α // M.IsToeplitz }

@[reducible, inline]

abbrev BinToeplitzMatrix (m n : ℕ) : Type

The type of binary Toeplitz matrices, equipped with a Fintype instance.

Equations

• BinToeplitzMatrix m n = ToeplitzMatrix m n (ZMod 2)

theorem toeplitzAdd {R : Type u_1} [AddMonoid R] {m n : ℕ} (M M' : ToeplitzMatrix m n R) : (↑M + ↑M').IsToeplitz

theorem toeplitzSub {R : Type u_1} [AddGroup R] {m n : ℕ} (M M' : ToeplitzMatrix m n R) : (↑M - ↑M').IsToeplitz

def ToeplitzMatrix.to_params {F : Type u_1} {m n : ℕ} [NeZero m] [NeZero n] (M : ToeplitzMatrix m n F) : Fin (m + n - 1) → F

Extract the defining parameters (diagonal entries) of a Toeplitz matrix.

Equations

• M.to_params k = if h : ↑k < n then ↑M 0 ⟨n - 1 - ↑k, ⋯⟩ else ↑M ⟨↑k - (n - 1), ⋯⟩ 0

def ToeplitzMatrix.from_params {F : Type u_1} {m n : ℕ} (v : Fin (m + n - 1) → F) : ToeplitzMatrix m n F

Construct a Toeplitz matrix from its defining parameters (diagonal entries).

Equations

• ToeplitzMatrix.from_params v = ⟨Matrix.of fun (i : Fin m) (j : Fin n) => v ⟨↑i + (n - 1) - ↑j, ⋯⟩, ⋯⟩

def ToeplitzMatrix.equiv_params {F : Type u_1} {m n : ℕ} [NeZero m] [NeZero n] : ToeplitzMatrix m n F ≃ (Fin (m + n - 1) → F)

A Toeplitz matrix is uniquely represented by a parameter vector (containing diagonal entries).

Equations

• ToeplitzMatrix.equiv_params = { toFun := ToeplitzMatrix.to_params, invFun := ToeplitzMatrix.from_params, left_inv := ⋯, right_inv := ⋯ }

instance inst_Fintype_ToeplitzMatrix {F : Type u_1} [Fintype F] [DecidableEq F] {m n : ℕ} : Fintype (ToeplitzMatrix m n F)

Note: instance computable but slow. For actually computing cardinality, use card_ToeplitzMatrix instead.

Equations

• inst_Fintype_ToeplitzMatrix = id (id inferInstance)

theorem card_ToeplitzMatrix {F : Type u_1} [Fintype F] [DecidableEq F] {m n : ℕ} [NeZero m] [NeZero n] : Fintype.card (ToeplitzMatrix m n F) = Fintype.card F ^ (m + n - 1)

The number of m x n Toeplitz matrices with Fintype entries is (EntryType.card) ^ (m + n - 1).

theorem card_BinToeplitzMatrix (m n : ℕ) [NeZero m] [NeZero n] : Fintype.card (BinToeplitzMatrix m n) = 2 ^ (m + n - 1)

Surjectivity of Toeplitz matrix-vector multiplication

M ↦ M * v is surjective for v ≠ 0.

theorem isToeplitz_diag {m n : ℕ} {F : Type u_1} [Zero F] [One F] (k : ℕ) : (Matrix.of fun (i : Fin m) (j : Fin n) => if ↑i + (n - 1) - ↑j = k then 1 else 0).IsToeplitz

The diagonal indicator matrix (1 on diagonal k, 0 elsewhere) is Toeplitz.

theorem isToeplitz_finsupp_linear_combination {F : Type u_1} [CommRing F] {m n : ℕ} (f : ToeplitzMatrix m n F →₀ F) : (Matrix.of fun (i : Fin m) (j : Fin n) => ∑ M ∈ f.support, f M * ↑M i j).IsToeplitz

A finite Finsupp linear combination of Toeplitz matrices is Toeplitz.

theorem linearMap_eq_dotProduct {R : Type u_1} [CommSemiring R] {m : ℕ} (w : (Fin m → R) →ₗ[R] R) : ∃ (v : Fin m → R), ∀ (x : Fin m → R), w x = v ⬝ᵥ x

Every linear functional on Fin m → R is represented by dot product with some vector.

theorem exists_dotProduct_annihilating {F : Type u_1} [Field F] {m : ℕ} {S : Submodule F (Fin m → F)} (hS : S ≠ ⊤) : ∃ (v : Fin m → F), v ≠ 0 ∧ ∀ x ∈ S, v ⬝ᵥ x = 0

If a submodule of Fin m → F is proper, there is a nonzero vector orthogonal to it.

theorem toeplitz_poly_coeff {F : Type u_1} [Field F] {m n : ℕ} (w : Fin m → F) (u : Fin n → F) (k : ℕ) : ((∑ i : Fin m, w i • Polynomial.X ^ ↑i) * ∑ j : Fin n, u j • Polynomial.X ^ (n - 1 - ↑j)).coeff k = w ⬝ᵥ (Matrix.of fun (i : Fin m) (j : Fin n) => if ↑i + (n - 1) - ↑j = k then 1 else 0).mulVec u

The k-th coefficient of (∑ wᵢ Xⁱ)(∑ uⱼ X^(n-1-j)) equals the dot product of w with the Toeplitz diagonal-k indicator matrix applied to u.

theorem natDegree_finset_sum_smul_pow_le {F : Type u_1} [CommSemiring F] {ι : Type u_2} {s : Finset ι} (c : ι → F) (e : ι → ℕ) {B : ℕ} (hB : ∀ i ∈ s, e i ≤ B) : (∑ i ∈ s, c i • Polynomial.X ^ e i).natDegree ≤ B

If all exponents in a finite sum ∑ cᵢ • X^(eᵢ) are bounded by B, the sum has degree at most B.

theorem natDegree_sum_smul_pow_le {F : Type u_1} [CommSemiring F] {m : ℕ} (c : Fin m → F) : (∑ i : Fin m, c i • Polynomial.X ^ ↑i).natDegree ≤ m - 1

Degree bound: a weighted sum of monomials ∑ c i • X^i for i : Fin m has degree at most m - 1.

theorem natDegree_sum_smul_pow_rev_le {F : Type u_1} [CommSemiring F] {n : ℕ} (c : Fin n → F) : (∑ j : Fin n, c j • Polynomial.X ^ (n - 1 - ↑j)).natDegree ≤ n - 1

Degree bound: a weighted sum of monomials ∑ c j • X^(n-1-j) for j : Fin n has degree at most n - 1.

theorem toeplitz_mulVec_surjective {F : Type u_1} [Field F] {m n : ℕ} [NeZero m] [NeZero n] {u : Fin n → F} (hu : u ≠ 0) : Function.Surjective fun (M : ToeplitzMatrix m n F) => (↑M).mulVec u

Multiplication by a nonzero vector is surjective from Toeplitz parameters to the output space.