Toeplitz matrices

DefinitionLower-triangular Toeplitz matrix#✓fully proved

Let \(R\) be a set with a zero element \(0\) and let \(a = (a_0, a_1, a_2, \dots)\) be a sequence in \(R\). The lower-triangular Toeplitz matrix of \(a\) is the matrix with rows and columns indexed by \(\mathbb{N}\) whose \((i, j)\) entry is \(a_{i-j}\) when \(j \le i\) and \(0\) when \(j > i\). In particular it is constant along each diagonal and vanishes strictly above the main diagonal.

def lowerToeplitz {R : Type*} [Zero R] (a : ℕ → R) : Matrix ℕ ℕ R :=
  fun i j => if j ≤ i then a (i - j) else 0
Sources
Used by 5
Used byTotal positivity of Bell-type Riordan arrays from a Pólya frequency series · Bell-type Riordan arrays with a Pólya frequency A-sequence are totally positive · Diagonal entries of a lower-triangular Toeplitz matrix · Entries above the diagonal of a lower-triangular Toeplitz matrix · Entries on and below the diagonal of a lower-triangular Toeplitz matrix

TheoremEntries on and below the diagonal of a lower-triangular Toeplitz matrix#✓fully proved

Let \(R\) be a set with a zero element and \(a = (a_0, a_1, \dots)\) a sequence in \(R\). For natural numbers \(j \le i\), the \((i, j)\) entry of the lower-triangular Toeplitz matrix of \(a\) is \(a_{i-j}\).

@[simp]
theorem lowerToeplitz_apply_of_le {R : Type*} [Zero R] (a : ℕ → R) {i j : ℕ}
    (h : j ≤ i) : lowerToeplitz a i j = a (i - j)
Uses 1 · Used by 1
Statement usesLower-triangular Toeplitz matrix
Used byDiagonal entries of a lower-triangular Toeplitz matrix

TheoremEntries above the diagonal of a lower-triangular Toeplitz matrix#✓fully proved

Let \(R\) be a set with a zero element and \(a = (a_0, a_1, \dots)\) a sequence in \(R\). For natural numbers \(i < j\), the \((i, j)\) entry of the lower-triangular Toeplitz matrix of \(a\) is \(0\).

@[simp]
theorem lowerToeplitz_apply_of_gt {R : Type*} [Zero R] (a : ℕ → R) {i j : ℕ}
    (h : i < j) : lowerToeplitz a i j = 0
Uses 1
Statement usesLower-triangular Toeplitz matrix

TheoremDiagonal entries of a lower-triangular Toeplitz matrix#✓fully proved

Let \(R\) be a set with a zero element and \(a = (a_0, a_1, \dots)\) a sequence in \(R\). For every natural number \(i\), the \((i, i)\) entry of the lower-triangular Toeplitz matrix of \(a\) is \(a_0\).

@[simp]
theorem lowerToeplitz_apply_diag {R : Type*} [Zero R] (a : ℕ → R) (i : ℕ) :
    lowerToeplitz a i i = a 0
Uses 2
Statement usesLower-triangular Toeplitz matrix
Proof usesEntries on and below the diagonal of a lower-triangular Toeplitz matrix

DefinitionToeplitz matrix#✓fully proved

A real \((n+1) \times (n+1)\) matrix \(A = (a_{ij})\), with rows and columns indexed by \(\{0, \dots, n\}\), is Toeplitz if there is a function \(c : \mathbb{Z} \to \mathbb{R}\) such that \(a_{ij} = c(i - j)\) for all \(i, j\). Equivalently, \(A\) is constant along each of its diagonals.

Only the values \(c(k)\) with \(-n \le k \le n\) enter the condition, so this is the same as asking for real coefficients \(c_{-n}, \dots, c_n\).

def IsToeplitzMatrix {n : ℕ} (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ) : Prop :=
  ∃ c : ℤ → ℝ, ∀ i j, A i j = c ((i.val : ℤ) - (j.val : ℤ))
Sources
  • https://cs.uwaterloo.ca/journals/JIS/VOL18/Felsner/felsner2.tex
Used by 2
Used bySymmetric Toeplitz matrices are Toeplitz · Toeplitz matrices from coefficients

DefinitionSymmetric Toeplitz matrix#✓fully proved

A real \((n+1) \times (n+1)\) matrix \(A = (a_{ij})\), with rows and columns indexed by \(\{0, \dots, n\}\), is symmetric Toeplitz if there is a function \(c : \mathbb{Z} \to \mathbb{R}\) such that \(c(-k) = c(k)\) for every integer \(k\) and \(a_{ij} = c(i - j)\) for all \(i, j\).

def IsSymmetricToeplitzMatrix {n : ℕ} (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ) : Prop :=
  ∃ c : ℤ → ℝ, (∀ k : ℤ, c (-k) = c k) ∧
    ∀ i j, A i j = c ((i.val : ℤ) - (j.val : ℤ))
Sources
  • https://cs.uwaterloo.ca/journals/JIS/VOL18/Felsner/felsner2.tex
Used by 3
Used bySymmetric Toeplitz matrices are symmetric · Symmetric Toeplitz matrices from even coefficients · Symmetric Toeplitz matrices are Toeplitz

TheoremToeplitz matrices from coefficients#✓fully proved

Let \(A = (a_{ij})\) be a real \((n+1) \times (n+1)\) matrix with rows and columns indexed by \(\{0, \dots, n\}\). If \(c : \mathbb{Z} \to \mathbb{R}\) satisfies \(a_{ij} = c(i - j)\) for all \(i, j\), then \(A\) is a Toeplitz matrix.

theorem isToeplitzMatrix_of_witness {n : ℕ}
    {A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} {c : ℤ → ℝ}
    (h : ∀ i j, A i j = c ((i.val : ℤ) - (j.val : ℤ))) : IsToeplitzMatrix A
Uses 1
Statement usesToeplitz matrix

TheoremSymmetric Toeplitz matrices from even coefficients#✓fully proved

Let \(A = (a_{ij})\) be a real \((n+1) \times (n+1)\) matrix with rows and columns indexed by \(\{0, \dots, n\}\). If \(c : \mathbb{Z} \to \mathbb{R}\) satisfies \(c(-k) = c(k)\) for every integer \(k\) and \(a_{ij} = c(i - j)\) for all \(i, j\), then \(A\) is a symmetric Toeplitz matrix.

theorem isSymmetricToeplitzMatrix_of_witness {n : ℕ}
    {A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} {c : ℤ → ℝ}
    (hsym : ∀ k : ℤ, c (-k) = c k)
    (h : ∀ i j, A i j = c ((i.val : ℤ) - (j.val : ℤ))) : IsSymmetricToeplitzMatrix A
Uses 1
Statement usesSymmetric Toeplitz matrix

TheoremSymmetric Toeplitz matrices are Toeplitz#✓fully proved

Every real \((n+1) \times (n+1)\) symmetric Toeplitz matrix is a Toeplitz matrix.

theorem IsSymmetricToeplitzMatrix.isToeplitz {n : ℕ}
    {A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ}
    (h : IsSymmetricToeplitzMatrix A) : IsToeplitzMatrix A
Uses 2
Statement usesSymmetric Toeplitz matrix · Toeplitz matrix

TheoremSymmetric Toeplitz matrices are symmetric#✓fully proved

If \(A = (a_{ij})\) is a real \((n+1) \times (n+1)\) symmetric Toeplitz matrix, with rows and columns indexed by \(\{0, \dots, n\}\), then \(a_{ij} = a_{ji}\) for all \(i, j\).

theorem IsSymmetricToeplitzMatrix.entry_comm {n : ℕ}
    {A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ}
    (h : IsSymmetricToeplitzMatrix A) (i j : Fin (n + 1)) : A i j = A j i
Uses 1
Statement usesSymmetric Toeplitz matrix
10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.