---

Step * of Lemma rabs-Riemann-sum

∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:[a, b] ⟶ℝ]. ∀[k:ℕ+].  (|Riemann-sum(f;a;b;k)| ≤ Riemann-sum(λx.|f x|;a;b;k))
BY
{ (Auto
   THEN DVar `b'⋅
   THEN (Unhide THENA Auto)
   THEN (Assert icompact([a, b]) BY
               EAuto 1)
   THEN (Unfold `Riemann-sum` 0 THEN (CallByValueReduce 0 THENA Auto))
   THEN (Assert ⌜full-partition([a, b];uniform-partition([a, b];k)) ∈ {x:ℝ| (a ≤ x) ∧ (x ≤ b)}  List⌝⋅
   THENM ((GenConclAtAddr [2;1] THENA Auto)
          THEN (CallByValueReduce 0 THENA Auto)
          THEN RepUR ``partition-sum default-partition-choice`` 0)
   )) }

1
.....assertion..... 
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : [a, b] ⟶ℝ
5. k : ℕ+
6. icompact([a, b])
⊢ full-partition([a, b];uniform-partition([a, b];k)) ∈ {x:ℝ| (a ≤ x) ∧ (x ≤ b)}  List

2
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : [a, b] ⟶ℝ
5. k : ℕ+
6. icompact([a, b])
7. full-partition([a, b];uniform-partition([a, b];k)) ∈ {x:ℝ| (a ≤ x) ∧ (x ≤ b)}  List
8. v : {x:ℝ| (a ≤ x) ∧ (x ≤ b)}  List@i
9. full-partition([a, b];uniform-partition([a, b];k)) = v ∈ ({x:ℝ| (a ≤ x) ∧ (x ≤ b)}  List)@i
⊢ |Σ{(f v[i]) * (v[i + 1] - v[i]) | 0≤i≤||v|| - 2}| ≤ Σ{|f v[i]| * (v[i + 1] - v[i]) | 0≤i≤||v|| - 2}

---

Latex:

---

Latex:
\mforall{}[a:\mBbbR{}].  \mforall{}[b:\{b:\mBbbR{}|  a  \mleq{}  b\}  ].  \mforall{}[f:[a,  b]  {}\mrightarrow{}\mBbbR{}].  \mforall{}[k:\mBbbN{}\msupplus{}].
    (|Riemann-sum(f;a;b;k)|  \mleq{}  Riemann-sum(\mlambda{}x.|f  x|;a;b;k))


By

---

Latex:
(Auto
  THEN  DVar  `b'\mcdot{}
  THEN  (Unhide  THENA  Auto)
  THEN  (Assert  icompact([a,  b])  BY
                          EAuto  1)
  THEN  (Unfold  `Riemann-sum`  0  THEN  (CallByValueReduce  0  THENA  Auto))
  THEN  (Assert  \mkleeneopen{}full-partition([a,  b];uniform-partition([a,  b];k))  \mmember{}  \{x:\mBbbR{}|  (a  \mleq{}  x)  \mwedge{}  (x  \mleq{}  b)\}    List\mkleeneclose{}\mcdot{}
  THENM  ((GenConclAtAddr  [2;1]  THENA  Auto)
                THEN  (CallByValueReduce  0  THENA  Auto)
                THEN  RepUR  ``partition-sum  default-partition-choice``  0)
  ))

---

Home Index