---

Step * of Lemma integral-from-Taylor-1

∀a:ℝ. ∀t:{t:ℝ| r0 < t} . ∀F:ℕ ⟶ (a - t, a + t) ⟶ℝ.
  ((∀k:ℕ. ∀x,y:{x:ℝ| x ∈ (a - t, a + t)} .  ((x = y) ⇒ (F[k;x] = F[k;y])))
  ⇒ infinite-deriv-seq((a - t, a + t);i,x.F[i;x])
  ⇒ (∀r:{r:ℝ| (r0 ≤ r) ∧ (r < t)} . lim k→∞.r^k * (F[k + 1;x]/r((k)!)) = λx.r0 for x ∈ (a - t, a + t))
  ⇒ (∀b:{b:ℝ| b ∈ (a - t, a + t)} 
        lim n→∞.b_∫-x Σ{(F[i;a]/r((i)!)) * t - a^i | 0≤i≤n} dt = λx.b_∫-x F[0;t] dt for x ∈ (a - t, a + t)))
BY
{ (TACTIC:InstLemma `Taylor-series-converges` []
   THEN RepeatFor 6 ((ParallelLast' THENA Auto))
   THEN Intro
   THEN InstLemma `fun-converges-to-integral` [⌜(a - t, a + t)⌝;⌜λ2k x.Σ{(F[i;a]/r((i)!)) * x - a^i | 0≤i≤k}⌝;
   ⌜λ2x.F[0;x]⌝;⌜b⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}t:\{t:\mBbbR{}|  r0  <  t\}  .  \mforall{}F:\mBbbN{}  {}\mrightarrow{}  (a  -  t,  a  +  t)  {}\mrightarrow{}\mBbbR{}.
    ((\mforall{}k:\mBbbN{}.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  (a  -  t,  a  +  t)\}  .    ((x  =  y)  {}\mRightarrow{}  (F[k;x]  =  F[k;y])))
    {}\mRightarrow{}  infinite-deriv-seq((a  -  t,  a  +  t);i,x.F[i;x])
    {}\mRightarrow{}  (\mforall{}r:\{r:\mBbbR{}|  (r0  \mleq{}  r)  \mwedge{}  (r  <  t)\} 
                lim  k\mrightarrow{}\minfty{}.r\^{}k  *  (F[k  +  1;x]/r((k)!))  =  \mlambda{}x.r0  for  x  \mmember{}  (a  -  t,  a  +  t))
    {}\mRightarrow{}  (\mforall{}b:\{b:\mBbbR{}|  b  \mmember{}  (a  -  t,  a  +  t)\} 
                lim  n\mrightarrow{}\minfty{}.b\_\mint{}\msupminus{}x  \mSigma{}\{(F[i;a]/r((i)!))  *  t  -  a\^{}i  |  0\mleq{}i\mleq{}n\}  dt  =  \mlambda{}x.b\_\mint{}\msupminus{}x  F[0;t]  dt  for  x  \mmember{}  (a 
                -  t,  a  +  t)))


By

---

Latex:
(TACTIC:InstLemma  `Taylor-series-converges`  []
  THEN  RepeatFor  6  ((ParallelLast'  THENA  Auto))
  THEN  Intro
  THEN  InstLemma  `fun-converges-to-integral`  [\mkleeneopen{}(a  -  t,  a  +  t)\mkleeneclose{};
  \mkleeneopen{}\mlambda{}\msubtwo{}k  x.\mSigma{}\{(F[i;a]/r((i)!))  *  x  -  a\^{}i  |  0\mleq{}i\mleq{}k\}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.F[0;x]\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index