Cyclic projection of analytic functions

Proof of Theorem 3.1

Substitution of the power series gives

The inner average is one when \(m\equiv j\bmod N\) and zero otherwise. The operator identities follow from the disjoint residue classes.

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

Proof of Proposition 3.2

Every monomial selected by \({\mathcal B}_{N,j}\) has the stated covariance. Conversely, write \(F=\sum_k{\mathcal B}_{N,k}F\). Replacing \(z\) by \(\omega z\) gives

Application of \({\mathcal B}_{N,k}\) gives

The powers \(1,\omega,\ldots,\omega^{N-1}\) are distinct, so \({\mathcal B}_{N,k}F=0\) for \(k\ne j\).

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

Proof of Theorem 3.3

Write \(F=\sum_iF_i\) and \(G=\sum_jG_j\), where \(F_i={\mathcal B}_{N,i}F\) and \(G_j={\mathcal B}_{N,j}G\). Their covariance gives

so \(F_iG_j\) belongs to the packet labelled by \(i+j\) modulo \(N\). Expanding the finite product and applying \({\mathcal B}_{N,k}\) gives the formula.

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