English
Let E = (E_i)_{i∈ι} be a finite family of normed spaces and F a normed space. If f is a continuous multilinear map f: ⨂?∏_{i∈ι} E_i → F, then the function x ↦ f(x) is differentiable in the sense of Fréchet at every point x, and its derivative is given by the linear map x ↦ f.linearDeriv(x), i.e. Df(x)(h) = ∑_{i∈ι} f(x_1, …, h_i, …, x_n).
Русский
Пусть E = (E_i)_{i∈ι} — конечное семейство нормированных пространств, F — нормированное пространство. Пусть f: ⨂ E → F — непрерывно мультилинейное отображение. Тогда отображение x ↦ f(x) по элементу x из произведения E является Фреше-дифференцируемым в точке x, производной является линейное отображение f.linearDeriv(x); то есть Df(x)(h) = ∑_i f(…, h_i, …).
LaTeX
$$$\text{HasStrictFDerivAt}(f,\ f(.x) , x)\ \,\text{with derivative }\ f.linearDeriv(x).$$$
Lean4
protected theorem hasStrictFDerivAt [DecidableEq ι] : HasStrictFDerivAt f (f.linearDeriv x) x :=
by
rw [← changeOrigin_toFormalMultilinearSeries]
convert f.hasFiniteFPowerSeriesOnBall.hasStrictFDerivAt (y := x) ENNReal.coe_lt_top
rw [zero_add]
