---

Step * 2 1 1 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. 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 ∈ ℤ
10. b : ℕ+
11. (|u| + 1) = b ∈ ℕ+
12. z : ℤ
13. (x b) = z ∈ ℤ
14. 1-approx(x;b;z)
15. 1-approx(v;2 * N;u)
16. (x * v) = arctan-poly(x;k)
⊢ 1-approx(arctan-poly(x;k);N;(u * z) ÷ 4 * b)
BY
{ ((RWO "-1<" 0 THENA Auto)
   THEN (Subst' u * z ~ z * u 0 THENA Auto)
   THEN InstLemma `ireal-approx-rmul2` [⌜x⌝;⌜v⌝;⌜1⌝;⌜N⌝;⌜z⌝;u;⌜b⌝]⋅
   THEN Auto) }

---

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.  v  :  \mBbbR{}
7.  \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
8.  u  :  \mBbbZ{}
9.  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
10.  b  :  \mBbbN{}\msupplus{}
11.  (|u|  +  1)  =  b
12.  z  :  \mBbbZ{}
13.  (x  b)  =  z
14.  1-approx(x;b;z)
15.  1-approx(v;2  *  N;u)
16.  (x  *  v)  =  arctan-poly(x;k)
\mvdash{}  1-approx(arctan-poly(x;k);N;(u  *  z)  \mdiv{}  4  *  b)


By

---

Latex:
((RWO  "-1<"  0  THENA  Auto)
  THEN  (Subst'  u  *  z  \msim{}  z  *  u  0  THENA  Auto)
  THEN  InstLemma  `ireal-approx-rmul2`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}N\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};u;\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index