---

Step * 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. lim k→∞.Riemann-sum(λx.f[x];a;b;k + 1) = ∫ f[x] dx on [a, b]
12. e1 : {e:ℝ| r0 < e} @i
⊢ |S(λx.(f x);full-partition([a, b];p)) - ∫ f x dx on [a, b]| ≤ (e + e1)
BY
{ ((InstLemma `small-reciprocal-real` [⌜e1⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (D -4 With ⌜k⌝  THENA Auto)
   THEN D -1
   THEN (Unhide THENA Auto)
   THEN (RWO "-3<" 0 THENA Auto)
   THEN ThinVar `e1') }

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))))
⊢ |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.  lim  k\mrightarrow{}\minfty{}.Riemann-sum(\mlambda{}x.f[x];a;b;k  +  1)  =  \mint{}  f[x]  dx  on  [a,  b]
12.  e1  :  \{e:\mBbbR{}|  r0  <  e\}  @i
\mvdash{}  |S(\mlambda{}x.(f  x);full-partition([a,  b];p))  -  \mint{}  f  x  dx  on  [a,  b]|  \mleq{}  (e  +  e1)


By

---

Latex:
((InstLemma  `small-reciprocal-real`  [\mkleeneopen{}e1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (D  -4  With  \mkleeneopen{}k\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  (Unhide  THENA  Auto)
  THEN  (RWO  "-3<"  0  THENA  Auto)
  THEN  ThinVar  `e1')

---

Home Index