---

Step * of Lemma rexp-poly-approx

∀[x:{x:ℝ| |x| ≤ (r1/r(4))} ]. ∀[k:ℕ]. ∀[N:ℕ+].
  (|e^x - (r(rexp-approx(x;k;N))/r(2 * N))| ≤ ((r1/r(4^k * 3 * (k)!)) + (r1/r(N))))
BY
{ (Auto
   THEN (InstLemma `small-rexp-remainder` [⌜x⌝;⌜k⌝]⋅ THENA Auto)
   THEN (InstLemma `rexp-approx-property` [⌜x⌝;⌜k⌝;⌜N⌝]⋅ THENA Auto)
   THEN UnfoldTopAb (-1)) }

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)/(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:
\mforall{}[x:\{x:\mBbbR{}|  |x|  \mleq{}  (r1/r(4))\}  ].  \mforall{}[k:\mBbbN{}].  \mforall{}[N:\mBbbN{}\msupplus{}].
    (|e\^{}x  -  (r(rexp-approx(x;k;N))/r(2  *  N))|  \mleq{}  ((r1/r(4\^{}k  *  3  *  (k)!))  +  (r1/r(N))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `small-rexp-remainder`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rexp-approx-property`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}N\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  UnfoldTopAb  (-1))

---

Home Index