---

Step * 1 1 1 1 1 1 of Lemma partition-sums-converge


1. a : ℝ@i
2. b : {b:ℝ| a ≤ b} @i
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])} @i
4. e : {e:ℝ| r0 < e} @i
5. icompact([a, b])
6. d : {d:ℝ| r0 < d} 
7. ∀p,q:{p:partition([a, b])| partition-mesh([a, b];p) ≤ d} . ∀x:partition-choice(full-partition([a, b];p)).
   ∀y:partition-choice(full-partition([a, b];q)).
     (|S(λx.(f x);full-partition([a, b];q)) - S(λx.(f x);full-partition([a, b];p))| ≤ e)
8. p : partition([a, b])@i
9. partition-mesh([a, b];p) ≤ d
10. y : partition-choice(full-partition([a, b];p))@i
11. k : ℕ+
12. N : ℕ
13. ∀k@0:ℕ. ((N ≤ k@0) ⇒ (|Riemann-sum(λx.(f x);a;b;k@0 + 1) - ∫ f x dx on [a, b]| ≤ (r1/r(k))))
14. M : ℕ+
15. (|[a, b]|/r(M)) ≤ d
16. |Riemann-sum(λx.(f x);a;b;imax(N;M) + 1) - ∫ f x dx on [a, b]| ≤ (r1/r(k))
17. 0 < imax(N;M) + 1
18. r(M) ≤ r(imax(N;M) + 1)
⊢ |S(λx.(f x);full-partition([a, b];p)) - S(λx.(f x);full-partition([a, b];uniform-partition([a, b];imax(N;M)
+ 1)))| ≤ e
BY
{ (Assert (|[a, b]|/r(imax(N;M) + 1)) ≤ d BY
         ((nRMul ⌜|[a, b]|⌝ (-1)⋅ THENA EAuto 1)
          THEN (Assert ⌜(|[a, b]|/r(imax(N;M) + 1)) ≤ (|[a, b]|/r(M))⌝⋅ THENM (RelRST THEN Auto))
          THEN (Assert M ≤ (imax(N;M) + 1) BY
                      (RWO "imax_unfold" 0 THEN Auto))
          THEN (Assert r(M) ≤ r(imax(N;M) + 1) BY
                      Auto)
          THEN (Assert (r1/r(imax(N;M) + 1)) ≤ (r1/r(M)) BY
                      Auto)
          THEN nRMul ⌜|[a, b]|⌝ (-1)⋅
          THEN Auto
          THEN DVar `b'
          THEN (Unhide THENA Auto)
          THEN RepUR ``i-length`` 0
          THEN Auto)) }

1
1. a : ℝ@i
2. b : {b:ℝ| a ≤ b} @i
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])} @i
4. e : {e:ℝ| r0 < e} @i
5. icompact([a, b])
6. d : {d:ℝ| r0 < d} 
7. ∀p,q:{p:partition([a, b])| partition-mesh([a, b];p) ≤ d} . ∀x:partition-choice(full-partition([a, b];p)).
   ∀y:partition-choice(full-partition([a, b];q)).
     (|S(λx.(f x);full-partition([a, b];q)) - S(λx.(f x);full-partition([a, b];p))| ≤ e)
8. p : partition([a, b])@i
9. partition-mesh([a, b];p) ≤ d
10. y : partition-choice(full-partition([a, b];p))@i
11. k : ℕ+
12. N : ℕ
13. ∀k@0:ℕ. ((N ≤ k@0) ⇒ (|Riemann-sum(λx.(f x);a;b;k@0 + 1) - ∫ f x dx on [a, b]| ≤ (r1/r(k))))
14. M : ℕ+
15. (|[a, b]|/r(M)) ≤ d
16. |Riemann-sum(λx.(f x);a;b;imax(N;M) + 1) - ∫ f x dx on [a, b]| ≤ (r1/r(k))
17. 0 < imax(N;M) + 1
18. r(M) ≤ r(imax(N;M) + 1)
19. (|[a, b]|/r(imax(N;M) + 1)) ≤ d
⊢ |S(λx.(f x);full-partition([a, b];p)) - S(λx.(f x);full-partition([a, b];uniform-partition([a, b];imax(N;M)
+ 1)))| ≤ e

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}@i
2.  b  :  \{b:\mBbbR{}|  a  \mleq{}  b\}  @i
3.  f  :  \{f:[a,  b]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[a,  b])\}  @i
4.  e  :  \{e:\mBbbR{}|  r0  <  e\}  @i
5.  icompact([a,  b])
6.  d  :  \{d:\mBbbR{}|  r0  <  d\} 
7.  \mforall{}p,q:\{p:partition([a,  b])|  partition-mesh([a,  b];p)  \mleq{}  d\}  .
      \mforall{}x:partition-choice(full-partition([a,  b];p)).  \mforall{}y:partition-choice(full-partition([a,  b];q)).
          (|S(\mlambda{}x.(f  x);full-partition([a,  b];q))  -  S(\mlambda{}x.(f  x);full-partition([a,  b];p))|  \mleq{}  e)
8.  p  :  partition([a,  b])@i
9.  partition-mesh([a,  b];p)  \mleq{}  d
10.  y  :  partition-choice(full-partition([a,  b];p))@i
11.  k  :  \mBbbN{}\msupplus{}
12.  N  :  \mBbbN{}
13.  \mforall{}k@0:\mBbbN{}.  ((N  \mleq{}  k@0)  {}\mRightarrow{}  (|Riemann-sum(\mlambda{}x.(f  x);a;b;k@0  +  1)  -  \mint{}  f  x  dx  on  [a,  b]|  \mleq{}  (r1/r(k))))
14.  M  :  \mBbbN{}\msupplus{}
15.  (|[a,  b]|/r(M))  \mleq{}  d
16.  |Riemann-sum(\mlambda{}x.(f  x);a;b;imax(N;M)  +  1)  -  \mint{}  f  x  dx  on  [a,  b]|  \mleq{}  (r1/r(k))
17.  0  <  imax(N;M)  +  1
18.  r(M)  \mleq{}  r(imax(N;M)  +  1)
\mvdash{}  |S(\mlambda{}x.(f  x);full-partition([a,  b];p)) 
-  S(\mlambda{}x.(f  x);full-partition([a,  b];uniform-partition([a,  b];imax(N;M)  +  1)))|  \mleq{}  e


By

---

Latex:
(Assert  (|[a,  b]|/r(imax(N;M)  +  1))  \mleq{}  d  BY
              ((nRMul  \mkleeneopen{}|[a,  b]|\mkleeneclose{}  (-1)\mcdot{}  THENA  EAuto  1)
                THEN  (Assert  \mkleeneopen{}(|[a,  b]|/r(imax(N;M)  +  1))  \mleq{}  (|[a,  b]|/r(M))\mkleeneclose{}\mcdot{}  THENM  (RelRST  THEN  Auto))
                THEN  (Assert  M  \mleq{}  (imax(N;M)  +  1)  BY
                                        (RWO  "imax\_unfold"  0  THEN  Auto))
                THEN  (Assert  r(M)  \mleq{}  r(imax(N;M)  +  1)  BY
                                        Auto)
                THEN  (Assert  (r1/r(imax(N;M)  +  1))  \mleq{}  (r1/r(M))  BY
                                        Auto)
                THEN  nRMul  \mkleeneopen{}|[a,  b]|\mkleeneclose{}  (-1)\mcdot{}
                THEN  Auto
                THEN  DVar  `b'
                THEN  (Unhide  THENA  Auto)
                THEN  RepUR  ``i-length``  0
                THEN  Auto))

---

Home Index