English
Under suitable differentiability and uniform summability hypotheses, the derivative of the sum equals the sum of derivatives: derivWithin (sum_n f_n) s = sum_n derivWithin f_n s.
Русский
При подходящих допущениях равномерной суммируемости производная суммы равна сумме производных: derivWithin(∑ f_n) s = ∑ derivWithin f_n s.
LaTeX
$$$\\text{derivWithin}_s(\\sum_n f_n)=\\sum_n \\text{derivWithin}_s(f_n)$$$
Lean4
theorem of_locally_bounded_eventually [TopologicalSpace β] [LocallyCompactSpace β] {f : α → β → F} {s : Set β}
(hs : IsOpen s) (hu : ∀ K ⊆ s, IsCompact K → ∃ u : α → ℝ, Summable u ∧ ∀ᶠ n in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n) :
SummableLocallyUniformlyOn f s :=
by
apply HasSumLocallyUniformlyOn.summableLocallyUniformlyOn (g := fun x ↦ ∑' n, f n x)
rw [hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn, tendstoLocallyUniformlyOn_iff_forall_isCompact hs]
intro K hK hKc
obtain ⟨u, hu1, hu2⟩ := hu K hK hKc
exact tendstoUniformlyOn_tsum_of_cofinite_eventually hu1 hu2
