Step
*
of Lemma
cosine-poly-approx-1
No Annotations
∀[x:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} ]. ∀[k:ℕ].
(|cosine(x) - Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤k}| ≤ (x^(2 * k) + 2/r(((2 * k) + 2)!)))
BY
{ (Auto
THEN BLemma `rleq-iff-all-rless`
THEN Auto
THEN (InstLemma `small-reciprocal-real` [⌜e⌝]⋅ THENA Auto)
THEN D -1
THEN (InstLemma `cosine-is-limit` [⌜x⌝]⋅ THENA Auto)
THEN (D -1 With ⌜k1⌝ THENA Auto)
THEN ExRepD
THEN (InstHyp [⌜N⌝] (-1)⋅ THENA Auto)
THEN ((Decide ⌜N ≤ k⌝⋅ THENA Auto)
THENL [((FHyp (-3) [-1] THENA Auto)
THEN (RWO "rabs-difference-symmetry" 0 THENA Auto)
THEN (RWO "-1" 0 THENA Auto))
; UseTriangleInequality [⌜Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤N}⌝]⋅]
)) }
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. |Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤N} - cosine(x)| ≤ (r1/r(k1))
9. N ≤ k
10. |Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤k} - cosine(x)| ≤ (r1/r(k1))
⊢ (r1/r(k1)) ≤ ((x^(2 * k) + 2/r(((2 * k) + 2)!)) + e)
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)
⊢ ((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)
Latex:
Latex:
No Annotations
\mforall{}[x:\{x:\mBbbR{}| (r0 \mleq{} x) \mwedge{} (x \mleq{} r1)\} ]. \mforall{}[k:\mBbbN{}].
(|cosine(x) - \mSigma{}\{-1\^{}i * (x\^{}2 * i)/(2 * i)! | 0\mleq{}i\mleq{}k\}| \mleq{} (x\^{}(2 * k) + 2/r(((2 * k) + 2)!)))
By
Latex:
(Auto
THEN BLemma `rleq-iff-all-rless`
THEN Auto
THEN (InstLemma `small-reciprocal-real` [\mkleeneopen{}e\mkleeneclose{}]\mcdot{} THENA Auto)
THEN D -1
THEN (InstLemma `cosine-is-limit` [\mkleeneopen{}x\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (D -1 With \mkleeneopen{}k1\mkleeneclose{} THENA Auto)
THEN ExRepD
THEN (InstHyp [\mkleeneopen{}N\mkleeneclose{}] (-1)\mcdot{} THENA Auto)
THEN ((Decide \mkleeneopen{}N \mleq{} k\mkleeneclose{}\mcdot{} THENA Auto)
THENL [((FHyp (-3) [-1] THENA Auto)
THEN (RWO "rabs-difference-symmetry" 0 THENA Auto)
THEN (RWO "-1" 0 THENA Auto))
; UseTriangleInequality [\mkleeneopen{}\mSigma{}\{-1\^{}i * (x\^{}2 * i)/(2 * i)! | 0\mleq{}i\mleq{}N\}\mkleeneclose{}]\mcdot{}]
))
Home
Index