theorem
proved
tactic proof
divConstraint_eq_zero_of_forall
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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. -/