---

Step * 1 1 1 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))| ≤ (r(k + 1)/r(B * N))
⊢ |v - (r(z ÷ B)/r(2 * N))| ≤ (r1/r(N))
BY
{ ((Assert (r(k + 1)/r(B * N)) = (r1/r(2 * N)) BY
          (Eliminate ⌜B⌝⋅ THEN Auto))
   THEN (RWO "-1" (-2) THENA Auto)
   THEN Thin (-1)) }

1
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))
⊢ |v - (r(z ÷ B)/r(2 * N))| ≤ (r1/r(N))

---

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{}  (r(k  +  1)/r(B  *  N))
\mvdash{}  |v  -  (r(z  \mdiv{}  B)/r(2  *  N))|  \mleq{}  (r1/r(N))


By

---

Latex:
((Assert  (r(k  +  1)/r(B  *  N))  =  (r1/r(2  *  N))  BY
                (Eliminate  \mkleeneopen{}B\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (RWO  "-1"  (-2)  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index