stokesODE

proof body

Tactic-mode proof.

 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
 231    intro s hs
 232    -- `hs : 0 ≤ s`
 233    simpa [a] using (h s hs k)
 234  have huEq_t : (fun s : ℝ => (u s) k) t = (fun s : ℝ => (heatFactor ν s k) • a) t := by
 235    simpa [a] using (h t ht k)
 236
 237  have huDeriv :
 238      HasDerivWithinAt (fun s : ℝ => (u s) k) ((heatFactor ν t k * (-ν * kSq k)) • a)
 239        (Set.Ici (0 : ℝ)) t :=
 240    hform.congr huEq huEq_t
 241
 242  -- Simplify the derivative into `-(ν|k|^2) • u(t,k)`.
 243  have hsimp :
 244      ((heatFactor ν t k * (-ν * kSq k)) • a) = (-(ν * kSq k)) • ((u t) k) := by
 245    -- Use commutativity of real multiplication to flip the order, then `mul_smul`.
 246    have hut : (u t) k = (heatFactor ν t k) • a := by
 247      simpa [a] using (h t ht k)
 248    -- Rewrite to match `mul_smul` and then substitute `hut`.
 249    calc
 250      (heatFactor ν t k * (-ν * kSq k)) • a
 251          = ((-ν * kSq k) * heatFactor ν t k) • a := by
 252              simp [mul_comm, mul_assoc]
 253      _ = (-ν * kSq k) • ((heatFactor ν t k) • a) := by
 254              simp [mul_smul]
 255      _ = (-(ν * kSq k)) • ((heatFactor ν t k) • a) := by ring_nf
 256      _ = (-(ν * kSq k)) • ((u t) k) := by simp [hut]
 257
 258  -- `simp` may rewrite `heatFactor * (-ν*kSq)` as `-(heatFactor * (ν*kSq))`, so we also register
 259  -- a simp-friendly variant with the outer negation.
 260  have hsimp_neg :
 261      -((heatFactor ν t k * (ν * kSq k)) • a) = (-(ν * kSq k)) • ((u t) k) := by
 262    -- Move the `-` inside as `(-1) • _` and simplify using `hsimp`.
 263    have : (heatFactor ν t k * (-ν * kSq k)) • a = -((heatFactor ν t k * (ν * kSq k)) • a) := by
 264      -- scalar arithmetic in `ℝ` + `(-r) • a = -(r • a)`
 265      calc
 266        (heatFactor ν t k * (-ν * kSq k)) • a
 267            = (-(heatFactor ν t k * (ν * kSq k))) • a := by ring_nf
 268        _ = -((heatFactor ν t k * (ν * kSq k)) • a) := by
 269            simp [neg_smul]
 270    -- Now rewrite and finish.
 271    simpa [this] using hsimp
 272
 273  simpa [IsStokesODETraj, hsimp_neg] using huDeriv
 274
 275end IsStokesMildTraj
 276
 277/-!
 278## Galerkin → Fourier coefficient dynamics (modewise ODE, with nonlinearity)
 279
 280This is the first genuinely “Navier–Stokes shaped” bridge lemma: if a Galerkin trajectory satisfies
 281the finite-dimensional ODE `u' = νΔu - B(u,u)`, then every Fourier mode of its zero-extension
 282-- ... 4 more lines elided ...