---

Step * of Lemma Riemann-sums-converge-ext

∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f:[a, b] ⟶ℝ. ∀mc:f[x] continuous for x ∈ [a, b].  Riemann-sum(f;a;b;k + 1)↓ as k→∞
BY
{ Extract of Obid: Riemann-sums-converge
  normalizes to:
  
  λa,b,f,mc. <accelerate(2;λn.(Riemann-sum(f;a;b;if rless-case(r0;mc 1 
                                                                  canonical-bound(|r(2 * n)
                                                                  * (b - a)|);rlessw(r0;mc 1 
                                                                                        canonical-bound(|r(2 * n)
                                                                                        * (b - a)|));b - a)
                               then (canonical-bound(|(b - a/mc 1 canonical-bound(|r(2 * n) * (b - a)|))|) - 1) + 1
                               else 1
                               fi ) 
                               n))
             , λk.if rless-case(r0;mc 1 canonical-bound(|r(2 * 4 * k) * (b - a)|);rlessw(r0;mc 1 
                                                                                            canonical-bound(|r(2
                                                                                            * 4
                                                                                            * k)
                                                                                            * (b - a)|));b - a)
                  then (canonical-bound(|(b - a/mc 1 canonical-bound(|r(2 * 4 * k) * (b - a)|))|) - 1) + 1
                  else 1
                  fi 
             >
  
  not unfolding  Riemann-sum canonical-bound radd rabs rsub rdiv rmul rless-case int-to-real rlessw accelerate
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  \mleq{}  b\}  .  \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.  \mforall{}mc:f[x]  continuous  for  x  \mmember{}  [a,  b].
    Riemann-sum(f;a;b;k  +  1)\mdownarrow{}  as  k\mrightarrow{}\minfty{}


By

---

Latex:
...

---

Home Index