divFree_of_forall

formal source

1198
1199/-- Divergence-free passes to the limit under modewise convergence, assuming each approximant is
1200divergence-free (in the Fourier-side sense) at every time. -/
1201theorem divFree_of_forall {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1202    (hDF : ∀ N : ℕ, ∀ t : ℝ, ∀ k : Mode2, divConstraint k ((extendByZero (H.uN N t)) k) = 0) :
1203    IsDivergenceFreeTraj HC.u := by
1204  intro t k
1205  exact divConstraint_eq_zero_of_forall (HC := HC) (t := t) (k := k) (hDF := fun N => hDF N t k)
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