English
If each f_i has a strictly differentiable product at x with derivative f_i', then the product has a strict derivative described by the corresponding product rule sum.
Русский
Если каждую f_i можно считать строго дифференцируемой в точке x, то произведение даёт строгую производную, заданную как соответствующая сумма по правилу произведения.
LaTeX
$$$ \text{HasStrictDerivAt}\left( \prod_{i \in u} f_i, \; \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} f_j(x) \right) f_i'(x) \right) $$
Lean4
theorem fun_finset_prod (hf : ∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x) :
HasStrictDerivAt (∏ i ∈ u, f i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x := by
simpa [ContinuousLinearMap.sum_apply, ContinuousLinearMap.smul_apply] using
(HasStrictFDerivAt.finset_prod (fun i hi ↦ (hf i hi).hasStrictFDerivAt)).hasStrictDerivAt
