---

Step * 1 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
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))
BY
{ (Subst' k * m ~ m * k -1 THENA 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;m * k)| ≤ ((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
14.  |Riemann-sum(f;a;b;k)  -  Riemann-sum(f;a;b;m  *  k)|  \mleq{}  ((r1/r(n))  *  (b  -  a))
15.  |Riemann-sum(f;a;b;m)  -  Riemann-sum(f;a;b;k  *  m)|  \mleq{}  ((r1/r(n))  *  (b  -  a))
\mvdash{}  |Riemann-sum(f;a;b;k)  -  Riemann-sum(f;a;b;m)|  \mleq{}  ((r(2)/r(n))  *  (b  -  a))


By

---

Latex:
(Subst'  k  *  m  \msim{}  m  *  k  -1  THENA  Auto)

---

Home Index