---

Step * 2 of Lemma small-rexp-remainder


1. x : {x:ℝ| |x| ≤ (r1/r(4))} 
2. n : ℕ
3. ¬(n = 0 ∈ ℤ)
⊢ |e^x - Σ{(x^k/r((k)!)) | 0≤k≤n}| ≤ (r1/r(4^n * 3 * (n)!))
BY
{ (BLemma `rleq-iff-all-rless`
   THEN Auto
   THEN (InstLemma `Taylor-theorem` [⌜(-∞, ∞)⌝;⌜n⌝;⌜λ2i x.e^x⌝;⌜r0⌝;⌜x⌝;⌜e⌝]⋅ THENA (Auto THEN D 0 THEN Auto))
   THEN ExRepD)⋅ }

1
1. x : {x:ℝ| |x| ≤ (r1/r(4))} 
2. n : ℕ
3. ¬(n = 0 ∈ ℤ)
4. e : {e:ℝ| r0 < e} 
5. c : ℝ
6. rmin(r0;x) ≤ c
7. c ≤ rmax(r0;x)
8. |Taylor-remainder((-∞, ∞);n;x;r0;k,x.e^x) - (x - c^n * (e^c/r((n)!))) * (x - r0)| ≤ e
⊢ |e^x - Σ{(x^k/r((k)!)) | 0≤k≤n}| ≤ ((r1/r(4^n * 3 * (n)!)) + e)

---

Latex:

---

Latex:

1.  x  :  \{x:\mBbbR{}|  |x|  \mleq{}  (r1/r(4))\} 
2.  n  :  \mBbbN{}
3.  \mneg{}(n  =  0)
\mvdash{}  |e\^{}x  -  \mSigma{}\{(x\^{}k/r((k)!))  |  0\mleq{}k\mleq{}n\}|  \mleq{}  (r1/r(4\^{}n  *  3  *  (n)!))


By

---

Latex:
(BLemma  `rleq-iff-all-rless`
  THEN  Auto
  THEN  (InstLemma  `Taylor-theorem`  [\mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i  x.e\^{}x\mkleeneclose{};\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  D  0  THEN  Auto)
              )
  THEN  ExRepD)\mcdot{}

---

Home Index