---

Step * 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
⊢ |S(λx.(f x);full-partition([a, b];p)) - ∫ f x dx on [a, b]| ≤ (e + (r1/r(k)))
BY
{ ((InstHyp [⌜imax(N;M)⌝] (-3)⋅ THENA Auto)
   THEN All (RepUR ``so_apply``)⋅
   THEN Assert ⌜|S(λx.(f x);full-partition([a, b];p)) - Riemann-sum(λx.(f x);a;b;imax(N;M) + 1)| ≤ e⌝⋅) }

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

2
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. |S(λx.(f x);full-partition([a, b];p)) - Riemann-sum(λx.(f x);a;b;imax(N;M) + 1)| ≤ e
⊢ |S(λx.(f x);full-partition([a, b];p)) - ∫ f x dx on [a, b]| ≤ (e + (r1/r(k)))

---

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
\mvdash{}  |S(\mlambda{}x.(f  x);full-partition([a,  b];p))  -  \mint{}  f  x  dx  on  [a,  b]|  \mleq{}  (e  +  (r1/r(k)))


By

---

Latex:
((InstHyp  [\mkleeneopen{}imax(N;M)\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  All  (RepUR  ``so\_apply``)\mcdot{}
  THEN  Assert  \mkleeneopen{}|S(\mlambda{}x.(f  x);full-partition([a,  b];p))  -  Riemann-sum(\mlambda{}x.(f  x);a;b;imax(N;M)  +  1)|  \mleq{}  e\mkleeneclose{}
  \mcdot{})

---

Home Index