hasDerivAt_extendByZero_apply
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove convergence of any Galerkin sequence to a continuum solution.
- Does not treat boundary conditions, external forcing, or incompressibility enforcement.
- Does not extend the differentiation result to three spatial dimensions.
- Does not supply quantitative error estimates between truncated and full states.
formal statement (Lean)
294lemma hasDerivAt_extendByZero_apply {N : ℕ} (k : Mode2)
295 (u : ℝ → GalerkinState N) (u' : GalerkinState N) {t : ℝ} (hu : HasDerivAt u u' t) :
296 HasDerivAt (fun s : ℝ => (extendByZero (u s)) k) ((extendByZero u') k) t := by
proof body
Tactic-mode proof.
297 classical
298 -- A constant continuous linear map: project the `k`-th Fourier coefficient after zero-extension.
299 let L : GalerkinState N →L[ℝ] VelCoeff :=
300 (ContinuousLinearMap.proj k).comp (extendByZeroCLM (N := N))
301 have hL : HasDerivAt (fun _ : ℝ => L) 0 t := by
302 simpa using (hasDerivAt_const (x := t) (c := L))
303 -- Differentiate `s ↦ L (u s)`.
304 have h := HasDerivAt.clm_apply (c := fun _ : ℝ => L) (c' := (0 : GalerkinState N →L[ℝ] VelCoeff))
305 (u := u) (u' := u') (x := t) hL hu
306 -- Unfold `L` back to `extendByZero` + evaluation at `k`.
307 simpa [L, extendByZeroCLM] using h
308