---

Step * 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] | 0≤i≤n - M} - Σ{f[i + M;x] | 0≤i≤m - M}| ≤ (r1/r(k))
12. i-approx(I;a) ⊆ I 
13. m ≤ n
⊢ |Σ{f[i;x] | 0≤i≤n} - Σ{f[i;x] | 0≤i≤m}| ≤ (r1/r(k))
BY
{ ((RWO "rsum-difference" 0 THENA Auto) THEN (RWO "rsum-difference" (-3) THENA Auto)⋅)⋅ }

1
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))

---

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]  |  0\mleq{}i\mleq{}n  -  M\}  -  \mSigma{}\{f[i  +  M;x]  |  0\mleq{}i\mleq{}m  -  M\}|  \mleq{}  (r1/r(k))
12.  i-approx(I;a)  \msubseteq{}  I 
13.  m  \mleq{}  n
\mvdash{}  |\mSigma{}\{f[i;x]  |  0\mleq{}i\mleq{}n\}  -  \mSigma{}\{f[i;x]  |  0\mleq{}i\mleq{}m\}|  \mleq{}  (r1/r(k))


By

---

Latex:
((RWO  "rsum-difference"  0  THENA  Auto)  THEN  (RWO  "rsum-difference"  (-3)  THENA  Auto)\mcdot{})\mcdot{}

---

Home Index