stokesODE

formal source

 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 :
 225      HasDerivWithinAt (fun s : ℝ => (heatFactor ν s k) • a)
 226        ((heatFactor ν t k * (-ν * kSq k)) • a) (Set.Ici (0 : ℝ)) t :=
 227    hscalarW.smul_const a
 228
 229  -- Replace the formula by `u` using the mild identity on the domain `[0,∞)`.
 230  have huEq : ∀ s ∈ Set.Ici (0 : ℝ), (fun s : ℝ => (u s) k) s = (fun s : ℝ => (heatFactor ν s k) • a) s := by