English
If a family f_n is locally bounded on every compact in an open set s, then SummableLocallyUniformlyOn f s.
Русский
Если семейство функций f_n ограничено локально на каждый компакт в открытом множестве s, то SummableLocallyUniformlyOn f s.
LaTeX
$$$\\text{IsOpen } s \\to (\\forall K\\subset s, IsCompact K\\to \\exists u:α→ℝ, \\text{Summable }u ∧ \\forall n, \\forall k∈K, ‖f_n k‖≤u_n) →SummableLocallyUniformlyOn f s$$$
Lean4
/-- The `derivWithin` of a sum whose derivative is absolutely and uniformly convergent sum on an
open set `s` is the sum of the derivatives of sequence of functions on the open set `s` -/
theorem derivWithin_tsum {f : ι → E → F} (hs : IsOpen s) {x : E} (hx : x ∈ s) (hf : ∀ y ∈ s, Summable fun n ↦ f n y)
(h : SummableLocallyUniformlyOn (fun n ↦ (derivWithin (fun z ↦ f n z) s)) s)
(hf2 : ∀ n r, r ∈ s → DifferentiableAt E (f n) r) :
derivWithin (fun z ↦ ∑' n, f n z) s x = ∑' n, derivWithin (f n) s x :=
by
apply HasDerivWithinAt.derivWithin ?_ (hs.uniqueDiffWithinAt hx)
apply HasDerivAt.hasDerivWithinAt
apply
hasDerivAt_of_tendstoLocallyUniformlyOn hs _ _ (fun y hy ↦ (hf y hy).hasSum) hx (f' := fun n : Finset ι ↦ fun a ↦
∑ i ∈ n, derivWithin (fun z ↦ f i z) s a)
· obtain ⟨g, hg⟩ := h
apply (hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn.mp hg).congr_right
exact fun _ hb ↦ (hg.tsum_eqOn hb).symm
·
filter_upwards with t r hr using
HasDerivAt.fun_sum (fun q hq ↦ ((hf2 q r hr).differentiableWithinAt.hasDerivWithinAt.hasDerivAt) (hs.mem_nhds hr))
