---

Step * 2 1 1 of Lemma atan-approx-property


1. k : ℕ
2. x : ℝ
3. N : ℕ+
4. |x| ≤ (r1/r(2))
5. |x * x| ≤ (r1/r(4))
6. 1-approx(Σ{(r(if (i rem 2 =z 0) then 1 else -1 fi ))/(2 * i) + 1 * x * x^i | 0≤i≤k};2
* N;poly-approx(λi.(r(if (i rem 2 =z 0) then 1 else -1 fi ))/(2 * i) + 1;x * x;k;2 * N))
7. (x * Σ{(r(if (i rem 2 =z 0) then 1 else -1 fi ))/(2 * i) + 1 * x * x^i | 0≤i≤k}) = arctan-poly(x;k)
⊢ 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)
BY
{ (RepeatFor 2 (MoveToConcl (-1))
   THEN (GenConcl ⌜Σ{(r(if (i rem 2 =z 0) then 1 else -1 fi ))/(2 * i) + 1 * x * x^i | 0≤i≤k} = v ∈ ℝ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜poly-approx(λi.(r(if (i rem 2 =z 0) then 1 else -1 fi ))/(2 * i) + 1;x * x;k;2 * N) = u ∈ ℤ⌝⋅
         THENA Auto
         )) }

1
1. k : ℕ
2. x : ℝ
3. N : ℕ+
4. |x| ≤ (r1/r(2))
5. |x * x| ≤ (r1/r(4))
6. v : ℝ
7. Σ{(r(if (i rem 2 =z 0) then 1 else -1 fi ))/(2 * i) + 1 * x * x^i | 0≤i≤k} = v ∈ ℝ
8. u : ℤ
9. poly-approx(λi.(r(if (i rem 2 =z 0) then 1 else -1 fi ))/(2 * i) + 1;x * x;k;2 * N) = u ∈ ℤ
⊢ 1-approx(v;2 * N;u)
⇒ ((x * v) = arctan-poly(x;k))
⇒ 1-approx(arctan-poly(x;k);N;eval u = u in
                               eval b = |u| + 1 in
                               eval z = x b in
                                 (u * z) ÷ 4 * b)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  x  :  \mBbbR{}
3.  N  :  \mBbbN{}\msupplus{}
4.  |x|  \mleq{}  (r1/r(2))
5.  |x  *  x|  \mleq{}  (r1/r(4))
6.  1-approx(\mSigma{}\{(r(if  (i  rem  2  =\msubz{}  0)  then  1  else  -1  fi  ))/(2  *  i)  +  1  *  x  *  x\^{}i  |  0\mleq{}i\mleq{}k\};2
*  N;poly-approx(\mlambda{}i.(r(if  (i  rem  2  =\msubz{}  0)  then  1  else  -1  fi  ))/(2  *  i)  +  1;x  *  x;k;2  *  N))
7.  (x  *  \mSigma{}\{(r(if  (i  rem  2  =\msubz{}  0)  then  1  else  -1  fi  ))/(2  *  i)  +  1  *  x  *  x\^{}i  |  0\mleq{}i\mleq{}k\})
=  arctan-poly(x;k)
\mvdash{}  1-approx(arctan-poly(x;k);N;eval  u  =  poly-approx(\mlambda{}i.(r(if  (i  rem  2  =\msubz{}  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)  \mdiv{}  4  *  b)


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}\mSigma{}\{(r(if  (i  rem  2  =\msubz{}  0)  then  1  else  -1  fi  ))/(2  *  i)  +  1  *  x  *  x\^{}i  |  0\mleq{}i\mleq{}k\}  =  v\mkleeneclose{}\mcdot{}
              THENA  Auto
              )
  THEN  (GenConcl  \mkleeneopen{}poly-approx(\mlambda{}i.(r(if  (i  rem  2  =\msubz{}  0)  then  1  else  -1  fi  ))/(2  *  i)  +  1;x  *  x;k;2  *  N)
                                  =  u\mkleeneclose{}\mcdot{}
              THENA  Auto
              ))

---

Home Index