The transfer exponential basis

Proof of Theorem 4.2

Termwise differentiation gives the cyclic derivative formulas. One full cycle contributes \(\lambda^N\). The first nonzero term of \({\mathsf E}_{N,j}(\lambda z)\) is \((\lambda z)^j/j!\), which gives the initial data. The initial value vectors are linearly independent when \(\lambda\ne0\). The solution space of an order \(N\) constant coefficient equation has dimension \(N\), so these functions form a basis.

Back to statement · Read statement and proof side by side · Permalink · Source line 471 · Claim record · Lean coverage · Code · Worked examples

Proof of Corollary 4.3

At the origin, the derivative matrix is diagonal with entries

For an explicit determinant proof, write each basis function as a finite sum of exponentials with exponents \(a_\ell=\lambda\omega^\ell\). Its derivative matrix factors as

where \(C\) is the constant matrix of Fourier weights. Thus

because \(N\geq2\) implies \(\sum_\ell\omega^\ell=0\). The product of the diagonal initial values is the stated power of \(\lambda\).

Back to statement · Read statement and proof side by side · Permalink · Source line 487 · Claim record · Lean coverage · Code · Worked examples

Proof of Corollary 4.4

Expand \(e^{\lambda(z+w)}=e^{\lambda z}e^{\lambda w}\) as a bivariate power series. A term \(z^a w^b\) contributes to the \(k\)th section exactly when \(a+b\equiv k\bmod N\). Grouping first by \(i\equiv a\bmod N\) and \(j\equiv b\bmod N\) gives the displayed sum.

Back to statement · Read statement and proof side by side · Permalink · Source line 517 · Claim record · Lean coverage · Code · Worked examples

Proof of Theorem 4.5

The multiplication formula for the gamma function gives

Indeed, the \(N\) Pochhammer factors supplied by the multiplication formula are \(((j+m)/N)_n\) for \(1\leq m\leq N\); the excluded factor is \(((j+N-j)/N)_n=(1)_n=n!\). Insertion into the defining series gives the stated hypergeometric expansion.

Back to statement · Read statement and proof side by side · Permalink · Source line 553 · Claim record · Lean coverage · Code · Worked examples