duhamelKernelIntegral
plain-language theorem explainer
The definition supplies the integral operator that accumulates a time-dependent Fourier forcing trajectory under the heat kernel for 2D velocity fields. Analysts formalizing continuum limits of Galerkin Navier-Stokes approximations cite it when rewriting remainder terms into kernel form. The definition is a direct pointwise construction that maps each (t, k) to the negative integral from 0 to t of heatFactor(ν, t-s, k) applied to F(s, k).
Claim. The Duhamel kernel integral is the operator sending a forcing trajectory $F : ℝ → FourierState2D$ to the map $(t, k) ↦ -∫_0^t heatFactor(ν, t-s, k) · F(s, k) ds$, where FourierState2D denotes the space of all Fourier coefficients Mode2 → VelCoeff and heatFactor(ν, τ, k) = exp(-ν |k|^2 τ).
background
The ContinuumLimit2D module (Milestone M5) constructs a Lean-checkable pipeline from finite Galerkin approximations to a continuum Fourier object on the 2-torus. FourierState2D is the abbrev Mode2 → VelCoeff giving the full infinite coefficient space; extendByZero embeds truncated Galerkin states by zero outside the truncation window. heatFactor is the modewise multiplier exp(-ν kSq(k) t) solving the linear heat/Stokes equation in Fourier space.
proof idea
This is a direct definition. The body is the lambda that, for each t and mode k, returns the negative interval integral from 0 to t of the scalar heatFactor(ν, t-s, k) multiplied by the forcing value F(s, k).
why it matters
The definition is invoked by duhamelRemainderOfGalerkin_kernel to rewrite the integrating-factor remainder into kernel form and by galerkin_duhamelKernel_identity to obtain the modewise Duhamel identity for Galerkin solutions. It supplies the kernel-integral case of the identification constructors nsDuhamelCoeffBound_kernelIntegral and nsDuhamelCoeffBound_galerkinKernel that close the continuum-limit pipeline. It contributes to the classical-bridge milestone by making the analytic operator explicit so that dominated-convergence hypotheses can be stated separately; the open question it touches is the eventual replacement of those hypotheses by proved bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.