---

Step * 1 1 of Lemma accelerate-bdd-diff


1. k : ℕ+@i
2. f : {f:ℕ+ ⟶ ℤ| k-regular-seq(f)} 
3. n : ℕ+@i
⊢ |(f ((2 * k) * n)) - f ((2 * k) * n) rem 2 * k - (2 * k) * (f n)| ≤ ((2 * k) * ((2 * k) + 2))
BY
{ ((Assert |(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)|) BY
          ((RWO "int-triangle-inequality<" 0 THENA Auto) THEN RW IntNormC 0 THEN Auto))
   THEN (RWO "-1" 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)| + |-(f ((2 * k) * n) rem 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
\mvdash{}  |(f  ((2  *  k)  *  n))  -  f  ((2  *  k)  *  n)  rem  2  *  k  -  (2  *  k)  *  (f  n)|  \mleq{}  ((2  *  k)  *  ((2  *  k)  +  2))


By

---

Latex:
((Assert  |(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)|)  BY
                ((RWO  "int-triangle-inequality<"  0  THENA  Auto)  THEN  RW  IntNormC  0  THEN  Auto))
  THEN  (RWO  "-1"  0  THENA  Auto)
  )

---

Home Index