---

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


1. x : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} 
2. k : ℕ
3. e : {e:ℝ| r0 < e} 
4. k1 : ℕ+
5. (r1/r(k1)) < e
6. N : ℕ
7. ∀i:ℕ. ((N ≤ i) ⇒ (|Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤i} - cosine(x)| ≤ (r1/r(k1))))
8. |cosine(x) - Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤N}| ≤ (r1/r(k1))
9. ¬(N ≤ k)
⊢ ((r1/r(k1)) + |Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤N} - Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤k}|) ≤ ((x^(2 * k) + 2/r(((2
* k)
+ 2)!))
+ e)
BY
{ ((RWO "rsum-difference" 0 THENA Auto)
   THEN (InstLemma `alternating-series-tail-bound` [⌜λ2i.(x^2 * i)/(2 * i)!⌝;⌜0⌝;⌜k + 1⌝;⌜N⌝]⋅ THENA Auto)⋅
   ) }

1
1. x : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} 
2. k : ℕ
3. e : {e:ℝ| r0 < e} 
4. k1 : ℕ+
5. (r1/r(k1)) < e
6. N : ℕ
7. ∀i:ℕ. ((N ≤ i) ⇒ (|Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤i} - cosine(x)| ≤ (r1/r(k1))))
8. |cosine(x) - Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤N}| ≤ (r1/r(k1))
9. ¬(N ≤ k)
10. n : ℕ
11. 0 ≤ n
⊢ r0 ≤ (x^2 * n)/(2 * n)!

2
1. x : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} 
2. k : ℕ
3. e : {e:ℝ| r0 < e} 
4. k1 : ℕ+
5. (r1/r(k1)) < e
6. N : ℕ
7. ∀i:ℕ. ((N ≤ i) ⇒ (|Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤i} - cosine(x)| ≤ (r1/r(k1))))
8. |cosine(x) - Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤N}| ≤ (r1/r(k1))
9. ¬(N ≤ k)
10. n : ℕ
11. 0 ≤ n
12. r0 ≤ (x^2 * n)/(2 * n)!
⊢ (x^2 * (n + 1))/(2 * (n + 1))! ≤ (x^2 * n)/(2 * n)!

3
.....antecedent..... 
1. x : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} 
2. k : ℕ
3. e : {e:ℝ| r0 < e} 
4. k1 : ℕ+
5. (r1/r(k1)) < e
6. N : ℕ
7. ∀i:ℕ. ((N ≤ i) ⇒ (|Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤i} - cosine(x)| ≤ (r1/r(k1))))
8. |cosine(x) - Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤N}| ≤ (r1/r(k1))
9. ¬(N ≤ k)
⊢ lim n→∞.(x^2 * n)/(2 * n)! = r0

4
1. x : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} 
2. k : ℕ
3. e : {e:ℝ| r0 < e} 
4. k1 : ℕ+
5. (r1/r(k1)) < e
6. N : ℕ
7. ∀i:ℕ. ((N ≤ i) ⇒ (|Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤i} - cosine(x)| ≤ (r1/r(k1))))
8. |cosine(x) - Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤N}| ≤ (r1/r(k1))
9. ¬(N ≤ k)
10. |Σ{-1^i * (x^2 * i)/(2 * i)! | k + 1≤i≤N}| ≤ (x^2 * (k + 1))/(2 * (k + 1))!
⊢ ((r1/r(k1)) + |Σ{-1^i * (x^2 * i)/(2 * i)! | k + 1≤i≤N}|) ≤ ((x^(2 * k) + 2/r(((2 * k) + 2)!)) + e)

---

Latex:

---

Latex:

1.  x  :  \{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\} 
2.  k  :  \mBbbN{}
3.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
4.  k1  :  \mBbbN{}\msupplus{}
5.  (r1/r(k1))  <  e
6.  N  :  \mBbbN{}
7.  \mforall{}i:\mBbbN{}.  ((N  \mleq{}  i)  {}\mRightarrow{}  (|\mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  |  0\mleq{}i\mleq{}i\}  -  cosine(x)|  \mleq{}  (r1/r(k1))))
8.  |cosine(x)  -  \mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  |  0\mleq{}i\mleq{}N\}|  \mleq{}  (r1/r(k1))
9.  \mneg{}(N  \mleq{}  k)
\mvdash{}  ((r1/r(k1))
+  |\mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  |  0\mleq{}i\mleq{}N\}  -  \mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  |  0\mleq{}i\mleq{}k\}|)  \mleq{}  ((x\^{}(2  *  k)
+  2/r(((2  *  k)  +  2)!))
+  e)


By

---

Latex:
((RWO  "rsum-difference"  0  THENA  Auto)
  THEN  (InstLemma  `alternating-series-tail-bound`  [\mkleeneopen{}\mlambda{}\msubtwo{}i.(x\^{}2  *  i)/(2  *  i)!\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}k  +  1\mkleeneclose{};\mkleeneopen{}N\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )\mcdot{}
  )

---

Home Index