compAlongOrderedFinpartition_apply

English

If q and p provide Taylor series up to n for all n in their domains, then the Taylor series of the composition g ∘ f is given by q.taylorComp p.

Русский

Если q и p задают разложения Тейлора, то композиция g ∘ f имеет разложение, данное q.taylorComp p.

LaTeX

$$HasFTaylorSeriesUpToOn n g q t → HasFTaylorSeriesUpToOn n f p s → MapsTo f s t → HasFTaylorSeriesUpToOn n (g ∘ f) (fun x => (q (f x)).taylorComp (p x)) s$$

Lean4

@[simp]
theorem compAlongOrderedFinpartition_apply {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
    (p : FormalMultilinearSeries 𝕜 E F) (c : OrderedFinpartition n) (v : Fin n → E) :
    (q.compAlongOrderedFinpartition p c) v = q c.length (c.applyOrderedFinpartition (fun m ↦ (p (c.partSize m))) v) :=
  rfl

Похожие утверждения