galerkinForcing
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove convergence of the Galerkin approximations to a continuum solution.
- Does not impose continuity or measurability assumptions on the convection operators.
- Does not supply any integrable domination or pointwise convergence statements.
- Does not depend on the viscosity parameter or the specific form of the Navier-Stokes nonlinearity.
Lean usage
forcingDCTAt hF t ht kformal statement (Lean)
971noncomputable def galerkinForcing (H : UniformBoundsHypothesis) (Bop : (N : ℕ) → ConvectionOp N) :
972 ℕ → ℝ → FourierState2D :=
proof body
Definition body.
973 fun N s => extendByZero ((Bop N) (H.uN N s) (H.uN N s))
974
975/-- A more concrete, user-facing hypothesis for dominated convergence of the *Galerkin forcing*
976`galerkinForcing H Bop`, expressed directly in terms of:
977
978- measurability of the forcing modes,
979- an integrable dominating function on each time interval `[0,t]`, and
980- pointwise convergence of forcing modes.
981
982This packages exactly what you need to build `ForcingDominatedConvergenceAt` for the Galerkin forcing. -/
used by (7)
-
aestronglyMeasurable_galerkinForcing_mode_of_continuous -
forcingDCTAt -
GalerkinForcingDominatedConvergenceHypothesis -
nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp -
of_convectionNormBound -
of_convectionNormBound_of_continuous -
rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp