 282satisfies the corresponding modewise ODE with a forcing given by the zero-extended nonlinear term.
 283-/
 284
 285lemma extendByZero_laplacianCoeff {N : ℕ} (u : GalerkinState N) (k : Mode2) :
 286    (extendByZero (laplacianCoeff (N := N) u)) k = (-kSq k) • (extendByZero u) k := by
 287  classical
 288  by_cases hk : k ∈ modes N
 289  · ext j
 290    fin_cases j <;> simp [extendByZero, coeffAt, hk, laplacianCoeff]
 291  · ext j
 292    fin_cases j <;> simp [extendByZero, coeffAt, hk]
 293
 294lemma hasDerivAt_extendByZero_apply {N : ℕ} (k : Mode2)
 295    (u : ℝ → GalerkinState N) (u' : GalerkinState N) {t : ℝ} (hu : HasDerivAt u u' t) :
 296    HasDerivAt (fun s : ℝ => (extendByZero (u s)) k) ((extendByZero u') k) t := by
 297  classical
 298  -- A constant continuous linear map: project the `k`-th Fourier coefficient after zero-extension.
 299  let L : GalerkinState N →L[ℝ] VelCoeff :=
 300    (ContinuousLinearMap.proj k).comp (extendByZeroCLM (N := N))
 301  have hL : HasDerivAt (fun _ : ℝ => L) 0 t := by
 302    simpa using (hasDerivAt_const (x := t) (c := L))
 303  -- Differentiate `s ↦ L (u s)`.
 304  have h := HasDerivAt.clm_apply (c := fun _ : ℝ => L) (c' := (0 : GalerkinState N →L[ℝ] VelCoeff))
 305    (u := u) (u' := u') (x := t) hL hu
 306  -- Unfold `L` back to `extendByZero` + evaluation at `k`.
 307  simpa [L, extendByZeroCLM] using h
 308
 309theorem galerkinNS_hasDerivAt_extendByZero_mode {N : ℕ} (ν : ℝ) (B : ConvectionOp N)
 310    (u : ℝ → GalerkinState N) (k : Mode2) {t : ℝ}
 311    (hu : HasDerivAt u (galerkinNSRHS (N := N) ν B (u t)) t) :
 312    HasDerivAt (fun s : ℝ => (extendByZero (u s)) k)
 313      ((ν * (-kSq k)) • (extendByZero (u t)) k - (extendByZero (B (u t) (u t))) k) t := by
 314  -- Start from the generic differentiation-through-zero-extension lemma.
 315  have h0 :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.