IsStokesODETraj

formal source

 172`d/dt u(t,k) = -(ν |k|^2) • u(t,k)`
 173
 174as a derivative **within** the half-line `[0,∞)`. -/
 175def IsStokesODETraj (ν : ℝ) (u : ℝ → FourierState2D) : Prop :=
 176  ∀ t ≥ 0, ∀ k : Mode2,
 177    HasDerivWithinAt (fun s : ℝ => (u s) k) (-(ν * kSq k) • (u t) k) (Set.Ici (0 : ℝ)) t
 178
 179/-!
 180## First nonlinear (Duhamel-style) identification: heat evolution + remainder
 181
 182To start introducing the nonlinear Navier–Stokes term without committing to the full analytic
 183infrastructure (time integrals, dominated convergence, etc.), we use a *Duhamel-like remainder*
 184term `D(t,k)`:
 185
 186`u(t,k) = heatFactor(ν,t,k) • u(0,k) + D(t,k)`.
 187
 188In a future milestone, `D` will be instantiated as the time-integrated nonlinear forcing.
 189For now, this already gives a useful “nonlinear-shaped” identity that can be passed to the limit
 190under modewise convergence, provided the remainders also converge modewise.
 191-/
 192
 193/-- Duhamel-style (nonlinear) remainder form: `u = heatFactor • u0 + D` (modewise, for `t ≥ 0`). -/
 194def IsNSDuhamelTraj (ν : ℝ) (D : ℝ → FourierState2D) (u : ℝ → FourierState2D) : Prop :=
 195  ∀ t ≥ 0, ∀ k : Mode2, (u t) k = (heatFactor ν t k) • (u 0) k + (D t) k
 196
 197namespace IsStokesMildTraj
 198
 199/-- Mild Stokes/heat identity implies the corresponding differential equation (within `t ≥ 0`). -/
 200theorem stokesODE {ν : ℝ} {u : ℝ → FourierState2D} (h : IsStokesMildTraj ν u) :
 201    IsStokesODETraj ν u := by
 202  intro t ht k
 203  -- Let `a = u(0,k)` so the mild formula reads `u(s,k) = exp(-ν|k|^2 s) • a` for `s ≥ 0`.
 204  let a : VelCoeff := (u 0) k
 205