---

Step * of Lemma arctan-poly-approx

∀[x:ℝ]. ∀[k:ℕ].  (|arctangent(x) - arctan-poly(x;k)| ≤ (|x|^(2 * k) + 3/r((2 * k) + 3)))
BY
{ (Auto THEN (StableCases ⌜r0 < x⌝⋅ THENA Auto)) }

1
1. x : ℝ
2. k : ℕ
3. r0 < x
⊢ |arctangent(x) - arctan-poly(x;k)| ≤ (|x|^(2 * k) + 3/r((2 * k) + 3))

2
1. x : ℝ
2. k : ℕ
3. ¬(r0 < x)
⊢ |arctangent(x) - arctan-poly(x;k)| ≤ (|x|^(2 * k) + 3/r((2 * k) + 3))

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  \mforall{}[k:\mBbbN{}].    (|arctangent(x)  -  arctan-poly(x;k)|  \mleq{}  (|x|\^{}(2  *  k)  +  3/r((2  *  k)  +  3)))


By

---

Latex:
(Auto  THEN  (StableCases  \mkleeneopen{}r0  <  x\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index