---

Step * 1 1 of Lemma poly-approx-property


1. k : ℕ
2. a : ℕ ⟶ ℝ
3. x : ℝ
4. ∀[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)))
5. N : ℕ+
6. |x| ≤ (r1/r(4))
7. B : ℕ+
8. (2 * (k + 1)) = B ∈ ℕ+
9. M : ℕ+
10. (B * N) = M ∈ ℕ+
11. xM : ℤ
12. (x M) = xM ∈ ℤ
13. 1-approx(x;M;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;M;0;k) = z ∈ ℤ
17. v : ℝ
18. Σ{(a i) * x^i | 0≤i≤k} = v ∈ ℝ
19. k + 1-approx(v;M;z)
⊢ 1-approx(v;N;z ÷ B)
BY
{ (Eliminate ⌜M⌝⋅ THEN ParallelLast) }

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

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
3.  x  :  \mBbbR{}
4.  \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)))
5.  N  :  \mBbbN{}\msupplus{}
6.  |x|  \mleq{}  (r1/r(4))
7.  B  :  \mBbbN{}\msupplus{}
8.  (2  *  (k  +  1))  =  B
9.  M  :  \mBbbN{}\msupplus{}
10.  (B  *  N)  =  M
11.  xM  :  \mBbbZ{}
12.  (x  M)  =  xM
13.  1-approx(x;M;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;M;0;k)  =  z
17.  v  :  \mBbbR{}
18.  \mSigma{}\{(a  i)  *  x\^{}i  |  0\mleq{}i\mleq{}k\}  =  v
19.  k  +  1-approx(v;M;z)
\mvdash{}  1-approx(v;N;z  \mdiv{}  B)


By

---

Latex:
(Eliminate  \mkleeneopen{}M\mkleeneclose{}\mcdot{}  THEN  ParallelLast)

---

Home Index