GalerkinForcingDominatedConvergenceHypothesis
plain-language theorem explainer
GalerkinForcingDominatedConvergenceHypothesis packages the dominated-convergence data for the Galerkin forcing family arising from uniform-bounded 2D trajectories. Analysts constructing continuum limits of finite Galerkin truncations for the Navier-Stokes equations cite it to justify passage of the nonlinear term inside Duhamel integrals. The declaration is a structure that directly records the limiting Fourier state F, an integrable dominating bound, strong measurability of each mode on every interval [0,t], pointwise domination, and pointwise
Claim. Let $H$ be a uniform-in-$N$ bound hypothesis on Galerkin trajectories $u_N$ and let $Bop_N$ be a family of convection operators. A structure $G$ is a Galerkin forcing dominated convergence hypothesis when it supplies a limiting forcing $F:ℝ→(Mode2→VelCoeff)$, a dominating bound function $b(t,k,s)$, the integrability of $b(t,k,·)$ on each $[0,t]$, the almost-everywhere strong measurability of each Galerkin forcing mode on $[0,t]$, the inequality $‖galerkinForcing(H,Bop,N,s)(k)‖≤b(t,k,s)$, and the pointwise limit of the Galerkin forcing modes to $F(s)(k)$ as $N→∞$.
background
The ContinuumLimit2D module formalizes the passage from finite-dimensional Galerkin approximations of the 2D Navier-Stokes equations on the torus to a continuum Fourier-state limit. UniformBoundsHypothesis records a family of trajectories $u_N(t)$ together with a uniform bound $B$ such that $‖u_N(t)‖≤B$ for all $N$ and $t≥0$. FourierState2D is the type of all functions from Mode2 to velocity coefficients, obtained by extending truncated Galerkin states by zero. The auxiliary definition galerkinForcing produces the family $N,s↦extendByZero(Bop_N(u_N(s),u_N(s)))$ in full Fourier variables.
proof idea
This declaration is a structure definition. It directly encodes the five analytic fields required by the dominated-convergence hypothesis for the Galerkin forcing: the limiting state $F$, the dominating bound function, its interval integrability, the strong measurability of each mode, the domination inequality, and the pointwise convergence statement. No lemmas or tactics are invoked; the structure simply assembles these conditions so that downstream definitions can instantiate ForcingDominatedConvergenceAt.
why it matters
The structure supplies the concrete hypothesis that forcingDCTAt, nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp, and the global regularity statements in Regularity2D rely upon. It closes one link in the M5 pipeline of ContinuumLimit2D by packaging exactly the measurability, domination, and convergence data needed to pass the nonlinear forcing term to the limit inside the Duhamel formula. In the Recognition Science setting it supports the controlled continuum limit that is a prerequisite for deriving the classical Navier-Stokes equations from the underlying discrete forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.