---

Step * 1 of Lemma Riemann-sums-near


1. a : ℝ@i
2. b : ℝ@i
3. a < b@i
4. f : [a, b] ⟶ℝ@i
5. mc : f[x] continuous for x ∈ [a, b]@i
6. ∀k,n:ℕ+.
     ((partition-mesh([a, b];uniform-partition([a, b];k)) ≤ (mc 1 n))
     ⇒ (∀m:ℕ+. (|Riemann-sum(f;a;b;k) - Riemann-sum(f;a;b;m * k)| ≤ ((r1/r(n)) * (b - a)))))
7. icompact([a, b])
8. icompact(i-approx([a, b];1))
9. k : ℕ+@i
10. m : ℕ+@i
11. n : ℕ+@i
12. (b - a/r(k)) ≤ (mc 1 n)@i
13. (b - a/r(m)) ≤ (mc 1 n)@i
⊢ |Riemann-sum(f;a;b;k) - Riemann-sum(f;a;b;m)| ≤ ((r(2)/r(n)) * (b - a))
BY
{ ((InstHyp [⌜k⌝;⌜n⌝;⌜m⌝] 6⋅
    THENA (Auto THEN (RWO "mesh-uniform-partition" 0 THENA Auto) THEN RepUR ``i-length`` 0 THEN Auto)
    )
   THEN (InstHyp [⌜m⌝;⌜n⌝;⌜k⌝] 6⋅
         THENA (Auto THEN (RWO "mesh-uniform-partition" 0 THENA Auto) THEN RepUR ``i-length`` 0 THEN Auto)
         )
   ) }

1
1. a : ℝ@i
2. b : ℝ@i
3. a < b@i
4. f : [a, b] ⟶ℝ@i
5. mc : f[x] continuous for x ∈ [a, b]@i
6. ∀k,n:ℕ+.
     ((partition-mesh([a, b];uniform-partition([a, b];k)) ≤ (mc 1 n))
     ⇒ (∀m:ℕ+. (|Riemann-sum(f;a;b;k) - Riemann-sum(f;a;b;m * k)| ≤ ((r1/r(n)) * (b - a)))))
7. icompact([a, b])
8. icompact(i-approx([a, b];1))
9. k : ℕ+@i
10. m : ℕ+@i
11. n : ℕ+@i
12. (b - a/r(k)) ≤ (mc 1 n)@i
13. (b - a/r(m)) ≤ (mc 1 n)@i
14. |Riemann-sum(f;a;b;k) - Riemann-sum(f;a;b;m * k)| ≤ ((r1/r(n)) * (b - a))
15. |Riemann-sum(f;a;b;m) - Riemann-sum(f;a;b;k * m)| ≤ ((r1/r(n)) * (b - a))
⊢ |Riemann-sum(f;a;b;k) - Riemann-sum(f;a;b;m)| ≤ ((r(2)/r(n)) * (b - a))

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}@i
2.  b  :  \mBbbR{}@i
3.  a  <  b@i
4.  f  :  [a,  b]  {}\mrightarrow{}\mBbbR{}@i
5.  mc  :  f[x]  continuous  for  x  \mmember{}  [a,  b]@i
6.  \mforall{}k,n:\mBbbN{}\msupplus{}.
          ((partition-mesh([a,  b];uniform-partition([a,  b];k))  \mleq{}  (mc  1  n))
          {}\mRightarrow{}  (\mforall{}m:\mBbbN{}\msupplus{}.  (|Riemann-sum(f;a;b;k)  -  Riemann-sum(f;a;b;m  *  k)|  \mleq{}  ((r1/r(n))  *  (b  -  a)))))
7.  icompact([a,  b])
8.  icompact(i-approx([a,  b];1))
9.  k  :  \mBbbN{}\msupplus{}@i
10.  m  :  \mBbbN{}\msupplus{}@i
11.  n  :  \mBbbN{}\msupplus{}@i
12.  (b  -  a/r(k))  \mleq{}  (mc  1  n)@i
13.  (b  -  a/r(m))  \mleq{}  (mc  1  n)@i
\mvdash{}  |Riemann-sum(f;a;b;k)  -  Riemann-sum(f;a;b;m)|  \mleq{}  ((r(2)/r(n))  *  (b  -  a))


By

---

Latex:
((InstHyp  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]  6\mcdot{}
    THENA  (Auto  THEN  (RWO  "mesh-uniform-partition"  0  THENA  Auto)  THEN  RepUR  ``i-length``  0  THEN  Auto)
    )
  THEN  (InstHyp  [\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]  6\mcdot{}
              THENA  (Auto
                            THEN  (RWO  "mesh-uniform-partition"  0  THENA  Auto)
                            THEN  RepUR  ``i-length``  0
                            THEN  Auto)
              )
  )

---

Home Index