duhamelRemainderOfGalerkin_kernel

formal source

 524`R(t,k) = -∫₀ᵗ heatFactor ν (t - s) k • F(s,k) ds`.
 525
 526This is a purely algebraic rewrite of `duhamelRemainderOfGalerkin_integratingFactor`. -/
 527theorem duhamelRemainderOfGalerkin_kernel
 528    {N : ℕ} (ν : ℝ) (B : ConvectionOp N) (u : ℝ → GalerkinState N) (k : Mode2) (t : ℝ)
 529    (hu : ∀ s : ℝ, HasDerivAt u (galerkinNSRHS (N := N) ν B (u s)) s)
 530    (hint :
 531      IntervalIntegrable (fun s : ℝ =>
 532        (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k))
 533        MeasureTheory.volume 0 t) :
 534    duhamelRemainderOfGalerkin (N := N) ν u t k
 535      =
 536        -∫ s in (0 : ℝ)..t, (heatFactor ν (t - s) k) • (extendByZero (B (u s) (u s)) k) := by
 537  -- Start from the integrating-factor identity.
 538  have hIF :=
 539    duhamelRemainderOfGalerkin_integratingFactor (N := N) (ν := ν) (B := B) (u := u) (k := k) (t := t) hu hint
 540
 541  -- Multiply both sides by the heat factor at time `t` to cancel the integrating factor.
 542  have hmul : (heatFactor ν t k) • ((Real.exp (-(ν * (-kSq k)) * t)) • duhamelRemainderOfGalerkin (N := N) ν u t k)
 543      =
 544        (heatFactor ν t k) • (-∫ s in (0 : ℝ)..t,
 545          (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k)) := by
 546    simpa using congrArg (fun v => (heatFactor ν t k) • v) hIF
 547
 548  -- Simplify the left-hand side: `heatFactor(t) * exp(ν|k|^2 t) = 1`.
 549  have hcancel :
 550      (heatFactor ν t k) • ((Real.exp (-(ν * (-kSq k)) * t)) • duhamelRemainderOfGalerkin (N := N) ν u t k)
 551        = duhamelRemainderOfGalerkin (N := N) ν u t k := by
 552    -- turn nested smul into product scalar
 553    have hprod : (heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * t)) = 1 := by
 554      calc
 555        (heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * t))
 556            = Real.exp (-ν * kSq k * t) * Real.exp (ν * kSq k * t) := by
 557                simp [heatFactor]