Hankel matrices

DefinitionInfinite Hankel matrix#✓fully proved

For a sequence \(s \colon \mathbb{N} \to \alpha\) with values in a set \(\alpha\), the infinite Hankel matrix generated by \(s\) has rows and columns indexed by \(\mathbb{N}\) and \((i, j)\) entry \(s_{i+j}\).

def hankel {α : Type*} (s : ℕ → α) : Matrix ℕ ℕ α :=
  fun i j ↦ s (i + j)

DefinitionFinite Hankel matrix#✓fully proved

For \(n \in \mathbb{N}\) and a sequence \(s \colon \mathbb{N} \to \alpha\) with values in a set \(\alpha\), the \(n \times n\) Hankel matrix generated by \(s\) has rows and columns indexed by \(\{0, \dots, n-1\}\) and \((i, j)\) entry \(s_{i+j}\), where \(i + j\) is the sum in \(\mathbb{N}\).

def hankelFin {α : Type*} (n : ℕ) (s : ℕ → α) : Matrix (Fin n) (Fin n) α :=
  fun i j ↦ s (i + j)

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.