forcingDCTAt
plain-language theorem explainer
forcingDCTAt assembles a ForcingDominatedConvergenceAt record for the Galerkin forcing family from the concrete hypothesis structure that encodes measurability, integrable bounds, and pointwise limits of the forcing modes. Analysts studying the continuum limit of 2D Galerkin approximations to Navier-Stokes would invoke this to satisfy the dominated-convergence step in Duhamel estimates. The definition is a direct wrapper that feeds the hypothesis fields into the of_forall constructor of ForcingDominatedConvergenceAt.
Claim. Given a uniform bounds hypothesis $H$ on the family of Galerkin trajectories $u_N$ and a family of convection operators $B_N$, together with the hypothesis $hF$ that the associated forcing $F_N(N,s) = extendByZero(B_N(u_N(N,s),u_N(N,s)))$ satisfies the dominated convergence conditions with limit $F$, then for each $t ≥ 0$ and Fourier mode $k$ the pair $(F_N,F)$ satisfies the ForcingDominatedConvergenceAt property at time $t$ for mode $k$.
background
UniformBoundsHypothesis packages a family of Galerkin trajectories $uN : ℕ → ℝ → GalerkinState N$ together with a uniform bound $B$ such that ‖uN N t‖ ≤ B for all N and t ≥ 0. GalerkinForcingDominatedConvergenceHypothesis supplies the limiting forcing F : ℝ → FourierState2D, an integrable dominating function bound, and the required measurability and pointwise convergence statements for the Galerkin forcing modes. ForcingDominatedConvergenceAt is the structure that records an integrable bound, almost-everywhere strong measurability of the approximating forcing modes, and pointwise convergence to the limit forcing, all at fixed time t and mode k.
proof idea
The definition is a one-line wrapper that applies the constructor ForcingDominatedConvergenceAt.of_forall, passing the bound, measurability, domination, integrability, and limit statements directly from the fields of the input hypothesis hF.
why it matters
This definition supplies the concrete bridge from GalerkinForcingDominatedConvergenceHypothesis to ForcingDominatedConvergenceAt, which is consumed by nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp to obtain coefficient bounds and ultimately by the global regularity theorem rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp. It fills the analytic identification step in the M5 continuum-limit pipeline for 2D fluids, keeping the dependency graph explicit so that later milestones can replace the hypothesis with a proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.