galerkin_duhamelKernel_identity
plain-language theorem explainer
The modewise Duhamel identity equates the zero-extended Fourier coefficient of a Galerkin trajectory for the 2D Navier-Stokes equations to the heat-damped initial value plus the time-integrated effect of the nonlinear convection term. Analysts studying convergence of Galerkin schemes to continuum weak solutions cite the identity to justify modewise integral representations. The proof is a direct algebraic rearrangement that invokes the kernel-form remainder identity and adds the heat term to both sides of the resulting equation.
Claim. Let $u$ be a trajectory in the finite-dimensional Galerkin space that satisfies the projected Navier-Stokes ODE with viscosity parameter $ν$ and convection operator $B$. Assume the integrand formed by the heat kernel times the extended convection term is interval-integrable on $[0,t]$. Then the zero-extended Fourier coefficient at wavevector $k$ obeys $û(t,k)=e^{-ν|k|^2 t}û(0,k)-∫_0^t e^{-ν|k|^2(t-s)}B̂(u(s),u(s))(k)ds$.
background
The module ContinuumLimit2D supplies the explicit objects needed to embed a family of finite Galerkin truncations into an infinite Fourier lattice while keeping every analytic compactness step visible as a hypothesis. The zero-extension map pads a truncated coefficient vector with zeros to produce a full Fourier state. The heat factor multiplies each mode by the exponential damping $e^{-ν|k|^2 t}$. The Duhamel kernel integral convolves a forcing trajectory against this heat kernel, producing the explicit integral term $-∫_0^t heatFactor(ν,t-s,k)·F(s,k)ds$. The upstream theorem duhamelRemainderOfGalerkin_kernel rewrites the difference between the evolved coefficient and its heat-evolved initial value into precisely this integral form against the convection forcing.
proof idea
The argument first applies the kernel-form remainder theorem duhamelRemainderOfGalerkin_kernel, which already encodes the integral representation of the difference between the extended state at time $t$ and the heat-evolved initial state. It then unfolds the definition of the Duhamel remainder to identify that difference with the kernel integral of the extended convection term. The final step adds the heat term to both sides of the resulting equation via the equivalence sub_eq_iff_eq_add'.
why it matters
The identity supplies the exact Duhamel representation required by the coefficient bounds nsDuhamelCoeffBound_galerkinKernel and nsDuhamelCoeffBound_galerkinKernel_of_forcing. Those bounds are the analytic input to the global regularity theorems rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel and its forcing variant in Regularity2D. Within the Recognition Science pipeline it closes the modewise integral link in the classical bridge from discrete Galerkin systems to continuum limits at milestone M5, where the forcing chain and three-dimensional octave structure remain downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.