hasDerivAt_extendByZero_apply

formal source

 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 :
 316      HasDerivAt (fun s : ℝ => (extendByZero (u s)) k)
 317        ((extendByZero (galerkinNSRHS (N := N) ν B (u t))) k) t :=
 318    hasDerivAt_extendByZero_apply (N := N) k u (galerkinNSRHS (N := N) ν B (u t)) hu
 319  -- Simplify the RHS using linearity of `extendByZero` and the diagonal Laplacian.
 320  -- `extendByZero (ν•Δu - B(u,u)) = ν•extendByZero(Δu) - extendByZero(B(u,u))`
 321  have hR :
 322      (extendByZero (galerkinNSRHS (N := N) ν B (u t)) k)
 323        = (ν * (-kSq k)) • (extendByZero (u t)) k - (extendByZero (B (u t) (u t))) k := by
 324    -- Push `extendByZero` through the RHS definition.