---

Step * of Lemma fun-series-converges-to-everywhere

∀f:ℕ ⟶ ℝ ⟶ ℝ
  ((∀n:ℕ. ∀x,y:ℝ.  ((x = y) ⇒ (f[n;x] = f[n;y])))
  ⇒ (∀m:ℕ+. ∃c:ℝ. ((r0 ≤ c) ∧ (c < r1) ∧ (∃N:ℕ. ∀n:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} .  (|f[n + 1;x]| ≤ (c * |f[n;x]|)))))
  ⇒ (∀g:ℝ ⟶ ℝ. ((∀x:ℝ. lim n→∞.Σ{f[i;x] | 0≤i≤n} = g[x]) ⇒ lim n→∞.Σ{f[i;x] | 0≤i≤n} = λx.g[x] for x ∈ (-∞, ∞))))
BY
{ (InstLemma  `fun-ratio-test-everywhere` []⋅
   THEN RepeatFor 3 ((ParallelLast' THENA Auto))
   THEN FLemma `fun-series-converges-absolutely-converges` [-1]
   THEN Auto
   THEN RepUR ``fun-series-converges`` -3
   THEN BLemma `fun-converges-converges-to`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
    ((\mforall{}n:\mBbbN{}.  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f[n;x]  =  f[n;y])))
    {}\mRightarrow{}  (\mforall{}m:\mBbbN{}\msupplus{}
                \mexists{}c:\mBbbR{}
                  ((r0  \mleq{}  c)
                  \mwedge{}  (c  <  r1)
                  \mwedge{}  (\mexists{}N:\mBbbN{}.  \mforall{}n:\{N...\}.  \mforall{}x:\{x:\mBbbR{}|  |x|  \mleq{}  r(m)\}  .    (|f[n  +  1;x]|  \mleq{}  (c  *  |f[n;x]|)))))
    {}\mRightarrow{}  (\mforall{}g:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}
                ((\mforall{}x:\mBbbR{}.  lim  n\mrightarrow{}\minfty{}.\mSigma{}\{f[i;x]  |  0\mleq{}i\mleq{}n\}  =  g[x])
                {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.\mSigma{}\{f[i;x]  |  0\mleq{}i\mleq{}n\}  =  \mlambda{}x.g[x]  for  x  \mmember{}  (-\minfty{},  \minfty{}))))


By

---

Latex:
(InstLemma    `fun-ratio-test-everywhere`  []\mcdot{}
  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto))
  THEN  FLemma  `fun-series-converges-absolutely-converges`  [-1]
  THEN  Auto
  THEN  RepUR  ``fun-series-converges``  -3
  THEN  BLemma  `fun-converges-converges-to`
  THEN  Auto)

---

Home Index