English
The k-th coefficient is used to build the Taylor polynomial inside a set s and accumulate contributions from all orders up to n.
Русский
K-й коэффициент используется для построения ряда Тейлора внутри множества s и суммирования вкладов по всем степеням до n.
LaTeX
$$$taylorWithin(f,n,s,x_0)=\sum_{k=0}^{n} (x-x_0)^k/k! \cdot \operatorname{iteratedDerivWithin}(k)f\,s\ x_0$$$
Lean4
/-- The Taylor polynomial with derivatives inside of a set `s`.
The Taylor polynomial is given by
$$∑_{k=0}^n \frac{(x - x₀)^k}{k!} f^{(k)}(x₀),$$
where $f^{(k)}(x₀)$ denotes the iterated derivative in the set `s`. -/
noncomputable def taylorWithin (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ : ℝ) : PolynomialModule ℝ E :=
(Finset.range (n + 1)).sum fun k =>
PolynomialModule.comp (Polynomial.X - Polynomial.C x₀) (PolynomialModule.single ℝ k (taylorCoeffWithin f k s x₀))
