English
Let (f_i)_{i∈ι} be functions with values in their respective normed spaces. The map x ↦ (f_i(x)) is expandable in a formal power series with coordinates given by p_i if and only if the coordinate functions admit their own power series with p_i at e. Equivalently, the joint power series at e is determined coordinatewise.
Русский
Пусть для каждого индекса i∈ι функция f_i имеет разложение в форму степенного ряда вокруг точки e в своей нормированной пространственной области. Тогда отображение x ↦ (f_i(x))_{i∈ι} имеет степенной ряд, заданный через π-оператор pi(p), в точке e, тогда и только тогда для каждого i выполняется HasFPowerSeriesAt (f_i) (p_i) e.
LaTeX
$$$HasFPowerSeriesAt\,(\lambda x,\,(f \cdot x))\,(\mathrm{FormalMultilinearSeries}.\mathrm{pi}\,p)\,e \;\Longleftrightarrow\; \forall i, HasFPowerSeriesAt\,(f_i)\,(p_i)\,e$$$
Lean4
theorem hasFPowerSeriesAt_pi_iff :
HasFPowerSeriesAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e ↔ ∀ i, HasFPowerSeriesAt (f i) (p i) e :=
by
simp_rw [← hasFPowerSeriesWithinAt_univ]
exact hasFPowerSeriesWithinAt_pi_iff
