aestronglyMeasurable_galerkinForcing_mode_of_continuous
plain-language theorem explainer
Under a uniform bounds hypothesis on Galerkin trajectories together with continuity of each convection operator Bop_N and of the trajectories u_N, the time-dependent forcing coefficient in each Fourier mode is continuous on bounded intervals. Analysts constructing continuum limits from 2D Galerkin approximations invoke the result to secure AE-strong measurability before applying dominated convergence. The argument composes the product continuity of the pair (u_N(s), u_N(s)) with the given continuity of Bop_N, then with the continuous linear map
Claim. Let $H$ be a uniform bounds hypothesis supplying trajectories $u_N : [0,∞) →$ GalerkinState $N$ with $‖u_N(t)‖ ≤ B$ for all $N$ and $t ≥ 0$. Let each $Bop_N$ be continuous as a map from pairs of Galerkin states to the convection term. Assume each $u_N$ is continuous. Then for every $N ∈ ℕ$, $t ≥ 0$, and mode $k$, the map $s ↦$ [extendByZero$(Bop_N(u_N(s), u_N(s)))]_k$ is continuous on $[0,t]$ and therefore AE-strongly measurable with respect to Lebesgue measure restricted to $[0,t]$.
background
Module ContinuumLimit2D develops an explicit Lean pipeline from finite-dimensional 2D Galerkin approximations to an infinite Fourier coefficient state. UniformBoundsHypothesis packages a family of trajectories $uN$ together with a single global bound $B$ that holds uniformly in $N$ and for all $t ≥ 0$. The definition galerkinForcing assembles the nonlinear term $Bop_N(uN N s, uN N s)$ and embeds the result into the full FourierState2D via the zero-extension map extendByZero. The auxiliary definition extendByZeroCLM realizes this embedding as a continuous linear map from the finite-dimensional Galerkin space to the coefficient space.
proof idea
The tactic proof first constructs the continuous path $s ↦ (uN N s, uN N s)$ by applying ContinuousAt.prodMk to the two copies of the assumed continuity of $uN N$. Composition with the given continuity of $Bop N$ yields continuity of the convection term. The target coefficient is recovered by composing the continuous linear map (proj $k$) ∘ extendByZeroCLM with this path. The resulting real-valued function of $s$ is therefore continuous, from which AE-strong measurability on the restricted interval follows immediately.
why it matters
The theorem discharges the measurability requirement for each mode of the Galerkin forcing, which is needed to apply dominated convergence when passing to the continuum limit. It is used directly by of_convectionNormBound_of_continuous to close the bound_integrable and dom fields of GalerkinForcingDominatedConvergenceHypothesis once a uniform norm bound on the convection term is supplied. Within the M5 milestone the result removes one analytic prerequisite for identifying the limit object with a weak solution of the 2D Navier-Stokes system.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.