nsDuhamel_of_forall_kernelIntegral
plain-language theorem explainer
The theorem shows that if Galerkin trajectories satisfy uniform bounds and converge pointwise to a limit trajectory u, and if their Duhamel remainders are realized as kernel integrals of forcing families F_N that converge to the integral of a limit forcing F under a dominated-convergence assumption, then u obeys the mild Duhamel form with the integrated forcing. Analysts working on continuum limits of 2D Navier-Stokes Galerkin schemes cite this when passing to the limit inside mild formulations. The proof first obtains pointwise convergence of
Claim. Let $H$ be a uniform-bounds hypothesis on Galerkin trajectories $u_N$, let $HC$ be a convergence hypothesis to a limit trajectory $u$, let $ν ∈ ℝ$, and let $F_N : ℕ → ℝ →$ Fourier states and $F$ be forcing trajectories. Assume that for every $t ≥ 0$ and mode $k$ the Duhamel-kernel integrands of $F_N$ satisfy dominated convergence to those of $F$, and that each zero-extended Galerkin coefficient at time $t$ equals the heat-evolved initial datum plus the kernel integral of $F_N(N)$. Then $u$ satisfies $u(t,k) = $ heat factor$(ν,t,k) · u(0,k) + $ (kernel integral of $F$)$(t,k)$ for all $t ≥ 0$ and modes $k$.
background
The ContinuumLimit2D module supplies a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to a continuum Fourier limit on the torus. A UniformBoundsHypothesis packages a family of Galerkin trajectories $u_N$ together with a uniform norm bound $B$ that holds for all $N$ and all $t ≥ 0$. The ConvergenceHypothesis, built on top of such bounds, supplies a candidate limit trajectory $u : ℝ →$ FourierState2D (the space of all mode-to-velocity-coefficient maps) and asserts pointwise convergence of the zero-extended Galerkin coefficients to those of $u$. The Duhamel kernel integral of a forcing trajectory $F$ is the map $(t,k) ↦ -∫_0^t$ heatFactor$(ν,t-s,k) · F(s,k) ds$. The predicate IsNSDuhamelTraj$(ν,D,u)$ asserts that $u(t,k)$ equals heatFactor$(ν,t,k) · u(0,k) + D(t,k)$ for every $t ≥ 0$ and mode $k$.
proof idea
The proof first builds the required pointwise convergence of the Duhamel remainders by applying the lemma tendsto_duhamelKernelIntegral_of_dominated_convergence at each fixed $t$ and $k$, using the supplied dominated-convergence data. It then invokes the general identification theorem nsDuhamel_of_forall on the families of kernel integrals, passing the newly obtained convergence statement together with the given identity hypothesis.
why it matters
This wrapper belongs to milestone M5 of the continuum-limit pipeline for 2D fluids. It is used directly by the constructor nsDuhamelCoeffBound_kernelIntegral and thereby by the global-regularity theorem rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel in Regularity2D. Within the Recognition Science framework it supplies one concrete step that replaces an analytic hypothesis with an explicit identification, advancing the program of obtaining global regularity for the 2D Navier-Stokes equations in mild form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.