4.2 Banded multiplication, differentiation and conversion

In Jacobi and ultraspherical bases, multiplication by \(x\) is tridiagonal. Differentiation raises the parameters and has a single superdiagonal. One-step conversion has bandwidth \((0,1)\) for Jacobi and \((0,2)\) for ultraspherical bases. These sparse matrices are those of the ultraspherical spectral method [OT13], used by ApproxFun [AF]. The identities with denominators cleared hold over every commutative \(\mathbb {Q}\)-algebra. Divided entries and bandwidths require nonvanishing denominators; these conditions hold in the real orthogonality ranges.

Theorem 4.2.1 Jacobi multiplication matrix

✓ 🤖

In a Jacobi target basis, write \(s=\alpha +\beta \). For input degree \(n\ge 1\), only rows \(n+1,n,n-1\) can be nonzero, with respective entries

\[ \frac{2(n+1)(n+s+1)}{(2n+s+1)(2n+s+2)},\qquad \frac{\beta ^2-\alpha ^2}{(2n+s)(2n+s+2)},\qquad \frac{2(n+\alpha )(n+\beta )}{(2n+s)(2n+s+1)}. \]

Column zero has entries \(2/(s+2)\) in row one and \((\beta -\alpha )/(s+2)\) in row zero. The divided formulas hold over fields with a rational algebra structure when the displayed denominator factors are nonzero; cleared identities hold over commutative rational algebras. For real \(\alpha ,\beta {\gt}-1\) all factors are nonzero and the matrix has bandwidths \((1,1)\).

Reference: [DLMF, 18.9.1–18.9.2].

Lean Formalisation

theorem Polynomial.jacobi_mul_matrix_succ.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (α β : R)
  (b : Module.Basis ℕ R (Polynomial R)) (hb : ∀ (k : ℕ), b k = Polynomial.jacobi α β k) (n i : ℕ) :
  (2 * ↑n + α + β + 3) * (2 * ↑n + α + β + 2) * (2 * ↑n + α + β + 4) *
      b.toMatrix (fun j => Polynomial.X * Polynomial.jacobi α β j) i (n + 1) =
    ((if i = n + 2 then 2 * (↑n + 2) * (↑n + α + β + 2) * (2 * ↑n + α + β + 2) else 0) -
        if i = n + 1 then (2 * ↑n + α + β + 3) * (α ^ 2 - β ^ 2) else 0) +
      if i = n then 2 * (↑n + α + 1) * (↑n + β + 1) * (2 * ↑n + α + β + 4) else 0

Lean proof

/-- Cleared multiplication entries for positive-index columns (DLMF 18.9.1--2). -/
theorem jacobi_mul_matrix_succ
    (hb : ∀ k, b k = jacobi α β k) (n i : ℕ) :
    ((2 * n + α + β + 3) * (2 * n + α + β + 2) * (2 * n + α + β + 4)) *
        b.toMatrix (fun j ↦ X * jacobi α β j) i (n + 1) =
      (if i = n + 2 then 2 * (n + 2) * (n + α + β + 2) *
        (2 * n + α + β + 2) else 0) -
      (if i = n + 1 then (2 * n + α + β + 3) * (α ^ 2 - β ^ 2) else 0) +
      (if i = n then 2 * (n + α + 1) * (n + β + 1) *
        (2 * n + α + β + 4) else 0) := by
  have he : C ((2 * n + α + β + 3) * (2 * n + α + β + 2) *
        (2 * n + α + β + 4)) * (X * jacobi α β (n + 1)) =
      C (2 * (n + 2) * (n + α + β + 2) * (2 * n + α + β + 2)) *
        jacobi α β (n + 2) -
      C ((2 * n + α + β + 3) * (α ^ 2 - β ^ 2)) * jacobi α β (n + 1) +
      C (2 * (n + α + 1) * (n + β + 1) * (2 * n + α + β + 4)) * jacobi α β n := by
    have h := jacobi_recurrence α β n
    simp only [map_mul, map_add, map_sub, map_pow, map_natCast, map_ofNat] at h ⊢
    linear_combination -h
  have h := congrArg (fun p : R[X] ↦ b.repr p i) he
  simp only [← smul_eq_C_mul] at h
  simp only [map_add, map_sub, map_smul, Finsupp.coe_add, Finsupp.coe_sub,
    Pi.add_apply, Pi.sub_apply, Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul] at h
  simpa [Basis.toMatrix_apply, ← hb, Finsupp.single_apply, eq_comm, mul_ite] using h

4.2 Banded multiplication, differentiation and conversion

Example (Julia).