English
If each f_i has a strict Fréchet derivative f′_i at x, then the product map x ↦ ∏ f_i(x) has a strict Fréchet derivative given by the sum of the appropriate products times the derivatives f′_i.
Русский
Если для каждого i из списка f_i имеет строгую производную f′_i в x, то отображение x ↦ ∏ f_i(x) имеет строгую производную, равную сумме по i соответствующих произведений на обеих сторонах идущих далее/ранее, умноженных на f′_i.
LaTeX
$$$\\text{HasStrictFDerivAt }\\big( x \\mapsto \\prod_{i\\in l} f_i(x) \\big) \\,= \\, \\sum_{i=0}^{|l|-1} \\Big(\\prod_{ji} f_j(x)\\Big)$$$
Lean4
@[fun_prop]
theorem hasStrictFDerivAt_list_prod' [Fintype ι] {l : List ι} {x : ι → 𝔸} :
HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.map x).prod)
(∑ i : Fin l.length, ((l.take i).map x).prod • proj l[i] <• ((l.drop (.succ i)).map x).prod) x :=
by
induction l with
| nil => simp [hasStrictFDerivAt_const]
| cons a l IH =>
simp only [List.map_cons, List.prod_cons, ← proj_apply (R := 𝕜) (φ := fun _ : ι ↦ 𝔸) a]
exact
.congr_fderiv (.mul' (ContinuousLinearMap.hasStrictFDerivAt _) IH)
(by ext; simp [Fin.sum_univ_succ, Finset.mul_sum, mul_assoc, add_comm])
