DuhamelKernelDominatedConvergenceAt
plain-language theorem explainer
DuhamelKernelDominatedConvergenceAt encodes the dominated-convergence hypotheses for the heat-weighted Duhamel integrands at fixed time t and Fourier mode k. Analysts justifying passage from Galerkin approximations to the continuum 2D Navier-Stokes solution cite it to interchange limit and integral. The declaration is a structure that bundles an integrable dominating function, eventual strong measurability, domination, integrability, and pointwise convergence of the integrands.
Claim. Fix viscosity parameter $ν$, sequence of forcing maps $F_N : ℕ → ℝ →$ Fourier coefficient state, limiting forcing $F : ℝ →$ Fourier coefficient state, time $t$, and Fourier mode $k$. The structure asserts an integrable bound function $b : ℝ → ℝ$, eventual strong measurability of the map $s ↦$ (heat factor $ν (t-s) k$) · ($F_N N s k$), domination of these terms by $b(s)$ almost everywhere on $(0,t)$, integrability of $b$ over $[0,t]$, and almost-everywhere pointwise convergence of the sequence to the corresponding limit integrand.
background
The ContinuumLimit2D module packages the analytic steps required to pass from finite Galerkin truncations to an infinite Fourier coefficient state for 2D velocity fields on the torus. Fourier coefficient states are maps from Fourier modes (integer pairs) to velocity coefficients; the heat factor at mode $k$ is the real exponential damping $exp(-ν |k|^2 t)$ that solves the linear Stokes evolution modewise.
proof idea
This is a structure definition that collects the five fields required by the dominated convergence theorem: an $L^1$ bound, eventual AEStronglyMeasurable, the domination inequality almost everywhere, IntervalIntegrable of the bound, and almost-everywhere pointwise convergence of the heat-weighted approximants.
why it matters
It supplies the analytic hypothesis for nsDuhamelCoeffBound_kernelIntegral and the related identification theorems that connect Galerkin solutions to the continuum object. These feed directly into the regularity results in Regularity2D. Within the Recognition framework it contributes to milestone M5 by making the dominated-convergence step for the Duhamel kernel explicit rather than axiomatic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.