duhamelRemainderOfGalerkin_kernel
plain-language theorem explainer
The theorem rewrites the integrating-factor form of the Galerkin Duhamel remainder into the standard heat-kernel integral. Analysts constructing continuum limits of 2D Navier-Stokes Galerkin approximations cite it to reach the Fourier Duhamel representation. The argument is an algebraic cancellation that multiplies by heatFactor at time t, cancels the integrating factor via its definition, and combines exponentials inside the integral.
Claim. $R(t,k) = -∫_0^t heatFactor(ν, t-s, k) · (extendByZero(B(u(s), u(s))))(k) ds$, where $R(t,k)$ is the Duhamel remainder $û(t,k) - heatFactor(ν,t,k) · û(0,k)$ for a trajectory $u$ satisfying the projected Navier-Stokes ODE with interval-integrable convection term.
background
The ContinuumLimit2D module builds a Lean pipeline from finite Galerkin projections of 2D Navier-Stokes to full Fourier coefficient states. extendByZero pads a GalerkinState N with zeros to produce a FourierState2D; heatFactor ν t k is defined as exp(-ν |k|^2 t), the modewise multiplier for the linear Stokes operator. The Duhamel remainder is defined as extendByZero(u t) k minus heatFactor ν t k times extendByZero(u 0) k.
proof idea
Invoke duhamelRemainderOfGalerkin_integratingFactor to obtain the integrating-factor identity. Multiply both sides by heatFactor ν t k. Cancel the product heatFactor(t) * exp(ν |k|^2 t) to 1 by direct computation with exp_add and ring_nf. Move the outer scalar inside the integral and rewrite the combined exponential as heatFactor ν (t-s) k via another exp_add and ring simplification.
why it matters
This identity is the immediate predecessor of galerkin_duhamelKernel_identity, which assembles the full Duhamel formula û(t,k) = heatFactor ν t k · û(0,k) + duhamelKernelIntegral ν (extendByZero ∘ B(u,u)) (t,k). It closes an algebraic step inside the M5 milestone of the ClassicalBridge.Fluids module, where all compactness and identification steps remain explicit hypotheses. The result prepares the ground for the dominated-convergence theorem that passes N to infinity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.