stokesMild_of_forall
The theorem shows that the mild Stokes/heat identity passes to the modewise limit trajectory whenever every Galerkin approximant satisfies the same identity. Researchers constructing rigorous continuum limits for 2D viscous flows would cite it when identifying the limit object. The argument extracts modewise convergence at fixed t and k, transports the initial data through continuous scalar multiplication by the heat factor, and concludes equality by uniqueness of limits once the sequences agree for all N.
claimLet $H$ be a uniform bounds hypothesis supplying a family of Galerkin trajectories $u_N$ and let $HC$ be the associated convergence hypothesis with candidate limit trajectory $u$. For viscosity parameter $ν$, suppose that for every truncation level $N$, every $t≥0$ and every mode $k$ the zero-extended coefficient satisfies $extendByZero(u_N(N,t),k)=(heatFactor ν t k)·extendByZero(u_N(N,0),k)$. Then the limit trajectory satisfies the mild Stokes equation: for all $t≥0$ and modes $k$, $u(t,k)=(heatFactor ν t k)·u(0,k)$.
background
The ContinuumLimit2D module (milestone M5) packages the passage from finite-dimensional Galerkin approximations to a continuum Fourier trajectory as an explicit pipeline of hypotheses. A UniformBoundsHypothesis consists of a family of Galerkin trajectories $uN$ together with a uniform bound $B$ such that $‖uN N t‖≤B$ for all $N$ and $t≥0$. The ConvergenceHypothesis built on top of it supplies a limit map $u:ℝ→FourierState2D$ and asserts modewise convergence of the zero-extended Galerkin coefficients to the corresponding coefficients of $u$.
proof idea
The proof fixes arbitrary $t≥0$ and mode $k$. It obtains convergence of the extended coefficients at time $t$ and at time $0$ directly from the convergence hypothesis. Continuity of scalar multiplication by the constant heatFactor $ν t k$ transports the time-zero convergence to a convergence statement for the multiplied sequence. The mild hypothesis on the approximants yields that the two sequences agree for every $N$, hence are eventually equal. Uniqueness of limits in a Hausdorff space then forces the desired equality for the limit trajectory.
why it matters in Recognition Science
The result supplies the mild Stokes identity inside the identification constructor stokesMildCoeffBound, which is invoked by the regularity theorems rs_implies_global_regularity_2d_stokesMildCoeffBound and rs_implies_global_regularity_2d_stokesODECoeffBound in Regularity2D. It therefore closes one explicit step of the M5 pipeline that replaces Galerkin approximants by a continuum object while keeping every identification hypothesis visible. Within the Recognition Science framework it contributes to the classical bridge by showing how linear evolution identities survive the continuum limit under the stated modewise convergence.
scope and limits
- Does not establish the uniform bounds hypothesis or the convergence of the Galerkin family.
- Does not address the nonlinear convective term of the Navier-Stokes equations.
- Does not supply an explicit rate of convergence for the approximants.
- Does not prove existence of the limit trajectory beyond the convergence hypothesis.
formal statement (Lean)
1209theorem stokesMild_of_forall {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1210 (hMild :
1211 ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1212 (extendByZero (H.uN N t) k) = (heatFactor ν t k) • (extendByZero (H.uN N 0) k)) :
1213 IsStokesMildTraj ν HC.u := by
proof body
Tactic-mode proof.
1214 intro t ht k
1215 -- convergence at time t and at time 0
1216 have hconv_t : Tendsto (fun N : ℕ => extendByZero (H.uN N t) k) atTop (nhds ((HC.u t) k)) :=
1217 HC.converges t k
1218 have hconv_0 : Tendsto (fun N : ℕ => extendByZero (H.uN N 0) k) atTop (nhds ((HC.u 0) k)) :=
1219 HC.converges 0 k
1220 -- push convergence at time 0 through the continuous map `v ↦ heatFactor • v`
1221 have hsmul :
1222 Tendsto (fun N : ℕ => (heatFactor ν t k) • (extendByZero (H.uN N 0) k)) atTop
1223 (nhds ((heatFactor ν t k) • ((HC.u 0) k))) := by
1224 have hcont : Continuous fun v : VelCoeff => (heatFactor ν t k) • v := continuous_const_smul _
1225 exact (hcont.tendsto ((HC.u 0) k)).comp hconv_0
1226 -- but the two sequences are equal for all N (by hypothesis), hence have the same limit
1227 have hEq :
1228 (fun N : ℕ => extendByZero (H.uN N t) k)
1229 =ᶠ[atTop] (fun N : ℕ => (heatFactor ν t k) • (extendByZero (H.uN N 0) k)) := by
1230 refine Filter.Eventually.of_forall ?_
1231 intro N
1232 exact hMild N t ht k
1233 -- uniqueness of limits in a T2 space
1234 have : (HC.u t) k = (heatFactor ν t k) • ((HC.u 0) k) :=
1235 tendsto_nhds_unique_of_eventuallyEq hconv_t hsmul hEq
1236 simpa using this
1237
1238/-- Duhamel-remainder identity passes to the limit under modewise convergence,
1239assuming it holds for every approximant with remainders `D_N` that converge modewise. -/