English
If a function f has a finite power series on a ball and g is a continuous linear map, then g ∘ f has the finite power series on the same ball with the composed series.
Русский
Если функция f имеет конечный степенной ряд на шаре, и g – непрерывный линейный отображатель, тогда g ∘ f имеет конечный степенной ряд на том же шаре с композиционным рядом.
LaTeX
$$$g : F \to\_L[\mathbb{K}] G,\ HasFiniteFPowerSeriesOnBall\ f\ p\ x\ n\ r \Rightarrow HasFiniteFPowerSeriesOnBall\ (g \circ f)\ (g.compFormalMultilinearSeries\ p)\ x\ n\ r.$$$
Lean4
/-- If a function `f` has a finite power series `p` on a ball and `g` is a continuous linear map,
then `g ∘ f` has the finite power series `g ∘ p` on the same ball. -/
theorem comp_hasFiniteFPowerSeriesOnBall (g : F →L[𝕜] G) (h : HasFiniteFPowerSeriesOnBall f p x n r) :
HasFiniteFPowerSeriesOnBall (g ∘ f) (g.compFormalMultilinearSeries p) x n r :=
⟨g.comp_hasFPowerSeriesOnBall h.1, fun m hm ↦
by
rw [compFormalMultilinearSeries_apply, h.finite m hm]
ext; exact map_zero g⟩
