rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel
plain-language theorem explainer
This theorem shows that uniform bounds on Galerkin approximants together with pointwise convergence and dominated convergence on the Duhamel kernel integrands yield a limit Fourier trajectory satisfying the 2D Navier-Stokes equation in Duhamel form driven by the limiting nonlinearity. Researchers closing the continuum limit from finite-mode schemes for incompressible fluids would cite it to obtain the nonlinear remainder identity without separate forcing data. The proof constructs the forcing family from the Galerkin operators, invokes the pre-
Claim. Let $H$ be a uniform bound hypothesis on Galerkin states $u_N$, let $H_c$ be a convergence hypothesis supplying a limit trajectory $u$ with pointwise mode convergence, let $B_N$ be convection operators, and assume the Galerkin right-hand side is differentiable, the kernel integrands are interval-integrable, and the Duhamel kernel satisfies dominated convergence to a limit forcing $F$. Then there exists a trajectory $u$ such that the zero-extended Galerkin coefficients converge to $u(t,k)$ in each mode $k$, the coefficients remain bounded by the uniform radius, and $u$ satisfies the integral equation $u(t) = $ heat evolution of initial data plus the Duhamel kernel integral of $F$.
background
FourierState2D is the space of all mode-indexed velocity coefficients on the torus. extendByZero pads a finite GalerkinState N by zero outside its truncation window. duhamelKernelIntegral ν F is the operator sending (t,k) to the integral from 0 to t of heatFactor ν (t-s) k applied to F(s,k). ConvergenceHypothesis packages a candidate limit u together with the statement that the extended Galerkin coefficients converge pointwise to u(t,k) at every time and mode. DuhamelKernelDominatedConvergenceAt encodes the L1 bound and measurability needed to pass the integral to the limit. The module Regularity2D composes the Galerkin, LNAL, simulation, CPM and continuum-limit packages into an abstract existence statement for 2D continuum solutions without axioms or sorry.
proof idea
The tactic proof begins in classical mode and refines the triple (convergence, bound, Duhamel property) using the limit u supplied by the convergence hypothesis. Pointwise convergence and the coefficient bound are obtained by direct simplification and the lemma coeff_bound_of_uniformBounds. The forcing family F_N is defined by applying the convection operator to the approximants and extending by zero. The Galerkin Duhamel identity is recovered from galerkin_duhamelKernel_identity. The dominated-convergence hypothesis is lifted to F_N and the wrapper nsDuhamel_of_forall_kernelIntegral is applied to conclude that the limit satisfies the required integral equation.
why it matters
The declaration supplies the nonlinear Duhamel remainder for the Galerkin kernel inside the 2D regularity pipeline, removing the need to postulate separate forcing data D_N and D. It is a direct sibling of rs_implies_global_regularity_2d_nsDuhamelCoeffBound and contributes to the top-level composition rs_implies_global_regularity_2d. In the Recognition Science setting it completes one branch of the M5 continuum-limit packaging in ClassicalBridge.Fluids, supporting the claim that global 2D solutions exist once the analytic hypotheses are granted. It leaves open whether the dominated-convergence hypothesis follows from the uniform bounds alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.