pith. machine review for the scientific record. sign in
def definition def or abbrev high

duhamelKernelIntegral

show as:
view Lean formalization →

The declaration defines the Duhamel kernel integral operator that maps a time-dependent forcing trajectory in Fourier space to its integrated effect under the linear heat kernel. Analysts constructing continuum limits from 2D Galerkin approximations for Navier-Stokes would cite this when rewriting mild solutions. The definition is assembled directly as a modewise integral of heatFactor times the forcing value.

claimThe Duhamel kernel integral applied to a forcing trajectory $F : ℝ →$ (Fourier coefficient state) is the operator whose value at time $t$ and mode $k$ equals $-∫_0^t$ heatFactor$(ν, t-s, k) · F(s, k) ds$, where heatFactor$(ν, τ, k) = exp(-ν |k|^2 τ)$.

background

The ContinuumLimit2D module builds a Lean-checkable pipeline from finite-dimensional Galerkin states to an infinite Fourier coefficient state on the torus. FourierState2D is the type of all functions from modes to velocity coefficients, obtained by extending truncated states by zero outside the truncation window. heatFactor is the explicit multiplier exp(-ν kSq(k) t) that solves the linear Stokes/heat equation mode by mode.

proof idea

The definition is a direct one-line construction: for each t and k it returns the negative integral from 0 to t of heatFactor(ν, t-s, k) scaled by the forcing component F(s, k). No lemmas or tactics are applied; the body simply assembles the integral expression using the already-defined heatFactor.

why it matters in Recognition Science

This operator supplies the kernel form of the Duhamel remainder that appears in duhamelRemainderOfGalerkin_kernel and galerkin_duhamelKernel_identity, and it is the central ingredient in the identification constructors nsDuhamelCoeffBound_kernelIntegral and nsDuhamelCoeffBound_galerkinKernel. It completes the algebraic step from integrating-factor remainders to standard convolution form inside the M5 continuum-limit pipeline. The construction leaves open the replacement of the packaged dominated-convergence hypotheses by explicit bounds.

scope and limits

formal statement (Lean)

 655noncomputable def duhamelKernelIntegral (ν : ℝ) (F : ℝ → FourierState2D) : ℝ → FourierState2D :=

proof body

Definition body.

 656  fun t k => -∫ s in (0 : ℝ)..t, (heatFactor ν (t - s) k) • (F s k)
 657
 658/-- Hypothesis (at fixed `t,k`): the Duhamel-kernel integrands satisfy the assumptions of dominated
 659convergence, so the corresponding interval integrals converge. -/

used by (12)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (14)

Lean names referenced from this declaration's body.