extendByZeroLinear
plain-language theorem explainer
The definition packages the zero-extension of a truncated Galerkin velocity state into the full Fourier coefficient space on the torus as a linear map over the reals. Researchers building the M5 continuum-limit pipeline in 2D fluids would cite it to obtain the canonical embedding before passing to continuous-linear versions. It is assembled directly from the additivity and homogeneity lemmas for the underlying function.
Claim. The linear map $GalerkinState(N) →_ℝ FourierState2D$ that sends each finite truncation of velocity coefficients on the 2-torus to its zero-padded extension in the infinite mode space.
background
The ContinuumLimit2D module defines a Lean-checkable pipeline shape that carries finite-dimensional 2D Galerkin approximations to an infinite Fourier coefficient state. GalerkinState N is the Euclidean space of velocity coefficients indexed by the truncated modes and the two vector components. FourierState2D is the function type Mode2 → VelCoeff that holds coefficients for every mode. The upstream function extendByZero realizes the zero-padding map, while the sibling lemmas extendByZero_add and extendByZero_smul record that this map respects vector addition and scalar multiplication.
proof idea
The definition builds a LinearMap record whose toFun field is extendByZero; the map_add' field is supplied by extendByZero_add and the map_smul' field is supplied by extendByZero_smul (via a simpa that rewrites the scalar action).
why it matters
It supplies the linear-map structure required by the downstream definition extendByZeroCLM, which converts the map to a continuous linear map via LinearMap.toContinuousLinearMap. The construction sits inside the M5 milestone that makes the discrete-to-continuum embedding explicit so that analytic compactness steps can later be discharged as theorems rather than hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.