English
If HasFPowerSeriesWithinAt f pf s e and HasFPowerSeriesWithinAt g qf s e, then the product map x ↦ (f x, g x) has a HasFPowerSeriesWithinAt with pf.prod qf.
Русский
Если у f и g есть локальные разложения внутри s в точке e, то отображение x ↦ (f x, g x) имеет разложение, коэффициенты которого получаются как pf.prod qf.
LaTeX
$$$\text{HasFPowerSeriesWithinAt}(f, pf, s, e) \land \text{HasFPowerSeriesWithinAt}(g, qf, s, e) \Rightarrow \text{HasFPowerSeriesWithinAt}(x \mapsto (f(x), g(x)), pf \prod qf, s, e)$$$
Lean4
theorem prod {e : E} {f : E → F} {g : E → G} {r s : ℝ≥0∞} {p : FormalMultilinearSeries 𝕜 E F}
{q : FormalMultilinearSeries 𝕜 E G} (hf : HasFPowerSeriesOnBall f p e r) (hg : HasFPowerSeriesOnBall g q e s) :
HasFPowerSeriesOnBall (fun x ↦ (f x, g x)) (p.prod q) e (min r s) :=
by
rw [← hasFPowerSeriesWithinOnBall_univ] at hf hg ⊢
exact hf.prod hg
