English
Assuming β is nonempty and directed both ways, (conditional β).NeBot.
Русский
При условии, что β непусто и есть направления в обе стороны, (conditional β).NeBot.
LaTeX
$$$[\\text{Nonempty }β]\\;[IsDirected]_{≤}\\;[IsDirected]_{≥}\\; (\\text{conditional }β).NeBot$$$
Lean4
/-- If a sequence of functions `fₙ` is such that `∑ fₙ (z)` is summable for each `z` in an
open set `s`, and for each `1 ≤ k ≤ m`, the series of `k`-th iterated derivatives
`∑ (iteratedDerivWithin k fₙ s) (z)`
is summable locally uniformly on `s`, and each `fₙ` is `m`-times differentiable, then the `m`-th
iterated derivative of the sum is the sum of the `m`-th iterated derivatives. -/
theorem iteratedDerivWithin_tsum {f : ι → E → F} (m : ℕ) (hs : IsOpen s) {x : E} (hx : x ∈ s)
(hsum : ∀ t ∈ s, Summable (fun n : ι ↦ f n t))
(h : ∀ k, 1 ≤ k → k ≤ m → SummableLocallyUniformlyOn (fun n ↦ (iteratedDerivWithin k (fun z ↦ f n z) s)) s)
(hf2 : ∀ n k r, k ≤ m → r ∈ s → DifferentiableAt E (iteratedDerivWithin k (fun z ↦ f n z) s) r) :
iteratedDerivWithin m (fun z ↦ ∑' n, f n z) s x = ∑' n, iteratedDerivWithin m (f n) s x := by
induction m generalizing x with
| zero => simp
| succ m hm =>
simp_rw [iteratedDerivWithin_succ]
rw [← derivWithin_tsum hs hx _ _ (fun n r hr ↦ hf2 n m r (by cutsat) hr)]
·
exact
derivWithin_congr
(fun t ht ↦ hm ht (fun k hk1 hkm ↦ h k hk1 (by cutsat)) (fun k r e hr he ↦ hf2 k r e (by cutsat) he))
(hm hx (fun k hk1 hkm ↦ h k hk1 (by cutsat)) (fun k r e hr he ↦ hf2 k r e (by cutsat) he))
· intro r hr
by_cases hm2 : m = 0
· simp [hm2, hsum r hr]
· exact ((h m (by cutsat) (by cutsat)).summable hr).congr (fun _ ↦ by simp)
· exact SummableLocallyUniformlyOn_congr (fun _ _ ht ↦ iteratedDerivWithin_succ) (h (m + 1) (by cutsat) (by cutsat))
