DuhamelKernelDominatedConvergenceAt
plain-language theorem explainer
DuhamelKernelDominatedConvergenceAt packages the five fields required to apply dominated convergence to the heat-weighted Duhamel integrands at fixed t and mode k. Analysts justifying passage of the N to infinity limit inside the mild-form integral for 2D Galerkin Navier-Stokes approximations would cite it. The declaration is a structure definition that collects an L1 bound, eventual strong measurability, domination, integrability of the bound, and pointwise convergence of the integrands.
Claim. Let $ν ∈ ℝ$, $F_N : ℕ → ℝ →$ (Mode2 → VelCoeff), $F : ℝ →$ (Mode2 → VelCoeff), $t ∈ ℝ$, $k ∈$ Mode2. The structure asserts a function bound : ℝ → ℝ together with eventual (in N) strong measurability of $s ↦$ (heatFactor $ν$ ($t-s$) $k$) · ($F_N N s k$) on [0,t], eventual domination by bound, integrability of bound over [0,t], and eventual pointwise convergence almost everywhere on [0,t] of the integrands to the corresponding limit integrand.
background
FourierState2D is the full infinite Fourier coefficient state Mode2 → VelCoeff for a 2D velocity field on the torus. heatFactor ν t k is the scalar multiplier exp(−ν |k|² t) that appears in the mild solution of the linear Stokes operator. The module ContinuumLimit2D supplies a Lean-checkable pipeline shape that embeds truncated Galerkin states into the full Fourier state via zero extension and packages the required analytic compactness and identification steps as explicit hypotheses rather than axioms.
proof idea
Definition that assembles the five fields: an L¹ bound function, eventual AEStronglyMeasurable on the restricted interval, eventual almost-everywhere domination by that bound, IntervalIntegrable of the bound on [0,t], and eventual pointwise Tendsto at infinity of the heat-weighted terms to the limit integrand.
why it matters
It is the hypothesis interface used by nsDuhamelCoeffBound_kernelIntegral, nsDuhamel_of_forall_kernelIntegral, and the Galerkin-specialized variant nsDuhamelCoeffBound_galerkinKernel to justify interchange of limit and integral in the Duhamel remainder term. The structure therefore supplies one of the explicit analytic hypotheses required by the M5 milestone for passing from finite-dimensional Galerkin approximations to a continuum limit object in 2D fluids.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.