English
ExpNear(n, x, r) is the finite initial segment of the exponential series up to n-1 plus x^n/n! times r.
Русский
ExpNear(n, x, r) есть конечная начальная часть ряда экспоненты до n-1 с добавлением членa x^n/n! · r.
LaTeX
$$$\\operatorname{expNear}(n, x, r) = \\sum_{m=0}^{n-1} \\frac{x^{m}}{m!} + \\frac{x^{n}}{n!} r.$$$
Lean4
/-- A finite initial segment of the exponential series, followed by an arbitrary tail.
For fixed `n` this is just a linear map w.r.t. `r`, and each map is a simple linear function
of the previous (see `expNear_succ`), with `expNear n x r ⟶ exp x` as `n ⟶ ∞`,
for any `r`. -/
noncomputable def expNear (n : ℕ) (x r : ℝ) : ℝ :=
(∑ m ∈ range n, x ^ m / m.factorial) + x ^ n / n.factorial * r
