nsDuhamelCoeffBound_galerkinKernel
plain-language theorem explainer
This definition constructs the identification hypothesis for the 2D Navier-Stokes continuum limit by specializing the Duhamel kernel bound to the actual Galerkin nonlinearity. Analysts working on rigorous passage from finite-mode truncations to weak solutions cite it as the bridge between Galerkin data and the limit trajectory. The construction defines the forcing family from the convection term, discharges the approximant Duhamel identity via the Galerkin kernel lemma, and reduces directly to the kernel-integral constructor under the supplied
Claim. Given uniform bounds hypothesis $H$ on Galerkin trajectories $u_N$, convergence hypothesis $HC$ for a candidate limit trajectory $u$, viscosity parameter $ν$, family of convection operators $B_N$, derivative condition that each $u_N$ satisfies the Galerkin right-hand side, interval integrability of the extended forcing, candidate limit state $F$, and dominated-convergence hypothesis at the forcing level, the definition yields the identification hypothesis for $HC$.
background
The module ContinuumLimit2D packages the analytic steps needed to pass from a family of finite-dimensional 2D Galerkin approximations to a continuum Fourier-state limit. UniformBoundsHypothesis supplies a family of trajectories $u_N : ℕ → ℝ → GalerkinState N$ together with a uniform norm bound $B$ independent of $N$ and $t ≥ 0$. ConvergenceHypothesis augments this with a candidate limit $u : ℝ → FourierState2D$ and the pointwise mode-by-mode convergence statement that the zero-extended coefficients of $u_N(t)$ converge to those of $u(t)$. FourierState2D is the type of all (infinite) Fourier coefficient maps Mode2 → VelCoeff; extendByZero embeds a truncated GalerkinState into this space by padding with zeros outside the retained modes.
proof idea
The definition first introduces the auxiliary forcing family $F_N(N,s) := extendByZero((Bop N)(u_N(s),u_N(s)))$. It then obtains the approximant Duhamel identity $hId'$ by applying galerkin_duhamelKernel_identity to each fixed $N$, $t ≥ 0$ and mode $k$, using the supplied derivative condition $hu$ and integrability hint. The final step refines to nsDuhamelCoeffBound_kernelIntegral, passing the dominated-convergence datum $hDC$ (re-expressed on $F_N$) as the remaining hypothesis.
why it matters
This supplies the concrete identification constructor required by the M5 milestone pipeline in ContinuumLimit2D. It specialises the general Duhamel-coefficient bound to the Galerkin nonlinearity, thereby closing the loop from the finite-dimensional energy estimates to the continuum Duhamel representation. The construction relies on the upstream galerkin_duhamelKernel_identity and duhamelKernelIntegral; because the used-by graph is currently empty it remains an explicit interface awaiting later replacement of the surrounding hypotheses by theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.