English
If u is summable and each Fi is differentiable on U with Fi bounded by ui on U, then the sum of derivatives has derivative equal to the derivative of the sum on U.
Русский
Если u суммируема и каждое Fi дифференцируемо на U с пределами нормы ≤ ui, то сумма производных равна производной суммы на U.
LaTeX
$$$HasSum\\left(\\lambda i, \\mathrm{deriv}(F_i)\\, z\\right)\\left(\\mathrm{deriv}\\left(\\lambda w, \\sum_i F_i w\\right) z\\right)$$$
Lean4
theorem _root_.TendstoUniformlyOn.cderiv (hF : TendstoUniformlyOn F f φ (cthickening δ K)) (hδ : 0 < δ)
(hFn : ∀ᶠ n in φ, ContinuousOn (F n) (cthickening δ K)) : TendstoUniformlyOn (cderiv δ ∘ F) (cderiv δ f) φ K :=
by
rcases φ.eq_or_neBot with rfl | hne
· simp only [TendstoUniformlyOn, eventually_bot, imp_true_iff]
have e1 : ContinuousOn f (cthickening δ K) := TendstoUniformlyOn.continuousOn hF hFn
rw [tendstoUniformlyOn_iff] at hF ⊢
rintro ε hε
filter_upwards [hF (ε * δ) (mul_pos hε hδ), hFn] with n h h' z hz
simp_rw [dist_eq_norm] at h ⊢
have e2 : ∀ w ∈ sphere z δ, ‖f w - F n w‖ < ε * δ := fun w hw1 =>
h w (closedBall_subset_cthickening hz δ (sphere_subset_closedBall hw1))
have e3 := sphere_subset_closedBall.trans (closedBall_subset_cthickening hz δ)
have hf : ContinuousOn f (sphere z δ) := e1.mono (sphere_subset_closedBall.trans (closedBall_subset_cthickening hz δ))
simpa only [mul_div_cancel_right₀ _ hδ.ne.symm] using norm_cderiv_sub_lt hδ e2 hf (h'.mono e3)
