English
Analyticity of the Taylor composition: if q is analytic on t and p analytic on s, then x ↦ (q (f x)).taylorComp (p x) is analytic on s under the hypotheses.
Русский
Аналитичность композиции Тейлора: если q аналитична на t и p аналитична на s, то x ↦ (q (f x)).taylorComp (p x) аналитична на s при предположениях.
LaTeX
$$analyticOn_taylorComp (hq) (hp) {f} (hf) (h) (n) : AnalyticOn 𝕜 (fun x => (q (f x)).taylorComp (p x)) s$$
Lean4
theorem analyticOn_taylorComp (hq : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x ↦ q x n) t)
(hp : ∀ n, AnalyticOn 𝕜 (fun x ↦ p x n) s) {f : E → F} (hf : AnalyticOn 𝕜 f s) (h : MapsTo f s t) (n : ℕ) :
AnalyticOn 𝕜 (fun x ↦ (q (f x)).taylorComp (p x) n) s :=
by
apply Finset.analyticOn_fun_sum _ (fun c _ ↦ ?_)
let B := c.compAlongOrderedFinpartitionL 𝕜 E F G
change AnalyticOn 𝕜 ((fun p ↦ B p.1 p.2) ∘ (fun x ↦ (q (f x) c.length, fun m ↦ p x (c.partSize m)))) s
apply B.analyticOnNhd_uncurry_of_multilinear.comp_analyticOn ?_ (mapsTo_univ _ _)
apply AnalyticOn.prod
· exact (hq c.length).comp hf h
· exact AnalyticOn.pi (fun i ↦ hp _)
