---

Step * 1 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)| + |2 * k|) ≤ ((2 * k) * ((2 * k) + 2))
BY
{ (Thin (-1)
   THEN (Assert |(f ((2 * k) * n)) - (2 * k) * (f n)| ≤ ((2 * k) * ((2 * k) + 1)) BY
               ((Using [`n',⌜|n|⌝] (BLemma `mul_cancel_in_le`)⋅ THENA (Auto THEN RWO "absval_pos" 0 THEN Auto))
                THEN RWW "absval_mul< left_mul_subtract_distrib" 0
                THEN Auto
                THEN (Subst ⌜n * (2 * k) * (f n) ~ ((2 * k) * n) * (f n)⌝ 0⋅ THENA Auto)
                THEN DVar `f'
                THEN (Unhide THENA Auto)
                THEN OnMaybeHyp 3 (\h. (Unfold `regular-int-seq` h THEN (RW (AddrC [1] (HypC h)) 0 THENA Auto)))
                THEN RWO "absval_pos" 0
                THEN Auto))
   ) }

1
1. k : ℕ+@i
2. f : {f:ℕ+ ⟶ ℤ| k-regular-seq(f)} 
3. n : ℕ+@i
4. |(f ((2 * k) * n)) - (2 * k) * (f n)| ≤ ((2 * k) * ((2 * k) + 1))
⊢ (|(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)|  +  |2  *  k|)  \mleq{}  ((2  *  k)  *  ((2  *  k)  +  2))


By

---

Latex:
(Thin  (-1)
  THEN  (Assert  |(f  ((2  *  k)  *  n))  -  (2  *  k)  *  (f  n)|  \mleq{}  ((2  *  k)  *  ((2  *  k)  +  1))  BY
                          ((Using  [`n',\mkleeneopen{}|n|\mkleeneclose{}]  (BLemma  `mul\_cancel\_in\_le`)\mcdot{}
                              THENA  (Auto  THEN  RWO  "absval\_pos"  0  THEN  Auto)
                              )
                            THEN  RWW  "absval\_mul<  left\_mul\_subtract\_distrib"  0
                            THEN  Auto
                            THEN  (Subst  \mkleeneopen{}n  *  (2  *  k)  *  (f  n)  \msim{}  ((2  *  k)  *  n)  *  (f  n)\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                            THEN  DVar  `f'
                            THEN  (Unhide  THENA  Auto)
                            THEN  OnMaybeHyp  3  (\mbackslash{}h.  (Unfold  `regular-int-seq`  h
                                                                            THEN  (RW  (AddrC  [1]  (HypC  h))  0  THENA  Auto)
                                                                            ))
                            THEN  RWO  "absval\_pos"  0
                            THEN  Auto))
  )

---

Home Index