---

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

.....assertion..... 
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))
⊢ |S(λx.(f x);full-partition([a, b];p)) - Riemann-sum(λx.(f x);a;b;imax(N;M) + 1)| ≤ e
BY
{ ((Assert 0 < imax(N;M) + 1 BY
          (GenConcl ⌜imax(N;M) = K ∈ ℕ⌝⋅ THEN Auto))
   THEN RepUR ``Riemann-sum let so_apply`` 0
   THEN (Assert r(M) ≤ r(imax(N;M) + 1) BY
               (Auto THEN RWO "imax_unfold" 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)
⊢ |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:
.....assertion..... 
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))
\mvdash{}  |S(\mlambda{}x.(f  x);full-partition([a,  b];p))  -  Riemann-sum(\mlambda{}x.(f  x);a;b;imax(N;M)  +  1)|  \mleq{}  e


By

---

Latex:
((Assert  0  <  imax(N;M)  +  1  BY
                (GenConcl  \mkleeneopen{}imax(N;M)  =  K\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  RepUR  ``Riemann-sum  let  so\_apply``  0
  THEN  (Assert  r(M)  \mleq{}  r(imax(N;M)  +  1)  BY
                          (Auto  THEN  RWO  "imax\_unfold"  0  THEN  Auto)))

---

Home Index