extendByZero_laplacianCoeff
The lemma shows that the Fourier Laplacian commutes with zero-extension from a finite Galerkin truncation to the full Fourier coefficient field. Researchers deriving continuum limits of 2D Navier-Stokes Galerkin approximations would cite it when passing derivatives through the embedding map. The proof reduces to case analysis on whether the mode lies inside the truncation window, followed by direct simplification of the coefficient definitions.
claimLet $u$ be a Galerkin state truncated at level $N$. For any mode $k$, the zero-extended Laplacian coefficient satisfies $ (extendByZero (laplacianCoeff u)) (k) = (-|k|^2) · (extendByZero u) (k) $, where laplacianCoeff multiplies each coefficient by $-|k|^2$ and extendByZero pads with zeros outside the truncation window.
background
The ContinuumLimit2D module constructs a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to continuum Fourier states. GalerkinState N is the Euclidean space of velocity coefficients indexed by modes with max(|k1|,|k2|) ≤ N and two real components per mode. extendByZero embeds such a state into the full FourierState2D by reading components via coeffAt and setting them to zero for modes outside the truncation. laplacianCoeff applies the Fourier Laplacian, multiplying each coefficient by -kSq(k) where kSq(k) = k1² + k2². This identity is a direct algebraic consequence of those definitions.
proof idea
The term-mode proof opens with classical logic and splits on whether k belongs to modes N. When k is inside the truncation, it extends the vector equality componentwise and simplifies using the definitions of extendByZero, coeffAt, and laplacianCoeff. When k lies outside, it simplifies directly via extendByZero and coeffAt, both of which return zero.
why it matters in Recognition Science
The lemma is invoked inside galerkinNS_hasDerivAt_extendByZero_mode to pass the time derivative through the zero-extension for the full Navier-Stokes right-hand side. It supplies an elementary step in the M5 milestone for identifying Galerkin trajectories with continuum Fourier objects, relying only on the embedding and Laplacian definitions without analytic estimates.
scope and limits
- Does not establish convergence of Galerkin states as N tends to infinity.
- Does not treat the nonlinear convection term or its projection.
- Does not supply coefficient bounds or Sobolev estimates.
- Does not address time-dependent trajectories or mild-solution identification.
Lean usage
theorem galerkinNS_hasDerivAt_extendByZero_mode {N : ℕ} (ν : ℝ) (B : ConvectionOp N) (u : ℝ → GalerkinState N) (k : Mode2) {t : ℝ} (hu : HasDerivAt u (galerkinNSRHS ν B (u t)) t) : HasDerivAt (fun s => (extendByZero (u s)) k) ((ν * (-kSq k)) • (extendByZero (u t)) k - (extendByZero (B (u t) (u t))) k) t := by apply galerkinNS_hasDerivAt_extendByZero_mode; exact extendByZero_laplacianCoeff (u t) kformal statement (Lean)
285lemma extendByZero_laplacianCoeff {N : ℕ} (u : GalerkinState N) (k : Mode2) :
286 (extendByZero (laplacianCoeff (N := N) u)) k = (-kSq k) • (extendByZero u) k := by
proof body
Term-mode proof.
287 classical
288 by_cases hk : k ∈ modes N
289 · ext j
290 fin_cases j <;> simp [extendByZero, coeffAt, hk, laplacianCoeff]
291 · ext j
292 fin_cases j <;> simp [extendByZero, coeffAt, hk]
293