extendByZeroCLM
plain-language theorem explainer
The zero-extension operator from a finite-dimensional Galerkin velocity state at truncation level N into the full Fourier coefficient space is packaged as a continuous linear map. Researchers constructing the passage from discrete fluid approximations to continuum limits cite it to carry continuity and differentiability forward under modewise convergence. The definition is a one-line wrapper that invokes the general fact that every linear map out of a finite-dimensional space is continuous.
Claim. Let $G_N$ be the finite-dimensional space of Galerkin velocity coefficients truncated at level $N$, and let $F$ be the space of all maps from modes to velocity coefficients. The zero-extension map from $G_N$ to $F$ is a continuous linear operator.
background
The ContinuumLimit2D module constructs an explicit pipeline from finite Galerkin approximations of 2D velocity fields on the torus to an infinite Fourier coefficient object. GalerkinState N is the Euclidean space over the product of the truncated mode set and the two velocity components. FourierState2D is the type of unrestricted maps from all modes to velocity coefficients. The upstream linear map extendByZeroLinear realizes zero extension as a linear map between these spaces; the present definition wraps it to obtain a continuous linear map.
proof idea
The definition applies LinearMap.toContinuousLinearMap directly to extendByZeroLinear N. Finite dimensionality of the domain guarantees that the linear map is automatically continuous, so the wrapper requires no separate continuity argument.
why it matters
This supplies the continuous embedding required to transfer analytic properties such as measurability of forcing terms and differentiability of trajectories into the continuum limit. It is used in aestronglyMeasurable_galerkinForcing_mode_of_continuous and hasDerivAt_extendByZero_apply. Within the Recognition framework it advances the M5 milestone by making the Galerkin-to-Fourier embedding explicit, so that linear constraints such as the divergence-free condition can be preserved under the limit while hypotheses remain visible for later discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.