duhamelKernelDominatedConvergenceAt_of_forcing
plain-language theorem explainer
Definition that lifts a dominated-convergence hypothesis stated directly on the forcing terms to the corresponding hypothesis on the Duhamel-kernel integrands. Analysts formalizing Galerkin-to-continuum passages for 2D incompressible flow would invoke it when the heat kernel must be inserted into the integral estimates. The construction is a structure refinement that re-uses the forcing bound and measurability data while inserting the factor |heatFactor| ≤ 1 and composing the pointwise limit with scalar multiplication.
Claim. Let $0 ≤ ν$ and $0 ≤ t$. Suppose the sequence of forcings $F_N$ converges to the limit forcing $F$ in the dominated sense at fixed time $t$ and mode $k$. Then the family of integrands $s ↦ heatFactor(ν, t-s, k) · F_N(s, k)$ satisfies the dominated-convergence hypotheses on the interval $[0,t]$ (same bound, eventual strong measurability, and eventual domination).
background
The module ContinuumLimit2D supplies a Lean-checkable pipeline shape that carries finite-dimensional 2D Galerkin approximations to an infinite Fourier coefficient state on the torus. FourierState2D is the type Mode2 → VelCoeff that represents the full (untruncated) velocity field in Fourier space. ForcingDominatedConvergenceAt packages the minimal data needed for dominated convergence of the raw forcing: an L¹ bound function, eventual strong measurability of the coefficient maps on the restricted interval, and eventual domination by that bound. DuhamelKernelDominatedConvergenceAt is the analogous structure whose integrand now includes the explicit heat-factor multiplier heatFactor ν (t-s) k.
proof idea
The definition builds the target structure by copying bound and bound_integrable from the input hypothesis. Measurability is obtained by showing that multiplication by the continuous scalar heatFactor preserves eventual strong measurability. Domination follows from the lemma abs_heatFactor_le_one, which supplies |heatFactor ν τ k| ≤ 1 for τ ≥ 0, so the product norm is bounded by the original forcing bound. Pointwise convergence is recovered by composing the forcing limit with the continuous map of scalar multiplication by the fixed heat factor.
why it matters
The definition supplies the missing link that lets the user-facing forcing convergence hypothesis feed the kernel-level dominated-convergence data required by the theorem nsDuhamel_of_forall_kernelIntegral_of_forcing. It therefore closes one analytic compactness step inside the M5 milestone pipeline that identifies continuum limits of 2D Galerkin sequences. In the broader Recognition Science setting it keeps the classical-bridge hypotheses explicit rather than axiomatic, supporting later replacement by concrete estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.