galerkinNS_hasDerivAt_duhamelRemainder_mode
plain-language theorem explainer
If a Galerkin trajectory u satisfies the projected Navier-Stokes ODE at time t, then the modewise Duhamel remainder R(s,k) obeys the forced linear ODE whose derivative at s=t is nu times negative k-squared times R(t,k) minus the zero-extended convection term. Analysts building rigorous Galerkin-to-continuum passages for 2D incompressible flow cite this differential identity. The proof differentiates the remainder by parts, invoking the known derivative of the zero-extended state, explicit differentiation of the heat factor, and algebraic rewrit
Claim. Suppose the map $u : ℝ →$ GalerkinState N satisfies the discrete Navier-Stokes right-hand side at a fixed time $t$. Define the Duhamel remainder by $R(s,k) :=$ (zero-extended $u(s)$ at mode $k$) $-$ heatFactor($ν$,$s$,$k$) ⋅ (zero-extended $u(0)$ at $k$). Then the derivative of $R(·,k)$ at $s=t$ equals $ν(-|k|^2) R(t,k)$ minus the zero-extended convection operator applied to $(u(t),u(t))$ at mode $k$.
background
The ContinuumLimit2D module constructs an explicit embedding of finite Galerkin approximations into an infinite Fourier coefficient space. The zero-extension map pads a truncated GalerkinState N with zeros in all higher modes to produce a FourierState2D. The heatFactor is the explicit multiplier Real.exp(−ν ⋅ kSq(k) ⋅ t) that solves the linear heat equation modewise. The Duhamel remainder of Galerkin subtracts the heat-evolved initial datum from the actual trajectory, isolating the effect of the nonlinear convection term. An upstream lemma already records that the zero-extended Galerkin state itself satisfies a forced linear ODE whose forcing is precisely the zero-extended convection operator B(u,u).
proof idea
The tactic proof first calls galerkinNS_hasDerivAt_extendByZero_mode to obtain the derivative of the extended coefficient. It then differentiates the scalar heatFactor via the chain rule on the exponential, producing a multiplier −ν kSq(k). Subtracting the two derivatives yields the derivative of the raw remainder expression. Algebraic rewrites (mul_smul, ring_nf, sub_eq_add_neg) push the heat-term contribution through the subtraction so that it factors as ν(−kSq) times the remainder itself; a final simpa then matches the target forced form.
why it matters
This differential statement is the direct predecessor of duhamelRemainderOfGalerkin_integratingFactor, which integrates the forced ODE under an interval-integrability hypothesis to obtain the variation-of-constants formula. It supplies the analytic bridge inside the ClassicalBridge.Fluids layer that lets later compactness arguments identify a continuum limit object. The step sits at the M5 milestone where all analytic identifications remain explicit hypotheses rather than axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.