galerkinForcing
plain-language theorem explainer
The definition constructs the nonlinear forcing family for Galerkin truncations by applying the convection operator Bop N to the pair of bounded trajectories from UniformBoundsHypothesis and embedding the result into full Fourier space via zero extension. Researchers formalizing the continuum limit of 2D Navier-Stokes Galerkin approximations cite this when packaging the forcing term for dominated-convergence arguments. It is realized as a direct functional composition with no additional lemmas.
Claim. Let $H$ be a UniformBoundsHypothesis supplying Galerkin trajectories $u_N$ with uniform bound $B$. For convection operators $B_N$, the Galerkin forcing is the map $(N,s)mapsto$ extendByZero$(B_N(u_N(N,s),u_N(N,s)))$ with values in FourierState2D $:=$ Mode2 $to$ VelCoeff.
background
The ContinuumLimit2D module defines objects and explicit hypotheses for passing from finite Galerkin approximations of 2D fluids on the torus to a continuum Fourier limit object. FourierState2D is the type of all coefficient maps indexed by Mode2. UniformBoundsHypothesis is the structure containing the family of truncated trajectories uN together with a single real bound B such that the norm of uN(N,t) is at most B for every truncation level N and every time t.
proof idea
One-line wrapper that applies extendByZero to the output of the bilinear convection operator Bop N evaluated on the pair of velocity fields drawn from H.uN at time s.
why it matters
This definition supplies the concrete forcing family F_N used to build ForcingDominatedConvergenceAt and GalerkinForcingDominatedConvergenceHypothesis. It is invoked by aestronglyMeasurable_galerkinForcing_mode_of_continuous, of_convectionNormBound, and nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp, which in turn support the regularity pipeline in Regularity2D. It fills the M5 milestone by making the nonlinear term explicit inside the hypothesis-driven continuum-limit graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.