---

Step * 1 1 of Lemma weighted-sum-linear

.....assertion..... 
1. a : ℚ
2. b : ℚ
⊢ ∀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))) ∈ ℚ))
BY
{ ((CompleteInductionOnNat THEN Auto) THEN DVar `p') }

1
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))) ∈ ℚ

2
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. ||[u / v]|| ≤ n@i
⊢ weighted-sum([u / v];λx.((a * (F x)) + (b * (G x))))
= ((a * weighted-sum([u / v];F)) + (b * weighted-sum([u / v];G)))
∈ ℚ

---

Latex:


.....assertion..... 
1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
\mvdash{}  \mforall{}n:\mBbbN{}.  \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)))))


By

((CompleteInductionOnNat  THEN  Auto)  THEN  DVar  `p')

---

Home Index