galerkin_duhamelKernel_identity
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence or uniqueness of Galerkin trajectories.
- Applies only to the two-dimensional incompressible Navier-Stokes system.
- Retains the dominated-convergence hypothesis for the continuum limit.
- Does not address the three-dimensional regularity problem.
- Assumes the convection operator is supplied as a fixed bilinear map on the truncated space.
formal statement (Lean)
831theorem galerkin_duhamelKernel_identity
832 {N : ℕ} (ν : ℝ) (B : ConvectionOp N) (u : ℝ → GalerkinState N) (k : Mode2) (t : ℝ)
833 (hu : ∀ s : ℝ, HasDerivAt u (galerkinNSRHS (N := N) ν B (u s)) s)
proof body
Tactic-mode proof.
834 (hint :
835 IntervalIntegrable (fun s : ℝ =>
836 (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k))
837 MeasureTheory.volume 0 t) :
838 (extendByZero (u t) k)
839 =
840 (heatFactor ν t k) • (extendByZero (u 0) k)
841 + (duhamelKernelIntegral ν (fun s : ℝ => extendByZero (B (u s) (u s))) t) k := by
842 -- Start from the kernel-form remainder identity.
843 have hR :=
844 duhamelRemainderOfGalerkin_kernel (N := N) (ν := ν) (B := B) (u := u) (k := k) (t := t) hu hint
845 -- Unfold the remainder and rearrange.
846 -- `R(t,k) = û(t,k) - heatFactor(t)•û(0,k)` and `R(t,k) = kernelIntegral(t,k)`.
847 have :
848 (extendByZero (u t) k) - (heatFactor ν t k) • (extendByZero (u 0) k)
849 =
850 (duhamelKernelIntegral ν (fun s : ℝ => extendByZero (B (u s) (u s))) t) k := by
851 simpa [duhamelRemainderOfGalerkin, duhamelKernelIntegral] using hR
852 -- Add the heat term to both sides.
853 exact (sub_eq_iff_eq_add').1 this
854
855/-!
856## A derived bound: single coefficient ≤ global norm
857
858Even before doing any PDE analysis, we can prove a simple but useful fact:
859the norm of one Fourier coefficient (after zero-extension) is bounded by the
860global Euclidean norm of the truncated Galerkin state.
861-/
862