---

Step * 1 1 of Lemma partition-sum-constant


1. I : Interval
2. icompact(I)
3. c : ℝ
4. p : partition(I)
5. y : partition-choice(full-partition(I;p))
6. v : ℝ List
7. full-partition(I;p) = v ∈ (ℝ List)
⊢ Σ{(c * v[i + 1]) - c * v[i] | 0≤i≤||v|| - 2} = (c * |I|)
BY
{ ((Assert 1 < ||v|| BY
          ((StrongRevHypSubst (-1) 0 THENA Auto) THEN RepUR ``full-partition`` 0 THEN Auto'))
   THEN RWO "rsum-telescopes" 0
   THEN Auto
   THEN (Subst' (||v|| - 2) + 1 ~ ||v|| - 1 0 THENA Auto)
   THEN Fold `last` 0
   THEN (RWO  "rmul-rsub-distrib.1<" 0 THENA Auto)) }

1
1. I : Interval
2. icompact(I)
3. c : ℝ
4. p : partition(I)
5. y : partition-choice(full-partition(I;p))
6. v : ℝ List
7. full-partition(I;p) = v ∈ (ℝ List)
8. 1 < ||v||
⊢ (c * (last(v) - v[0])) = (c * |I|)

---

Latex:

---

Latex:

1.  I  :  Interval
2.  icompact(I)
3.  c  :  \mBbbR{}
4.  p  :  partition(I)
5.  y  :  partition-choice(full-partition(I;p))
6.  v  :  \mBbbR{}  List
7.  full-partition(I;p)  =  v
\mvdash{}  \mSigma{}\{(c  *  v[i  +  1])  -  c  *  v[i]  |  0\mleq{}i\mleq{}||v||  -  2\}  =  (c  *  |I|)


By

---

Latex:
((Assert  1  <  ||v||  BY
                ((StrongRevHypSubst  (-1)  0  THENA  Auto)  THEN  RepUR  ``full-partition``  0  THEN  Auto'))
  THEN  RWO  "rsum-telescopes"  0
  THEN  Auto
  THEN  (Subst'  (||v||  -  2)  +  1  \msim{}  ||v||  -  1  0  THENA  Auto)
  THEN  Fold  `last`  0
  THEN  (RWO    "rmul-rsub-distrib.1<"  0  THENA  Auto))

---

Home Index