IsNSDuhamelTraj

formal source

 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
 206  -- Derivative of the scalar heat factor.
 207  have hlin : HasDerivAt (fun s : ℝ => (-ν * kSq k) * s) (-ν * kSq k) t := by
 208    simpa [mul_assoc] using (hasDerivAt_id t).const_mul (-ν * kSq k)
 209  have hscalar :
 210      HasDerivAt (fun s : ℝ => heatFactor ν s k)
 211        (heatFactor ν t k * (-ν * kSq k)) t := by
 212    -- `d/ds exp(g(s)) = exp(g(s)) * g'(s)` with `g(s) = (-ν|k|^2) * s`.
 213    have hexp :
 214        HasDerivAt (fun s : ℝ => Real.exp ((-ν * kSq k) * s))
 215          (Real.exp ((-ν * kSq k) * t) * (-ν * kSq k)) t :=
 216      (Real.hasDerivAt_exp ((-ν * kSq k) * t)).comp t hlin
 217    simpa [heatFactor, mul_assoc] using hexp
 218  have hscalarW :
 219      HasDerivWithinAt (fun s : ℝ => heatFactor ν s k)
 220        (heatFactor ν t k * (-ν * kSq k)) (Set.Ici (0 : ℝ)) t :=
 221    hscalar.hasDerivWithinAt
 222
 223  -- Differentiate `s ↦ heatFactor ν s k • a` within `[0,∞)`.
 224  have hform :