English
If summable majorant controls the differentiability of each Fi, then tsum Fi is differentiable on U.
Русский
Если есть суммируемый мажорант, контролирующий дифференцируемость каждого Fi, то сумма Fi по тз не противоречит дифференцируемости.
LaTeX
$$$DifferentiableOn\\ (\\lambda w, \\text{tsum}_{i} F_i w)\\ U$$$
Lean4
/-- If the terms in the sum `∑' (i : ι), F i` are uniformly bounded on `U` by a
summable function, and each term in the sum is differentiable on `U`, then so is the sum. -/
theorem differentiableOn_tsum_of_summable_norm {u : ι → ℝ} (hu : Summable u) (hf : ∀ i : ι, DifferentiableOn ℂ (F i) U)
(hU : IsOpen U) (hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i) :
DifferentiableOn ℂ (fun w : ℂ => ∑' i : ι, F i w) U := by
classical
have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
refine hc.differentiableOn (Eventually.of_forall fun s => ?_) hU
exact DifferentiableOn.fun_sum fun i _ => hf i
