Bell matrices

StructureBell matrix#✓fully proved

Let \(R\) be a commutative ring. A Bell matrix over \(R\) is given by a formal power series \(g \in R[[X]]\) whose constant coefficient is a unit of \(R\). The corresponding Riordan-array pair is \((g, Xg)\).

structure BellMatrix (R : Type*) [CommRing R] where
  g : PowerSeries R
  isUnit_const : IsUnit g.constantCoeff
Used by 3
Used byCentral coefficients of Bell matrices · Entries of a Bell matrix · Second component of a Bell matrix

DefinitionSecond component of a Bell matrix#✓fully proved

For a Bell matrix over a commutative ring \(R\) given by the power series \(g\), the second component of its Riordan-array pair is the power series \(h = Xg \in R[[X]]\).

noncomputable def BellMatrix.h {R : Type*} [CommRing R] (M : BellMatrix R) :
    PowerSeries R :=
  PowerSeries.X * M.g
Uses 1
Statement usesBell matrix

DefinitionEntries of a Bell matrix#✓fully proved

For a Bell matrix over a commutative ring \(R\) given by the power series \(g\), and natural numbers \(n\) and \(k\), the entry in row \(n\) and column \(k\) is the coefficient of \(X^n\) in \(g \cdot (Xg)^k\).

noncomputable def BellMatrix.entry {R : Type*} [CommRing R] (M : BellMatrix R)
    (n k : ℕ) : R :=
  (M.g * (PowerSeries.X * M.g) ^ k).coeff n
Uses 1 · Used by 1
Statement usesBell matrix
Used byCentral coefficients of Bell matrices

TheoremCentral coefficients of Bell matrices#✓fully proved

Let \(g \in \mathbb{Z}[[X]]\) be the power series of a Bell matrix over \(\mathbb{Z}\), with constant coefficient \(g(0) = 1\), and let \(u \in \mathbb{Z}[[X]]\) be a power series with constant coefficient \(0\) such that substituting \(u\) for \(X\) in \(X \, g(X)^{-1}\) gives \(X\). Then for every natural number \(n\), the entry of the Bell matrix in row \(2n\) and column \(n\) equals \((n+1)\) times the coefficient of \(X^{n+1}\) in \(u\).

The source writes the right-hand side as \((n+1)\,[x^n]\,\tfrac{1}{x} u(x)\).

theorem bell_riordan_central_coefficient
    (M : BellMatrix ℤ) (u : PowerSeries ℤ)
    (hg : PowerSeries.constantCoeff M.g = 1)
    (hu₀ : PowerSeries.constantCoeff u = 0)
    (hu : (PowerSeries.X * PowerSeries.invOfUnit M.g (1 : ℤˣ)).subst u = PowerSeries.X)
    (n : ℕ) :
    M.entry (2 * n) n =
      (n + 1 : ℤ) * PowerSeries.coeff (n + 1) u
Sources
Uses 3
Statement usesBell matrix · Entries of a Bell matrix
Proof usesLagrange–Bürmann formula from the fixed-point equation alone
4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.