nsDuhamel_of_forall
plain-language theorem explainer
The theorem shows that if Galerkin approximants satisfy a Duhamel remainder identity with modewise-convergent remainders D_N, then the limiting Fourier trajectory satisfies the same identity with remainder D. Researchers formalizing the mild formulation of 2D Navier-Stokes would cite this when justifying passage to the continuum limit. The proof extracts convergent sequences for the extended approximants and remainders, passes the heat-factor multiplication through continuity, and invokes uniqueness of limits after establishing eventual pointw-
Claim. Let $H$ be a uniform bounds hypothesis on Galerkin trajectories $u_N$, let $HC$ be the convergence hypothesis yielding limit trajectory $u$, let $ν ∈ ℝ$, and let $D_N, D$ be remainder maps with $D_N(t,k) → D(t,k)$ for each mode $k$. If each approximant satisfies $extendByZero(u_N(t),k) = (heatFactor ν t k) · extendByZero(u_N(0),k) + D_N(t,k)$ for all $N$, $t ≥ 0$, $k$, then the limit satisfies $u(t,k) = (heatFactor ν t k) · u(0,k) + D(t,k)$ for all $t ≥ 0$, $k$.
background
The ContinuumLimit2D module packages a Lean-checkable pipeline from finite Galerkin approximations of 2D incompressible flow on the torus to an infinite Fourier coefficient trajectory. UniformBoundsHypothesis supplies a family of Galerkin states $uN : ℕ → ℝ → GalerkinState N$ together with a uniform norm bound $B$. ConvergenceHypothesis (depending on $H$) supplies a candidate limit $u : ℝ → FourierState2D$ and the modewise convergence statement that extendByZero($uN(t)$) converges to $u(t)$ at every mode. FourierState2D is the type Mode2 → VelCoeff; extendByZero embeds a truncated Galerkin state by zero outside its truncation window. The target predicate IsNSDuhamelTraj ν D u asserts the mild form $u(t,k) = (heatFactor ν t k) · u(0,k) + D(t,k)$ for all $t ≥ 0$ and modes $k$.
proof idea
Fix $t ≥ 0$ and mode $k$. Extract three convergent sequences: the zero-extended approximants at time $t$ (from HC.converges), at time 0 (again from HC), and the remainders $D_N(t,k)$ (from hD). Pass the continuous scalar multiplication by heatFactor ν t k through the limit at time 0 using continuous_const_smul. Add the resulting limits to obtain convergence of the right-hand side. The hypothesis hId supplies eventual equality of the two sequences, so tendsto_nhds_unique_of_eventuallyEq yields the identity for the limit coefficients. The final simpa unfolds IsNSDuhamelTraj.
why it matters
This identification step is used by nsDuhamelCoeffBound to assemble the full Duhamel-style coefficient bound for the limit trajectory and by nsDuhamel_of_forall_kernelIntegral when remainders are realized as kernel integrals. It is invoked in the regularity results rs_implies_global_regularity_2d_nsDuhamelCoeffBound and rs_implies_global_regularity_2d_stokesODECoeffBound. Within the Recognition Science classical bridge it makes the passage from discrete Galerkin data to continuum mild solutions explicit for 2D fluids, supporting later claims that global regularity follows once the Recognition hypotheses close the compactness gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.