---

Step * of Lemma accelerate-bdd-diff

∀k:ℕ+. ∀[f:{f:ℕ+ ⟶ ℤ| k-regular-seq(f)} ]. bdd-diff(accelerate(k;f);f)
BY
{ (Auto
   THEN With ⌜(2 * k) + 2⌝ (D 0)⋅
   THEN Auto
   THEN (Using [`n',⌜|2 * k|⌝] (BLemma `mul_cancel_in_le`)⋅ THENA Auto)
   THEN (RWO "absval_mul<" 0 THENA Auto)
   THEN (Subst ⌜|2 * k| ~ 2 * k⌝ 0⋅ THENA (RWO "absval_pos" 0 THEN Auto))
   THEN (Subst ⌜(2 * k) * ((accelerate(k;f) n) - f n) ~ ((2 * k) * (accelerate(k;f) n)) - (2 * k) * (f n)⌝ 0⋅
         THENA Auto
         )) }

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

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}\msupplus{}.  \mforall{}[f:\{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  k-regular-seq(f)\}  ].  bdd-diff(accelerate(k;f);f)


By

---

Latex:
(Auto
  THEN  With  \mkleeneopen{}(2  *  k)  +  2\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  (Using  [`n',\mkleeneopen{}|2  *  k|\mkleeneclose{}]  (BLemma  `mul\_cancel\_in\_le`)\mcdot{}  THENA  Auto)
  THEN  (RWO  "absval\_mul<"  0  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}|2  *  k|  \msim{}  2  *  k\mkleeneclose{}  0\mcdot{}  THENA  (RWO  "absval\_pos"  0  THEN  Auto))
  THEN  (Subst  \mkleeneopen{}(2  *  k)  *  ((accelerate(k;f)  n)  -  f  n)  \msim{}  ((2  *  k)  *  (accelerate(k;f)  n))  -  (2  *  k)
                            *  (f  n)\mkleeneclose{}  0\mcdot{}
              THENA  Auto
              ))

---

Home Index