---

Step * 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 ─→ ℚ@i
6. G : ℕn ─→ ℚ@i
7. ||[]|| ≤ n@i
⊢ weighted-sum([];λx.((a * (F x)) + (b * (G x)))) = ((a * weighted-sum([];F)) + (b * weighted-sum([];G))) ∈ ℚ
BY
{ (Reduce 0 THEN 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.  ||[]||  \mleq{}  n@i
\mvdash{}  weighted-sum([];\mlambda{}x.((a  *  (F  x))  +  (b  *  (G  x))))
=  ((a  *  weighted-sum([];F))  +  (b  *  weighted-sum([];G)))


By

(Reduce  0  THEN  QNorm  0  THEN  Auto)

---

Home Index