English
If f i : E → F are differentiable within s for i in a finite list l, then the derivative of the product of all these functions equals the sum over i of the derivative of the i-th factor times the product of the preceding factors times the product of the following factors.
Русский
Если для всех i из конечного списка l функции f i : E → F дифференцируемы внутри s, то производная по x от произведения всех этих функций равна сумме по i: производная i-й функции умноженная на произведение стоящих слева и справа от нее.
LaTeX
$$$\displaystyle fderivWithin\_\mathbb{K} (\lambda x. (l.map (f \cdot x)).prod) \, s \, x = \sum_{i : Fin\; l.length} ( (l.take i).map (f \cdot x).prod ) \, • \, ( fderivWithin\_\mathbb{K} (\lambda x. f(l[i]) x) \, s \, x) \, <• \, ((l.drop (\mathsf{succ}\, i)).map (f \cdot x)).prod.$$$
Lean4
theorem fderivWithin_list_prod' {l : List ι} {x : E} (hxs : UniqueDiffWithinAt 𝕜 s x)
(h : ∀ i ∈ l, DifferentiableWithinAt 𝕜 (f i ·) s x) :
fderivWithin 𝕜 (fun x ↦ (l.map (f · x)).prod) s x =
∑ i : Fin l.length,
((l.take i).map (f · x)).prod •
(fderivWithin 𝕜 (fun x ↦ f l[i] x) s x) <• ((l.drop (.succ i)).map (f · x)).prod :=
(HasFDerivWithinAt.list_prod' fun i hi ↦ (h i hi).hasFDerivWithinAt).fderivWithin hxs
