divConstraint_eq_zero_of_forall

formal source

1170
1171/-- If the approximants satisfy the (Fourier) divergence constraint at a fixed `t,k`, then so does
1172the limit coefficient (by continuity + uniqueness of limits in `ℝ`). -/
1173theorem divConstraint_eq_zero_of_forall {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1174    (t : ℝ) (k : Mode2)
1175    (hDF : ∀ N : ℕ, divConstraint k ((extendByZero (H.uN N t)) k) = 0) :
1176    divConstraint k ((HC.u t) k) = 0 := by
1177  -- Push convergence through the continuous map `divConstraint k`.
1178  have hT :
1179      Tendsto (fun N : ℕ => divConstraint k ((extendByZero (H.uN N t)) k)) atTop
1180        (𝓝 (divConstraint k ((HC.u t) k))) := by
1181    have hcont : Continuous (fun v : VelCoeff => divConstraint k v) := divConstraint_continuous k
1182    have hcontT :
1183        Tendsto (fun v : VelCoeff => divConstraint k v) (𝓝 ((HC.u t) k))
1184          (𝓝 (divConstraint k ((HC.u t) k))) :=
1185      hcont.tendsto ((HC.u t) k)
1186    exact hcontT.comp (HC.converges t k)
1187
1188  -- The sequence is constantly 0 by assumption.
1189  have heq : (fun N : ℕ => divConstraint k ((extendByZero (H.uN N t)) k)) = fun _ : ℕ => (0 : ℝ) := by
1190    funext N
1191    simpa using (hDF N)
1192
1193  have hT0 : Tendsto (fun _ : ℕ => (0 : ℝ)) atTop (𝓝 (divConstraint k ((HC.u t) k))) := by
1194    simpa [heq] using hT
1195  have hconst : Tendsto (fun _ : ℕ => (0 : ℝ)) atTop (𝓝 (0 : ℝ)) := tendsto_const_nhds
1196
1197  exact tendsto_nhds_unique hT0 hconst
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