---

Step * 1 1 of Lemma rexp-poly-approx


1. x : {x:ℝ| |x| ≤ (r1/r(4))} 
2. k : ℕ
3. N : ℕ+
4. |e^x - Σ{(x^k/r((k)!)) | 0≤k≤k}| ≤ (r1/r(4^k * 3 * (k)!))
5. |Σ{(x^i/r((i)!)) | 0≤i≤k} - (r(rexp-approx(x;k;N))/r(2 * N))| ≤ (r1/r(N))
⊢ |e^x - (r(rexp-approx(x;k;N))/r(2 * N))| ≤ ((r1/r(4^k * 3 * (k)!)) + (r1/r(N)))
BY
{ UseTriangleInequality [⌜Σ{(x^i/r((i)!)) | 0≤i≤k}⌝]⋅ }

---

Latex:

---

Latex:

1.  x  :  \{x:\mBbbR{}|  |x|  \mleq{}  (r1/r(4))\} 
2.  k  :  \mBbbN{}
3.  N  :  \mBbbN{}\msupplus{}
4.  |e\^{}x  -  \mSigma{}\{(x\^{}k/r((k)!))  |  0\mleq{}k\mleq{}k\}|  \mleq{}  (r1/r(4\^{}k  *  3  *  (k)!))
5.  |\mSigma{}\{(x\^{}i/r((i)!))  |  0\mleq{}i\mleq{}k\}  -  (r(rexp-approx(x;k;N))/r(2  *  N))|  \mleq{}  (r1/r(N))
\mvdash{}  |e\^{}x  -  (r(rexp-approx(x;k;N))/r(2  *  N))|  \mleq{}  ((r1/r(4\^{}k  *  3  *  (k)!))  +  (r1/r(N)))


By

---

Latex:
UseTriangleInequality  [\mkleeneopen{}\mSigma{}\{(x\^{}i/r((i)!))  |  0\mleq{}i\mleq{}k\}\mkleeneclose{}]\mcdot{}

---

Home Index