---

Step * 1 1 1 1 of Lemma accelerate-bdd-diff


1. k : ℕ+@i
2. f : {f:ℕ+ ⟶ ℤ| k-regular-seq(f)} 
3. n : ℕ+@i
4. |(f ((2 * k) * n)) - f ((2 * k) * n) rem 2 * k - (2 * k) * (f n)| ≤ (|(f ((2 * k) * n)) - (2 * k) * (f n)|
   + |-(f ((2 * k) * n) rem 2 * k)|)
⊢ (|(f ((2 * k) * n)) - (2 * k) * (f n)| + |f ((2 * k) * n) rem 2 * k|) ≤ ((2 * k) * ((2 * k) + 2))
BY
{ (RWO "rem_bounds_absval_le" 0 THENA Auto) }

1
1. k : ℕ+@i
2. f : {f:ℕ+ ⟶ ℤ| k-regular-seq(f)} 
3. n : ℕ+@i
4. |(f ((2 * k) * n)) - f ((2 * k) * n) rem 2 * k - (2 * k) * (f n)| ≤ (|(f ((2 * k) * n)) - (2 * k) * (f n)|
   + |-(f ((2 * k) * n) rem 2 * k)|)
⊢ (|(f ((2 * k) * n)) - (2 * k) * (f n)| + |2 * k|) ≤ ((2 * k) * ((2 * k) + 2))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}@i
2.  f  :  \{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  k-regular-seq(f)\} 
3.  n  :  \mBbbN{}\msupplus{}@i
4.  |(f  ((2  *  k)  *  n))  -  f  ((2  *  k)  *  n)  rem  2  *  k  -  (2  *  k)  *  (f  n)|  \mleq{}  (|(f  ((2  *  k)  *  n))  -  (2  *  k)
      *  (f  n)|
      +  |-(f  ((2  *  k)  *  n)  rem  2  *  k)|)
\mvdash{}  (|(f  ((2  *  k)  *  n))  -  (2  *  k)  *  (f  n)|  +  |f  ((2  *  k)  *  n)  rem  2  *  k|)  \mleq{}  ((2  *  k)  *  ((2  *  k)  +  2))


By

---

Latex:
(RWO  "rem\_bounds\_absval\_le"  0  THENA  Auto)

---

Home Index