---

Step * 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...}
⊢ |Σ{f[i;x] | 0≤i≤n} - Σ{f[i;x] | 0≤i≤m}| ≤ (r1/r(k))
BY
{ ((InstHyp [⌜x⌝;⌜n - M⌝;⌜m - M⌝] (-4)⋅ THENA Auto')
   THEN (Assert i-approx(I;a) ⊆ I  BY
               Auto)
   THEN ( Decide ⌜m ≤ n⌝⋅ 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] | 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))

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

---

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...\}
\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:
((InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}n  -  M\mkleeneclose{};\mkleeneopen{}m  -  M\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto')
  THEN  (Assert  i-approx(I;a)  \msubseteq{}  I    BY
                          Auto)
  THEN  (  Decide  \mkleeneopen{}m  \mleq{}  n\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index