nsDuhamel_of_forall_kernelIntegral_of_forcing
plain-language theorem explainer
The theorem shows that if Galerkin approximants satisfy the Duhamel identity with forcing terms and the forcing sequences obey a dominated-convergence condition at each time and mode, then the continuum limit trajectory satisfies the corresponding integral equation driven by the limiting forcing. Researchers formalizing 2D Navier-Stokes regularity or discrete-to-continuum passages would cite this identification step. The proof obtains pointwise convergence of the approximants, applies dominated convergence to the kernel integrals via an of_forc
Claim. Let $H$ be a uniform-bounds hypothesis on Galerkin trajectories $u_N$, let $HC$ be the convergence hypothesis to a limit trajectory $u$, let $ν≥0$, and let $F_N,F$ be forcing fields such that for every $t≥0$ and mode $k$ the sequence $F_N(·,k)$ satisfies dominated convergence to $F(·,k)$. Assume that for all $N,t≥0,k$ the zero-extended coefficients obey $ũ_N(t,k)=(heatFactor ν t k)·ũ_N(0,k)+(duhamelKernelIntegral ν(F_N N)t)k$. Then $u$ satisfies the analogous Duhamel identity with the integral of $F$.
background
The ContinuumLimit2D module constructs an explicit pipeline from finite-dimensional 2D Galerkin approximations to a continuum Fourier-state limit for the Navier-Stokes equation. UniformBoundsHypothesis packages a family of Galerkin states uN together with a uniform norm bound B that is independent of truncation level N. ConvergenceHypothesis supplies a candidate limit trajectory u:ℝ→FourierState2D together with the pointwise statement that the zero-extended Galerkin coefficients converge in N to those of u. FourierState2D is the space of all maps from Mode2 to VelCoeff; extendByZero embeds a truncated GalerkinState N into this space by zero outside the retained modes. ForcingDominatedConvergenceAt encodes the dominated-convergence hypothesis directly on the forcing terms (without the heat kernel factor), which is sufficient under ν≥0 and t≥0 because |heatFactor ν(t-s)k|≤1 on the integration interval.
proof idea
Fix t≥0 and mode k. Obtain hconv_t and hconv_0 from the convergence hypothesis. For the kernel-integral remainder, invoke duhamelKernelDominatedConvergenceAt_of_forcing to upgrade the forcing-level hypothesis to DuhamelKernelDominatedConvergenceAt, then apply tendsto_duhamelKernelIntegral_of_dominated_convergence to obtain hconv_D. Use continuity of scalar multiplication by the constant heatFactor ν t k to pass hconv_0 to the heat term (hsmul). Add the two convergent sequences to obtain hsum. The given identity hId supplies eventual equality between the approximant sequence and the sum sequence. Uniqueness of limits in a Hausdorff space then yields the Duhamel identity for u; the final simpa matches the IsNSDuhamelTraj predicate.
why it matters
This identification step feeds directly into nsDuhamelCoeffBound_kernelIntegral_of_forcing (which extracts coefficient bounds) and rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcing (the 2D regularity pipeline). It occupies the classical-bridge layer of the Recognition Science framework at milestone M5, where the passage from discrete Galerkin systems to the continuum Navier-Stokes Duhamel trajectory is kept as an explicit hypothesis so that later compactness arguments can discharge it. The result touches the open question of replacing ConvergenceHypothesis by a compactness theorem derived from the uniform bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.