of_convectionNormBound
plain-language theorem explainer
A uniform bound on Galerkin trajectories together with a quadratic norm bound on the convection operator produces an integrable dominating function for every forcing mode. Researchers constructing the 2D continuum limit from finite Galerkin systems cite this to close the domination requirement inside dominated-convergence arguments. The definition assembles the hypothesis record by setting the bound to the constant C B squared and verifies integrability by constancy on finite intervals.
Claim. Let $H$ be a uniform-bounds hypothesis with global bound $B$, let $Bop$ be a family of convection operators satisfying $‖Bop_N(u,u)‖ ≤ C ‖u‖² for $C ≥ 0$, and let $F : ℝ → FourierState2D$. Suppose the Galerkin forcing modes are strongly measurable on each interval $[0,t]$ and converge pointwise to $F(s)$. Then the structure GalerkinForcingDominatedConvergenceHypothesis $H$ $Bop$ holds with dominating bound equal to the constant $C B²$.
background
The ContinuumLimit2D module packages the analytic steps needed to pass from finite-dimensional 2D Galerkin approximations of incompressible flow to a continuum Fourier coefficient state. FourierState2D is the type Mode2 → VelCoeff representing the full infinite-dimensional velocity field on the torus. The Galerkin forcing is defined by galerkinForcing H Bop := extendByZero ∘ (Bop N (H.uN N s) (H.uN N s)).
proof idea
The definition uses classical refinement to build the hypothesis record. It supplies the supplied limiting field F, sets the dominating bound to the constant function C · H.B², and obtains bound_integrable by simplification because a constant is interval-integrable on any finite interval. The dom field is discharged by applying the uniform trajectory bound to obtain ‖uN N s‖ ≤ B, squaring the inequality, invoking the assumed convection bound hB, and finally applying norm_extendByZero_le to transfer the norm control to each Fourier coefficient.
why it matters
This supplies a concrete, checkable route to the dominated-convergence hypothesis for the Galerkin forcing inside the 2D continuum-limit pipeline. It is invoked directly by the downstream definition of_convectionNormBound_of_continuous, which further discharges measurability once continuity of Bop is assumed. In the Recognition Science monolith the construction closes one explicit analytic-compactness requirement of milestone M5, keeping the dependency graph free of axioms or hidden hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.