galerkin_duhamelKernel_identity

formal source

 828`û(t,k) = heatFactor ν t k • û(0,k) + duhamelKernelIntegral ν (extendByZero ∘ B(u,u)) (t,k)`.
 829
 830This is just `duhamelRemainderOfGalerkin_kernel` rewritten using the definition of the remainder. -/
 831theorem galerkin_duhamelKernel_identity
 832    {N : ℕ} (ν : ℝ) (B : ConvectionOp N) (u : ℝ → GalerkinState N) (k : Mode2) (t : ℝ)
 833    (hu : ∀ s : ℝ, HasDerivAt u (galerkinNSRHS (N := N) ν B (u s)) s)
 834    (hint :
 835      IntervalIntegrable (fun s : ℝ =>
 836        (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k))
 837        MeasureTheory.volume 0 t) :
 838    (extendByZero (u t) k)
 839      =
 840        (heatFactor ν t k) • (extendByZero (u 0) k)
 841          + (duhamelKernelIntegral ν (fun s : ℝ => extendByZero (B (u s) (u s))) t) k := by
 842  -- Start from the kernel-form remainder identity.
 843  have hR :=
 844    duhamelRemainderOfGalerkin_kernel (N := N) (ν := ν) (B := B) (u := u) (k := k) (t := t) hu hint
 845  -- Unfold the remainder and rearrange.
 846  -- `R(t,k) = û(t,k) - heatFactor(t)•û(0,k)` and `R(t,k) = kernelIntegral(t,k)`.
 847  have :
 848      (extendByZero (u t) k) - (heatFactor ν t k) • (extendByZero (u 0) k)
 849        =
 850          (duhamelKernelIntegral ν (fun s : ℝ => extendByZero (B (u s) (u s))) t) k := by
 851    simpa [duhamelRemainderOfGalerkin, duhamelKernelIntegral] using hR
 852  -- Add the heat term to both sides.
 853  exact (sub_eq_iff_eq_add').1 this
 854
 855/-!
 856## A derived bound: single coefficient ≤ global norm
 857
 858Even before doing any PDE analysis, we can prove a simple but useful fact:
 859the norm of one Fourier coefficient (after zero-extension) is bounded by the
 860global Euclidean norm of the truncated Galerkin state.
 861-/