---

Step * of Lemma poly-approx-property

∀[k:ℕ]. ∀[a:ℕ ⟶ ℝ]. ∀[x:ℝ]. ∀[N:ℕ+].  ((|x| ≤ (r1/r(4))) ⇒ 1-approx(Σ{(a i) * x^i | 0≤i≤k};N;poly-approx(a;x;k;N)))
BY
{ ((InstLemma `poly-approx-aux-property` [] THEN RepeatFor 3 (ParallelLast'))
   THEN Auto
   THEN Unfold `poly-approx` 0
   THEN (GenConcl ⌜(2 * (k + 1)) = B ∈ ℕ+⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0⋅ THENA Auto)
   THEN (GenConcl ⌜(B * N) = M ∈ ℕ+⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0⋅ THENA Auto)
   THEN (Assert 1-approx(x;M;x M) BY
               Auto)
   THEN MoveToConcl (-1)
   THEN GenConcl ⌜(x M) = xM ∈ ℤ⌝⋅
   THEN Auto
   THEN (CallByValueReduce 0⋅ THENA Auto)) }

1
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)
⊢ 1-approx(Σ{(a i) * x^i | 0≤i≤k};N;eval z = poly-approx-aux(a;x;xM;M;0;k) in
                                    z ÷ B)

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[a:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[x:\mBbbR{}].  \mforall{}[N:\mBbbN{}\msupplus{}].
    ((|x|  \mleq{}  (r1/r(4)))  {}\mRightarrow{}  1-approx(\mSigma{}\{(a  i)  *  x\^{}i  |  0\mleq{}i\mleq{}k\};N;poly-approx(a;x;k;N)))


By

---

Latex:
((InstLemma  `poly-approx-aux-property`  []  THEN  RepeatFor  3  (ParallelLast'))
  THEN  Auto
  THEN  Unfold  `poly-approx`  0
  THEN  (GenConcl  \mkleeneopen{}(2  *  (k  +  1))  =  B\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(B  *  N)  =  M\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0\mcdot{}  THENA  Auto)
  THEN  (Assert  1-approx(x;M;x  M)  BY
                          Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConcl  \mkleeneopen{}(x  M)  =  xM\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (CallByValueReduce  0\mcdot{}  THENA  Auto))

---

Home Index