IsStokesMildTraj

formal source

 161  Real.exp (-ν * kSq k * t)
 162
 163/-- Mild Stokes/heat solution in Fourier coefficients (modewise, for `t ≥ 0`). -/
 164def IsStokesMildTraj (ν : ℝ) (u : ℝ → FourierState2D) : Prop :=
 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,∞)`. -/
 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 :=