Diagonal sequences of square zig-zag shapes

DefinitionRight-down diagonal coefficient#✓fully proved

For natural numbers \(k\) and \(i\), the coefficient \(c_k(i)\) of the right-down diagonal recurrence is the integer \((-1)^i \binom{k+1-i}{i+1}\) when \(i \le k+1\), and \(0\) when \(i > k+1\).

def rightDownDiagonalCoefficient (k i : ℕ) : ℤ :=
  (-1) ^ i * Nat.choose (k + 1 - i) (i + 1)

Used by 1

Used byRight-down diagonal families of order \(k\)

DefinitionRight-down diagonal families of order \(k\)#✓fully proved

For a natural number \(k\), a family \((A_j)_{0 \le j \le k+1}\) of integer sequences \(A_j : \mathbb{N} \to \mathbb{Z}\) is a family of right-down diagonal sequences of order \(k\) when \(k \ge 1\) and, for every \(j\) and every natural number \(n \ge \lfloor k/2 \rfloor + 1\),

\[A_j(n) = \sum_{i=0}^{\lfloor k/2 \rfloor} c_k(i)\, A_j(n-1-i),\]

where \(c_k(i) = (-1)^i \binom{k+1-i}{i+1}\) is the right-down diagonal coefficient.

def IsRightDownDiagonalFamily (k : ℕ) (A : Fin (k + 2) → ℕ → ℤ) : Prop :=
  1 ≤ k ∧ ∀ j n, k / 2 + 1 ≤ n →
    A j n = ∑ i ∈ Finset.range (k / 2 + 1),
      rightDownDiagonalCoefficient k i * A j (n - 1 - i)

Sources

• László Németh and László Szalay, Sequences Involving Square Zig-Zag Shapes, Journal of Integer Sequences 24 (2021), Article 21.5.2.

Uses 1

Statement usesRight-down diagonal coefficient

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.