---

Step * of Lemma q-linear-unroll

∀[k:ℕ+]. ∀[X:ℕ ⟶ ℚ]. ∀[y:ℚ List].
  q-linear(k;j.X[j];y) = (q-linear(k - 1;j.X[j];y) + (X[k] * y[k - 1])) ∈ ℚ supposing k ≤ ||y||
BY
{ xxx(Unfold `q-linear` 0
      THEN Auto
      THEN ((RW (AddrC [2;2] (LemmaC `sum_unroll_hi_q`)) 0) THENA Auto)
      THEN QNorm 0
      THEN (RW IntNormC 0 THENA Auto)
      THEN QNorm 0
      THEN EqCD
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[X:\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[y:\mBbbQ{}  List].
    q-linear(k;j.X[j];y)  =  (q-linear(k  -  1;j.X[j];y)  +  (X[k]  *  y[k  -  1]))  supposing  k  \mleq{}  ||y||


By

---

Latex:
xxx(Unfold  `q-linear`  0
        THEN  Auto
        THEN  ((RW  (AddrC  [2;2]  (LemmaC  `sum\_unroll\_hi\_q`))  0)  THENA  Auto)
        THEN  QNorm  0
        THEN  (RW  IntNormC  0  THENA  Auto)
        THEN  QNorm  0
        THEN  EqCD
        THEN  Auto)xxx

---

Home Index