IsStokesODETraj
plain-language theorem explainer
IsStokesODETraj defines the modewise differential form of the linear Stokes equation on Fourier coefficients for 2D velocity fields on the torus. Analysts working on continuum limits of Galerkin schemes or regularity questions for Navier-Stokes cite this predicate when moving from mild to strong formulations. The definition directly encodes the required derivative condition via HasDerivWithinAt on each coefficient trajectory restricted to t ≥ 0.
Claim. Let ν ∈ ℝ be viscosity and let u : ℝ → (ℤ × ℤ → VelCoeff) be a trajectory of Fourier states. The predicate holds precisely when, for every t ≥ 0 and every mode k ∈ ℤ × ℤ, the map s ↦ u(s)(k) admits derivative −(ν |k|²) u(t)(k) at s = t, where the derivative is taken within the half-line [0, ∞).
background
The module ContinuumLimit2D supplies a Lean-checkable pipeline shape for extracting continuum objects from finite 2D Galerkin truncations. FourierState2D is the type of all sequences of velocity coefficients indexed by Mode2 = ℤ × ℤ; kSq returns the squared wavenumber |k|² that appears in the Fourier Laplacian. The local setting keeps all compactness and identification steps as explicit hypotheses so that later milestones can replace them with proofs.
proof idea
As a definition the body is the predicate itself: universal quantification over t ≥ 0 and k : Mode2 of the HasDerivWithinAt statement for the coefficient map, with the expected linear right-hand side built from ν and kSq. No lemmas or tactics are invoked.
why it matters
The predicate is applied by the theorem stokesODE, which converts the mild trajectory assumption into the differential form, and by rs_implies_global_regularity_2d_stokesODECoeffBound, which lifts coefficient bounds from the mild to the differential setting. It supplies the analytic identification step inside the 2D fluid bridge of the Recognition framework, keeping the linear evolution separate from nonlinear terms until later milestones.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.