---

Step * 2 2 of Lemma expectation-qsum


1. k : ℤ
2. 0 < k
3. ∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:ℕk - 1 ─→ RandomVariable(p;n)].
     (E(n;λs.Σ0 ≤ i < k - 1. X i s) = Σ0 ≤ i < k - 1. E(n;X i) ∈ ℚ)
4. p : FinProbSpace
5. n : ℕ
6. X : ℕk ─→ RandomVariable(p;n)
⊢ E(n;λs.Σ0 ≤ i < k. X i s) = (Σ0 ≤ i < k - 1. E(n;X i) + E(n;X (k - 1))) ∈ ℚ
BY
{ Subst' λs.Σ0 ≤ i < k. X i s ~ λs.Σ0 ≤ i < k - 1. X i s + X (k - 1) 0⋅ }

1
.....equality..... 
1. k : ℤ
2. 0 < k
3. ∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:ℕk - 1 ─→ RandomVariable(p;n)].
     (E(n;λs.Σ0 ≤ i < k - 1. X i s) = Σ0 ≤ i < k - 1. E(n;X i) ∈ ℚ)
4. p : FinProbSpace
5. n : ℕ
6. X : ℕk ─→ RandomVariable(p;n)
⊢ λs.Σ0 ≤ i < k. X i s ~ λs.Σ0 ≤ i < k - 1. X i s + X (k - 1)

2
1. k : ℤ
2. 0 < k
3. ∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:ℕk - 1 ─→ RandomVariable(p;n)].
     (E(n;λs.Σ0 ≤ i < k - 1. X i s) = Σ0 ≤ i < k - 1. E(n;X i) ∈ ℚ)
4. p : FinProbSpace
5. n : ℕ
6. X : ℕk ─→ RandomVariable(p;n)
⊢ E(n;λs.Σ0 ≤ i < k - 1. X i s + X (k - 1)) = (Σ0 ≤ i < k - 1. E(n;X i) + E(n;X (k - 1))) ∈ ℚ

---

Latex:



1.  k  :  \mBbbZ{}
2.  0  <  k
3.  \mforall{}[p:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[X:\mBbbN{}k  -  1  {}\mrightarrow{}  RandomVariable(p;n)].
          (E(n;\mlambda{}s.\mSigma{}0  \mleq{}  i  <  k  -  1.  X  i  s)  =  \mSigma{}0  \mleq{}  i  <  k  -  1.  E(n;X  i))
4.  p  :  FinProbSpace
5.  n  :  \mBbbN{}
6.  X  :  \mBbbN{}k  {}\mrightarrow{}  RandomVariable(p;n)
\mvdash{}  E(n;\mlambda{}s.\mSigma{}0  \mleq{}  i  <  k.  X  i  s)  =  (\mSigma{}0  \mleq{}  i  <  k  -  1.  E(n;X  i)  +  E(n;X  (k  -  1)))


By

Subst'  \mlambda{}s.\mSigma{}0  \mleq{}  i  <  k.  X  i  s  \msim{}  \mlambda{}s.\mSigma{}0  \mleq{}  i  <  k  -  1.  X  i  s  +  X  (k  -  1)  0\mcdot{}

---

Home Index