English
If a family f_i is differentiable and there are uniform bounds on fderiv, then fderiv of tsum equals tsum of fderivs: fderiv 𝕜 (λ y, ∑' n f_n(y)) x = ∑' n fderiv 𝕜 (f_n) x.
Русский
Если семейство f_i дифференцируемо и существует предел по fderiv, то производная суммы равна сумма производных.
LaTeX
$$$$ fderiv_𝕜(\lambda y. \sum_n f_n(y))(x) = \sum_n fderiv_𝕜(f_n)(x). $$$$
Lean4
/-- Consider a series of `C^n` functions, with summable uniform bounds on the successive
derivatives. Then the iterated derivative of the sum is the sum of the iterated derivative. -/
theorem iteratedFDeriv_tsum (hf : ∀ i, ContDiff 𝕜 N (f i)) (hv : ∀ k : ℕ, (k : ℕ∞) ≤ N → Summable (v k))
(h'f : ∀ (k : ℕ) (i : α) (x : E), (k : ℕ∞) ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) {k : ℕ} (hk : (k : ℕ∞) ≤ N) :
(iteratedFDeriv 𝕜 k fun y => ∑' n, f n y) = fun x => ∑' n, iteratedFDeriv 𝕜 k (f n) x := by
induction k with
| zero =>
ext1 x
simp_rw [iteratedFDeriv_zero_eq_comp]
exact (continuousMultilinearCurryFin0 𝕜 E F).symm.toContinuousLinearEquiv.map_tsum
| succ k IH =>
have h'k : (k : ℕ∞) < N := lt_of_lt_of_le (WithTop.coe_lt_coe.2 (Nat.lt_succ_self _)) hk
have A : Summable fun n => iteratedFDeriv 𝕜 k (f n) 0 := .of_norm_bounded (hv k h'k.le) fun n ↦ h'f k n 0 h'k.le
simp_rw [iteratedFDeriv_succ_eq_comp_left, IH h'k.le]
rw [fderiv_tsum (hv _ hk) (fun n => (hf n).differentiable_iteratedFDeriv (mod_cast h'k)) _ A]
· ext1 x
exact (continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (k + 1) => E) F).symm.toContinuousLinearEquiv.map_tsum
· intro n x
simpa only [iteratedFDeriv_succ_eq_comp_left, LinearIsometryEquiv.norm_map, comp_apply] using h'f k.succ n x hk
