norm_extendByZero_le
plain-language theorem explainer
The lemma shows that extending a finite Galerkin velocity field by zero outside its truncation window never increases the size of any individual Fourier coefficient beyond the global norm of the original field. Researchers formalizing convergence of spectral approximations to the Navier-Stokes equations cite this when controlling pointwise coefficients from uniform energy bounds. The argument splits on membership of the mode in the truncation set and reduces the claim to a comparison between a two-term sum of squares and the full sum over all (
Claim. Let $N$ be a natural number, let $u$ be a Galerkin state of velocity coefficients on the truncated modes, and let $k$ be a two-dimensional Fourier mode. Then the Euclidean norm of the coefficient of $k$ in the zero-extended Fourier state satisfies $||widetilde{u}(k)|| leq ||u||$, where $widetilde{u}$ denotes the zero-extension of $u$.
background
In the ContinuumLimit2D module the goal is to construct a Lean-checkable passage from families of finite-dimensional Galerkin approximations to a continuum Fourier state. A GalerkinState N is the Euclidean space of real coefficients indexed by the product of the finite set of modes with max-norm at most N and the two velocity components. The function extendByZero pads any such truncated state to a full FourierState2D by setting coefficients outside the truncation window to zero, using the auxiliary coeffAt to read individual components or return zero. This bound is a preliminary estimate that holds independently of any dynamics. It relies on the Euclidean norm definition on the finite-dimensional space and the fact that the zero-extension simply copies the existing coefficients while adding zeros.
proof idea
The proof proceeds by case analysis on whether the mode k belongs to the truncation set modes N. When it does, the extended coefficient is assembled from the two components of u at that mode; its squared norm is therefore the sum of those two squared components. This partial sum is bounded above by the full sum of squares that defines the squared norm of u, via the monotonicity of summation over a subset. The square-root inequality then yields the claim. When k lies outside the window the extended coefficient vanishes identically, so the inequality holds trivially.
why it matters
This elementary comparison supplies the key step that lets uniform bounds on the Galerkin norms pass to uniform bounds on every coefficient of the limit state, as required by coeff_bound_of_uniformBounds. It therefore supports the construction of the ConvergenceHypothesis in the continuum-limit pipeline. Within the Recognition Science formalization it belongs to the classical-bridge layer that prepares the ground for later identification of continuum objects with the phi-ladder structures of the foundation. The module itself packages analytic compactness steps as explicit hypotheses rather than axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.