---

Step * 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))))
⊢ |S(λx.(f x);full-partition([a, b];p)) - ∫ f x dx on [a, b]| ≤ (e + (r1/r(k)))
BY
{ ((InstLemma `r-archimedean-implies2` [⌜|[a, b]|⌝;⌜d⌝]⋅ THENA Auto) THEN ExRepD) }

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
⊢ |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))))
\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:
((InstLemma  `r-archimedean-implies2`  [\mkleeneopen{}|[a,  b]|\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)

---

Home Index