---

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


1. B : ℕ+
2. N : ℕ+
3. k : ℕ
4. a : ℕ ⟶ ℝ
5. x : ℝ
6. ∀[xM:ℤ]. ∀[M:ℕ+]. ∀[n:ℕ].
     ((|x| ≤ (r1/r(4)))
     ⇒ 1-approx(x;M;xM)
     ⇒ k + 1-approx(Σ{(a (n + i)) * x^i | 0≤i≤k};M;poly-approx-aux(a;x;xM;M;n;k)))
7. |x| ≤ (r1/r(4))
8. (2 * (k + 1)) = B ∈ ℕ+
9. M : ℕ+
10. (B * N) = M ∈ ℕ+
11. xM : ℤ
12. (x (B * N)) = xM ∈ ℤ
13. 1-approx(x;B * N;xM)
14. Σ{(a (0 + i)) * x^i | 0≤i≤k} = Σ{(a i) * x^i | 0≤i≤k}
15. z : ℤ
16. poly-approx-aux(a;x;xM;B * N;0;k) = z ∈ ℤ
17. v : ℝ
18. Σ{(a i) * x^i | 0≤i≤k} = v ∈ ℝ
19. |v - (r(z)/r(2 * B * N))| ≤ (r1/r(2 * N))
20. |(r(z)/r(2 * B * N)) - (r(z ÷ B)/r(2 * N))| ≤ (r1/r(2 * N))
⊢ ((r1/r(2 * N)) + |(r(z)/r(2 * B * N)) - (r(z ÷ B)/r(2 * N))|) ≤ (r1/r(N))
BY
{ (RWO  "-1" 0 THEN Auto THEN (RWO "radd-rdiv" 0 THENA Auto) THEN RWO "radd-int" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  B  :  \mBbbN{}\msupplus{}
2.  N  :  \mBbbN{}\msupplus{}
3.  k  :  \mBbbN{}
4.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
5.  x  :  \mBbbR{}
6.  \mforall{}[xM:\mBbbZ{}].  \mforall{}[M:\mBbbN{}\msupplus{}].  \mforall{}[n:\mBbbN{}].
          ((|x|  \mleq{}  (r1/r(4)))
          {}\mRightarrow{}  1-approx(x;M;xM)
          {}\mRightarrow{}  k  +  1-approx(\mSigma{}\{(a  (n  +  i))  *  x\^{}i  |  0\mleq{}i\mleq{}k\};M;poly-approx-aux(a;x;xM;M;n;k)))
7.  |x|  \mleq{}  (r1/r(4))
8.  (2  *  (k  +  1))  =  B
9.  M  :  \mBbbN{}\msupplus{}
10.  (B  *  N)  =  M
11.  xM  :  \mBbbZ{}
12.  (x  (B  *  N))  =  xM
13.  1-approx(x;B  *  N;xM)
14.  \mSigma{}\{(a  (0  +  i))  *  x\^{}i  |  0\mleq{}i\mleq{}k\}  =  \mSigma{}\{(a  i)  *  x\^{}i  |  0\mleq{}i\mleq{}k\}
15.  z  :  \mBbbZ{}
16.  poly-approx-aux(a;x;xM;B  *  N;0;k)  =  z
17.  v  :  \mBbbR{}
18.  \mSigma{}\{(a  i)  *  x\^{}i  |  0\mleq{}i\mleq{}k\}  =  v
19.  |v  -  (r(z)/r(2  *  B  *  N))|  \mleq{}  (r1/r(2  *  N))
20.  |(r(z)/r(2  *  B  *  N))  -  (r(z  \mdiv{}  B)/r(2  *  N))|  \mleq{}  (r1/r(2  *  N))
\mvdash{}  ((r1/r(2  *  N))  +  |(r(z)/r(2  *  B  *  N))  -  (r(z  \mdiv{}  B)/r(2  *  N))|)  \mleq{}  (r1/r(N))


By

---

Latex:
(RWO    "-1"  0  THEN  Auto  THEN  (RWO  "radd-rdiv"  0  THENA  Auto)  THEN  RWO  "radd-int"  0  THEN  Auto)

---

Home Index