---

Step * of Lemma Riemann-sum-refinement

∀a,b:ℝ.
  ((a < b)
  ⇒ (∀f:[a, b] ⟶ℝ. ∀mc:f[x] continuous for x ∈ [a, b]. ∀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)))))))
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN (Assert icompact([a, b]) ∧ icompact(i-approx([a, b];1)) BY
               (RepUR ``i-approx`` 0 THEN EAuto 1))
   THEN Auto
   THEN (InstLemma `partition-refinement-sum` [⌜[a, b]⌝;⌜f⌝;⌜mc⌝;⌜uniform-partition([a, b];k)⌝;⌜n⌝]⋅ THENA Auto)) }

1
.....antecedent..... 
1. a : ℝ@i
2. b : ℝ@i
3. a < b@i
4. icompact([a, b])
5. icompact(i-approx([a, b];1))
6. f : [a, b] ⟶ℝ@i
7. mc : f[x] continuous for x ∈ [a, b]@i
8. k : ℕ+@i
9. n : ℕ+@i
10. partition-mesh([a, b];uniform-partition([a, b];k)) ≤ (mc 1 n)@i
11. m : ℕ+@i
⊢ frs-increasing(uniform-partition([a, b];k))

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

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.
    ((a  <  b)
    {}\mRightarrow{}  (\mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.  \mforall{}mc:f[x]  continuous  for  x  \mmember{}  [a,  b].  \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)))))))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  (Assert  icompact([a,  b])  \mwedge{}  icompact(i-approx([a,  b];1))  BY
                          (RepUR  ``i-approx``  0  THEN  EAuto  1))
  THEN  Auto
  THEN  (InstLemma  `partition-refinement-sum`  [\mkleeneopen{}[a,  b]\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}mc\mkleeneclose{};\mkleeneopen{}uniform-partition([a,  b];k)\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
              THENA  Auto
              ))

---

Home Index