nsDuhamelCoeffBound_kernelIntegral
plain-language theorem explainer
This definition assembles an IdentificationHypothesis for a candidate limit Fourier trajectory by combining a uniform bound on coefficients with a Duhamel representation whose remainder is expressed as a kernel integral over a forcing term. Researchers formalizing rigorous continuum limits for 2D Navier-Stokes Galerkin schemes would cite it when packaging convergence data into an abstract solution concept. The construction directly inherits the coefficient bound from the convergence hypothesis and applies a kernel-integral Duhamel lemma to the轨
Claim. Let $H$ be a uniform-bounds hypothesis on a family of Galerkin trajectories $u_N$, let $HC$ be a convergence hypothesis to a limit trajectory $u$, let $F_N$ and $F$ be forcing families, and assume that the Duhamel kernel integrals satisfy dominated convergence at every time and mode together with the exact Duhamel identity for each approximant. The definition then produces an identification hypothesis asserting that $u$ satisfies the chosen solution concept for the 2D Navier-Stokes equation via the kernel-integral remainder.
background
The module ContinuumLimit2D develops a Lean-checkable pipeline for passing from finite-dimensional 2D Galerkin approximations to a continuum Fourier limit for fluid equations on the torus. It introduces FourierState2D as the type of functions from modes to velocity coefficients and extendByZero as the canonical zero-extension map from truncated Galerkin states. UniformBoundsHypothesis packages a family of Galerkin trajectories $u_N$ together with a global bound $B$ such that the norm of each approximant remains at most $B$ for all $N$ and all $t$ at least 0. ConvergenceHypothesis augments this with a candidate limit trajectory $u$ and the assumption of pointwise mode-by-mode convergence of the extended coefficients. DuhamelKernelDominatedConvergenceAt encodes the $L^1$ bound and eventual strong measurability conditions that justify interchanging limits and integrals in the Duhamel formula. The upstream theorem coeff_bound_of_uniformBounds shows that the limit coefficients inherit the same uniform bound by closedness of the closed ball.
proof idea
The definition constructs the IdentificationHypothesis record by setting IsSolution to the conjunction of the uniform coefficient bound and the non-standard Duhamel trajectory property with the kernel integral of $F$. The bound clause is discharged by a direct application of coeff_bound_of_uniformBounds to the convergence hypothesis. The trajectory clause is obtained by invoking the lemma nsDuhamel_of_forall_kernelIntegral on the supplied dominated-convergence and identity hypotheses.
why it matters
This definition supplies a concrete constructor for IdentificationHypothesis, one of the terminal objects needed to close the continuum-limit pipeline at milestone M5. It is invoked by the Galerkin-kernel specialization and the forcing-level variant, both of which appear in the used-by graph. Within the Recognition Science framework it contributes to the classical bridge by making explicit the analytic hypotheses that compactness arguments must later discharge, keeping the dependency graph free of axioms or sorries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.