---

Step * of Lemma ratio-test-ext

∀x:ℕ ⟶ ℝ. ∀N:ℕ.
  ((∀c:{c:ℝ| (r0 ≤ c) ∧ (c < r1)} . ((∀n:{N...}. (|x[n + 1]| ≤ (c * |x[n]|))) ⇒ Σn.x[n]↓))
  ∧ (∀c:{c:ℝ| r1 < c} . ((∀n:{N...}. ((c * |x[n]|) < |x[n + 1]|)) ⇒ Σn.x[n]↑)))
BY
{ Extract of Obid: ratio-test
  not unfolding  divide absval rsum radd rminus rmul rdiv rlessw exp-ratio int-to-real canonical-bound
  finishing with Auto
  normalizes to:
  
  λx,N. <λc,%. <λn.eval m = 4 * n in
                   (Σ{x i | 0≤i≤N
                    + eval m@0 = canonical-bound(λn.||x N n||) in
                      eval n = rlessw(r0;(r1 + -(c)) * (r1/r(m@0 * 2 * m))) in
                      eval x1 = rlessw(λn.|c n|;r1) in
                        exp-ratio(|c x1| + (r1 x1);4 * x1;0;n + 1;1)} 
                    m) ÷ 4
               , λk.((N
                    + eval m = canonical-bound(λn.||x N n||) in
                      eval n = rlessw(r0;(r1 + -(c)) * (r1/r(m * 2 * 4 * k))) in
                      eval x1 = rlessw(λn.|c n|;r1) in
                        exp-ratio(|c x1| + (r1 x1);4 * x1;0;n + 1;1))
                    + 1)
               >
        , λc,%. <λn.|x (N + 1) n|
                , ((((% N) * 20) + 1) * 16) + 1
                , λk.<((k + 1) + 1) + N
                     , (((k + 1) + 1) + N) - 1
                     , if (((k + 1) + 1) + N) < (k)  then Ax  else <λ%.Ax, Ax, Ax>
                     , if ((((k + 1) + 1) + N) - 1) < (k)  then Ax  else <λ%.Ax, Ax, Ax>
                     , λn.<λv.Ax, Ax, Ax>>>
        > }

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}N:\mBbbN{}.
    ((\mforall{}c:\{c:\mBbbR{}|  (r0  \mleq{}  c)  \mwedge{}  (c  <  r1)\}  .  ((\mforall{}n:\{N...\}.  (|x[n  +  1]|  \mleq{}  (c  *  |x[n]|)))  {}\mRightarrow{}  \mSigma{}n.x[n]\mdownarrow{}))
    \mwedge{}  (\mforall{}c:\{c:\mBbbR{}|  r1  <  c\}  .  ((\mforall{}n:\{N...\}.  ((c  *  |x[n]|)  <  |x[n  +  1]|))  {}\mRightarrow{}  \mSigma{}n.x[n]\muparrow{})))


By

---

Latex:
Extract  of  Obid:  ratio-test
not  unfolding    divide  absval  rsum  radd  rminus  rmul  rdiv  rlessw  exp-ratio  int-to-real  canonical-bound
finishing  with  Auto
normalizes  to:

\mlambda{}x,N.  <\mlambda{}c,\%.  <\mlambda{}n.eval  m  =  4  *  n  in
                                  (\mSigma{}\{x  i  |  0\mleq{}i\mleq{}N
                                    +  eval  m@0  =  canonical-bound(\mlambda{}n.||x  N  n||)  in
                                        eval  n  =  rlessw(r0;(r1  +  -(c))  *  (r1/r(m@0  *  2  *  m)))  in
                                        eval  x1  =  rlessw(\mlambda{}n.|c  n|;r1)  in
                                            exp-ratio(|c  x1|  +  (r1  x1);4  *  x1;0;n  +  1;1)\} 
                                    m)  \mdiv{}  4
                          ,  \mlambda{}k.((N
                                    +  eval  m  =  canonical-bound(\mlambda{}n.||x  N  n||)  in
                                        eval  n  =  rlessw(r0;(r1  +  -(c))  *  (r1/r(m  *  2  *  4  *  k)))  in
                                        eval  x1  =  rlessw(\mlambda{}n.|c  n|;r1)  in
                                            exp-ratio(|c  x1|  +  (r1  x1);4  *  x1;0;n  +  1;1))
                                    +  1)
                          >
            ,  \mlambda{}c,\%.  <\mlambda{}n.|x  (N  +  1)  n|
                            ,  ((((\%  N)  *  20)  +  1)  *  16)  +  1
                            ,  \mlambda{}k.<((k  +  1)  +  1)  +  N
                                      ,  (((k  +  1)  +  1)  +  N)  -  1
                                      ,  if  (((k  +  1)  +  1)  +  N)  <  (k)    then  Ax    else  <\mlambda{}\%.Ax,  Ax,  Ax>
                                      ,  if  ((((k  +  1)  +  1)  +  N)  -  1)  <  (k)    then  Ax    else  <\mlambda{}\%.Ax,  Ax,  Ax>
                                      ,  \mlambda{}n.<\mlambda{}v.Ax,  Ax,  Ax>>>
            >

---

Home Index