The exact retained-packet approximation shares the same discontinuity as its target. If \(f=s+j\) and \(Q_ms\to s\) uniformly, then
The approximants themselves may be discontinuous. There is no conflict with the failure of continuous Fourier polynomials to converge uniformly to a jump.
Reading the drawing
The plot compares a signal containing a jump, a Fourier approximation and a reconstruction that retains the jump packet. The Fourier curve oscillates near the jump while the packet reconstruction follows the chosen target. This plot illustrates a conditional approximation comparison; it supplies no independent recovery certificate.
Evidence note from the source edition
Preserved vector figure from the expanded source. It illustrates the choice of approximation target; it is not an independent universal recovery certificate.
Estimated packets need the operator norm too
If the bounded linear operators satisfy \(\sup_m\|Q_m\|_{L^p\to L^p}\le C_Q\), then
For an orthogonal \(L^2\) projection one may use \(\|I-Q_m\|\le1\), sharpening the packet multiplier to one. Such a bound must be justified in the norm actually being used. In particular, uniform boundedness of Fourier partial sums in the supremum norm is not supplied by this theorem.
What the complete guide establishes
V1 to V26 preserve the original worked layer. V27 to V40 explain the additional traditional developments, outside the inherited twenty-result Lean map. The new exact examples have their own finite arithmetic record. They do not extend the formal coverage merely by appearing beside formally mapped results. The final package keeps current computations and inherited compiler reports attached to their stated scope. The symbolic visual suite was rerun, with 181 checks passed and seven invalid controls rejected. Lean compiler evidence remains inherited. No fresh Lean run is claimed.
Read this as
A complete error claim specifies the signal class, the recovered packet, the approximation operator, and the norm. Each term can then be improved and checked on its own terms.