forcingDCTAt
plain-language theorem explainer
forcingDCTAt constructs the ForcingDominatedConvergenceAt instance for the Galerkin forcing family at fixed time t and Fourier mode k. Analysts studying the continuum limit of 2D Galerkin approximations to the Navier-Stokes equations would cite this definition to instantiate the dominated convergence hypothesis from the concrete GalerkinForcingDominatedConvergenceHypothesis. It is realized as a one-line wrapper that feeds the hypothesis fields directly into the of_forall constructor of ForcingDominatedConvergenceAt.
Claim. Given a uniform bounds hypothesis $H$ on the family of Galerkin trajectories $u_N$, a family of convection operators $B_N$, and a Galerkin forcing dominated convergence hypothesis $h_F$ supplying the limiting forcing $F$, an integrable dominating function, and pointwise convergence, then for $t ≥ 0$ and mode $k$ the family $F_N(s) := extendByZero(B_N(u_N(s), u_N(s)))$ satisfies the dominated convergence property at $(t, k)$.
background
Module ContinuumLimit2D develops a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to a continuum Fourier state. UniformBoundsHypothesis packages a family of trajectories $u_N : ℕ → ℝ → GalerkinState N$ together with a uniform norm bound $B$. GalerkinForcingDominatedConvergenceHypothesis supplies the limiting forcing $F$, a dominating integrable bound, measurability, and pointwise limits for the Galerkin forcing modes. ForcingDominatedConvergenceAt is the structure recording the dominated convergence data at fixed $t$ and mode $k$ for a forcing family $F_N$. The upstream definition galerkinForcing builds the concrete forcing as $F_N(N,s) = extendByZero(B_N(u_N(N,s), u_N(N,s)))$.
proof idea
This definition is a one-line wrapper that applies the constructor ForcingDominatedConvergenceAt.of_forall to the Galerkin forcing family, passing the dominating bound, measurability, domination, integrability, and limit statements directly from the supplied GalerkinForcingDominatedConvergenceHypothesis.
why it matters
This definition supplies the concrete instance of ForcingDominatedConvergenceAt needed by the downstream results nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp and rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp. It closes one link in the M5 pipeline that converts Galerkin hypotheses into the Duhamel coefficient bounds required for global regularity statements in 2D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.