---

Step * 1 2 of Lemma weighted-sum-split


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])
∈ ℚ
⊢ Σ||p|| ≤ j < ||p|| + ||q||. (F j) * p @ q[j]
= Σ0 + ||p|| ≤ i < ||q|| + ||p||. (F ((i - ||p||) + ||p||)) * q[i - ||p||]
∈ ℚ
BY
{ (EqCD THEN Auto' THEN RWO  "select_append_back" 0 THEN Auto') }

---

Latex:



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{}||p||  \mleq{}  j  <  ||p||  +  ||q||.  (F  j)  *  p  @  q[j]
=  \mSigma{}0  +  ||p||  \mleq{}  i  <  ||q||  +  ||p||.  (F  ((i  -  ||p||)  +  ||p||))  *  q[i  -  ||p||]


By

(EqCD  THEN  Auto'  THEN  RWO    "select\_append\_back"  0  THEN  Auto')

---

Home Index