---

Step * 1 1 2 1 2 1 of Lemma weighted-sum-linear


1. a : ℚ
2. b : ℚ
3. n : ℕ
4. ∀n:ℕn. ∀F,G:ℕn ─→ ℚ. ∀p:ℚ List.
     ((||p|| ≤ n)
     ⇒ (weighted-sum(p;λx.((a * (F x)) + (b * (G x)))) = ((a * weighted-sum(p;F)) + (b * weighted-sum(p;G))) ∈ ℚ))
5. F : ℕn ─→ ℚ@i
6. G : ℕn ─→ ℚ@i
7. u : ℚ
8. v : ℚ List
9. (||v|| + 1) ≤ n@i
10. ¬(||v|| ≤ 0)
11. weighted-sum(v;λx.((a * (F (x + 1))) + (b * (G (x + 1)))))
= ((a * weighted-sum(v;λx.(F (x + 1)))) + (b * weighted-sum(v;λx.(G (x + 1)))))
∈ ℚ
⊢ ((0 + (((a * (F 0)) + (b * (G 0))) * u))
+ (a * weighted-sum(v;λx.(F (x + 1))))
+ (b * weighted-sum(v;λx.(G (x + 1)))))
= ((a * ((0 + ((F 0) * u)) + weighted-sum(v;λi.(F (i + 1)))))
  + (b * ((0 + ((G 0) * u)) + weighted-sum(v;λi.(G (i + 1))))))
∈ ℚ
BY
{ (QNorm 0 THEN Auto)⋅ }

---

Latex:



1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
3.  n  :  \mBbbN{}
4.  \mforall{}n:\mBbbN{}n.  \mforall{}F,G:\mBbbN{}n  {}\mrightarrow{}  \mBbbQ{}.  \mforall{}p:\mBbbQ{}  List.
          ((||p||  \mleq{}  n)
          {}\mRightarrow{}  (weighted-sum(p;\mlambda{}x.((a  *  (F  x))  +  (b  *  (G  x))))
                =  ((a  *  weighted-sum(p;F))  +  (b  *  weighted-sum(p;G)))))
5.  F  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbQ{}@i
6.  G  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbQ{}@i
7.  u  :  \mBbbQ{}
8.  v  :  \mBbbQ{}  List
9.  (||v||  +  1)  \mleq{}  n@i
10.  \mneg{}(||v||  \mleq{}  0)
11.  weighted-sum(v;\mlambda{}x.((a  *  (F  (x  +  1)))  +  (b  *  (G  (x  +  1)))))
=  ((a  *  weighted-sum(v;\mlambda{}x.(F  (x  +  1))))  +  (b  *  weighted-sum(v;\mlambda{}x.(G  (x  +  1)))))
\mvdash{}  ((0  +  (((a  *  (F  0))  +  (b  *  (G  0)))  *  u))
+  (a  *  weighted-sum(v;\mlambda{}x.(F  (x  +  1))))
+  (b  *  weighted-sum(v;\mlambda{}x.(G  (x  +  1)))))
=  ((a  *  ((0  +  ((F  0)  *  u))  +  weighted-sum(v;\mlambda{}i.(F  (i  +  1)))))
    +  (b  *  ((0  +  ((G  0)  *  u))  +  weighted-sum(v;\mlambda{}i.(G  (i  +  1))))))


By

(QNorm  0  THEN  Auto)\mcdot{}

---

Home Index