stokesMild_of_forall

formal source

1206
1207/-- Mild Stokes/heat identity passes to the limit under modewise convergence,
1208assuming it holds for every approximant (modewise, for `t ≥ 0`). -/
1209theorem stokesMild_of_forall {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1210    (hMild :
1211      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1212        (extendByZero (H.uN N t) k) = (heatFactor ν t k) • (extendByZero (H.uN N 0) k)) :
1213    IsStokesMildTraj ν HC.u := by
1214  intro t ht k
1215  -- convergence at time t and at time 0
1216  have hconv_t : Tendsto (fun N : ℕ => extendByZero (H.uN N t) k) atTop (nhds ((HC.u t) k)) :=
1217    HC.converges t k
1218  have hconv_0 : Tendsto (fun N : ℕ => extendByZero (H.uN N 0) k) atTop (nhds ((HC.u 0) k)) :=
1219    HC.converges 0 k
1220  -- push convergence at time 0 through the continuous map `v ↦ heatFactor • v`
1221  have hsmul :
1222      Tendsto (fun N : ℕ => (heatFactor ν t k) • (extendByZero (H.uN N 0) k)) atTop
1223        (nhds ((heatFactor ν t k) • ((HC.u 0) k))) := by
1224    have hcont : Continuous fun v : VelCoeff => (heatFactor ν t k) • v := continuous_const_smul _
1225    exact (hcont.tendsto ((HC.u 0) k)).comp hconv_0
1226  -- but the two sequences are equal for all N (by hypothesis), hence have the same limit
1227  have hEq :
1228      (fun N : ℕ => extendByZero (H.uN N t) k)
1229        =ᶠ[atTop] (fun N : ℕ => (heatFactor ν t k) • (extendByZero (H.uN N 0) k)) := by
1230    refine Filter.Eventually.of_forall ?_
1231    intro N
1232    exact hMild N t ht k
1233  -- uniqueness of limits in a T2 space
1234  have : (HC.u t) k = (heatFactor ν t k) • ((HC.u 0) k) :=
1235    tendsto_nhds_unique_of_eventuallyEq hconv_t hsmul hEq
1236  simpa using this
1237
1238/-- Duhamel-remainder identity passes to the limit under modewise convergence,
1239assuming it holds for every approximant with remainders `D_N` that converge modewise. -/