English
Definition compPartialSumTarget defines a Finset of index pairs describing all valid compositions for partial sums of two formal multilinear series.
Русский
Определение compPartialSumTarget задаёт конечный набор пар индексов, описывающий все допустимые композиции для частичных сумм двух формальных многочленовых рядов.
LaTeX
$$$\\mathrm{compPartialSumTarget}(m,M,N) := \\mathrm{Set.toFinset}\\Bigl( (\\sum)\\Bigr).$$$
Lean4
/-- If two functions `g` and `f` have power series `q` and `p` respectively at `f x` and `x`,
then `g ∘ f` admits the power series `q.comp p` at `x`. -/
theorem comp {g : F → G} {f : E → F} {q : FormalMultilinearSeries 𝕜 F G} {p : FormalMultilinearSeries 𝕜 E F} {x : E}
(hg : HasFPowerSeriesAt g q (f x)) (hf : HasFPowerSeriesAt f p x) : HasFPowerSeriesAt (g ∘ f) (q.comp p) x :=
by
rw [← hasFPowerSeriesWithinAt_univ] at hf hg ⊢
apply hg.comp hf (by simp)
