Step
*
4
of Lemma
Taylor-series-converges-everywhere
1. a : ℝ
2. F : ℕ ⟶ ℝ ⟶ ℝ
3. ∀k:ℕ. ∀x,y:ℝ. ((x = y)
⇒ (F[k;x] = F[k;y]))
4. infinite-deriv-seq((-∞, ∞);i,x.F[i;x])
5. ∀r:{r:ℝ| r0 ≤ r} . lim k→∞.r^k * (F[k + 1;x]/r((k)!)) = λx.r0 for x ∈ (-∞, ∞)
6. m : ℕ+
7. [%4] : icompact([r(-m), r(m)])
8. t : {t:ℝ| r0 < t}
9. [r(-m), r(m)] ⊆ (a - t, a + t)
10. lim k→∞.Σ{(F[i;a]/r((i)!)) * x - a^i | 0≤i≤k} = λx.F[0;x] for x ∈ (a - t, a + t)
⊢ ∀k@0:ℕ+
∃N:ℕ+
∀x:{x:ℝ| (r(-m) ≤ x) ∧ (x ≤ r(m))} . ∀k:{N...}. (|Σ{(F[i;a]/r((i)!)) * x - a^i | 0≤i≤k} - F[0;x]| ≤ (r1/r(k@0)))
BY
{ ((InstLemma `i-approx-containing2` [⌜(a - t, a + t)⌝;⌜r(-m)⌝;⌜r(m)⌝]⋅ THENA Auto) THEN D -1) }
1
1. a : ℝ
2. F : ℕ ⟶ ℝ ⟶ ℝ
3. ∀k:ℕ. ∀x,y:ℝ. ((x = y)
⇒ (F[k;x] = F[k;y]))
4. infinite-deriv-seq((-∞, ∞);i,x.F[i;x])
5. ∀r:{r:ℝ| r0 ≤ r} . lim k→∞.r^k * (F[k + 1;x]/r((k)!)) = λx.r0 for x ∈ (-∞, ∞)
6. m : ℕ+
7. [%4] : icompact([r(-m), r(m)])
8. t : {t:ℝ| r0 < t}
9. [r(-m), r(m)] ⊆ (a - t, a + t)
10. lim k→∞.Σ{(F[i;a]/r((i)!)) * x - a^i | 0≤i≤k} = λx.F[0;x] for x ∈ (a - t, a + t)
11. n : ℕ+
12. (r(-m) ∈ i-approx((a - t, a + t);n)) ∧ (r(m) ∈ i-approx((a - t, a + t);n))
⊢ ∀k@0:ℕ+
∃N:ℕ+
∀x:{x:ℝ| (r(-m) ≤ x) ∧ (x ≤ r(m))} . ∀k:{N...}. (|Σ{(F[i;a]/r((i)!)) * x - a^i | 0≤i≤k} - F[0;x]| ≤ (r1/r(k@0)))
Latex:
Latex:
1. a : \mBbbR{}
2. F : \mBbbN{} {}\mrightarrow{} \mBbbR{} {}\mrightarrow{} \mBbbR{}
3. \mforall{}k:\mBbbN{}. \mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} (F[k;x] = F[k;y]))
4. infinite-deriv-seq((-\minfty{}, \minfty{});i,x.F[i;x])
5. \mforall{}r:\{r:\mBbbR{}| r0 \mleq{} r\} . lim k\mrightarrow{}\minfty{}.r\^{}k * (F[k + 1;x]/r((k)!)) = \mlambda{}x.r0 for x \mmember{} (-\minfty{}, \minfty{})
6. m : \mBbbN{}\msupplus{}
7. [\%4] : icompact([r(-m), r(m)])
8. t : \{t:\mBbbR{}| r0 < t\}
9. [r(-m), r(m)] \msubseteq{} (a - t, a + t)
10. lim k\mrightarrow{}\minfty{}.\mSigma{}\{(F[i;a]/r((i)!)) * x - a\^{}i | 0\mleq{}i\mleq{}k\} = \mlambda{}x.F[0;x] for x \mmember{} (a - t, a + t)
\mvdash{} \mforall{}k@0:\mBbbN{}\msupplus{}
\mexists{}N:\mBbbN{}\msupplus{}
\mforall{}x:\{x:\mBbbR{}| (r(-m) \mleq{} x) \mwedge{} (x \mleq{} r(m))\} . \mforall{}k:\{N...\}.
(|\mSigma{}\{(F[i;a]/r((i)!)) * x - a\^{}i | 0\mleq{}i\mleq{}k\} - F[0;x]| \mleq{} (r1/r(k@0)))
By
Latex:
((InstLemma `i-approx-containing2` [\mkleeneopen{}(a - t, a + t)\mkleeneclose{};\mkleeneopen{}r(-m)\mkleeneclose{};\mkleeneopen{}r(m)\mkleeneclose{}]\mcdot{} THENA Auto) THEN D -1)
Home
Index