stokesODE
plain-language theorem explainer
The theorem shows that any trajectory satisfying the mild form of the linear Stokes/heat equation in 2D Fourier coefficients also satisfies the differential form on the half-line t ≥ 0. Analysts constructing regularity statements for Galerkin approximations to the 2D Navier-Stokes equations cite this identification. The proof differentiates the explicit scalar heat factor by the chain rule, lifts the derivative through scalar multiplication, substitutes the mild identity by congruence, and simplifies the resulting expression algebraically.
Claim. Let $u : ℝ → (Mode₂ → VelCoeff)$. Suppose that for all $t ≥ 0$ and all modes $k$, $u(t)_k = e^{-ν |k|^2 t} · u(0)_k$. Then for every $t ≥ 0$ and every $k$, the map $s ↦ u(s)_k$ admits a derivative within the interval $[0,∞)$ at the point $t$ equal to $-(ν |k|^2) · u(t)_k$.
background
The ContinuumLimit2D module constructs the passage from finite Galerkin truncations to an infinite Fourier coefficient state on the 2-torus. FourierState2D is the type of all functions from Mode2 to VelCoeff. The predicate IsStokesMildTraj ν u encodes the explicit solution formula: each coefficient evolves by multiplication with the scalar heatFactor ν t k := exp(-ν kSq k t) applied to the initial value. Its counterpart IsStokesODETraj requires that the time derivative of each coefficient, taken as a derivative within [0,∞), equals -(ν |k|^2) times the current coefficient.
proof idea
Fix t ≥ 0 and mode k; let a be the initial coefficient at that mode. Differentiate the scalar heatFactor by composing the exponential derivative with the linear map s ↦ (-ν kSq k) s. Lift the scalar derivative to the map s ↦ heatFactor(s,k) • a via the smul rule for HasDerivWithinAt. Apply congruence to replace the abstract heat map by the actual trajectory u, using the mild assumption on the interval [0,∞). Algebraic rewriting then converts the derivative expression into -(ν kSq k) • u(t,k), with an auxiliary negation identity to obtain a simp-friendly form.
why it matters
The result supplies the differential Stokes identity required by the two downstream theorems rs_implies_global_regularity_2d_stokesODECoeffBound and rs_implies_global_regularity_2d_stokesMildCoeffBound in Regularity2D. Those theorems combine uniform bounds and convergence hypotheses with the linear identity to obtain global regularity statements for the 2D continuum limit. Within the Recognition framework the lemma closes the linear identification step inside the classical bridge, immediately preceding the introduction of the nonlinear Duhamel remainder in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.