English
The derivative sum formula holds under summable majorant for Fi on U with differentiability.
Русский
Формула суммы производных справедлива при суммируемом мажоранте Fi на U и дифференцируемости.
LaTeX
$$$HasSum\\left(\\lambda i, \\mathrm{deriv}(F_i) z\\right)\\left(\\mathrm{deriv}\\left(\\lambda w, \\sum' i: ι, F_i w\\right) z\\right)$.$$
Lean4
/-- If the terms in the sum `∑' (i : ι), F i` are uniformly bounded on `U` by a
summable function, then the sum of `deriv F i` at a point in `U` is the derivative of the
sum. -/
theorem hasSum_deriv_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) (hz : z ∈ U) :
HasSum (fun i : ι => deriv (F i) z) (deriv (fun w : ℂ => ∑' i : ι, F i w) z) :=
by
rw [HasSum]
have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
convert (hc.deriv (Eventually.of_forall fun s => DifferentiableOn.fun_sum fun i _ => hf i) hU).tendsto_at hz using 1
ext1 s
exact (deriv_fun_sum fun i _ => (hf i).differentiableAt (hU.mem_nhds hz)).symm
