---

Step * 1 1 1 of Lemma fun-series-converges-tail


1. M : ℕ
2. I : Interval
3. f : ℕ ⟶ I ⟶ℝ
4. a : {a:ℕ+| icompact(i-approx(I;a))} 
5. k : ℕ+
6. N : ℕ+
7. ∀x:{x:ℝ| x ∈ i-approx(I;a)} . ∀n,m:{N...}.  (|Σ{f[i + M;x] | 0≤i≤n} - Σ{f[i + M;x] | 0≤i≤m}| ≤ (r1/r(k)))
8. x : {x:ℝ| x ∈ i-approx(I;a)} 
9. n : {N + M...}
10. m : {N + M...}
11. |Σ{f[i + M;x] | (m - M) + 1≤i≤n - M}| ≤ (r1/r(k))
12. i-approx(I;a) ⊆ I 
13. m ≤ n
⊢ |Σ{f[i;x] | m + 1≤i≤n}| ≤ (r1/r(k))
BY
{ TACTIC:((Subst' (m - M) + 1 ~ (m + 1) - M -3 THENA Auto)
          THEN (InstLemma `rsum-shift` [⌜M⌝;⌜m + 1⌝;⌜n⌝;⌜λ2i.f[i;x]⌝]⋅ THENA Auto)
          THEN RWO "-1" 0
          THEN Auto) }

---

Latex:

---

Latex:

1.  M  :  \mBbbN{}
2.  I  :  Interval
3.  f  :  \mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}
4.  a  :  \{a:\mBbbN{}\msupplus{}|  icompact(i-approx(I;a))\} 
5.  k  :  \mBbbN{}\msupplus{}
6.  N  :  \mBbbN{}\msupplus{}
7.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  i-approx(I;a)\}  .  \mforall{}n,m:\{N...\}.
          (|\mSigma{}\{f[i  +  M;x]  |  0\mleq{}i\mleq{}n\}  -  \mSigma{}\{f[i  +  M;x]  |  0\mleq{}i\mleq{}m\}|  \mleq{}  (r1/r(k)))
8.  x  :  \{x:\mBbbR{}|  x  \mmember{}  i-approx(I;a)\} 
9.  n  :  \{N  +  M...\}
10.  m  :  \{N  +  M...\}
11.  |\mSigma{}\{f[i  +  M;x]  |  (m  -  M)  +  1\mleq{}i\mleq{}n  -  M\}|  \mleq{}  (r1/r(k))
12.  i-approx(I;a)  \msubseteq{}  I 
13.  m  \mleq{}  n
\mvdash{}  |\mSigma{}\{f[i;x]  |  m  +  1\mleq{}i\mleq{}n\}|  \mleq{}  (r1/r(k))


By

---

Latex:
TACTIC:((Subst'  (m  -  M)  +  1  \msim{}  (m  +  1)  -  M  -3  THENA  Auto)
                THEN  (InstLemma  `rsum-shift`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}m  +  1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.f[i;x]\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  RWO  "-1"  0
                THEN  Auto)

---

Home Index