English
Evaluating the Taylor polynomial with derivatives inside a set s at a point x gives a value in E, obtained by applying the polynomial to x to the derivatives inside s evaluated at x0.
Русский
Оценка полинома Тейлора внутри множества s в точке x дает значение в E, получаемое путем применения полинома к x к производным внутри s в точке x0.
LaTeX
$$$taylorWithinEval(f,n,s,x_0,x)=\text{PolynomialModule.eval }x\bigl( taylorWithin f\ n\ s\ x_0\bigr)$$$
Lean4
/-- The Taylor polynomial with derivatives inside of a set `s` considered as a function `ℝ → E` -/
noncomputable def taylorWithinEval (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ x : ℝ) : E :=
PolynomialModule.eval x (taylorWithin f n s x₀)
