---

Step * 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)/(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
{ (RWO "int-rdiv-req" (-1) THENA Auto) }

1
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)))

---

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)/(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:
(RWO  "int-rdiv-req"  (-1)  THENA  Auto)

---

Home Index