---

Step * 1 1 of Lemma weighted-sum-split

.....equality..... 
1. p : ℚ List
2. q : ℚ List
3. F : ℕ||p @ q|| ─→ ℚ
4. Σ0 ≤ j < ||p|| + ||q||. (F j) * p @ q[j]
= (Σ0 ≤ j < ||p||. (F j) * p @ q[j] + Σ||p|| ≤ j < ||p|| + ||q||. (F j) * p @ q[j])
∈ ℚ
⊢ Σ0 ≤ i < ||q||. (F (i + ||p||)) * q[i] = Σ0 + ||p|| ≤ i < ||q|| + ||p||. (F ((i - ||p||) + ||p||)) * q[i - ||p||] ∈ ℚ
BY
{ (BLemma `sum_shift_q` THEN Auto') }

---

Latex:


.....equality..... 
1.  p  :  \mBbbQ{}  List
2.  q  :  \mBbbQ{}  List
3.  F  :  \mBbbN{}||p  @  q||  {}\mrightarrow{}  \mBbbQ{}
4.  \mSigma{}0  \mleq{}  j  <  ||p||  +  ||q||.  (F  j)  *  p  @  q[j]
=  (\mSigma{}0  \mleq{}  j  <  ||p||.  (F  j)  *  p  @  q[j]  +  \mSigma{}||p||  \mleq{}  j  <  ||p||  +  ||q||.  (F  j)  *  p  @  q[j])
\mvdash{}  \mSigma{}0  \mleq{}  i  <  ||q||.  (F  (i  +  ||p||))  *  q[i]
=  \mSigma{}0  +  ||p||  \mleq{}  i  <  ||q||  +  ||p||.  (F  ((i  -  ||p||)  +  ||p||))  *  q[i  -  ||p||]


By

(BLemma  `sum\_shift\_q`  THEN  Auto')

---

Home Index