---

Step * 1 2 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] | (n - M) + 1≤i≤m - M}| ≤ (r1/r(k))
12. i-approx(I;a) ⊆ I 
13. ¬(m ≤ n)
⊢ |Σ{f[i;x] | n + 1≤i≤m}| ≤ (r1/r(k))
BY
{ ((Subst' (n - M) + 1 ~ (n + 1) - M -3 THENA Auto)
   THEN (InstLemma `rsum-shift` [⌜M⌝;⌜n + 1⌝;⌜m⌝;⌜λ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]  |  (n  -  M)  +  1\mleq{}i\mleq{}m  -  M\}|  \mleq{}  (r1/r(k))
12.  i-approx(I;a)  \msubseteq{}  I 
13.  \mneg{}(m  \mleq{}  n)
\mvdash{}  |\mSigma{}\{f[i;x]  |  n  +  1\mleq{}i\mleq{}m\}|  \mleq{}  (r1/r(k))


By

---

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

---

Home Index