English
Under ContDiff hypotheses and bounds, the iterated derivative of tsum is tsum of iterated derivatives.
Русский
При гипотезах ContDiff и ограничениях итеративная производная суммы равна сумме итеративных производных.
LaTeX
$$$$ \text{iteratedFDeriv}_𝕜 k(\lambda y, \sum_n f_n(y)) = \sum_n \text{iteratedFDeriv}_𝕜 k(f_n). $$$$
Lean4
/-- Consider a series of functions `∑' i, f i x`. Assume that each individual function `f i` is of
class `C^N`, and moreover there is a uniform summable upper bound on the `k`-th derivative
for each `k ≤ N`. Then the series is also `C^N`. -/
theorem contDiff_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) :
ContDiff 𝕜 N fun x => ∑' i, f i x :=
by
rw [contDiff_iff_continuous_differentiable]
constructor
· intro m hm
rw [iteratedFDeriv_tsum hf hv h'f hm]
refine continuous_tsum ?_ (hv m hm) ?_
· intro i
exact ContDiff.continuous_iteratedFDeriv (mod_cast hm) (hf i)
· intro n x
exact h'f _ _ _ hm
· intro m hm
have h'm : ((m + 1 : ℕ) : ℕ∞) ≤ N := by simpa only [ENat.coe_add, ENat.coe_one] using Order.add_one_le_of_lt hm
rw [iteratedFDeriv_tsum hf hv h'f hm.le]
have A n x : HasFDerivAt (iteratedFDeriv 𝕜 m (f n)) (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x :=
(ContDiff.differentiable_iteratedFDeriv (mod_cast hm) (hf n)).differentiableAt.hasFDerivAt
refine differentiable_tsum (hv _ h'm) A fun n x => ?_
rw [fderiv_iteratedFDeriv, comp_apply, LinearIsometryEquiv.norm_map]
exact h'f _ _ _ h'm
