forcingDCTAt
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.
claimGiven 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 in Recognition Science
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.
scope and limits
- Does not prove the uniform bounds or the convergence hypothesis; these remain assumptions.
- Does not address the viscous term or the full Duhamel integral.
- Does not extend to three dimensions or the inviscid case.
- Does not supply explicit rates of convergence.
formal statement (Lean)
1008noncomputable def forcingDCTAt
1009 {H : UniformBoundsHypothesis} {Bop : (N : ℕ) → ConvectionOp N}
1010 (hF : GalerkinForcingDominatedConvergenceHypothesis H Bop)
1011 (t : ℝ) (ht : 0 ≤ t) (k : Mode2) :
1012 ForcingDominatedConvergenceAt (F_N := galerkinForcing H Bop) (F := hF.F) t k :=
proof body
Definition body.
1013 ForcingDominatedConvergenceAt.of_forall (F_N := galerkinForcing H Bop) (F := hF.F) (t := t) (k := k)
1014 (bound := hF.bound t k)
1015 (h_meas := by intro N; exact hF.meas N t ht k)
1016 (h_bound := by intro N s hs; exact hF.dom N t ht k s hs)
1017 (bound_integrable := hF.bound_integrable t ht k)
1018 (h_lim := by intro s hs; exact hF.lim t ht k s hs)
1019
1020/-- If each Galerkin trajectory `uN N` is continuous and each `Bop N` is continuous as a map
1021`(u,v) ↦ Bop N u v`, then each forcing mode `s ↦ (galerkinForcing H Bop N s) k` is continuous (hence
1022AE-strongly measurable on any finite interval). -/