galerkinForcing
plain-language theorem explainer
galerkinForcing supplies the nonlinear convection term for each Galerkin truncation by feeding the bounded trajectory pair into the convection operator and zero-extending the output into the full Fourier coefficient space. Researchers constructing dominated-convergence arguments for the 2D Navier-Stokes continuum limit would cite this when building ForcingDominatedConvergenceAt from concrete Galerkin data. The definition is a direct one-line composition of extendByZero with the supplied convection operator and uniform-bounds trajectory family.
Claim. Let $H$ be a uniform bounds hypothesis supplying a family of Galerkin trajectories $u_N$. For a family of convection operators $B_N$, the Galerkin forcing is the map $(N,s)mapstowidetilde{B_N(u_N(s),u_N(s))}$, where the tilde denotes zero-extension of the truncated state to the full Fourier coefficient state on the torus.
background
UniformBoundsHypothesis is a structure that packages a family of Galerkin trajectories $uN : (N:ℕ)→ℝ→GalerkinState N$ together with a uniform bound $B$ such that $‖uN N t‖≤B$ for all $N$ and $t≥0$. FourierState2D is the type of maps from Mode2 to velocity coefficients, representing the complete infinite Fourier expansion of a 2D velocity field on the torus. The module ContinuumLimit2D defines a Lean-checkable pipeline shape for passing from finite-dimensional 2D Galerkin approximations to a continuum limit object, keeping analytic compactness steps as explicit hypotheses rather than axioms.
proof idea
This is a one-line wrapper that applies extendByZero to the result of the convection operator Bop N acting on the pair (H.uN N s, H.uN N s).
why it matters
This definition supplies the concrete forcing family needed to instantiate ForcingDominatedConvergenceAt and GalerkinForcingDominatedConvergenceHypothesis inside the continuum-limit pipeline. It feeds downstream constructions such as forcingDCTAt, aestronglyMeasurable_galerkinForcing_mode_of_continuous, and nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp, which support regularity statements for the 2D Navier-Stokes equations. Within the Recognition Science framework it forms part of milestone M5 in the classical bridge, connecting finite-mode approximations to the continuum objects required for later steps in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.