stokesODE
plain-language theorem explainer
The mild form of the linear Stokes heat equation in Fourier coefficients on the 2-torus implies the differential form within t ≥ 0. Analysts constructing the continuum limit from 2D Galerkin approximations cite this conversion to obtain the ODE description required for regularity arguments. The proof differentiates the explicit exponential heat factor via the chain rule, applies the smul rule for coefficients, and invokes congruence under the mild identity to reach the target derivative expression.
Claim. If a map $u : ℝ → (Mode2 → VelCoeff)$ satisfies $u(t,k) = exp(-ν |k|^2 t) · u(0,k)$ for all $t ≥ 0$ and modes $k$, then for each such $t$ and $k$ the map $s ↦ u(s,k)$ admits the derivative $-(ν |k|^2) · u(t,k)$ within the half-line $[0,∞)$.
background
The ContinuumLimit2D module builds an explicit pipeline from finite Galerkin states to an infinite Fourier coefficient object on the 2-torus. FourierState2D is the type Mode2 → VelCoeff. The auxiliary heatFactor(ν,t,k) is defined as Real.exp(-ν · kSq(k) · t). IsStokesMildTraj(ν,u) asserts that every mode evolves exactly by multiplication with this scalar factor from its initial value. IsStokesODETraj(ν,u) asserts the corresponding differential statement: for each t ≥ 0 and mode k the function s ↦ u(s,k) has derivative -(ν · kSq(k)) · u(t,k) within the set Ici(0). The present lemma converts the mild identity into the differential form using only real-analysis differentiation rules.
proof idea
Fix t ≥ 0 and mode k; let a := u(0,k). Differentiate the scalar heatFactor by composing the exponential derivative with the linear map s ↦ (-ν kSq(k)) s, then apply the smul rule to obtain the derivative of the vector-valued map s ↦ heatFactor(ν,s,k) · a. Use congruence to replace the explicit formula by the given mild identity u(s,k) on [0,∞). Finally simplify the resulting scalar multiple via mul_comm, mul_smul and ring_nf to reach -(ν kSq(k)) · u(t,k), registering both the positive and negated forms for simp.
why it matters
The result is invoked inside rs_implies_global_regularity_2d_stokesODECoeffBound (and its mild-coefficient sibling) to pass from the proved mild identity on approximants to the differential Stokes equation in the continuum limit. It therefore supplies the linear evolution step required before the nonlinear Duhamel remainder can be introduced in the ClassicalBridge.Fluids pipeline. The conversion closes the analytic gap between integral and differential descriptions of the heat kernel, a prerequisite for any later global-regularity claim in two dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.