English
If two functions f and g admit Taylor series p and q on s, then the pair (f,g) admits the Cartesian-product Taylor series with coefficients given by (p y k).prod (q y k).
Русский
Если функции f и g допускают ряд Тейлора p и q на области s, то пара (f,g) допускает ряд Тейлора для произведения координат, коэффициенты которого равны (p y k).prod (q y k).
LaTeX
$$$ \HasFTaylorSeriesUpToOn_{\mathbb{K}}^{n} \; (f,g)\; s \;\text{с коэффициентами } k \mapsto (p(y,k)).prod (q(y,k)) $$$
Lean4
/-- If two functions `f` and `g` admit Taylor series `p` and `q` in a set `s`, then the Cartesian
product of `f` and `g` admits the Cartesian product of `p` and `q` as a Taylor series. -/
theorem prodMk {n : WithTop ℕ∞} (hf : HasFTaylorSeriesUpToOn n f p s) {g : E → G}
{q : E → FormalMultilinearSeries 𝕜 E G} (hg : HasFTaylorSeriesUpToOn n g q s) :
HasFTaylorSeriesUpToOn n (fun y => (f y, g y)) (fun y k => (p y k).prod (q y k)) s :=
by
set L := fun m => ContinuousMultilinearMap.prodL 𝕜 (fun _ : Fin m => E) F G
constructor
· intro x hx; rw [← hf.zero_eq x hx, ← hg.zero_eq x hx]; rfl
· intro m hm x hx
convert (L m).hasFDerivAt.comp_hasFDerivWithinAt x ((hf.fderivWithin m hm x hx).prodMk (hg.fderivWithin m hm x hx))
· intro m hm
exact (L m).continuous.comp_continuousOn ((hf.cont m hm).prodMk (hg.cont m hm))
