stokesODE
The mild form of the linear Stokes heat equation in Fourier coefficients on the 2-torus implies the differential form within t ≥ 0. Analysts constructing the continuum limit from 2D Galerkin approximations cite this conversion to obtain the ODE description required for regularity arguments. The proof differentiates the explicit exponential heat factor via the chain rule, applies the smul rule for coefficients, and invokes congruence under the mild identity to reach the target derivative expression.
claimIf a map $u : ℝ → (Mode2 → VelCoeff)$ satisfies $u(t,k) = exp(-ν |k|^2 t) · u(0,k)$ for all $t ≥ 0$ and modes $k$, then for each such $t$ and $k$ the map $s ↦ u(s,k)$ admits the derivative $-(ν |k|^2) · u(t,k)$ within the half-line $[0,∞)$.
background
The ContinuumLimit2D module builds an explicit pipeline from finite Galerkin states to an infinite Fourier coefficient object on the 2-torus. FourierState2D is the type Mode2 → VelCoeff. The auxiliary heatFactor(ν,t,k) is defined as Real.exp(-ν · kSq(k) · t). IsStokesMildTraj(ν,u) asserts that every mode evolves exactly by multiplication with this scalar factor from its initial value. IsStokesODETraj(ν,u) asserts the corresponding differential statement: for each t ≥ 0 and mode k the function s ↦ u(s,k) has derivative -(ν · kSq(k)) · u(t,k) within the set Ici(0). The present lemma converts the mild identity into the differential form using only real-analysis differentiation rules.
proof idea
Fix t ≥ 0 and mode k; let a := u(0,k). Differentiate the scalar heatFactor by composing the exponential derivative with the linear map s ↦ (-ν kSq(k)) s, then apply the smul rule to obtain the derivative of the vector-valued map s ↦ heatFactor(ν,s,k) · a. Use congruence to replace the explicit formula by the given mild identity u(s,k) on [0,∞). Finally simplify the resulting scalar multiple via mul_comm, mul_smul and ring_nf to reach -(ν kSq(k)) · u(t,k), registering both the positive and negated forms for simp.
why it matters in Recognition Science
The result is invoked inside rs_implies_global_regularity_2d_stokesODECoeffBound (and its mild-coefficient sibling) to pass from the proved mild identity on approximants to the differential Stokes equation in the continuum limit. It therefore supplies the linear evolution step required before the nonlinear Duhamel remainder can be introduced in the ClassicalBridge.Fluids pipeline. The conversion closes the analytic gap between integral and differential descriptions of the heat kernel, a prerequisite for any later global-regularity claim in two dimensions.
scope and limits
- Does not treat the nonlinear convective term.
- Does not prove existence or uniqueness of any trajectory.
- Does not extend the argument to three space dimensions.
- Does not quantify approximation error between Galerkin and continuum states.
formal statement (Lean)
200theorem stokesODE {ν : ℝ} {u : ℝ → FourierState2D} (h : IsStokesMildTraj ν u) :
201 IsStokesODETraj ν u := by
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 ...