2 Residue projectors and exact polyphase coordinates
On this page · Permalink · Source line 308
A packet has two useful representations
The masked packet keeps its original sample addresses and sets the other phases to zero. The decimated channel stores only the retained addresses, now indexed by the coarse coordinate. They carry the same values, but their domains differ. Refinement sums belong on the original lattice. Interleaving converts the channels back to that lattice.
Fix an integer \(N\ge1\). For \(0\le r<N\), define
The corresponding decimated channel is
Theorem 2.1: Polyphase projector theorem
The maps \(P_{N,r}\) are bounded orthogonal projectors on \(\ell^2\), with operator norm at most one, and satisfy
Consequently,
with no approximation.
Read proof · Visual guide: Decimation is a permutation, not a loss · Read statement and proof side by side · Permalink · Source line 325 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 2.1
Each integer belongs to exactly one residue class modulo \(N\). Multiplying the two indicator functions gives zero for distinct classes and the same indicator for equal classes. Summing all residue indicators gives one at every address. Moreover,
The mask is real-valued, so the inner-product identity follows term by term. Hence each projector is self-adjoint, and the ranges of different residue projectors are orthogonal.
Back to statement · Read statement and proof side by side · Permalink · Source line 339 · Claim record · Lean coverage · Code · Worked examples
Define the analysis and synthesis maps
Corollary 2.2: Analysis–synthesis identity
On the product of the channel spaces one also has \({\mathcal A}_N{\mathcal S}_N=I\). Equip this finite product with the Hilbert norm
Then \({\mathcal A}_N\) is a linear isometric equivalence and
Read proof · Visual guide: Decimation is a permutation, not a loss · Read statement and proof side by side · Permalink · Source line 356 · Claim record · Lean coverage · Code · Worked examples
Proof of Corollary 2.2
Euclidean division gives a unique pair \((r,q)\) with \(0\le r<N\) and \(n=Nq+r\), including negative \(n\). The address maps \(n\mapsto(n\bmod N,n\mathbin{\mathrm{div}}N)\) and \((r,q)\mapsto Nq+r\) are inverse. Analysis and synthesis are reindexing by this bijection. Reindexing the nonnegative sum \(\sum_n|x[n]|^2\) proves the norm identity and shows that both maps preserve square summability. In Lean the target is \(\ell^2(\{0,\ldots,N-1\}\times{\mathbb Z})\), which realizes exactly this Hilbert norm.
Back to statement · Read statement and proof side by side · Permalink · Source line 370 · Claim record · Lean coverage · Code · Worked examples
2.1 Nested refinement
On this page · Permalink · Source line 381
Suppose \(N,M\ge1\) and \(N\mid M\). Every coarse phase has a disjoint family of fine descendants:
Theorem 2.3: Exact nested refinement
For \(N,M\ge1\) and \(N\mid M\),
Read proof · Visual guide: Refine packets on a common lattice · Read statement and proof side by side · Permalink · Source line 390 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 2.3
An integer \(n\) satisfies \(n\equiv r\pmod N\) exactly when its unique residue \(s=n\bmod M\) lies among the listed descendants. The fine indicators are disjoint, so their sum is the coarse indicator.
Back to statement · Read statement and proof side by side · Permalink · Source line 401 · Claim record · Lean coverage · Code · Worked examples
This identity is the signal form of the refinement law introduced in Paper II. It is not merely a denser sampling rule. The coarse masked packet, represented on the original integer lattice, is exactly the sum of its fine masked descendants. Decimated channels at different moduli must first be placed in these common coordinates before being added.