---

Step * 1 1 of Lemma qabs-qsum-qle


1. n : ℤ
2. E : ℕ0 ⟶ ℚ
3. x : ℚ
4. ∀j:ℕ0. (|E[j]| ≤ x)
⊢ |Σ0 ≤ j < 0. E[j]| ≤ (0 * x)
BY
{ ((RWO "sum_unroll_base_q" 0 THENA Auto) THEN QNorm 0) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  E  :  \mBbbN{}0  {}\mrightarrow{}  \mBbbQ{}
3.  x  :  \mBbbQ{}
4.  \mforall{}j:\mBbbN{}0.  (|E[j]|  \mleq{}  x)
\mvdash{}  |\mSigma{}0  \mleq{}  j  <  0.  E[j]|  \mleq{}  (0  *  x)


By

---

Latex:
((RWO  "sum\_unroll\_base\_q"  0  THENA  Auto)  THEN  QNorm  0)

---

Home Index