hasDerivAt_extendByZero_apply
plain-language theorem explainer
Differentiation commutes with zero-extension of finite Galerkin states to full 2D Fourier coefficient fields. Researchers formalizing the passage from Galerkin approximations to continuum Navier-Stokes solutions cite this when justifying term-by-term differentiation of the embedded velocity field. The proof constructs the extension as a constant continuous linear map and invokes the chain rule for its application to the differentiable family u.
Claim. Let $N$ be a natural number, $k$ a 2D Fourier mode, $u:ℝ→$ (velocity coefficients on the $N$-truncated modes) and $u'$ a velocity coefficient vector. If $u$ is differentiable at $t$ with derivative $u'$, then the map $s↦$ (zero-padded $u(s)$ evaluated at mode $k$) is differentiable at $t$ with derivative (zero-padded $u'$ evaluated at $k$).
background
The ContinuumLimit2D module defines the pipeline shape from finite-dimensional 2D Galerkin approximations to a continuum Fourier object. extendByZero pads a GalerkinState N (Euclidean space of velocity coefficients on truncated modes) by zero outside the truncation to produce a full FourierState2D. extendByZeroCLM realizes this padding as a continuous linear map, which exists because the domain is finite-dimensional. Mode2 denotes a pair of integers indexing a 2D Fourier wavevector; VelCoeff is the corresponding real 2-vector of velocity components.
proof idea
The proof defines a constant continuous linear map L as the composition of projection onto coefficient k with extendByZeroCLM. It records that the constant map to L has derivative zero at t, applies HasDerivAt.clm_apply to differentiate the composition L∘u, and simplifies the result back to the stated form.
why it matters
The lemma is invoked directly by galerkinNS_hasDerivAt_extendByZero_mode to obtain the differentiated extended Navier-Stokes right-hand side. It supplies one of the analytic identification steps required by the M5 milestone, which packages compactness and limit passages as explicit hypotheses so that later work can replace them with proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.