165 ∀ t ≥ 0, ∀ k : Mode2, (u t) k = (heatFactor ν t k) • (u 0) k 166 167/-- Differential (within `t ≥ 0`) Stokes/heat equation in Fourier coefficients (modewise). 168 169This is a slightly more “PDE-like” statement than the mild form: for each fixed mode `k`, 170the coefficient trajectory satisfies 171 172`d/dt u(t,k) = -(ν |k|^2) • u(t,k)` 173 174as a derivative **within** the half-line `[0,∞)`. -/
used by (6)
From the project-wide theorem graph. These declarations reference this one in their body.