---

Step * 1 1 2 1 1 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 ⟶ ℚ
6. G : ℕn ⟶ ℚ
7. u : ℚ
8. 1 ≤ n
9. 0 ≤ 0
⊢ ((0 + (((a * (F 0)) + (b * (G 0))) * u)) + 0) = ((a * ((0 + ((F 0) * u)) + 0)) + (b * ((0 + ((G 0) * u)) + 0))) ∈ ℚ
BY
{ (QNorm 0 THEN Auto)⋅ }

---

Latex:

---

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{}
6.  G  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbQ{}
7.  u  :  \mBbbQ{}
8.  1  \mleq{}  n
9.  0  \mleq{}  0
\mvdash{}  ((0  +  (((a  *  (F  0))  +  (b  *  (G  0)))  *  u))  +  0)
=  ((a  *  ((0  +  ((F  0)  *  u))  +  0))  +  (b  *  ((0  +  ((G  0)  *  u))  +  0)))


By

---

Latex:
(QNorm  0  THEN  Auto)\mcdot{}

---

Home Index