---

Step * of Lemma atan-approx-property

∀[k:ℕ]. ∀[x:ℝ]. ∀[N:ℕ+].  ((|x| ≤ (r1/r(2))) ⇒ 1-approx(arctan-poly(x;k);N;atan-approx(k;x;N)))
BY
{ (Auto THEN Unfold `atan-approx` 0 THEN Assert ⌜|x * x| ≤ (r1/r(4))⌝⋅) }

1
.....assertion..... 
1. k : ℕ
2. x : ℝ
3. N : ℕ+
4. |x| ≤ (r1/r(2))
⊢ |x * x| ≤ (r1/r(4))

2
1. k : ℕ
2. x : ℝ
3. N : ℕ+
4. |x| ≤ (r1/r(2))
5. |x * x| ≤ (r1/r(4))
⊢ 1-approx(arctan-poly(x;k);N;eval u = poly-approx(λi.(r(if (i rem 2 =z 0) then 1 else -1 fi ))/(2 * i) + 1;x * x;k;2
                                       * N) in
                              eval b = |u| + 1 in
                              eval z = x b in
                                (u * z) ÷ 4 * b)

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[x:\mBbbR{}].  \mforall{}[N:\mBbbN{}\msupplus{}].    ((|x|  \mleq{}  (r1/r(2)))  {}\mRightarrow{}  1-approx(arctan-poly(x;k);N;atan-approx(k;x;N)))


By

---

Latex:
(Auto  THEN  Unfold  `atan-approx`  0  THEN  Assert  \mkleeneopen{}|x  *  x|  \mleq{}  (r1/r(4))\mkleeneclose{}\mcdot{})

---

Home Index