nsDuhamel_of_forall_kernelIntegral_of_forcing

formal source

1305
1306/-- Variant of `nsDuhamel_of_forall_kernelIntegral` that assumes dominated convergence only for the
1307*forcing* (not the kernel integrand), plus `0 ≤ ν` and `t ≥ 0` to control the kernel factor. -/
1308theorem nsDuhamel_of_forall_kernelIntegral_of_forcing {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1309    (ν : ℝ) (hν : 0 ≤ ν)
1310    (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D)
1311    (hF :
1312      ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2, ForcingDominatedConvergenceAt (F_N := F_N) (F := F) t k)
1313    (hId :
1314      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1315        (extendByZero (H.uN N t) k) =
1316          (heatFactor ν t k) • (extendByZero (H.uN N 0) k)
1317            + (duhamelKernelIntegral ν (F_N N) t) k) :
1318    IsNSDuhamelTraj ν (duhamelKernelIntegral ν F) HC.u := by
1319  intro t ht k
1320  -- convergence of the main trajectory at time `t` and at time `0`
1321  have hconv_t : Tendsto (fun N : ℕ => extendByZero (H.uN N t) k) atTop (nhds ((HC.u t) k)) :=
1322    HC.converges t k
1323  have hconv_0 : Tendsto (fun N : ℕ => extendByZero (H.uN N 0) k) atTop (nhds ((HC.u 0) k)) :=
1324    HC.converges 0 k
1325  -- convergence of the kernel-integral remainder at time `t` (from forcing-level DCT)
1326  have hconv_D :
1327      Tendsto (fun N : ℕ => (duhamelKernelIntegral ν (F_N N) t) k) atTop
1328        (nhds (((duhamelKernelIntegral ν F) t) k)) := by
1329    have hDC : DuhamelKernelDominatedConvergenceAt ν F_N F t k :=
1330      duhamelKernelDominatedConvergenceAt_of_forcing (ν := ν) (t := t) hν ht (hF t ht k)
1331    exact
1332      tendsto_duhamelKernelIntegral_of_dominated_convergence (ν := ν) (F_N := F_N) (F := F) (t := t) (k := k)
1333        hDC
1334  -- push convergence at time 0 through the continuous map `v ↦ heatFactor • v`
1335  have hsmul :
1336      Tendsto (fun N : ℕ => (heatFactor ν t k) • (extendByZero (H.uN N 0) k)) atTop
1337        (nhds ((heatFactor ν t k) • ((HC.u 0) k))) := by
1338    have hcont : Continuous fun v : VelCoeff => (heatFactor ν t k) • v := continuous_const_smul _