---

Step * of Lemma alternating-series-tail-bound

No Annotations
∀x:ℕ ⟶ ℝ. ∀M:ℕ.
  ((∀n:ℕ. ((M ≤ n) ⇒ ((r0 ≤ x[n]) ∧ (x[n + 1] ≤ x[n]))))
  ⇒ lim n→∞.x[n] = r0
  ⇒ (∀a:{M...}. ∀b:ℕ.  (|Σ{-1^i * x[i] | a≤i≤b}| ≤ x[a])))
BY
{ (Auto
   THEN ((Decide ⌜a ≤ b⌝⋅ THENA Auto)
         THENL [((Assert Σ{-1^i * x[i] | a≤i≤b} = Σ{r(-1)^i * x[i] | a≤i≤b} BY
                        ((BLemma `rsum_functionality`  THEN Auto)
                         THEN D 0
                         THEN Auto
                         THEN (RWO "int-rmul-req" 0 THENA Auto)
                         THEN RWO "rnexp-int" 0
                         THEN Auto
                         THEN RWO "exp-fastexp" 0
                         THEN Auto))
                 THEN (RWO "-1" 0 THENA Auto)
                 )
               ; (RWO "rsum-empty" 0 THEN Auto THEN RWO "rabs-abs" 0 THEN Auto THEN Subst' |0| ~ 0 0 THEN Auto)⋅]
        )
   ) }

1
1. x : ℕ ⟶ ℝ
2. M : ℕ
3. ∀n:ℕ. ((M ≤ n) ⇒ ((r0 ≤ x[n]) ∧ (x[n + 1] ≤ x[n])))
4. lim n→∞.x[n] = r0
5. a : {M...}
6. b : ℕ
7. a ≤ b
8. Σ{-1^i * x[i] | a≤i≤b} = Σ{r(-1)^i * x[i] | a≤i≤b}
⊢ |Σ{r(-1)^i * x[i] | a≤i≤b}| ≤ x[a]

---

Latex:

---

Latex:
No  Annotations
\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}M:\mBbbN{}.
    ((\mforall{}n:\mBbbN{}.  ((M  \mleq{}  n)  {}\mRightarrow{}  ((r0  \mleq{}  x[n])  \mwedge{}  (x[n  +  1]  \mleq{}  x[n]))))
    {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x[n]  =  r0
    {}\mRightarrow{}  (\mforall{}a:\{M...\}.  \mforall{}b:\mBbbN{}.    (|\mSigma{}\{-1\^{}i  *  x[i]  |  a\mleq{}i\mleq{}b\}|  \mleq{}  x[a])))


By

---

Latex:
(Auto
  THEN  ((Decide  \mkleeneopen{}a  \mleq{}  b\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [((Assert  \mSigma{}\{-1\^{}i  *  x[i]  |  a\mleq{}i\mleq{}b\}  =  \mSigma{}\{r(-1)\^{}i  *  x[i]  |  a\mleq{}i\mleq{}b\}  BY
                                            ((BLemma  `rsum\_functionality`    THEN  Auto)
                                              THEN  D  0
                                              THEN  Auto
                                              THEN  (RWO  "int-rmul-req"  0  THENA  Auto)
                                              THEN  RWO  "rnexp-int"  0
                                              THEN  Auto
                                              THEN  RWO  "exp-fastexp"  0
                                              THEN  Auto))
                              THEN  (RWO  "-1"  0  THENA  Auto)
                              )
                          ;  (RWO  "rsum-empty"  0
                                THEN  Auto
                                THEN  RWO  "rabs-abs"  0
                                THEN  Auto
                                THEN  Subst'  |0|  \msim{}  0  0
                                THEN  Auto)\mcdot{}]
            )
  )

---

Home Index